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.