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_seq.v | 834 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 834 insertions(+) create mode 100644 server/formal/period_seq.v (limited to 'server/formal/period_seq.v') diff --git a/server/formal/period_seq.v b/server/formal/period_seq.v new file mode 100644 index 0000000..705e505 --- /dev/null +++ b/server/formal/period_seq.v @@ -0,0 +1,834 @@ +From stdpp Require Import numbers option sorting ssreflect. +From stdpp Require Import options. +From routemon Require Import period util. + +(* This setup would require the proof irrelevance stuff + +Record period_seq := + PeriodSeq + { periods : list period + ; Hnonempty : Forall period_nonempty periods + ; Hsorted : Sorted period_before periods + }. +*) + +Definition period_seq := list ne_period. + +Definition period_seq_nf (ps : period_seq) := + Sorted period_before ps. + +Instance period_seq_elem_of : ElemOf timestamp period_seq := + λ t, Exists (λ p, t ∈ p). +Instance period_seq_elem_of_dec t (ps : period_seq) : Decision (t ∈ ps). +Proof. + induction ps as [|p ps]. + - right. inv 1. + - destruct IHps. + + left. by apply Exists_cons_tl. + + destruct (decide (t ∈ p)). + * left. by apply Exists_cons_hd. + * right. by inv 1. +Qed. + +Instance period_seq_equiv : Equiv period_seq := + λ ps1 ps2, ∀ t, t ∈ ps1 ↔ t ∈ ps2. + +Definition ne_period_intersection (p1 p2 : ne_period) := + let p := `p1 ∩ `p2 in + match decide (period_nonempty p) with + | left H => Some (p ↾ H) + | right _ => None + end. + +Definition ne_period_start (p : ne_period) := + period_start (`p). +Definition ne_period_end (p : ne_period) := + period_end (`p). + +Definition period_seq_intersection_1 go ps1 ps2 := + match ps1, ps2 with + | p1 :: ps1', p2 :: ps2' => + let mp12 := ne_period_intersection p1 p2 in + let rest := if decide (ne_period_end p1 < ne_period_end p2)%lim then go ps1' ps2 else go ps1 ps2' in + match mp12 with + | Some p12 => p12 :: rest + | None => rest + end + | _, _ => [] + end. +Fixpoint period_seq_intersection_aux n := + match n with + | 0 => const (const []) + | S n => period_seq_intersection_1 (period_seq_intersection_aux n) + end. +Instance period_seq_intersection : Intersection period_seq := + λ ps1 ps2, period_seq_intersection_aux (S (length ps1 + length ps2)) ps1 ps2. + +Lemma period_seq_intersection_eq ps1 ps2 : + period_seq_intersection ps1 ps2 = + match ps1, ps2 with + | p1 :: ps1', p2 :: ps2' => + let mp12 := ne_period_intersection p1 p2 in + let rest := if decide (ne_period_end p1 < ne_period_end p2)%lim + then period_seq_intersection ps1' ps2 + else period_seq_intersection ps1 ps2' in + match mp12 with + | Some p12 => p12 :: rest + | None => rest + end + | _, _ => [] + end. +Proof. + destruct ps1 as [|p1 ps1], ps2 as [|p2 ps2]; [done..|]. + have Hlen1 : S (S (length ps1 + length ps2)) = S (length (p1 :: ps1) + length ps2) by simpl; lia. + have Hlen2 : S (S (length ps1 + length ps2)) = S (length ps1 + length (p2 :: ps2)) by simpl; lia. + by rewrite + /period_seq_intersection /period_seq_intersection_aux + !length_cons Nat.add_succ_l Nat.add_succ_r -/period_seq_intersection_aux. +Qed. + +Opaque period_seq_intersection. + +Lemma period_seq_nf_cons p ps : + period_seq_nf (p :: ps) ↔ + period_seq_nf ps ∧ + Forall (λ q, ne_period_end p < ne_period_start q)%lim ps. +Proof. + split. + - intros HSort%Sorted_StronglySorted; last apply _. + inv HSort. repeat split; try done. + + by apply StronglySorted_Sorted. + + eapply Forall_impl; first done. + intros [[sq eq] Hq] Hbef. + by destruct p as [[sp ep] Hp]. + - intros (Hnf & Hlt). + constructor; first done. destruct ps as [|q ps]; constructor. + inv Hlt. destruct p as [[sp ep] Hp], q as [[sq eq] Hq]. by simpl in *. +Qed. + +(* +Lemma list_elem_of_cons_inv `{!EqDecision A} (x y : A) (l : list A) : + x ∈ y :: l ↔ x = y ∨ x ≠ y ∧ x ∈ l. +Proof. + split. + - destruct (decide (x = y)) as [<-|H]. + + intros _. by left. + + inv 1. by right. + - by intros [<-|[_ H]]; constructor. +Qed. +*) + +Lemma list_elem_of_cons_inv {A} (x y : A) (l : list A) : + x ∈ y :: l ↔ x = y ∨ x ∈ l. +Proof. + split. + - by inv 1; [left|right]. + - by intros [<-|H]; constructor. +Qed. + +Lemma Sorted_list_elem_of_R_trans {A} `{!Transitive R} (x y z : A) (l : list A) : + Sorted R (y :: l) → z ∈ y :: l → R x y → R x z. +Proof. + intros [HSort Hyl]%Sorted_inv. + revert y Hyl. + induction HSort as [|y' l' HSort IH Hy'l']; intros y. + - intros _. by inv 1; last inv H2. + - intros Hyy'%HdRel_inv. + intros [->|Hz]%list_elem_of_cons_inv; first done. + intros Hxy. + have : R x y' by eapply (_ : Transitive R). + by apply IH. +Qed. + +Lemma Sorted_list_elem_of_cons_inv {A} `{!Transitive R} (x y : A) (l : list A) : + Sorted R (y :: l) → + x ∈ y :: l → x = y ∧ Forall (R x) l ∨ R y x ∧ x ∈ l. +Proof. + intros HSort [->|H%list_elem_of_In]%list_elem_of_In%in_inv. + - left. by apply Sorted_StronglySorted in HSort as [_ ?]%StronglySorted_inv. + - right. inv HSort. inv H3; first inv H. + by split; first eapply Sorted_list_elem_of_R_trans. +Qed. + +Lemma period_seq_nf_elem_of_cons_inv (p1 p2 : ne_period) (ps : period_seq) : + period_seq_nf (p2 :: ps) → + p1 ∈ p2 :: ps → p1 = p2 ∧ Forall (period_before p1) ps ∨ + period_before p2 p1 ∧ p1 ∈ ps. +Proof. apply Sorted_list_elem_of_cons_inv. Qed. + +Inductive option_Exists {A} (Φ : A → Prop) : option A → Prop := + | Exists_Some (x : A) : Φ x → option_Exists Φ (Some x). + +Lemma option_Exists_from_option {A} Φ (mx : option A) : + option_Exists Φ mx ↔ from_option Φ False mx. +Proof. split; by [inv 1 | destruct mx]. Qed. + +Lemma period_seq_intersect_lem_aux (p1 p2 : ne_period) (ps1 ps2 : period_seq) : + is_Some (ne_period_intersection p1 p2) → + period_seq_nf ps1 → period_seq_nf ps2 → + p1 ∈ ps1 → p2 ∈ ps2 → + option_Exists (.∈ ps1 ∩ ps2) (ne_period_intersection p1 p2). +Proof. + intros Hne. revert ps2. + induction ps1 as [|[s1 e1] ps1]; first inv 3. + intros ps2 Hnf1 Hnf2 H1 H2. revert ps2 Hnf2 H2. + induction ps2 as [|[s2 e2] ps2]; first inv 2. + intros Hnf2 H2. + + apply option_Exists_from_option. + rewrite /intersection period_seq_intersection_eq /=. + apply period_seq_nf_elem_of_cons_inv in H1 as [[-> Hp1]|[Hlt1 H1]]; last done. + + apply period_seq_nf_elem_of_cons_inv in H2 as [[-> Hp2]|[Hlt2 H2]]; last done. + * unfold ne_period_intersection. + case_decide. + -- exfalso. simpl in Hne. + apply limit_le_cases in H as [contra|contra]. + ++ rewrite contra in Hne. by eapply (_ : Irreflexive limit_lt). + ++ by apply asymmetry in Hne. + -- constructor. + * case_decide. + -- case_decide. + ++ (* we need to show that [s1, e1) ## p2 *) + exfalso. assert ([s1, e1) ## p2). + { unfold disjoint, period_disjoint, period_empty. + destruct p2 as [s3 e3]. simpl. + destruct Hlt2 as [Hne2 [Hne3 Hlt2]]. + simpl in Hlt2. + + trans (e1 `min` e2)%lim. + { apply limit_le_cases. left. + trans e1. + - apply limit_min_eq_l, limit_le_cases. right. + by trans e2; last trans s3. + - apply symmetry, limit_min_eq_l, limit_le_cases. by right. } + etrans; first done. + apply limit_max_le. + split. + - apply limit_le_max. by left. + - apply limit_le_max. right. + apply limit_le_cases. right. by trans e2. } + by eapply period_empty_not_nonempty. + ++ by apply IHps2; first apply period_seq_nf_cons in Hnf2 as [_ [? _]]. + -- case_decide. + ++ apply not_limit_le in H. + (* [s1, e1) ## p2 since e1 < e2 and e2 < p2, but [s1, e1) ∩ p2 ≠ ∅ in hyp *) + exfalso. assert ([s1, e1) ## p2). + { unfold disjoint, period_disjoint, period_empty. + destruct p2 as [s3 e3]. simpl. + destruct Hlt2 as [Hne2 [Hne3 Hlt2]]. + simpl in Hlt2. + + rewrite limit_min_l; last first. + { apply limit_le_cases. right. + by trans e2; last trans s3. } + apply limit_le_max. right. + apply limit_le_cases. right. + by trans e2. } + by eapply period_empty_not_nonempty. + ++ constructor. by apply IHps2; first apply period_seq_nf_cons in Hnf2 as (_ & ? & _). + + apply period_seq_nf_elem_of_cons_inv in H2 as [[-> Hp2]|[Hlt2 H2]]; last done. + * case_decide. + -- case_decide. + ++ apply IHps1; try done. + ** by apply period_seq_nf_cons in Hnf1 as (_ & ? & _). + ** by constructor. + ++ apply not_limit_lt in H0. exfalso. assert (p1 ## [s2, e2)). + { unfold disjoint, period_disjoint, period_empty. + destruct p1 as [s3 e3]. simpl. + destruct Hlt1 as [Hne1 [Hne3 Hlt1]]. + simpl in Hlt1. + + trans (e1 `min` e2)%lim. + { apply limit_le_cases. left. + trans e2. + - apply limit_min_eq_r. trans e1; first done. + apply limit_le_cases. right. by trans s3. + - by apply symmetry, limit_min_eq_r. } + etrans; first done. + apply limit_max_le. + split. + - apply limit_le_max. left. + apply limit_le_cases. right. by trans e1. + - apply limit_le_max. by right. } + by eapply period_empty_not_nonempty. + -- case_decide. + ++ constructor. apply IHps1; try done. + ** by apply period_seq_nf_cons in Hnf1 as (_ & ? & _). + ** by constructor. + ++ apply not_limit_lt in H0. apply not_limit_le in H. + exfalso. assert (p1 ## [s2, e2)). + { unfold disjoint, period_disjoint, period_empty. + destruct p1 as [s3 e3]. simpl. + destruct Hlt1 as [Hne1 [Hne3 Hlt1]]. + simpl in Hlt1. + + rewrite limit_min_r; last first. + { trans e1; first done. + apply limit_le_cases. right. + by trans s3. } + trans e1; first done. + apply limit_le_max. left. + apply limit_le_cases. by right. } + by eapply period_empty_not_nonempty. + * case_decide. + -- case_decide. + ++ apply IHps1; try done. + ** by apply period_seq_nf_cons in Hnf1 as (_ & ? & _). + ** by constructor. + ++ by apply IHps2; first apply period_seq_nf_cons in Hnf2 as (_ & ? & _). + -- case_decide; constructor. + ++ apply IHps1; try done. + ** by apply period_seq_nf_cons in Hnf1 as (_ & ? & _). + ** by constructor. + ++ by apply IHps2; first apply period_seq_nf_cons in Hnf2 as (_ & ? & _). +Qed. + +Lemma period_seq_intersection_inv (p : period) (ps1 ps2 : period_seq) : + period_seq_nf ps1 → period_seq_nf ps2 → p ∈ ps1 ∩ ps2 → + ∃ p1 p2, p1 ∈ ps1 ∧ p2 ∈ ps2 ∧ p = p1 ∩ p2. +Proof. + intros Hnf1. revert ps2. + induction ps1; first inv 2. + induction ps2. + { intros _ contra. + rewrite period_seq_intersection_eq in contra. + destruct a. inv contra. } + destruct a as [s1 e1], a0 as [s2 e2]. + intros Hnf2 Hint. + rewrite period_seq_intersection_eq in Hint. + simpl in Hint. case_decide; case_decide. + - apply IHps1 in Hint as (q1 & q2 & Hq1 & Hq2 & ->); last done. + + exists q1, q2. by repeat split; first constructor. + + by apply period_seq_nf_cons in Hnf1 as (_ & ? & _). + - apply IHps2 in Hint as (q1 & q2 & Hq1 & Hq2 & ->). + + exists q1, q2. by repeat split; last constructor. + + by apply period_seq_nf_cons in Hnf2 as (_ & ? & _). + - inv Hint. + + exists [s1, e1), [s2, e2). repeat split; constructor. + + apply IHps1 in H3 as (q1 & q2 & Hq1 & Hq2 & ->); last done. + * exists q1, q2. by repeat split; first constructor. + * by apply period_seq_nf_cons in Hnf1 as (_ & ? & _). + - inv Hint. + + exists [s1, e1), [s2, e2). repeat split; constructor. + + apply IHps2 in H3 as (q1 & q2 & Hq1 & Hq2 & ->). + * exists q1, q2. by repeat split; last constructor. + * by apply period_seq_nf_cons in Hnf2 as (_ & ? & _). +Qed. + +Lemma period_seq_intersection_lem t (ps1 ps2 : period_seq) : + period_seq_nf ps1 → period_seq_nf ps2 → + t ∈ ps1 ∧ t ∈ ps2 ↔ t ∈ ps1 ∩ ps2. +Proof. + intros Hnf1 Hnf2. + split. + - intros [H1 H2]. + unfold elem_of, period_seq_elem_of in H1, H2. + apply Exists_exists in H1 as (p1 & Hp1 & Ht1). + apply Exists_exists in H2 as (p2 & Hp2 & Ht2). + assert (Ht : t ∈ p1 ∩ p2). { by apply intersect_and. } + clear Ht1 Ht2. + unfold elem_of, period_seq_elem_of. + apply Exists_exists. exists (p1 ∩ p2). + split; first apply period_seq_intersect_lem_aux; try done. + apply period_nonempty_alt_iff. by exists t. + - intros (p & Hp & Ht)%Exists_exists. + apply period_seq_intersection_inv in Hp as (p1 & p2 & Hp1 & Hp2 & ->); try done. + apply intersect_and in Ht as [Ht1 Ht2]. + split; apply Exists_exists; by eexists. +Qed. + +Definition period_seq_extent (ps : period_seq) : period := + match head ps, last ps with + | Some [s, _), Some [_, e) => [s, e) + | _, _ => ∅ + end. + +(* +Lemma period_seq_extent_hd ps : + period_seq_nf ps → + Forall (period_start (period_seq_extent ps) + +Lemma period_seq_extent_spec t ps : + period_seq_nf ps → t ∈ ps → + t ∈ period_seq_extent ps. +Proof. + Search StronglySorted. + induction ps as [|p ps]; first inv 2. + intros Hnf. inv 1. + - + +Qed. +*) + +(* +Definition period_seq_intersection_extent (ps1 ps2 : period_seq) : + period_seq_nf ps1 → period_seq_nf ps2 → + period_seq_extent (ps1 ∩ ps2) = period_seq_extent ps1 ∩ period_seq_extent ps2. +Proof. + intros Hnf1 Hnf2. + destruct (decide (period_empty (period_seq_extent (ps1 ∩ ps2)))). + - admit. + - apply period_empty_not_nonempty in n. + apply period_nonempty_equiv_L; first done. + + admit. + + intros t. + Search period equiv eq. +*) + +(* The intersection preserves normal forms *) +Lemma period_seq_intersection_nf (ps1 ps2 : period_seq) : + period_seq_nf ps1 → period_seq_nf ps2 → period_seq_nf (ps1 ∩ ps2). +Proof. + intros Hnf1. revert ps2. + induction ps1 as [|[s1 e1] ps1]; induction ps2 as [|[s2 e2] ps2]; [done..|]. + intros Hnf2. rewrite period_seq_intersection_eq /=. + case_decide. + - case_decide. + + by apply IHps1; first apply period_seq_nf_cons in Hnf1 as (_ & ? & _). + + apply IHps2. by apply period_seq_nf_cons in Hnf2 as (_ & ? & _). + - case_decide. + + apply IHps1 in Hnf2 as Hnf2'; last by apply period_seq_nf_cons in Hnf1 as (_ & ? & _). + destruct Hnf2' as [Hne HSort]. split. + * by constructor; first apply period_empty_not_nonempty. + * constructor; first done. + rewrite {1}/intersection /period_intersection. + apply period_seq_nf_cons in Hnf1 as (Hne1 & Hnf1 & Hlt1). + destruct (ps1 ∩ ([s2, e2) :: ps2)) as [|[sq eq] qs] eqn:Hqs; constructor. + assert (Hq : [sq, eq) ∈ ps1 ∩ ([s2, e2) :: ps2)). + { rewrite Hqs. constructor. } + unfold period_before. repeat split. + -- by apply period_empty_not_nonempty. + -- by eapply Forall_forall; first apply Hne. + -- specialize (IHps1 Hnf1). + apply period_seq_intersection_inv in Hq as ([sq1 eq1] & [sq2 eq2] & Hq1%list_elem_of_In & Hq2 & Hq); [|done..]. + apply (proj1 (List.Forall_forall _ _) Hlt1) in Hq1. + injection Hq as -> ->. + simplify_eq/=. + apply limit_min_lt. left. + apply limit_lt_max. by left. + + apply IHps1 in Hnf2 as Hnf2'; last by apply period_seq_nf_cons in Hnf1 as (_ & ? & _). + destruct Hnf2' as [Hne HSort]. + apply not_limit_lt in H0. split. + * constructor. + -- by apply period_empty_not_nonempty. + -- apply IHps2. by apply period_seq_nf_cons in Hnf2 as (_ & ? & _). + * constructor. + -- apply IHps2. by apply period_seq_nf_cons in Hnf2 as (_ & ? & _). + -- rewrite {1}/intersection /period_intersection. + apply period_seq_nf_cons in Hnf1 as Hnf1'. + destruct Hnf1' as (Hp1 & Hnf1' & Hne1). + apply period_seq_nf_cons in Hnf2 as (Hne2 & Hnf2 & Hlt2). + apply IHps2 in Hnf2 as Hnf2'. + destruct (([s1, e1) :: ps1) ∩ ps2) as [|[sq eq] qs] eqn:Hqs; constructor. + assert (Hq : [sq, eq) ∈ ([s1, e1) :: ps1) ∩ ps2). + { rewrite Hqs. constructor. } + unfold period_before. repeat split. + ++ by apply period_empty_not_nonempty. + ++ by eapply Forall_forall; first apply Hnf2'. + ++ apply period_seq_intersection_inv in Hq as ([sq1 eq1] & [sq2 eq2] & Hq1 & Hq2%list_elem_of_In & Hq); [|done..]. + apply (proj1 (List.Forall_forall _ _) Hlt2) in Hq2. + injection Hq as -> ->. + simplify_eq/=. + apply limit_min_lt. right. + apply limit_lt_max. by right. +Qed. + +Definition period_seq_intersection_comm_equiv ps1 ps2 : + period_seq_nf ps1 → period_seq_nf ps2 → + ps1 ∩ ps2 ≡ ps2 ∩ ps1. +Proof. + intros Hnf1 Hnf2 t. + split; by intros [H2 H1]%period_seq_intersection_lem; + first apply period_seq_intersection_lem. +Qed. + +Lemma period_seq_nf_cons_equiv_inv_start_1 p1 ps1 p2 ps2: + period_seq_nf (p1 :: ps1) → + period_seq_nf (p2 :: ps2) → + p1 :: ps1 ≡ p2 :: ps2 → + ¬ (period_start p1 < period_start p2)%lim. +Proof. + intros Hnf1 Hnf2 Hequiv Hp12. + apply period_seq_nf_cons in Hnf1 as (Hne1 & Hnf1 & Hlt1), Hnf2 as (Hne2 & Hnf2 & Hlt2). + destruct p1 as [s1 e1], p2 as [s2 e2]. simpl in Hp12. + destruct s2 as [|s2|]; [by destruct s1| |done]. + destruct s1 as [|s1|]; last done. + - destruct e1 as [|e1|]; first done. + + assert (Z.pred (s2 `min` e1) ∈ [-∞, e1) :: ps1). + { constructor. by split; [|simpl; lia]. } + apply Hequiv in H. inv H. + * destruct H1 as [H1 _]. simpl in H1. lia. + * apply Exists_exists in H1 as ([sp ep] & Hp & Hs2). + rewrite Forall_forall in Hlt2. + apply Hlt2 in Hp. simpl in Hp. + destruct Hs2 as [Hs21 Hs22]. + assert (contra : (s2 < s2)%lim). + { trans e2; first done. + apply (limit_lt_le_trans sp); first done. + etrans; first apply Hs21. simpl. lia. } + by eapply (_ : Irreflexive limit_lt). + + assert (Z.pred s2 ∈ [-∞, +∞) :: ps1). + { by constructor. } + apply Hequiv in H. inv H. + * destruct H1 as [H1 _]. simpl in H1. lia. + * apply Exists_exists in H1 as ([sp ep] & Hp & Hs2). + rewrite Forall_forall in Hlt2. + apply Hlt2 in Hp. simpl in Hp. + destruct Hs2 as [Hs21 Hs22]. + assert (contra : (s2 < s2)%lim). + { trans e2; first done. + apply (limit_lt_le_trans sp); first done. + etrans; first apply Hs21. simpl. lia. } + by eapply (_ : Irreflexive limit_lt). + - assert (s1 ∈ [s1, e1) :: ps1). + { by constructor. } + apply Hequiv in H. inv H. + + destruct H1 as [[[= ->]|H1]%limit_le_cases _]. + * by eapply (_ : Irreflexive limit_lt). + * by eapply (asymmetry (R:=limit_lt)). + + apply Exists_exists in H1 as ([sp ep] & Hp & Hs1). + rewrite Forall_forall in Hlt2. + apply Hlt2 in Hp. simpl in Hp. + assert (contra : (s1 < s1)%lim). + { trans s2; first done. + trans e2; first done. + by apply (limit_lt_le_trans sp); last apply Hs1. } + by eapply (_ : Irreflexive limit_lt). +Qed. + +Instance period_seq_equiv_trans : Transitive (≡@{period_seq}). +Proof. + intros ps1 ps2 ps3 Heq12 Heq23 t. split. + - by intros Ht%Heq12%Heq23. + - by intros Ht%Heq23%Heq12. +Qed. + +Instance period_seq_equiv_symm : Symmetric (≡@{period_seq}). +Proof. intros ps1 ps2 Heq12 t. split; by intros Ht%Heq12. Qed. + +Lemma period_seq_nf_cons_equiv_inv_start p1 ps1 p2 ps2: + period_seq_nf (p1 :: ps1) → + period_seq_nf (p2 :: ps2) → + p1 :: ps1 ≡ p2 :: ps2 → + period_start p1 = period_start p2. +Proof. + intros Hnf1 Hnf2 Hequiv. + destruct (decide (period_start p1 < period_start p2)%lim) as [Hs12|Hs21]. + - exfalso. by eapply period_seq_nf_cons_equiv_inv_start_1 in Hs12. + - apply not_limit_lt, limit_le_cases in Hs21 as [Hs21|Hs21]; first done. + exfalso. by eapply period_seq_nf_cons_equiv_inv_start_1 in Hs21. +Qed. + +Lemma period_seq_nf_cons_equiv_inv_end_1 p1 ps1 p2 ps2: + period_seq_nf (p1 :: ps1) → + period_seq_nf (p2 :: ps2) → + p1 :: ps1 ≡ p2 :: ps2 → + ¬ (period_end p1 < period_end p2)%lim. +Proof. + intros Hnf1 Hnf2 Hequiv Hp12. + assert (Hs : period_start p1 = period_start p2). + { by eapply period_seq_nf_cons_equiv_inv_start. } + apply period_seq_nf_cons in Hnf1 as (Hne1 & Hnf1 & Hlt1), Hnf2 as (Hne2 & Hnf2 & Hlt2). + destruct p1 as [s1 e1], p2 as [s2 e2]. simpl in Hs, Hp12. + rewrite <-Hs in *. rename s1 into s. clear Hs s2. + destruct e1 as [|e1|]; [by destruct s| |done]. + assert (e1 ∈ [s, e2) :: ps2). + { constructor. by split; [apply limit_le_cases; right|]. } + apply Hequiv in H. inv H. + + destruct H1 as [_ H12]. by eapply (_ : Irreflexive limit_lt). + + apply Exists_exists in H1 as (p & Hp & He1). + rewrite Forall_forall in Hlt1. + apply Hlt1 in Hp. + destruct p as [sp ep]. + unfold period_end, period_start in Hp. + assert (contra : (e1 < e1)%lim). + { by eapply limit_lt_le_trans; last apply He1. } + by eapply (_ : Irreflexive limit_lt). +Qed. + +Lemma period_seq_nf_cons_equiv_inv_end p1 ps1 p2 ps2: + period_seq_nf (p1 :: ps1) → + period_seq_nf (p2 :: ps2) → + p1 :: ps1 ≡ p2 :: ps2 → + period_end p1 = period_end p2. +Proof. + intros Hnf1 Hnf2 Hequiv. + destruct (decide (period_end p1 < period_end p2)%lim) as [He12|He21]. + - exfalso. by eapply period_seq_nf_cons_equiv_inv_end_1 in He12. + - apply not_limit_lt, limit_le_cases in He21 as [He21|He21]; first done. + exfalso. by eapply period_seq_nf_cons_equiv_inv_end_1 in He21. +Qed. + +Lemma period_seq_nf_cons_equiv_inv p1 ps1 p2 ps2: + period_seq_nf (p1 :: ps1) → + period_seq_nf (p2 :: ps2) → + p1 :: ps1 ≡ p2 :: ps2 → + p1 = p2. +Proof. + intros Hnf1 Hnf2 Hequiv. + trans [period_start p1, period_end p1); first by destruct p1. + trans [period_start p2, period_end p2); last by destruct p2. + erewrite period_seq_nf_cons_equiv_inv_start; try done. + by erewrite period_seq_nf_cons_equiv_inv_end. +Qed. + +Lemma period_seq_nf_equiv_L ps1 ps2 : + period_seq_nf ps1 → + period_seq_nf ps2 → + ps1 ≡ ps2 → ps1 = ps2. +Proof. + intros Hnf1. revert ps2. + induction ps1 as [|p1 ps1]; intros ps2 Hnf2 Hequiv. + - destruct ps2; first done. + assert (period_nonempty p) as [t Ht]%period_nonempty_alt_iff. + { inv Hnf2. by inv H. } + assert (t ∈ p :: ps2) as contra%Hequiv. + { by apply Exists_cons_hd. } + inv contra. + - destruct ps2 as [|p2 ps2]. + + assert (period_nonempty p1) as [t Ht]%period_nonempty_alt_iff. + { inv Hnf1. by inv H. } + assert (t ∈ p1 :: ps1) as contra%Hequiv. + { by apply Exists_cons_hd. } + inv contra. + + assert (p1 = p2) as <-. + { by eapply period_seq_nf_cons_equiv_inv. } + rename p1 into p. + apply period_seq_nf_cons in Hnf1 as (Hne1 & Hnf1 & Hlt1), Hnf2 as (Hne2 & Hnf2 & Hlt2). + f_equal. apply IHps1; [done..|]. + intros t. split; intros Ht. + * assert (t ∈ p :: ps1) as H%Hequiv. + { by apply Exists_cons_tl. } + inv H; last done. + apply Exists_exists in Ht as ([sq eq] & Hp & Ht). + rewrite Forall_forall in Hlt1. + apply Hlt1 in Hp. + exfalso. destruct p as [s e]. + simpl in *. + assert (contra : (t < t)%lim). + { trans e; first apply H1. + by eapply limit_lt_le_trans; last apply Ht. } + by eapply (_ : Irreflexive limit_lt). + * assert (t ∈ p :: ps2) as H%Hequiv. + { by apply Exists_cons_tl. } + inv H; last done. + apply Exists_exists in Ht as ([sq eq] & Hp & Ht). + rewrite Forall_forall in Hlt2. + apply Hlt2 in Hp. + exfalso. destruct p as [s e]. + simpl in *. + assert (contra : (t < t)%lim). + { trans e; first apply H1. + by eapply limit_lt_le_trans; last apply Ht. } + by eapply (_ : Irreflexive limit_lt). +Qed. + +Definition period_seq_intersection_comm ps1 ps2 : + period_seq_nf ps1 → period_seq_nf ps2 → + ps1 ∩ ps2 = ps2 ∩ ps1. +Proof. + intros Hnf1 Hnf2. + apply period_seq_nf_equiv_L. + - by apply period_seq_intersection_nf. + - by apply period_seq_intersection_nf. + - by apply period_seq_intersection_comm_equiv. +Qed. + +Instance period_seq_equiv_refl : Reflexive (≡@{period_seq}). +Proof. done. Qed. + +Instance period_seq_equiv_equivalence : Equivalence (≡@{period_seq}). +Proof. split; apply _. Qed. + +Variant bound := + | LtBound of limit + | GeBound of limit. + +Definition bound_le b1 b2 := + match b1, b2 with + | GeBound l1, GeBound l2 => (l1 ≤ l2)%lim + | GeBound _, LtBound _ => True + | LtBound l1, LtBound l2 => (l1 ≤ l2)%lim + | LtBound _, GeBound _ => False + end. +Instance bound_lt_dec : RelDecision bound_le. +Proof. intros [l1|l1] [l2|l2]; simpl; solve_decision. Qed. + +Instance bound_le_refl : Reflexive bound_le. +Proof. by intros []; simpl. Qed. + +Instance bound_le_trans : Transitive bound_le. +Proof. intros [] [] [] ? ?; simpl in *; done || by etrans. Qed. + +Instance bound_le_preorder : PreOrder bound_le. +Proof. split; apply _. Qed. + +Instance bound_le_antisymm : AntiSymm (=) bound_le. +Proof. intros [] [] ? ?; simpl in *; done || f_equal; by eapply (_ : AntiSymm (=) limit_le). Qed. + +Instance bound_le_partial_order : PartialOrder bound_le. +Proof. split; apply _. Qed. + +Instance bound_le_trichotomy : Trichotomy (strict bound_le). +Proof. + intros [] []; simpl in *. + - destruct (trichotomy _ l l0) as [?|[?|?]]. + + left. split; simpl. + * apply limit_le_cases. by right. + * by apply not_limit_le. + + right. left. by subst. + + right. right. split; simpl. + * apply limit_le_cases. by right. + * by apply not_limit_le. + - right. right. split; simpl; [done|by intros ?]. + - left. split; simpl; [done|by intros ?]. + - destruct (trichotomy _ l l0) as [?|[?|?]]. + + left. split; simpl. + * apply limit_le_cases. by right. + * by apply not_limit_le. + + right. left. by subst. + + right. right. split; simpl. + * apply limit_le_cases. by right. + * by apply not_limit_le. +Qed. + +Instance bound_le_total_order : TotalOrder bound_le. +Proof. split; apply _. Qed. + +Definition period_bounds '[s, e) := + if decide (period_nonempty [s, e)) then [GeBound s; LtBound e] else []. + +Definition period_seq_bounds (ps : period_seq) := + ps ≫= period_bounds. + +Definition period_seq_bounds_sorted (ps : period_seq) := + merge_sort bound_le (period_seq_bounds ps). + +Variant window_filter_action := + KickLeft | KickRight | NoAction. +Fixpoint window_filter_aux {A} (f : A → A → window_filter_action) (x : A) (l : list A) := + match l with + | [] => [x] + | y :: l' => + match f x y with + | KickLeft => window_filter_aux f y l' + | KickRight => window_filter_aux f x l' + | NoAction => x :: window_filter_aux f y l' + end + end. +Definition window_filter {A} (f : A → A → window_filter_action) (l : list A) := + match l with + | [] => [] + | x :: l' => window_filter_aux f x l' + end. + +Definition period_seq_bounds_clean (ps : period_seq) := + window_filter (λ b1 b2, match b1, b2 with + | GeBound _, LtBound _ => NoAction + | GeBound _, GeBound _ => KickRight + | LtBound _, GeBound _ => NoAction + | LtBound _, LtBound _ => KickLeft + end) + (period_seq_bounds_sorted ps). + +Fixpoint period_seq_from_bounds (bs : list bound) : period_seq := + match bs with + | GeBound s :: LtBound e :: bs' => [s, e) :: period_seq_from_bounds bs' + | _ => [] + end. + +Definition period_seq_normalize (ps : period_seq) := + period_seq_from_bounds (period_seq_bounds_clean ps). + + +Lemma period_seq_normalize_lem_1 (ps : period_seq) : + period_seq_normalize ps ≡ ps. +Proof. + Search merge_sort. + Search Total Trichotomy. + + +(* TODO: continue here *) Admitted. + +Lemma period_seq_normalize_lem_2 (ps : period_seq) : + period_seq_nf (period_seq_normalize ps). +Proof. (* TODO: and here *) Admitted. + +Definition period_seq_union (ps1 ps2 : period_seq) := + period_seq_normalize (ps1 ++ ps2). +Lemma period_seq_union_lem t ps1 ps2 : + t ∈ period_seq_union ps1 ps2 ↔ t ∈ ps1 ∨ t ∈ ps2. +Proof. + split. + - intros Ht%(period_seq_normalize_lem_1 (ps1 ++ ps2)). + apply Exists_app in Ht as [Ht|Ht]; by [left|right]. + - intros [Ht|Ht]; apply period_seq_normalize_lem_1, Exists_app; by [left|right]. +Qed. +Lemma period_seq_union_nf ps1 ps2 : + period_seq_nf (period_seq_union ps1 ps2). +Proof. apply period_seq_normalize_lem_2. Qed. + +Definition nf_period_seq := sig period_seq_nf. + +Instance period_seq_nf_pi ps : ProofIrrel (period_seq_nf ps). +Proof. + unfold period_seq_nf. intros [P11 P12] [P21 P22]. + f_equal; [apply Forall_pi | apply Sorted_pi]; apply _. +Qed. + +Instance period_seq_empty : Empty period_seq := []. +Lemma period_seq_empty_nf : period_seq_nf ∅. +Proof. done. Qed. + +Instance period_seq_singleton : Singleton timestamp period_seq := + λ t, [{[t]}]. +Lemma period_seq_singleton_lem_1 t : t ∈ ({[t]} : period_seq). +Proof. + unfold singleton, period_seq_singleton. + constructor. apply period_singleton_lem_1. +Qed. +Lemma period_seq_singleton_lem_2 t t' : t' ∈ ({[t]} : period_seq) → t' = t. +Proof. + unfold singleton, period_seq_singleton. + inv 1; last inv H1. + by apply period_singleton_lem_2. +Qed. +Lemma period_seq_singleton_nf t : period_seq_nf {[t]}. +Proof. + unfold singleton, period_seq_singleton. + split. + - constructor; last constructor. + apply period_singleton_nonempty. + - constructor; constructor. +Qed. + +Instance nf_period_seq_elem_of : ElemOf timestamp nf_period_seq := + λ t ps, t ∈ `ps. +Instance nf_period_seq_empty : Empty nf_period_seq := + ∅ ↾ period_seq_empty_nf. +Instance nf_period_seq_union : Union nf_period_seq := + λ '(ps1↾_) '(ps2↾_), period_seq_union ps1 ps2 ↾ (period_seq_union_nf ps1 ps2). +Instance nf_period_seq_singleton : Singleton timestamp nf_period_seq := + λ t, {[t]} ↾ period_seq_singleton_nf t. + +Instance nf_period_seq_semiset : SemiSet timestamp nf_period_seq. +Proof. + split. + - intros t Ht. inv Ht. + - split. + + apply period_seq_singleton_lem_2. + + intros <-. apply period_seq_singleton_lem_1. + - intros [ps1 Hnf1] [ps2 Hnf2] t. + unfold union, nf_period_seq_union, elem_of, nf_period_seq_elem_of. + simpl. apply period_seq_union_lem. +Qed. + +Instance nf_period_seq_intersection : Intersection nf_period_seq := + λ '(ps1↾Hnf1) '(ps2↾Hnf2), (ps1 ∩ ps2) ↾ (period_seq_intersection_nf ps1 ps2 Hnf1 Hnf2). + +(* TODO: difference! + +Instance nf_period_seq_set : Set_ timestamp nf_period_seq. +Proof. (* TODO *) Qed. + +*) -- cgit v1.3