Import from e4b104792206ee7ea64bf39c6b7d2c0c230f9d14

1 files changed, 828 insertions, 0 deletions

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