1 files changed, 834 insertions, 0 deletions

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.
+
+*)