From 973aec43ea54bbf95b64fbcb636403401d1ca60e Mon Sep 17 00:00:00 2001 From: Rutger Broekhoff Date: Fri, 28 Aug 2026 18:03:05 +0200 Subject: Import from e4b104792206ee7ea64bf39c6b7d2c0c230f9d14 --- server/formal/.envrc | 1 + server/formal/.gitignore | 17 + server/formal/Makefile | 55 +++ server/formal/_CoqProject | 5 + server/formal/flake.lock | 61 ++++ server/formal/flake.nix | 26 ++ server/formal/period.v | 828 ++++++++++++++++++++++++++++++++++++++++++++ server/formal/period_seq.v | 834 +++++++++++++++++++++++++++++++++++++++++++++ server/formal/util.v | 92 +++++ 9 files changed, 1919 insertions(+) create mode 100644 server/formal/.envrc create mode 100644 server/formal/.gitignore create mode 100644 server/formal/Makefile create mode 100644 server/formal/_CoqProject create mode 100644 server/formal/flake.lock create mode 100644 server/formal/flake.nix create mode 100644 server/formal/period.v create mode 100644 server/formal/period_seq.v create mode 100644 server/formal/util.v (limited to 'server/formal') diff --git a/server/formal/.envrc b/server/formal/.envrc new file mode 100644 index 0000000..3550a30 --- /dev/null +++ b/server/formal/.envrc @@ -0,0 +1 @@ +use flake diff --git a/server/formal/.gitignore b/server/formal/.gitignore new file mode 100644 index 0000000..9023475 --- /dev/null +++ b/server/formal/.gitignore @@ -0,0 +1,17 @@ +*.aux +*.glob +*.vio +*.vo +*.vok +*.vos +.CoqMakefile.d +.Makefile.coq.d +.direnv +.lia.cache +Makefile.coq +Makefile.coq.conf +*#*.v# +*#*.vok# +*~ +.#* +\#*# \ No newline at end of file diff --git a/server/formal/Makefile b/server/formal/Makefile new file mode 100644 index 0000000..ac8dba0 --- /dev/null +++ b/server/formal/Makefile @@ -0,0 +1,55 @@ +# Default target +all: Makefile.coq + +@$(MAKE) -f Makefile.coq all +.PHONY: all + +# Permit local customization +-include Makefile.local + +# Forward most targets to Coq makefile (with some trick to make this phony) +%: Makefile.coq phony + @#echo "Forwarding $@" + +@$(MAKE) -f Makefile.coq $@ +phony: ; +.PHONY: phony + +clean: Makefile.coq + +@$(MAKE) -f Makefile.coq clean + @# Make sure not to enter the `_opam` folder. + find [a-z]*/ \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true + rm -f Makefile.coq .lia.cache builddep/* +.PHONY: clean + +# Create Coq Makefile. +Makefile.coq: _CoqProject Makefile + "$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES) + +# Install build-dependencies +OPAMFILES=$(wildcard *.opam) +BUILDDEPFILES=$(addsuffix -builddep.opam, $(addprefix builddep/,$(basename $(OPAMFILES)))) + +builddep/%-builddep.opam: %.opam Makefile + @echo "# Creating builddep package for $<." + @mkdir -p builddep + @sed <$< -E 's/^(build|install|remove):.*/\1: []/; s/"(.*)"(.*= *version.*)$$/"\1-builddep"\2/;' >$@ + +builddep-opamfiles: $(BUILDDEPFILES) +.PHONY: builddep-opamfiles + +builddep: builddep-opamfiles + @# We want opam to not just install the build-deps now, but to also keep satisfying these + @# constraints. Otherwise, `opam upgrade` may well update some packages to versions + @# that are incompatible with our build requirements. + @# To achieve this, we create a fake opam package that has our build-dependencies as + @# dependencies, but does not actually install anything itself. + @echo "# Installing builddep packages." + @opam install $(OPAMFLAGS) $(BUILDDEPFILES) +.PHONY: builddep + +# Backwards compatibility target +build-dep: builddep +.PHONY: build-dep + +# Some files that do *not* need to be forwarded to Makefile.coq. +# ("::" lets Makefile.local overwrite this.) +Makefile Makefile.local _CoqProject $(OPAMFILES):: ; diff --git a/server/formal/_CoqProject b/server/formal/_CoqProject new file mode 100644 index 0000000..92d635c --- /dev/null +++ b/server/formal/_CoqProject @@ -0,0 +1,5 @@ +-Q . routemon + +util.v +period.v +period_seq.v \ No newline at end of file diff --git a/server/formal/flake.lock b/server/formal/flake.lock new file mode 100644 index 0000000..f4a7de9 --- /dev/null +++ b/server/formal/flake.lock @@ -0,0 +1,61 @@ +{ + "nodes": { + "flake-utils": { + "inputs": { + "systems": "systems" + }, + "locked": { + "lastModified": 1731533236, + "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1777077449, + "narHash": "sha256-AIiMJiqvGrN4HyLEbKAoCSRRYn0rnlW5VbKNIMIYqm4=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "a4bf06618f0b5ee50f14ed8f0da77d34ecc19160", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-25.11", + "repo": "nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "flake-utils": "flake-utils", + "nixpkgs": "nixpkgs" + } + }, + "systems": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/server/formal/flake.nix b/server/formal/flake.nix new file mode 100644 index 0000000..57efa11 --- /dev/null +++ b/server/formal/flake.nix @@ -0,0 +1,26 @@ +{ + inputs = { + nixpkgs.url = "github:NixOS/nixpkgs/nixos-25.11"; + flake-utils.url = "github:numtide/flake-utils"; + }; + + outputs = { self, nixpkgs, flake-utils, ... }: + flake-utils.lib.eachDefaultSystem (system: + let + pkgs = import nixpkgs { inherit system; }; + + # From 22-04-2026 + stdpp = with pkgs; coqPackages.lib.overrideCoqDerivation { + version = "dev"; + release."dev".sha256 = "hN+sEZcIaFoFF2+4dStTc0TRz5A03US6csEk5q0r/z8="; + release."dev".rev = "d3c67aa46ed22b1e593457cd34fc711f1a53b8be"; + } coqPackages.stdpp; + in + { + devShells.default = with pkgs; mkShell { + buildInputs = [ coq stdpp ]; + }; + + formatter = pkgs.nixpkgs-fmt; + }); +} 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. 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. + +*) diff --git a/server/formal/util.v b/server/formal/util.v new file mode 100644 index 0000000..8e16ffc --- /dev/null +++ b/server/formal/util.v @@ -0,0 +1,92 @@ +From stdpp Require Import numbers option sorting ssreflect. +From stdpp Require Import options. + +Definition transportf {X} (P : X → Type) {x x' : X} : x = x' → P x → P x'. +Proof. by induction 1. Defined. + +Instance HdRel_pi {A} (R : relation A) `{!EqDecision A} `{!∀ x y, ProofIrrel (R x y)} a l : ProofIrrel (HdRel R a l). +Proof. + intros HR1 HR2. + assert (Hnil : ∀ xs (Hxs : [] = xs) (HR : HdRel R a xs), + HR = transportf _ Hxs (HdRel_nil R a)). + { intros. destruct HR; last done. + by replace Hxs with (eq_refl ([] : list A)); last apply eq_pi, list_eq_dec. } + assert (Hcons : ∀ xs x y xs' (Hxs : y :: xs' = xs) (HR : HdRel R x xs) (Hxy : R x y), + HR = transportf (HdRel R x) Hxs (HdRel_cons R x y xs' Hxy)). + { intros. destruct HR; first done. + injection Hxs as <- <-. + replace Hxs with (eq_refl (y :: xs')); last apply eq_pi, list_eq_dec. + simpl. + by replace r with Hxy by apply H. } + destruct l. + - trans (transportf (HdRel R a) eq_refl (HdRel_nil R a)). + + apply Hnil. + + symmetry. apply Hnil. + - apply HdRel_inv in HR1 as Haa0. + trans (transportf (HdRel R a) eq_refl (HdRel_cons R a a0 l Haa0)). + + apply Hcons. + + symmetry. apply Hcons. +Qed. + +Instance Sorted_pi {A} (R : relation A) `{!EqDecision A} `{!∀ x y, ProofIrrel (R x y)} l : ProofIrrel (Sorted R l). +Proof. + intros HS1 HS2. + assert (Hbase : ∀ xs (Hxs : [] = xs) (HS : Sorted R xs), HS = transportf _ Hxs (Sorted_nil R)). + { intros. destruct HS; last done. + by replace Hxs with (eq_refl ([] : list A)); last apply eq_pi, list_eq_dec. } + assert (Hind : ∀ xs x xs' + (Hxs : x :: xs' = xs) (HS : Sorted R xs) + (Hx : HdRel R x xs') (HS' : Sorted R xs') + (IH : ∀ HS1' HS2' : Sorted R xs', HS1' = HS2'), + HS = transportf _ Hxs (Sorted_cons HS' Hx)). + { intros. destruct HS; first done. + injection Hxs as <- <-. + replace Hxs with (eq_refl (x :: xs')); last apply eq_pi, list_eq_dec. + simpl. + replace h with Hx by apply: HdRel_pi. + by replace HS with HS' by apply IH. } + induction l. + - trans (transportf _ eq_refl (Sorted_nil R)). + + apply Hbase. + + symmetry. apply Hbase. + - destruct (Sorted_inv HS1) as [Hl Hal]. + trans (transportf _ eq_refl (Sorted_cons Hl Hal)). + + apply Hind, IHl. + + symmetry. apply Hind, IHl. +Qed. + +Instance Forall_pi {A} (P : A → Prop) (l : list A) `{!EqDecision A} `{!∀ a, ProofIrrel (P a)} : ProofIrrel (Forall P l). +Proof. + intros HF1 HF2. + assert (Hbase : ∀ xs (Hxs : [] = xs) (HF : Forall P xs), HF = transportf (Forall P) Hxs (ListDef.Forall_nil P)). + { intros xs Hxs HF. destruct HF; last done. + by replace Hxs with (eq_refl ([] : list A)); last apply eq_pi, list_eq_dec. } + assert (Hind : ∀ xs x xs' + (Hxs : x :: xs' = xs) (HF : Forall P xs) + (Hx : P x) (HF' : Forall P xs') + (IH : ∀ HF1' HF2' : Forall P xs', HF1' = HF2'), + HF = transportf _ Hxs (ListDef.Forall_cons P x xs' Hx HF')). + { intros. destruct HF; first done. + injection Hxs as <- <-. + replace Hxs with (eq_refl (x :: xs')); last apply eq_pi, list_eq_dec. + simpl. + replace p with Hx by apply H. + by replace HF with HF' by apply IH. } + induction l. + - trans (transportf _ eq_refl (ListDef.Forall_nil P)). + + apply Hbase. + + symmetry. apply Hbase. + - apply Forall_inv in HF1 as Ha. + apply Forall_inv_tail in HF1 as Hl. + trans (transportf _ eq_refl (ListDef.Forall_cons P a l Ha Hl)). + + apply Hind, IHl. + + symmetry. apply Hind, IHl. +Qed. + +Instance ex_pi {A} {B : A → Prop} `{!ProofIrrel A} `{!∀ x, ProofIrrel (B x)} : + ProofIrrel (∃ (x : A), B x). +Proof. + intros [x Hx] [y Hy]. + assert (y = x) by apply proof_irrel. subst. + assert (Hx = Hy) by apply proof_irrel. by subst. +Qed. -- cgit v1.3