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 : period_seq → Prop :=
  Sorted period_before.

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.

*)