From 973aec43ea54bbf95b64fbcb636403401d1ca60e Mon Sep 17 00:00:00 2001 From: Rutger Broekhoff Date: Fri, 28 Aug 2026 18:03:05 +0200 Subject: Import from e4b104792206ee7ea64bf39c6b7d2c0c230f9d14 --- server/formal/period.v | 828 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 828 insertions(+) create mode 100644 server/formal/period.v (limited to 'server/formal/period.v') diff --git a/server/formal/period.v b/server/formal/period.v new file mode 100644 index 0000000..82921db --- /dev/null +++ b/server/formal/period.v @@ -0,0 +1,828 @@ +From stdpp Require Import numbers option sorting ssreflect. +From stdpp Require Import options. +From routemon Require Import util. + +Definition timestamp := Z. +Variant limit := + | NegInftyLimit + | TsLimit (x : timestamp) + | PosInftyLimit. +Instance limit_eq_dec : EqDecision limit. +Proof. solve_decision. Qed. + +Notation "-∞" := NegInftyLimit. +Notation "+∞" := PosInftyLimit. +Coercion TsLimit : timestamp >-> limit. + +(* The interval [start, end). Considered empty when start >= end. *) +Record period := + Period + { period_start : limit + ; period_end : limit + }. +Notation "'[' s ',' e ')'" := (Period s e). + +(* Consider making an inductive variant of these? *) +Definition limit_le (l1 l2 : limit) := + match l1, l2 with + | -∞, _ | _, +∞ => True + | TsLimit t1, TsLimit t2 => (t1 ≤ t2)%Z + | _, _ => False + end. +Arguments limit_le !_ !_ / : assert. +Definition limit_lt l1 l2 := + match l1 with + | -∞ => + match l2 with + | -∞ => False + | _ => True + end + | TsLimit t1 => + match l2 with + | -∞ => False + | TsLimit t2 => (t1 < t2)%Z + | +∞ => True + end + | +∞ => False + end. +Arguments limit_lt !_ !_ / : assert. +Instance limit_le_dec : RelDecision limit_le. +Proof. intros [] []; simpl; solve_decision. Qed. +Instance limit_lt_dec : RelDecision limit_lt. +Proof. intros [] []; simpl; solve_decision. Qed. +Instance limit_lt_pi l1 l2 : ProofIrrel (limit_lt l1 l2). +Proof. destruct l1, l2; apply _. Qed. + +Instance relation_equiv {A} : Equiv (relation A) := + λ R1 R2, ∀ x y, R1 x y ↔ R2 x y. + +Lemma strict_limit_le_limit_lt : + strict limit_le ≡ limit_lt. +Proof. + split. + - intros []. destruct x, y; simpl in *; try done. lia. + - intros H. destruct x, y; unfold strict; simpl in *; try done; auto with lia. +Qed. + +Instance : Reflexive limit_le. +Proof. intros l. by destruct l; simpl. Qed. +Instance : Transitive limit_le. +Proof. intros [] [] []; simpl; try done. lia. Qed. +Instance : PreOrder limit_le. +Proof. constructor; apply _. Qed. +Instance : AntiSymm (=) limit_le. +Proof. + intros [] []; simpl; try done. + intros H1 H2. f_equal. by apply Z.le_antisymm. +Qed. +Instance : PartialOrder limit_le. +Proof. constructor; apply _. Qed. +Instance : Trichotomy (strict limit_le). +Proof with auto with lia. + intros [] []; unfold strict; simpl... + destruct (Z.lt_trichotomy x x0) as [H|[->|H]]... +Qed. +Instance : TotalOrder limit_le. +Proof. constructor; apply _. Qed. + +Instance : StrictOrder (strict limit_le) := _. +(* TODO: apparently useless?? +Instance rel_equiv_proper {A} (x y : A) : Proper ((≡) ==> (↔)) (λ R, R x y). +Proof. easy. Qed. +Search Proper iff eq. +*) +Instance complement_equiv {A} : Proper ((≡) ==> (≡)) (@complement A). +Proof. intros R1 R2 HR12. split; unfold complement; intros Hequiv []%HR12%Hequiv. Qed. +Instance Reflexive_equiv {A} : Proper ((≡) ==> (↔)) (@Reflexive A). +Proof. + intros R1 R2 Hequiv. unfold Reflexive. + split; intros H x; by apply Hequiv. +Qed. +Instance Irreflexive_equiv {A} : Proper ((≡) ==> (↔)) (@Irreflexive A). +Proof. unfold Irreflexive. by intros R1 R2 ->. Qed. +Instance Transitive_equiv {A} : Proper ((≡) ==> (↔)) (@Transitive A). +Proof. + intros R1 R2 Hequiv. unfold Transitive. + by split; intros H x y z Hxy%Hequiv Hyz%Hequiv; eapply Hequiv, H. +Qed. +Instance StrictOrder_equiv {A} : Proper ((≡) ==> (↔)) (@StrictOrder A). +Proof. + intros R1 R2 Hequiv. split; intros [Hirr Htrans]. + - by rewrite ->Hequiv in Hirr, Htrans. + - by rewrite <-Hequiv in Hirr, Htrans. +Qed. +Instance Trichotomy_equiv {A} : Proper ((≡) ==> (↔)) (@Trichotomy A). +Proof. + intros R1 R2 Hequiv. split; intros. + - intros x y. by rewrite -(Hequiv x y) -(Hequiv y x). + - intros x y. by rewrite (Hequiv x y) (Hequiv y x). +Qed. + +Instance : StrictOrder limit_lt. +Proof. rewrite -strict_limit_le_limit_lt. apply _. Qed. +Instance : Trichotomy limit_lt. +Proof. rewrite -strict_limit_le_limit_lt. apply _. Qed. + +Definition limit_lt_ts' (l : limit) (t2 : timestamp) := + match l with + | -∞ => True + | TsLimit t1 => (t1 < t2)%Z + | +∞ => False + end. +Definition ts_le_limit' (t1 : timestamp) (l : limit) := + match l with + | -∞ => False + | TsLimit t2 => (t1 ≤ t2)%Z + | +∞ => True + end. +Lemma limit_lt_limit_lt_ts' l t2 : limit_lt_ts' l t2 ↔ limit_lt l t2. +Proof. by destruct l. Qed. +Lemma ts_le_limit'_limit_le t1 l : ts_le_limit' t1 l ↔ limit_le t1 l. +Proof. by destruct l. Qed. + +Declare Scope limit_scope. +Delimit Scope limit_scope with lim. +Notation "l1 < l2" := (limit_lt l1 l2) : limit_scope. +Notation "l1 ≤ l2" := (limit_le l1 l2) : limit_scope. +Notation "l1 < l2 < l3" := (l1 < l2 ∧ l2 < l3)%lim : limit_scope. +Notation "l1 ≤ l2 < l3" := (l1 ≤ l2 ∧ l2 < l3)%lim : limit_scope. +Notation "l1 < l2 ≤ l3" := (l1 < l2 ∧ l2 ≤ l3)%lim : limit_scope. +Notation "l1 ≤ l2 ≤ l3" := (l1 ≤ l2 ∧ l2 ≤ l3)%lim : limit_scope. +Open Scope limit_scope. + +Instance period_elem_of : ElemOf timestamp period := + λ t '[s, e), (s ≤ t < e). +Instance period_elem_of_dec t (p : period) : Decision (t ∈ p). +Proof. destruct p as [s e]. apply _. Qed. + +Lemma limit_le_lt l1 l2 : l1 < l2 ↔ l1 ≤ l2 ∧ l1 ≠ l2. +Proof. by rewrite -(strict_limit_le_limit_lt l1 l2) strict_spec_alt. Qed. + +Lemma limit_le_cases {l1 l2} : l1 ≤ l2 ↔ l1 = l2 ∨ l1 < l2. +Proof. + rewrite -(strict_limit_le_limit_lt l1 l2) strict_spec_alt. split. + - intros Hl12. destruct (decide (l1 = l2)) as [<-|Hne]; tauto. + - by intros [<-|[Hl12 _]]. +Qed. + +Lemma limit_lt_le_lt {l1} l2 {l3} : l1 ≤ l2 < l3 → l1 < l3. +Proof. by intros [[<-|?]%limit_le_cases ?]; last etrans. Qed. + +Definition period_empty '[s, e) := e ≤ s. +Definition period_empty_alt (p : period) := ∀ t, t ∉ p. +Lemma period_empty_alt_iff p : period_empty p ↔ period_empty_alt p. +Proof. + destruct p as [s e]. + rewrite /period_empty /period_empty_alt /=. + split; intros H. + - intros t [contra []]%limit_lt_le_lt%limit_le_lt. + by eapply (anti_symm limit_le). + - destruct s as [|s|], e as [|e|]; try done. + + exfalso. apply (H (Z.pred e)). rewrite /elem_of /period_elem_of /=. lia. + + exfalso. by apply (H 0%Z). + + rewrite /elem_of /period_elem_of /= in H. + specialize (H s). simpl. lia. + + exfalso. apply (H s). rewrite /elem_of /period_elem_of /=. lia. +Qed. +Instance period_empty_dec p : Decision (period_empty p). +Proof. destruct p as [s e]. solve_decision. Qed. + +Definition period_nonempty '[s, e) := s < e. +Instance period_nonempty_dec p : Decision (period_nonempty p). +Proof. destruct p. apply _. Qed. +Instance period_nonempty_pi p : ProofIrrel (period_nonempty p). +Proof. destruct p. apply _. Qed. + +Instance period_equiv : Equiv period := + λ p1 p2, ∀ t, t ∈ p1 ↔ t ∈ p2. +Instance period_equiv_reflexive : Reflexive period_equiv. +Proof. done. Qed. +Instance period_equiv_trans : Transitive period_equiv. +Proof. intros p1 p2 p3 H1 H2 t. by rewrite H1. Qed. +Instance period_equiv_symm : Symmetric period_equiv. +Proof. by intros p1 p2 H t. Qed. +Instance period_equiv_equiv : Equivalence period_equiv. +Proof. constructor; apply _. Qed. + +(* All empty periods are equivalent *) +Lemma period_empty_equiv p1 p2 : period_empty p1 → period_empty p2 ↔ p1 ≡ p2. +Proof. + intros Hp1%period_empty_alt_iff. split. + - intros Hp2%period_empty_alt_iff. intros t. + split; [intros []%(Hp1 _) | intros []%(Hp2 _)]. + - intros Hequiv. apply period_empty_alt_iff. + intros t []%Hequiv%(Hp1 _). +Qed. + +Instance empty_period : Empty period := [TsLimit 0%Z, TsLimit 0%Z). +Definition empty_period_empty : period_empty empty_period. +Proof. done. Qed. + +Definition limit_min (l1 l2 : limit) := if decide (l1 ≤ l2) then l1 else l2. +Definition limit_max (l1 l2 : limit) := if decide (l1 ≤ l2) then l2 else l1. + +Notation "l1 '`min`' l2" := (limit_min l1 l2) : limit_scope. +Notation "l1 '`max`' l2" := (limit_max l1 l2) : limit_scope. + +Definition limit_min_ts (t1 t2 : timestamp) : + t1 `min` t2 = TsLimit (t1 `min` t2)%Z. +Proof. + unfold limit_min. + destruct (decide (t1 ≤ t2)); + simpl in *; f_equal; lia. +Qed. + +Definition limit_max_ts (t1 t2 : timestamp) : + t1 `max` t2 = TsLimit (t1 `max` t2)%Z. +Proof. + unfold limit_max. + destruct (decide (t1 ≤ t2)); + simpl in *; f_equal; lia. +Qed. + +Instance period_intersection : Intersection period := λ '[s1, e1) '[s2, e2), + [ s1 `max` s2, e1 `min` e2 ). + +Lemma intersect_and (p1 p2 : period) t : + t ∈ (p1 ∩ p2) ↔ t ∈ p1 ∧ t ∈ p2. +Proof. + (* It really should be possible to optimize this proof somehow. *) + destruct p1 as [[|s1|] [|e1|]], p2 as [[|s2|] [|e2|]]; + rewrite /intersection /period_intersection /elem_of /period_elem_of /limit_min /limit_max /limit_le /limit_lt /=; + repeat case_decide; tauto || lia. +Qed. + +(* The points in time given by p1 except those given by p2, given as a before/after pair. *) +Definition except '[s1, e1) '[s2, e2) : period * period := + ( [ s1, e1 `min` s2 ), + [ s1 `max` e2, e1 ) ). + +Lemma limit_lt_ne l1 l2 : l1 < l2 → l1 ≠ l2. +Proof. rewrite -(strict_limit_le_limit_lt l1 l2) strict_spec_alt. easy. Qed. + +Lemma not_limit_le l1 l2 : ¬ (l1 ≤ l2) ↔ l2 < l1. +Proof. + destruct (trichotomy limit_lt l1 l2) as [Hl12|[<-|Hl21]]. + - split; intros H. + + exfalso. apply H, limit_le_cases. by right. + + exfalso. by eapply asymmetry. + - split; intros H. + + exfalso. apply H, limit_le_cases. by left. + + by apply (_ : Irreflexive limit_lt) in H. + - split; intros H; first done. + intros [<-|Hl12]%limit_le_cases. + + by apply (_ : Irreflexive limit_lt) in H. + + by eapply asymmetry. +Qed. + +Lemma not_limit_le' : complement limit_le ≡ flip limit_lt. +Proof. apply: not_limit_le. Qed. + +Instance relation_equiv_reflexive {A} : Reflexive (@relation_equiv A). +Proof. done. Qed. +Instance relation_equiv_trans {A} : Transitive (@relation_equiv A). +Proof. intros R1 R2 R3 H12 H23 x y. by rewrite H12 -H23. Qed. +Instance relation_equiv_symm {A} : Symmetric (@relation_equiv A). +Proof. by intros R1 R2 H12 x y. Qed. +Instance relation_equiv_equiv {A} : Equivalence (@relation_equiv A). +Proof. constructor; apply _. Qed. + +Lemma relation_flip_equiv {A} : Proper ((≡@{relation A}) ==> (≡)) flip. +Proof. intros R1 R2 H12 x y. simpl. by rewrite (H12 y x). Qed. + +(* Could also be more generic *) +Lemma relation_flip_involutive {A} (R : relation A) : flip (flip R) ≡ R. +Proof. done. Qed. + +Lemma complement_involutive {A} `{!RelDecision (R : relation A)} : complement (complement R) ≡ R. +Proof. + intros x y. split; intros Hxy. + - by destruct (decide (R x y)). + - by apply. +Qed. + +Lemma not_limit_lt' : complement limit_lt ≡ flip limit_le. +Proof. + rewrite -(relation_flip_involutive limit_lt) complement_inverse. + trans (flip (complement (complement limit_le))). + { apply relation_flip_equiv, complement_equiv, symmetry, not_limit_le'. } + apply relation_flip_equiv, complement_involutive. +Qed. + +Lemma not_limit_lt l1 l2 : ¬ (l1 < l2) ↔ l2 ≤ l1. +Proof. apply not_limit_lt'. Qed. + +(* TODO: make conclusion positive? *) +Lemma period_nonempty_equiv_L_1 (s1 e1 s2 e2 : limit) : + period_nonempty [s1, e1) → + period_nonempty [s2, e2) → + [s1, e1) ≡ [s2, e2) → + ¬ s1 < s2. +Proof. + unfold period_nonempty. + intros Hne1 Hne2 Hequiv Hs12. + destruct s2 as [|s2|]; [by destruct s1|..|by destruct s1]. + destruct s1 as [|s1|]; last done. + * assert (Hs2a : s2 ∈ [s2, e2)). + { unfold elem_of, period_elem_of. by destruct e2. } + pose proof (proj2 (Hequiv s2) Hs2a) as [_ Hs2b]. + assert (Hs2c : Z.pred s2 ∈ [-∞, e1)). + { unfold elem_of, period_elem_of. + by destruct e1 as [|e1|]; [|simpl in *; lia|]. } + pose proof (proj1 (Hequiv (Z.pred s2)) Hs2c) as [contra _]. + simpl in contra. lia. + * assert (Hs1 : s1 ∈ [s1, e1)). + { unfold elem_of, period_elem_of. by destruct e1. } + pose proof (proj1 (Hequiv s1) Hs1) as [[Heq|Heq]%limit_le_cases _]. + { rewrite Heq in Hs12. by eapply (_ : Irreflexive limit_lt). } + by eapply asymmetry. +Qed. + +(* TODO: make conclusion positive? *) +Lemma period_nonempty_equiv_L_2 (s1 e1 s2 e2 : limit) : + period_nonempty [s1, e1) → + period_nonempty [s2, e2) → + [s1, e1) ≡ [s2, e2) → + ¬ e1 < e2. +Proof. + intros Hne1 Hne2 Hequiv He12. + destruct e1 as [|e1|]; [by destruct s1|..|done]. + destruct e2 as [|e2|]; first done. + * (* e2 - 1 ∈ [s2, e2) → e2 - 1 ∈ [s1, e1) → s1 ≤ e2 - 1 < e1 → e2 ≤ e1 → e2 = e1 ∨ e2 < e1 *) + assert (He2a : Z.pred e2 ∈ [s2, e2)). + { unfold elem_of, period_elem_of. + by destruct s2 as [|s2|]; [simpl in *; lia..|]. } + pose proof (proj2 (Hequiv (Z.pred e2)) He2a) as [_ He2b]. + simpl in *. lia. + * (* We want to plug e1 into the right side to get a + contradiction, so we need s2 ≤ e1. It suffices to show that + s2 ≤ e1 - 1 *) + assert (He1a : Z.pred e1 ∈ [s1, e1)). + { unfold elem_of, period_elem_of. + by destruct s1 as [|s1|]; [simpl in *; lia..|]. } + pose proof (proj1 (Hequiv (Z.pred e1)) He1a) as [He1b _]. + assert (He1c : e1 ∈ [s2, +∞)). + { unfold elem_of, period_elem_of. + by destruct s2 as [|s2|]; [|simpl in *; lia|]. } + pose proof (proj2 (Hequiv e1) He1c) as [_ []%(_ : Irreflexive limit_lt)]. +Qed. + +Lemma period_nonempty_equiv_L p1 p2 : + period_nonempty p1 → + period_nonempty p2 → + p1 ≡ p2 → p1 = p2. +Proof. + destruct p1 as [s1 e1], p2 as [s2 e2]. + unfold equiv, period_equiv. + intros Hne1 Hne2 Hequiv. + f_equal. + - destruct (decide (s1 < s2)) as [Hs12|[<-|Hs21]%not_limit_lt%limit_le_cases]; [|done|]. + + exfalso. by apply (period_nonempty_equiv_L_1 s1 e1 s2 e2). + + exfalso. by apply (period_nonempty_equiv_L_1 s2 e2 s1 e1). + - destruct (decide (e1 < e2)) as [He12|[<-|He21]%not_limit_lt%limit_le_cases]; [|done|]. + + exfalso. by apply (period_nonempty_equiv_L_2 s1 e1 s2 e2). + + exfalso. by apply (period_nonempty_equiv_L_2 s2 e2 s1 e1). +Qed. + +Definition period_empty_not_nonempty p : ¬ period_empty p ↔ period_nonempty p. +Proof. destruct p. apply not_limit_le. Qed. + +Lemma limit_lt_min l1 l2 l3 : + l1 < l2 ∧ l1 < l3 ↔ l1 < l2 `min` l3. +Proof. + split. + - intros [Hl12 Hl13]. unfold limit_min. by case_decide. + - unfold limit_min. intros H. case_decide. + + split; first done. + apply limit_le_cases in H0 as [<-|H0]; first done. + by etrans. + + apply not_limit_le in H0. + by split; first etrans. +Qed. + +Lemma limit_max_le l1 l2 l3 : + l1 ≤ l3 ∧ l2 ≤ l3 ↔ l1 `max` l2 ≤ l3. +Proof. + split. + - intros [Hl12 Hl23]. unfold limit_max. by case_decide. + - unfold limit_max. intros H. case_decide. + + by split; first etrans. + + apply not_limit_le in H0. split; first done. + apply limit_le_lt in H0 as [H0 _]. by etrans. +Qed. +Lemma limit_le_max l1 l2 l3 : + l1 ≤ l2 `max` l3 ↔ l1 ≤ l2 ∨ l1 ≤ l3. +Proof. + unfold limit_max. + destruct (decide (l2 ≤ l3)) as [Hl23|Hl23%not_limit_le]. + - split; first tauto. intros [H|H]; last done. by etrans. + - split; first tauto. intros [H|H]; first done. + by trans l3; last (apply limit_le_cases; right). +Qed. + +Lemma except_lem p1 p2 t : + t ∈ p1 ∧ t ∉ p2 ↔ + t ∈ (except p1 p2).1 ∨ t ∈ (except p1 p2).2. +Proof. + destruct p1 as [s1 e1], p2 as [s2 e2]. split. + - intros [Hp1 Hp2]. + (* on the left if t < s2, on the right if e2 ≤ t *) + destruct (decide (t < s2)) as [Hts2|Hts2]. + + (* t < s2 *) + left. simpl. split. + * apply Hp1. + * apply limit_lt_min. split; last done. + rewrite /elem_of /period_elem_of in Hp1. easy. + + (* ¬ (t < s2) (↔ s2 ≤ t) *) + apply not_limit_lt in Hts2. + right. simpl. split. + * apply limit_max_le. split. + -- apply Hp1. + -- apply not_limit_lt. intros contra. by apply Hp2. + * apply Hp1. + - intros [H|H]; simpl in *. + + split. + * unfold elem_of, period_elem_of in *. split. + -- apply H. + -- by destruct H as [_ [H _]%limit_lt_min]. + * unfold elem_of, period_elem_of in *. + destruct H as [H1 [H2 H3]%limit_lt_min]. + intros [Hc1 Hc2]. + apply limit_le_cases in Hc1 as [Hc1|Hc1]. + -- inv Hc1. by apply (_ : Irreflexive limit_lt) in H3. + -- eapply asymmetry; [apply H3 | apply Hc1]. + + unfold elem_of, period_elem_of in H. + rewrite -limit_max_le in H. destruct H as [[H1 H2] H3]. + split; first done. + intros [Hc1 Hc2]. + apply limit_le_cases in H2 as [H2|H2]. + -- inv H2. by apply (_ : Irreflexive limit_lt) in Hc2. + -- eapply asymmetry; [apply H2 | apply Hc2]. +Qed. + +Lemma limit_max_lt l1 l2 l3 : + l1 `max` l2 < l3 ↔ l1 < l3 ∧ l2 < l3. +Proof. + unfold limit_max. + destruct (decide (l1 ≤ l2)) as [Hl12|Hl12%not_limit_le]. + - split; last easy. intros H. by split; first eapply limit_lt_le_lt. + - split; last easy. intros H. by split; last etrans. +Qed. + +Lemma limit_min_lt l1 l2 l3 : + l1 `min` l2 < l3 ↔ l1 < l3 ∨ l2 < l3. +Proof. + unfold limit_min. + destruct (decide (l1 ≤ l2)%lim) as [Hl12|Hl12%not_limit_le]. + - split; first tauto. by intros [H|H]; last eapply limit_lt_le_lt. + - split; first tauto. by intros [H|H]; first etrans. +Qed. + +Lemma limit_lt_max l1 l2 l3 : + l1 < l2 `max` l3 ↔ l1 < l2 ∨ l1 < l3. +Proof. + unfold limit_max. + destruct (decide (l2 ≤ l3)) as [Hl23|Hl23%not_limit_le]. + - split; first tauto. intros [H|H]; last done. + by apply limit_le_cases in Hl23 as [<-|Hl23]; last etrans. + - split; first tauto. by intros [H|H]; last etrans. +Qed. + +Instance limit_min_comm : Comm (=) limit_min. +Proof. + unfold limit_min. + intros [] []; repeat case_decide; + try done; simpl in *; f_equal; lia. +Qed. +Instance limit_max_comm : Comm (=) limit_max. +Proof. + unfold limit_max. + intros [] []; repeat case_decide; + try done; simpl in *; f_equal; lia. +Qed. + +Lemma limit_max_eq_l l1 l2 : l1 `max` l2 = l1 ↔ l2 ≤ l1. +Proof. + unfold limit_max. case_decide; split. + - by intros ->. + - intros H12. by eapply (_ : AntiSymm (=) limit_le). + - intros _. apply limit_le_cases. right. + by apply not_limit_le. + - by intros _. +Qed. +Lemma limit_max_eq_r l1 l2 : l1 `max` l2 = l2 ↔ l1 ≤ l2. +Proof. rewrite [l1 `max` l2]comm. apply limit_max_eq_l. Qed. + +Lemma limit_max_l l1 l2 : l2 ≤ l1 → l1 `max` l2 = l1. +Proof. apply limit_max_eq_l. Qed. +Lemma limit_max_r l1 l2 : l1 ≤ l2 → l1 `max` l2 = l2. +Proof. apply limit_max_eq_r. Qed. + +Definition ne_period := { p : period | period_nonempty p }. + +Instance ne_period_elem_of : ElemOf timestamp ne_period := + λ t p, t ∈ `p. +Instance ne_period_elem_of_dec t (p : ne_period) : Decision (t ∈ p). +Proof. apply _. Qed. + +(* TODO: rename to ne_period_before *) +Definition period_before '([s1, e1) ↾ _ : ne_period) '([s2, e2) ↾ _ : ne_period) := + e1 < s2. + +Instance period_before_pi p1 p2 : ProofIrrel (period_before p1 p2). +Proof. destruct p1 as [[s1 e1] Hne1], p2 as [[s2 e2] Hne2]. apply _. Qed. + +Instance period_before_trans : Transitive period_before. +Proof. + intros [[s1 e1] Hne1] [[s2 e2] Hne2] [[s3 e3] Hne3] H1 H2. + unfold period_before in *. simpl in *. + by trans s2; last trans e2. +Qed. + +Instance period_before_irrefl : Irreflexive period_before. +Proof. + intros [[s e] Hne] Hp. simpl in *. + eapply (_ : Irreflexive limit_lt). by etrans. +Qed. + +Instance period_before_strict_order : StrictOrder period_before. +Proof. split; apply _. Qed. + +Definition ne_period_rel (R : relation ne_period) : relation period := + λ p1 p2, ∃ H1 H2, R (p1 ↾ H1) (p2 ↾ H2). + +Instance ne_period_rel_trans `{!Transitive R} : Transitive (ne_period_rel R). +Proof. + intros p1 p2 p3 (H1 & H2 & HR12) (H2' & H3 & HR23). + exists H1, H3. replace H2' with H2 in HR23; last apply proof_irrel. + by etrans. +Qed. + +Instance ne_period_rel_irrefl `{!Irreflexive R} : Irreflexive (ne_period_rel R). +Proof. + intros p. intros (H1 & H2 & HR). + replace H2 with H1 in HR; last apply proof_irrel. + by apply (_ : Irreflexive R) in HR. +Qed. + +Instance ne_period_rel_pi (R : relation ne_period) `{!∀ x y, ProofIrrel (R x y)} x y : + ProofIrrel (ne_period_rel R x y). +Proof. apply _. Qed. + +Lemma except_parts_order p1 p2 : + period_nonempty p2 → + period_nonempty (except p1 p2).1 → + period_nonempty (except p1 p2).2 → + ne_period_rel period_before (except p1 p2).1 (except p1 p2).2. +Proof. + destruct p1 as [s1 e1], p2 as [s2 e2]. simpl. intros H0 Hne1 Hne2. + unfold period_before. split; [done|split; [done|]]. + apply limit_min_lt. right. apply limit_lt_max. right. apply H0. +Qed. + +Definition period_nonempty_alt (p : period) := ∃ t, t ∈ p. + +Lemma period_nonempty_alt_iff p : + period_nonempty p ↔ period_nonempty_alt p. +Proof. + unfold period_nonempty, period_nonempty_alt. + destruct p as [s e]. split. + - intros Hlt. destruct s as [|s|]; last done. + + destruct e as [|e|]; first done. + * exists (Z.pred e). by split; last (simpl; lia). + * exists 0%Z. done. + + exists s. done. + - intros [t Ht]. by eapply limit_lt_le_lt. +Qed. + +Instance period_eq_dec : EqDecision period. +Proof. solve_decision. Qed. + +Instance period_disjoint : Disjoint period := + λ p1 p2, period_empty (p1 ∩ p2). + +Instance period_intersection_comm : Comm (=) period_intersection. +Proof. + intros [s1 e1] [s2 e2]. + by rewrite /= [s2 `max` s1]comm [e2 `min` e1]comm. +Qed. +Instance period_disjoint_symm : Symmetric period_disjoint. +Proof. intros p1 p2. unfold period_disjoint. by rewrite comm. Qed. + +Lemma limit_min_eq_l l1 l2 : l1 `min` l2 = l1 ↔ l1 ≤ l2. +Proof. + unfold limit_min. case_decide; first done. split. + - intros ->. exfalso. by apply H. + - intros []%H. +Qed. +Lemma limit_min_eq_r l1 l2 : l1 `min` l2 = l2 ↔ l2 ≤ l1. +Proof. rewrite [l1 `min` l2]comm. apply limit_min_eq_l. Qed. + +Lemma limit_min_l l1 l2 : l1 ≤ l2 → l1 `min` l2 = l1. +Proof. apply limit_min_eq_l. Qed. +Lemma limit_min_r l1 l2 : l2 ≤ l1 → l1 `min` l2 = l2. +Proof. apply limit_min_eq_r. Qed. + +Lemma limit_lt_le_trans {l1} l2 {l3} : l1 < l2 → l2 ≤ l3 → l1 < l3. +Proof. by intros Hlt12 [->|Hlt23]%limit_le_cases; last etrans. Qed. + +Instance period_union : Union period := + λ '[s1, e1) '[s2, e2), [s1 `min` s2, e1 `max` e2). + +Lemma limit_min_le l1 l2 l3 : + l1 ≤ l3 ∨ l2 ≤ l3 ↔ + l1 `min` l2 ≤ l3. +Proof. + unfold limit_min. case_decide; split. + - by intros [H13|H23]; last trans l2. + - intros H13. by left. + - apply not_limit_le in H. intros [H13|H23]; last done. + trans l1; last done. + apply limit_le_cases. by right. + - intros H23. by right. +Qed. + +Lemma limit_le_min l1 l2 l3 : + l1 ≤ l2 ∧ l1 ≤ l3 ↔ + l1 ≤ l2 `min` l3. +Proof. + unfold limit_min. case_decide; split. + - by intros [H12 _]. + - intros ?. by split; last trans l2. + - by intros [_ H13]. + - intros ?. split; last done. + apply not_limit_le in H. + trans l3; first done. + apply limit_le_cases. by right. +Qed. + +Lemma period_union_lem_1 t (p1 p2 : period) : + t ∈ p1 ∨ t ∈ p2 → t ∈ p1 ∪ p2. +Proof. + destruct p1 as [s1 e1], p2 as [s2 e2]. + unfold union, period_union. + intros [Ht|Ht]; split. + - apply limit_min_le. left. apply Ht. + - apply limit_lt_max. left. apply Ht. + - apply limit_min_le. right. apply Ht. + - apply limit_lt_max. right. apply Ht. +Qed. + +Definition unifiable '[s1, e1) '[s2, e2) := + s2 ≤ e1 ∧ s1 ≤ e2. + +Instance unifiable_dec : RelDecision unifiable. +Proof. intros [] []. solve_decision. Qed. + +Lemma not_limit_le_lt l1 l2 l3 : + ¬ l1 ≤ l2 < l3 ↔ l2 < l1 ∨ l3 ≤ l2. +Proof. + split. + - intros H123. + destruct (decide (l2 < l1)) as [?|H21%not_limit_lt]; first by left. + destruct (decide (l3 ≤ l2)) as [?|H32%not_limit_le]; first by right. + exfalso. by apply H123. + - intros [H21|H32] contra. + + eapply not_limit_le; [apply H21|apply contra]. + + eapply not_limit_lt; [apply H32|apply contra]. +Qed. + +Lemma limit_lt_le l1 l2 : l1 < l2 → l1 ≤ l2. +Proof. intros Hlt. apply limit_le_cases. by right. Qed. + +Lemma period_union_lem_2 t (p1 p2 : period) : + unifiable p1 p2 → + t ∈ p1 ∪ p2 → t ∈ p1 ∨ t ∈ p2. +Proof. + intros Hunif Hunion. + destruct (decide (t ∈ p1)) as [?|Ht1]; first by left. + destruct (decide (t ∈ p2)) as [?|Ht2]; first by right. + exfalso. + + destruct p1 as [s1 e1], p2 as [s2 e2]. + unfold elem_of, period_elem_of in *. + simpl in *. destruct Hunif as [Hunif1 Hunif2]. + + (* If t is not in p1, then it must be in p2 *) + apply Ht2. clear Ht2. + apply not_limit_le_lt in Ht1. + destruct Ht1 as [Ht1|Ht1]. + - (* t is not in p1 because it is before p1 (where p2 must hence be) *) + destruct Hunion as [Hunion1 Hunion2]. + apply limit_min_le in Hunion1 as [[->|contra]%limit_le_cases | Hunion1]. + { exfalso. by eapply (_ : Irreflexive limit_lt). } + { exfalso. by eapply (asymmetry (R:=limit_lt)). } + split; first done. by eapply limit_lt_le_trans. + - destruct Hunion as [Hunion1 Hunion2]. + apply limit_lt_max in Hunion2 as [Hunion2 | Hunion2]. + + apply limit_le_cases in Ht1 as [->|contra]. + { exfalso. by eapply (_ : Irreflexive limit_lt). } + { exfalso. by eapply (asymmetry (R:=limit_lt)). } + + split; last done. by trans e1. +Qed. + +Instance period_union_comm : Comm (=) period_union. +Proof. + unfold period_union. intros [s1 e1] [s2 e2]. + by rewrite limit_min_comm limit_max_comm. +Qed. + +Instance period_singleton : Singleton timestamp period := + λ t, [t, TsLimit (Z.succ t)). +Lemma period_singleton_lem_1 t : t ∈ ({[t]} : period). +Proof. by split; simpl; last lia. Qed. +Lemma period_singleton_lem_2 t t' : t' ∈ ({[t]} : period) → t' = t. +Proof. + unfold singleton, period_singleton. + intros [H11 H12]. destruct t, t'; try done; simpl in *; lia. +Qed. +Lemma period_singleton_nonempty t : period_nonempty {[t]}. +Proof. + apply period_nonempty_alt_iff. + exists t. apply period_singleton_lem_1. +Qed. + +Lemma unifiable_period_union p1 p2 p3 : + unifiable p1 p2 → unifiable p2 p3 → + unifiable (p1 ∪ p2) p3. +Proof. + destruct p1 as [s1 e1], p2 as [s2 e2], p3 as [s3 e3]. + intros [Hunif11 Hunif12] [Hunif21 Hunif22]. simpl. split. + + apply limit_le_max. by right. + + apply limit_min_le. by right. +Qed. + +Instance unifiable_symm : Symmetric unifiable. +Proof. by intros [] [] []. Qed. + +Definition Σlift {A} {Φ : A → Prop} (R : relation A) : relation {x : A | Φ x} := + λ '(x↾_) '(y↾_), R x y. + +Instance Σlift_symm {A Φ} `{!Symmetric R} : Symmetric (@Σlift A Φ R). +Proof. intros [x Hx] [y Hy] HR. simpl in *. by apply symmetry. Qed. + +(* TODO: probably unused? *) +Instance Σlift_dec {A Φ} `{!RelDecision R} : RelDecision (@Σlift A Φ R). +Proof. intros [x Hx] [y Hy]. by simpl. Qed. + +Definition ne_period_unifiable : relation ne_period := Σlift unifiable. + +Lemma period_unifiable_not_before p1 p2 : ne_period_unifiable p1 p2 → ¬ period_before p1 p2. +Proof. + destruct p1 as [[s1 e1] Hne1], p2 as [[s2 e2] Hne2]. simpl in *. + intros [Hunif1 Hunif2] Hbefore. + apply limit_le_cases in Hunif1 as [->|contra]. + - by eapply (_ : Irreflexive limit_lt). + - by eapply (asymmetry (R:=limit_lt)). +Qed. + +(* TODO: define total relation on Σperiod_nonempty, p1 p2 := unifiable p1 p2 ∨ p1 < p2. + (Then have [AntiSymm unifiable (≤@{Σperiod_nonempty})].) + Show decidability, perform mergesort. + Then make the rest of normalization consist in unification of the periods. + *) + +Definition ne_period_le p1 p2 := ne_period_unifiable p1 p2 ∨ period_before p1 p2. + +Instance ne_period_le_antisymm : AntiSymm ne_period_unifiable ne_period_le. +Proof. + intros p1 p2 [H12|H12] [H21|H21]; [done|done|..]. + - exfalso. apply symmetry in H21. + by eapply period_unifiable_not_before. + - exfalso. by eapply asymmetry. +Qed. + +Lemma ne_period_neither_before_unifiable p1 p2 : + ¬ period_before p1 p2 → ¬ period_before p2 p1 → + ne_period_unifiable p1 p2. +Proof. + destruct p1 as [[s1 e1] Hne1], p2 as [[s2 e2] Hne2]. + simpl in *. by intros ?%not_limit_lt ?%not_limit_lt. +Qed. + +Instance period_before_dec : RelDecision period_before. +Proof. + intros [[s1 e1] ?] [[s2 e2] ?]. simpl in *. + solve_decision. +Qed. + +Lemma ne_period_not_unifiable p1 p2 : + ¬ ne_period_unifiable p1 p2 → + period_before p1 p2 ∨ period_before p2 p1. +Proof. + intros Hnunif. + destruct (decide (period_before p1 p2)) as [?|H12]; first by left. + destruct (decide (period_before p2 p1)) as [?|H21]; first by right. + exfalso. by apply Hnunif, ne_period_neither_before_unifiable. +Qed. + +Instance ne_period_le_total : Total ne_period_le. +Proof. + intros p1 p2. + destruct (decide (ne_period_unifiable p1 p2)) as [Hunif|Hnunif]. + - (* which one we pick does not matter *) + by do 2 left. + - apply ne_period_not_unifiable in Hnunif as [H12|H21]. + + left. by right. + + right. by right. +Qed. -- cgit v1.3