summaryrefslogtreecommitdiffstats
path: root/server/formal
diff options
context:
space:
mode:
authorRutger Broekhoff2026-08-28 18:03:05 +0200
committerRutger Broekhoff2026-08-28 18:03:05 +0200
commit973aec43ea54bbf95b64fbcb636403401d1ca60e (patch)
tree41b7911c420766a9b463245b9296f44c5bf35258 /server/formal
downloadroutemon-973aec43ea54bbf95b64fbcb636403401d1ca60e.tar.gz
routemon-973aec43ea54bbf95b64fbcb636403401d1ca60e.zip
Import from e4b104792206ee7ea64bf39c6b7d2c0c230f9d14
Diffstat (limited to 'server/formal')
-rw-r--r--server/formal/.envrc1
-rw-r--r--server/formal/.gitignore17
-rw-r--r--server/formal/Makefile55
-rw-r--r--server/formal/_CoqProject5
-rw-r--r--server/formal/flake.lock61
-rw-r--r--server/formal/flake.nix26
-rw-r--r--server/formal/period.v828
-rw-r--r--server/formal/period_seq.v834
-rw-r--r--server/formal/util.v92
9 files changed, 1919 insertions, 0 deletions
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 @@
1*.aux
2*.glob
3*.vio
4*.vo
5*.vok
6*.vos
7.CoqMakefile.d
8.Makefile.coq.d
9.direnv
10.lia.cache
11Makefile.coq
12Makefile.coq.conf
13*#*.v#
14*#*.vok#
15*~
16.#*
17\#*# \ 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 @@
1# Default target
2all: Makefile.coq
3 +@$(MAKE) -f Makefile.coq all
4.PHONY: all
5
6# Permit local customization
7-include Makefile.local
8
9# Forward most targets to Coq makefile (with some trick to make this phony)
10%: Makefile.coq phony
11 @#echo "Forwarding $@"
12 +@$(MAKE) -f Makefile.coq $@
13phony: ;
14.PHONY: phony
15
16clean: Makefile.coq
17 +@$(MAKE) -f Makefile.coq clean
18 @# Make sure not to enter the `_opam` folder.
19 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
20 rm -f Makefile.coq .lia.cache builddep/*
21.PHONY: clean
22
23# Create Coq Makefile.
24Makefile.coq: _CoqProject Makefile
25 "$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
26
27# Install build-dependencies
28OPAMFILES=$(wildcard *.opam)
29BUILDDEPFILES=$(addsuffix -builddep.opam, $(addprefix builddep/,$(basename $(OPAMFILES))))
30
31builddep/%-builddep.opam: %.opam Makefile
32 @echo "# Creating builddep package for $<."
33 @mkdir -p builddep
34 @sed <$< -E 's/^(build|install|remove):.*/\1: []/; s/"(.*)"(.*= *version.*)$$/"\1-builddep"\2/;' >$@
35
36builddep-opamfiles: $(BUILDDEPFILES)
37.PHONY: builddep-opamfiles
38
39builddep: builddep-opamfiles
40 @# We want opam to not just install the build-deps now, but to also keep satisfying these
41 @# constraints. Otherwise, `opam upgrade` may well update some packages to versions
42 @# that are incompatible with our build requirements.
43 @# To achieve this, we create a fake opam package that has our build-dependencies as
44 @# dependencies, but does not actually install anything itself.
45 @echo "# Installing builddep packages."
46 @opam install $(OPAMFLAGS) $(BUILDDEPFILES)
47.PHONY: builddep
48
49# Backwards compatibility target
50build-dep: builddep
51.PHONY: build-dep
52
53# Some files that do *not* need to be forwarded to Makefile.coq.
54# ("::" lets Makefile.local overwrite this.)
55Makefile 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 @@
1-Q . routemon
2
3util.v
4period.v
5period_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 @@
1{
2 "nodes": {
3 "flake-utils": {
4 "inputs": {
5 "systems": "systems"
6 },
7 "locked": {
8 "lastModified": 1731533236,
9 "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
10 "owner": "numtide",
11 "repo": "flake-utils",
12 "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
13 "type": "github"
14 },
15 "original": {
16 "owner": "numtide",
17 "repo": "flake-utils",
18 "type": "github"
19 }
20 },
21 "nixpkgs": {
22 "locked": {
23 "lastModified": 1777077449,
24 "narHash": "sha256-AIiMJiqvGrN4HyLEbKAoCSRRYn0rnlW5VbKNIMIYqm4=",
25 "owner": "NixOS",
26 "repo": "nixpkgs",
27 "rev": "a4bf06618f0b5ee50f14ed8f0da77d34ecc19160",
28 "type": "github"
29 },
30 "original": {
31 "owner": "NixOS",
32 "ref": "nixos-25.11",
33 "repo": "nixpkgs",
34 "type": "github"
35 }
36 },
37 "root": {
38 "inputs": {
39 "flake-utils": "flake-utils",
40 "nixpkgs": "nixpkgs"
41 }
42 },
43 "systems": {
44 "locked": {
45 "lastModified": 1681028828,
46 "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
47 "owner": "nix-systems",
48 "repo": "default",
49 "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
50 "type": "github"
51 },
52 "original": {
53 "owner": "nix-systems",
54 "repo": "default",
55 "type": "github"
56 }
57 }
58 },
59 "root": "root",
60 "version": 7
61}
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 @@
1{
2 inputs = {
3 nixpkgs.url = "github:NixOS/nixpkgs/nixos-25.11";
4 flake-utils.url = "github:numtide/flake-utils";
5 };
6
7 outputs = { self, nixpkgs, flake-utils, ... }:
8 flake-utils.lib.eachDefaultSystem (system:
9 let
10 pkgs = import nixpkgs { inherit system; };
11
12 # From 22-04-2026
13 stdpp = with pkgs; coqPackages.lib.overrideCoqDerivation {
14 version = "dev";
15 release."dev".sha256 = "hN+sEZcIaFoFF2+4dStTc0TRz5A03US6csEk5q0r/z8=";
16 release."dev".rev = "d3c67aa46ed22b1e593457cd34fc711f1a53b8be";
17 } coqPackages.stdpp;
18 in
19 {
20 devShells.default = with pkgs; mkShell {
21 buildInputs = [ coq stdpp ];
22 };
23
24 formatter = pkgs.nixpkgs-fmt;
25 });
26}
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 @@
1From stdpp Require Import numbers option sorting ssreflect.
2From stdpp Require Import options.
3From routemon Require Import util.
4
5Definition timestamp := Z.
6Variant limit :=
7 | NegInftyLimit
8 | TsLimit (x : timestamp)
9 | PosInftyLimit.
10Instance limit_eq_dec : EqDecision limit.
11Proof. solve_decision. Qed.
12
13Notation "-∞" := NegInftyLimit.
14Notation "+∞" := PosInftyLimit.
15Coercion TsLimit : timestamp >-> limit.
16
17(* The interval [start, end). Considered empty when start >= end. *)
18Record period :=
19 Period
20 { period_start : limit
21 ; period_end : limit
22 }.
23Notation "'[' s ',' e ')'" := (Period s e).
24
25(* Consider making an inductive variant of these? *)
26Definition limit_le (l1 l2 : limit) :=
27 match l1, l2 with
28 | -∞, _ | _, +∞ => True
29 | TsLimit t1, TsLimit t2 => (t1 ≤ t2)%Z
30 | _, _ => False
31 end.
32Arguments limit_le !_ !_ / : assert.
33Definition limit_lt l1 l2 :=
34 match l1 with
35 | -∞ =>
36 match l2 with
37 | -∞ => False
38 | _ => True
39 end
40 | TsLimit t1 =>
41 match l2 with
42 | -∞ => False
43 | TsLimit t2 => (t1 < t2)%Z
44 | +∞ => True
45 end
46 | +∞ => False
47 end.
48Arguments limit_lt !_ !_ / : assert.
49Instance limit_le_dec : RelDecision limit_le.
50Proof. intros [] []; simpl; solve_decision. Qed.
51Instance limit_lt_dec : RelDecision limit_lt.
52Proof. intros [] []; simpl; solve_decision. Qed.
53Instance limit_lt_pi l1 l2 : ProofIrrel (limit_lt l1 l2).
54Proof. destruct l1, l2; apply _. Qed.
55
56Instance relation_equiv {A} : Equiv (relation A) :=
57 λ R1 R2, ∀ x y, R1 x y ↔ R2 x y.
58
59Lemma strict_limit_le_limit_lt :
60 strict limit_le ≡ limit_lt.
61Proof.
62 split.
63 - intros []. destruct x, y; simpl in *; try done. lia.
64 - intros H. destruct x, y; unfold strict; simpl in *; try done; auto with lia.
65Qed.
66
67Instance : Reflexive limit_le.
68Proof. intros l. by destruct l; simpl. Qed.
69Instance : Transitive limit_le.
70Proof. intros [] [] []; simpl; try done. lia. Qed.
71Instance : PreOrder limit_le.
72Proof. constructor; apply _. Qed.
73Instance : AntiSymm (=) limit_le.
74Proof.
75 intros [] []; simpl; try done.
76 intros H1 H2. f_equal. by apply Z.le_antisymm.
77Qed.
78Instance : PartialOrder limit_le.
79Proof. constructor; apply _. Qed.
80Instance : Trichotomy (strict limit_le).
81Proof with auto with lia.
82 intros [] []; unfold strict; simpl...
83 destruct (Z.lt_trichotomy x x0) as [H|[->|H]]...
84Qed.
85Instance : TotalOrder limit_le.
86Proof. constructor; apply _. Qed.
87
88Instance : StrictOrder (strict limit_le) := _.
89(* TODO: apparently useless??
90Instance rel_equiv_proper {A} (x y : A) : Proper ((≡) ==> (↔)) (λ R, R x y).
91Proof. easy. Qed.
92Search Proper iff eq.
93*)
94Instance complement_equiv {A} : Proper ((≡) ==> (≡)) (@complement A).
95Proof. intros R1 R2 HR12. split; unfold complement; intros Hequiv []%HR12%Hequiv. Qed.
96Instance Reflexive_equiv {A} : Proper ((≡) ==> (↔)) (@Reflexive A).
97Proof.
98 intros R1 R2 Hequiv. unfold Reflexive.
99 split; intros H x; by apply Hequiv.
100Qed.
101Instance Irreflexive_equiv {A} : Proper ((≡) ==> (↔)) (@Irreflexive A).
102Proof. unfold Irreflexive. by intros R1 R2 ->. Qed.
103Instance Transitive_equiv {A} : Proper ((≡) ==> (↔)) (@Transitive A).
104Proof.
105 intros R1 R2 Hequiv. unfold Transitive.
106 by split; intros H x y z Hxy%Hequiv Hyz%Hequiv; eapply Hequiv, H.
107Qed.
108Instance StrictOrder_equiv {A} : Proper ((≡) ==> (↔)) (@StrictOrder A).
109Proof.
110 intros R1 R2 Hequiv. split; intros [Hirr Htrans].
111 - by rewrite ->Hequiv in Hirr, Htrans.
112 - by rewrite <-Hequiv in Hirr, Htrans.
113Qed.
114Instance Trichotomy_equiv {A} : Proper ((≡) ==> (↔)) (@Trichotomy A).
115Proof.
116 intros R1 R2 Hequiv. split; intros.
117 - intros x y. by rewrite -(Hequiv x y) -(Hequiv y x).
118 - intros x y. by rewrite (Hequiv x y) (Hequiv y x).
119Qed.
120
121Instance : StrictOrder limit_lt.
122Proof. rewrite -strict_limit_le_limit_lt. apply _. Qed.
123Instance : Trichotomy limit_lt.
124Proof. rewrite -strict_limit_le_limit_lt. apply _. Qed.
125
126Definition limit_lt_ts' (l : limit) (t2 : timestamp) :=
127 match l with
128 | -∞ => True
129 | TsLimit t1 => (t1 < t2)%Z
130 | +∞ => False
131 end.
132Definition ts_le_limit' (t1 : timestamp) (l : limit) :=
133 match l with
134 | -∞ => False
135 | TsLimit t2 => (t1 ≤ t2)%Z
136 | +∞ => True
137 end.
138Lemma limit_lt_limit_lt_ts' l t2 : limit_lt_ts' l t2 ↔ limit_lt l t2.
139Proof. by destruct l. Qed.
140Lemma ts_le_limit'_limit_le t1 l : ts_le_limit' t1 l ↔ limit_le t1 l.
141Proof. by destruct l. Qed.
142
143Declare Scope limit_scope.
144Delimit Scope limit_scope with lim.
145Notation "l1 < l2" := (limit_lt l1 l2) : limit_scope.
146Notation "l1 ≤ l2" := (limit_le l1 l2) : limit_scope.
147Notation "l1 < l2 < l3" := (l1 < l2 ∧ l2 < l3)%lim : limit_scope.
148Notation "l1 ≤ l2 < l3" := (l1 ≤ l2 ∧ l2 < l3)%lim : limit_scope.
149Notation "l1 < l2 ≤ l3" := (l1 < l2 ∧ l2 ≤ l3)%lim : limit_scope.
150Notation "l1 ≤ l2 ≤ l3" := (l1 ≤ l2 ∧ l2 ≤ l3)%lim : limit_scope.
151Open Scope limit_scope.
152
153Instance period_elem_of : ElemOf timestamp period :=
154 λ t '[s, e), (s ≤ t < e).
155Instance period_elem_of_dec t (p : period) : Decision (t ∈ p).
156Proof. destruct p as [s e]. apply _. Qed.
157
158Lemma limit_le_lt l1 l2 : l1 < l2 ↔ l1 ≤ l2 ∧ l1 ≠ l2.
159Proof. by rewrite -(strict_limit_le_limit_lt l1 l2) strict_spec_alt. Qed.
160
161Lemma limit_le_cases {l1 l2} : l1 ≤ l2 ↔ l1 = l2 ∨ l1 < l2.
162Proof.
163 rewrite -(strict_limit_le_limit_lt l1 l2) strict_spec_alt. split.
164 - intros Hl12. destruct (decide (l1 = l2)) as [<-|Hne]; tauto.
165 - by intros [<-|[Hl12 _]].
166Qed.
167
168Lemma limit_lt_le_lt {l1} l2 {l3} : l1 ≤ l2 < l3 → l1 < l3.
169Proof. by intros [[<-|?]%limit_le_cases ?]; last etrans. Qed.
170
171Definition period_empty '[s, e) := e ≤ s.
172Definition period_empty_alt (p : period) := ∀ t, t ∉ p.
173Lemma period_empty_alt_iff p : period_empty p ↔ period_empty_alt p.
174Proof.
175 destruct p as [s e].
176 rewrite /period_empty /period_empty_alt /=.
177 split; intros H.
178 - intros t [contra []]%limit_lt_le_lt%limit_le_lt.
179 by eapply (anti_symm limit_le).
180 - destruct s as [|s|], e as [|e|]; try done.
181 + exfalso. apply (H (Z.pred e)). rewrite /elem_of /period_elem_of /=. lia.
182 + exfalso. by apply (H 0%Z).
183 + rewrite /elem_of /period_elem_of /= in H.
184 specialize (H s). simpl. lia.
185 + exfalso. apply (H s). rewrite /elem_of /period_elem_of /=. lia.
186Qed.
187Instance period_empty_dec p : Decision (period_empty p).
188Proof. destruct p as [s e]. solve_decision. Qed.
189
190Definition period_nonempty '[s, e) := s < e.
191Instance period_nonempty_dec p : Decision (period_nonempty p).
192Proof. destruct p. apply _. Qed.
193Instance period_nonempty_pi p : ProofIrrel (period_nonempty p).
194Proof. destruct p. apply _. Qed.
195
196Instance period_equiv : Equiv period :=
197 λ p1 p2, ∀ t, t ∈ p1 ↔ t ∈ p2.
198Instance period_equiv_reflexive : Reflexive period_equiv.
199Proof. done. Qed.
200Instance period_equiv_trans : Transitive period_equiv.
201Proof. intros p1 p2 p3 H1 H2 t. by rewrite H1. Qed.
202Instance period_equiv_symm : Symmetric period_equiv.
203Proof. by intros p1 p2 H t. Qed.
204Instance period_equiv_equiv : Equivalence period_equiv.
205Proof. constructor; apply _. Qed.
206
207(* All empty periods are equivalent *)
208Lemma period_empty_equiv p1 p2 : period_empty p1 → period_empty p2 ↔ p1 ≡ p2.
209Proof.
210 intros Hp1%period_empty_alt_iff. split.
211 - intros Hp2%period_empty_alt_iff. intros t.
212 split; [intros []%(Hp1 _) | intros []%(Hp2 _)].
213 - intros Hequiv. apply period_empty_alt_iff.
214 intros t []%Hequiv%(Hp1 _).
215Qed.
216
217Instance empty_period : Empty period := [TsLimit 0%Z, TsLimit 0%Z).
218Definition empty_period_empty : period_empty empty_period.
219Proof. done. Qed.
220
221Definition limit_min (l1 l2 : limit) := if decide (l1 ≤ l2) then l1 else l2.
222Definition limit_max (l1 l2 : limit) := if decide (l1 ≤ l2) then l2 else l1.
223
224Notation "l1 '`min`' l2" := (limit_min l1 l2) : limit_scope.
225Notation "l1 '`max`' l2" := (limit_max l1 l2) : limit_scope.
226
227Definition limit_min_ts (t1 t2 : timestamp) :
228 t1 `min` t2 = TsLimit (t1 `min` t2)%Z.
229Proof.
230 unfold limit_min.
231 destruct (decide (t1 ≤ t2));
232 simpl in *; f_equal; lia.
233Qed.
234
235Definition limit_max_ts (t1 t2 : timestamp) :
236 t1 `max` t2 = TsLimit (t1 `max` t2)%Z.
237Proof.
238 unfold limit_max.
239 destruct (decide (t1 ≤ t2));
240 simpl in *; f_equal; lia.
241Qed.
242
243Instance period_intersection : Intersection period := λ '[s1, e1) '[s2, e2),
244 [ s1 `max` s2, e1 `min` e2 ).
245
246Lemma intersect_and (p1 p2 : period) t :
247 t ∈ (p1 ∩ p2) ↔ t ∈ p1 ∧ t ∈ p2.
248Proof.
249 (* It really should be possible to optimize this proof somehow. *)
250 destruct p1 as [[|s1|] [|e1|]], p2 as [[|s2|] [|e2|]];
251 rewrite /intersection /period_intersection /elem_of /period_elem_of /limit_min /limit_max /limit_le /limit_lt /=;
252 repeat case_decide; tauto || lia.
253Qed.
254
255(* The points in time given by p1 except those given by p2, given as a before/after pair. *)
256Definition except '[s1, e1) '[s2, e2) : period * period :=
257 ( [ s1, e1 `min` s2 ),
258 [ s1 `max` e2, e1 ) ).
259
260Lemma limit_lt_ne l1 l2 : l1 < l2 → l1 ≠ l2.
261Proof. rewrite -(strict_limit_le_limit_lt l1 l2) strict_spec_alt. easy. Qed.
262
263Lemma not_limit_le l1 l2 : ¬ (l1 ≤ l2) ↔ l2 < l1.
264Proof.
265 destruct (trichotomy limit_lt l1 l2) as [Hl12|[<-|Hl21]].
266 - split; intros H.
267 + exfalso. apply H, limit_le_cases. by right.
268 + exfalso. by eapply asymmetry.
269 - split; intros H.
270 + exfalso. apply H, limit_le_cases. by left.
271 + by apply (_ : Irreflexive limit_lt) in H.
272 - split; intros H; first done.
273 intros [<-|Hl12]%limit_le_cases.
274 + by apply (_ : Irreflexive limit_lt) in H.
275 + by eapply asymmetry.
276Qed.
277
278Lemma not_limit_le' : complement limit_le ≡ flip limit_lt.
279Proof. apply: not_limit_le. Qed.
280
281Instance relation_equiv_reflexive {A} : Reflexive (@relation_equiv A).
282Proof. done. Qed.
283Instance relation_equiv_trans {A} : Transitive (@relation_equiv A).
284Proof. intros R1 R2 R3 H12 H23 x y. by rewrite H12 -H23. Qed.
285Instance relation_equiv_symm {A} : Symmetric (@relation_equiv A).
286Proof. by intros R1 R2 H12 x y. Qed.
287Instance relation_equiv_equiv {A} : Equivalence (@relation_equiv A).
288Proof. constructor; apply _. Qed.
289
290Lemma relation_flip_equiv {A} : Proper ((≡@{relation A}) ==> (≡)) flip.
291Proof. intros R1 R2 H12 x y. simpl. by rewrite (H12 y x). Qed.
292
293(* Could also be more generic *)
294Lemma relation_flip_involutive {A} (R : relation A) : flip (flip R) ≡ R.
295Proof. done. Qed.
296
297Lemma complement_involutive {A} `{!RelDecision (R : relation A)} : complement (complement R) ≡ R.
298Proof.
299 intros x y. split; intros Hxy.
300 - by destruct (decide (R x y)).
301 - by apply.
302Qed.
303
304Lemma not_limit_lt' : complement limit_lt ≡ flip limit_le.
305Proof.
306 rewrite -(relation_flip_involutive limit_lt) complement_inverse.
307 trans (flip (complement (complement limit_le))).
308 { apply relation_flip_equiv, complement_equiv, symmetry, not_limit_le'. }
309 apply relation_flip_equiv, complement_involutive.
310Qed.
311
312Lemma not_limit_lt l1 l2 : ¬ (l1 < l2) ↔ l2 ≤ l1.
313Proof. apply not_limit_lt'. Qed.
314
315(* TODO: make conclusion positive? *)
316Lemma period_nonempty_equiv_L_1 (s1 e1 s2 e2 : limit) :
317 period_nonempty [s1, e1) →
318 period_nonempty [s2, e2) →
319 [s1, e1) ≡ [s2, e2) →
320 ¬ s1 < s2.
321Proof.
322 unfold period_nonempty.
323 intros Hne1 Hne2 Hequiv Hs12.
324 destruct s2 as [|s2|]; [by destruct s1|..|by destruct s1].
325 destruct s1 as [|s1|]; last done.
326 * assert (Hs2a : s2 ∈ [s2, e2)).
327 { unfold elem_of, period_elem_of. by destruct e2. }
328 pose proof (proj2 (Hequiv s2) Hs2a) as [_ Hs2b].
329 assert (Hs2c : Z.pred s2 ∈ [-∞, e1)).
330 { unfold elem_of, period_elem_of.
331 by destruct e1 as [|e1|]; [|simpl in *; lia|]. }
332 pose proof (proj1 (Hequiv (Z.pred s2)) Hs2c) as [contra _].
333 simpl in contra. lia.
334 * assert (Hs1 : s1 ∈ [s1, e1)).
335 { unfold elem_of, period_elem_of. by destruct e1. }
336 pose proof (proj1 (Hequiv s1) Hs1) as [[Heq|Heq]%limit_le_cases _].
337 { rewrite Heq in Hs12. by eapply (_ : Irreflexive limit_lt). }
338 by eapply asymmetry.
339Qed.
340
341(* TODO: make conclusion positive? *)
342Lemma period_nonempty_equiv_L_2 (s1 e1 s2 e2 : limit) :
343 period_nonempty [s1, e1) →
344 period_nonempty [s2, e2) →
345 [s1, e1) ≡ [s2, e2) →
346 ¬ e1 < e2.
347Proof.
348 intros Hne1 Hne2 Hequiv He12.
349 destruct e1 as [|e1|]; [by destruct s1|..|done].
350 destruct e2 as [|e2|]; first done.
351 * (* e2 - 1 ∈ [s2, e2) → e2 - 1 ∈ [s1, e1) → s1 ≤ e2 - 1 < e1 → e2 ≤ e1 → e2 = e1 ∨ e2 < e1 *)
352 assert (He2a : Z.pred e2 ∈ [s2, e2)).
353 { unfold elem_of, period_elem_of.
354 by destruct s2 as [|s2|]; [simpl in *; lia..|]. }
355 pose proof (proj2 (Hequiv (Z.pred e2)) He2a) as [_ He2b].
356 simpl in *. lia.
357 * (* We want to plug e1 into the right side to get a
358 contradiction, so we need s2 ≤ e1. It suffices to show that
359 s2 ≤ e1 - 1 *)
360 assert (He1a : Z.pred e1 ∈ [s1, e1)).
361 { unfold elem_of, period_elem_of.
362 by destruct s1 as [|s1|]; [simpl in *; lia..|]. }
363 pose proof (proj1 (Hequiv (Z.pred e1)) He1a) as [He1b _].
364 assert (He1c : e1 ∈ [s2, +∞)).
365 { unfold elem_of, period_elem_of.
366 by destruct s2 as [|s2|]; [|simpl in *; lia|]. }
367 pose proof (proj2 (Hequiv e1) He1c) as [_ []%(_ : Irreflexive limit_lt)].
368Qed.
369
370Lemma period_nonempty_equiv_L p1 p2 :
371 period_nonempty p1 →
372 period_nonempty p2 →
373 p1 ≡ p2 → p1 = p2.
374Proof.
375 destruct p1 as [s1 e1], p2 as [s2 e2].
376 unfold equiv, period_equiv.
377 intros Hne1 Hne2 Hequiv.
378 f_equal.
379 - destruct (decide (s1 < s2)) as [Hs12|[<-|Hs21]%not_limit_lt%limit_le_cases]; [|done|].
380 + exfalso. by apply (period_nonempty_equiv_L_1 s1 e1 s2 e2).
381 + exfalso. by apply (period_nonempty_equiv_L_1 s2 e2 s1 e1).
382 - destruct (decide (e1 < e2)) as [He12|[<-|He21]%not_limit_lt%limit_le_cases]; [|done|].
383 + exfalso. by apply (period_nonempty_equiv_L_2 s1 e1 s2 e2).
384 + exfalso. by apply (period_nonempty_equiv_L_2 s2 e2 s1 e1).
385Qed.
386
387Definition period_empty_not_nonempty p : ¬ period_empty p ↔ period_nonempty p.
388Proof. destruct p. apply not_limit_le. Qed.
389
390Lemma limit_lt_min l1 l2 l3 :
391 l1 < l2 ∧ l1 < l3 ↔ l1 < l2 `min` l3.
392Proof.
393 split.
394 - intros [Hl12 Hl13]. unfold limit_min. by case_decide.
395 - unfold limit_min. intros H. case_decide.
396 + split; first done.
397 apply limit_le_cases in H0 as [<-|H0]; first done.
398 by etrans.
399 + apply not_limit_le in H0.
400 by split; first etrans.
401Qed.
402
403Lemma limit_max_le l1 l2 l3 :
404 l1 ≤ l3 ∧ l2 ≤ l3 ↔ l1 `max` l2 ≤ l3.
405Proof.
406 split.
407 - intros [Hl12 Hl23]. unfold limit_max. by case_decide.
408 - unfold limit_max. intros H. case_decide.
409 + by split; first etrans.
410 + apply not_limit_le in H0. split; first done.
411 apply limit_le_lt in H0 as [H0 _]. by etrans.
412Qed.
413Lemma limit_le_max l1 l2 l3 :
414 l1 ≤ l2 `max` l3 ↔ l1 ≤ l2 ∨ l1 ≤ l3.
415Proof.
416 unfold limit_max.
417 destruct (decide (l2 ≤ l3)) as [Hl23|Hl23%not_limit_le].
418 - split; first tauto. intros [H|H]; last done. by etrans.
419 - split; first tauto. intros [H|H]; first done.
420 by trans l3; last (apply limit_le_cases; right).
421Qed.
422
423Lemma except_lem p1 p2 t :
424 t ∈ p1 ∧ t ∉ p2 ↔
425 t ∈ (except p1 p2).1 ∨ t ∈ (except p1 p2).2.
426Proof.
427 destruct p1 as [s1 e1], p2 as [s2 e2]. split.
428 - intros [Hp1 Hp2].
429 (* on the left if t < s2, on the right if e2 ≤ t *)
430 destruct (decide (t < s2)) as [Hts2|Hts2].
431 + (* t < s2 *)
432 left. simpl. split.
433 * apply Hp1.
434 * apply limit_lt_min. split; last done.
435 rewrite /elem_of /period_elem_of in Hp1. easy.
436 + (* ¬ (t < s2) (↔ s2 ≤ t) *)
437 apply not_limit_lt in Hts2.
438 right. simpl. split.
439 * apply limit_max_le. split.
440 -- apply Hp1.
441 -- apply not_limit_lt. intros contra. by apply Hp2.
442 * apply Hp1.
443 - intros [H|H]; simpl in *.
444 + split.
445 * unfold elem_of, period_elem_of in *. split.
446 -- apply H.
447 -- by destruct H as [_ [H _]%limit_lt_min].
448 * unfold elem_of, period_elem_of in *.
449 destruct H as [H1 [H2 H3]%limit_lt_min].
450 intros [Hc1 Hc2].
451 apply limit_le_cases in Hc1 as [Hc1|Hc1].
452 -- inv Hc1. by apply (_ : Irreflexive limit_lt) in H3.
453 -- eapply asymmetry; [apply H3 | apply Hc1].
454 + unfold elem_of, period_elem_of in H.
455 rewrite -limit_max_le in H. destruct H as [[H1 H2] H3].
456 split; first done.
457 intros [Hc1 Hc2].
458 apply limit_le_cases in H2 as [H2|H2].
459 -- inv H2. by apply (_ : Irreflexive limit_lt) in Hc2.
460 -- eapply asymmetry; [apply H2 | apply Hc2].
461Qed.
462
463Lemma limit_max_lt l1 l2 l3 :
464 l1 `max` l2 < l3 ↔ l1 < l3 ∧ l2 < l3.
465Proof.
466 unfold limit_max.
467 destruct (decide (l1 ≤ l2)) as [Hl12|Hl12%not_limit_le].
468 - split; last easy. intros H. by split; first eapply limit_lt_le_lt.
469 - split; last easy. intros H. by split; last etrans.
470Qed.
471
472Lemma limit_min_lt l1 l2 l3 :
473 l1 `min` l2 < l3 ↔ l1 < l3 ∨ l2 < l3.
474Proof.
475 unfold limit_min.
476 destruct (decide (l1 ≤ l2)%lim) as [Hl12|Hl12%not_limit_le].
477 - split; first tauto. by intros [H|H]; last eapply limit_lt_le_lt.
478 - split; first tauto. by intros [H|H]; first etrans.
479Qed.
480
481Lemma limit_lt_max l1 l2 l3 :
482 l1 < l2 `max` l3 ↔ l1 < l2 ∨ l1 < l3.
483Proof.
484 unfold limit_max.
485 destruct (decide (l2 ≤ l3)) as [Hl23|Hl23%not_limit_le].
486 - split; first tauto. intros [H|H]; last done.
487 by apply limit_le_cases in Hl23 as [<-|Hl23]; last etrans.
488 - split; first tauto. by intros [H|H]; last etrans.
489Qed.
490
491Instance limit_min_comm : Comm (=) limit_min.
492Proof.
493 unfold limit_min.
494 intros [] []; repeat case_decide;
495 try done; simpl in *; f_equal; lia.
496Qed.
497Instance limit_max_comm : Comm (=) limit_max.
498Proof.
499 unfold limit_max.
500 intros [] []; repeat case_decide;
501 try done; simpl in *; f_equal; lia.
502Qed.
503
504Lemma limit_max_eq_l l1 l2 : l1 `max` l2 = l1 ↔ l2 ≤ l1.
505Proof.
506 unfold limit_max. case_decide; split.
507 - by intros ->.
508 - intros H12. by eapply (_ : AntiSymm (=) limit_le).
509 - intros _. apply limit_le_cases. right.
510 by apply not_limit_le.
511 - by intros _.
512Qed.
513Lemma limit_max_eq_r l1 l2 : l1 `max` l2 = l2 ↔ l1 ≤ l2.
514Proof. rewrite [l1 `max` l2]comm. apply limit_max_eq_l. Qed.
515
516Lemma limit_max_l l1 l2 : l2 ≤ l1 → l1 `max` l2 = l1.
517Proof. apply limit_max_eq_l. Qed.
518Lemma limit_max_r l1 l2 : l1 ≤ l2 → l1 `max` l2 = l2.
519Proof. apply limit_max_eq_r. Qed.
520
521Definition ne_period := { p : period | period_nonempty p }.
522
523Instance ne_period_elem_of : ElemOf timestamp ne_period :=
524 λ t p, t ∈ `p.
525Instance ne_period_elem_of_dec t (p : ne_period) : Decision (t ∈ p).
526Proof. apply _. Qed.
527
528(* TODO: rename to ne_period_before *)
529Definition period_before '([s1, e1) ↾ _ : ne_period) '([s2, e2) ↾ _ : ne_period) :=
530 e1 < s2.
531
532Instance period_before_pi p1 p2 : ProofIrrel (period_before p1 p2).
533Proof. destruct p1 as [[s1 e1] Hne1], p2 as [[s2 e2] Hne2]. apply _. Qed.
534
535Instance period_before_trans : Transitive period_before.
536Proof.
537 intros [[s1 e1] Hne1] [[s2 e2] Hne2] [[s3 e3] Hne3] H1 H2.
538 unfold period_before in *. simpl in *.
539 by trans s2; last trans e2.
540Qed.
541
542Instance period_before_irrefl : Irreflexive period_before.
543Proof.
544 intros [[s e] Hne] Hp. simpl in *.
545 eapply (_ : Irreflexive limit_lt). by etrans.
546Qed.
547
548Instance period_before_strict_order : StrictOrder period_before.
549Proof. split; apply _. Qed.
550
551Definition ne_period_rel (R : relation ne_period) : relation period :=
552 λ p1 p2, ∃ H1 H2, R (p1 ↾ H1) (p2 ↾ H2).
553
554Instance ne_period_rel_trans `{!Transitive R} : Transitive (ne_period_rel R).
555Proof.
556 intros p1 p2 p3 (H1 & H2 & HR12) (H2' & H3 & HR23).
557 exists H1, H3. replace H2' with H2 in HR23; last apply proof_irrel.
558 by etrans.
559Qed.
560
561Instance ne_period_rel_irrefl `{!Irreflexive R} : Irreflexive (ne_period_rel R).
562Proof.
563 intros p. intros (H1 & H2 & HR).
564 replace H2 with H1 in HR; last apply proof_irrel.
565 by apply (_ : Irreflexive R) in HR.
566Qed.
567
568Instance ne_period_rel_pi (R : relation ne_period) `{!∀ x y, ProofIrrel (R x y)} x y :
569 ProofIrrel (ne_period_rel R x y).
570Proof. apply _. Qed.
571
572Lemma except_parts_order p1 p2 :
573 period_nonempty p2 →
574 period_nonempty (except p1 p2).1 →
575 period_nonempty (except p1 p2).2 →
576 ne_period_rel period_before (except p1 p2).1 (except p1 p2).2.
577Proof.
578 destruct p1 as [s1 e1], p2 as [s2 e2]. simpl. intros H0 Hne1 Hne2.
579 unfold period_before. split; [done|split; [done|]].
580 apply limit_min_lt. right. apply limit_lt_max. right. apply H0.
581Qed.
582
583Definition period_nonempty_alt (p : period) := ∃ t, t ∈ p.
584
585Lemma period_nonempty_alt_iff p :
586 period_nonempty p ↔ period_nonempty_alt p.
587Proof.
588 unfold period_nonempty, period_nonempty_alt.
589 destruct p as [s e]. split.
590 - intros Hlt. destruct s as [|s|]; last done.
591 + destruct e as [|e|]; first done.
592 * exists (Z.pred e). by split; last (simpl; lia).
593 * exists 0%Z. done.
594 + exists s. done.
595 - intros [t Ht]. by eapply limit_lt_le_lt.
596Qed.
597
598Instance period_eq_dec : EqDecision period.
599Proof. solve_decision. Qed.
600
601Instance period_disjoint : Disjoint period :=
602 λ p1 p2, period_empty (p1 ∩ p2).
603
604Instance period_intersection_comm : Comm (=) period_intersection.
605Proof.
606 intros [s1 e1] [s2 e2].
607 by rewrite /= [s2 `max` s1]comm [e2 `min` e1]comm.
608Qed.
609Instance period_disjoint_symm : Symmetric period_disjoint.
610Proof. intros p1 p2. unfold period_disjoint. by rewrite comm. Qed.
611
612Lemma limit_min_eq_l l1 l2 : l1 `min` l2 = l1 ↔ l1 ≤ l2.
613Proof.
614 unfold limit_min. case_decide; first done. split.
615 - intros ->. exfalso. by apply H.
616 - intros []%H.
617Qed.
618Lemma limit_min_eq_r l1 l2 : l1 `min` l2 = l2 ↔ l2 ≤ l1.
619Proof. rewrite [l1 `min` l2]comm. apply limit_min_eq_l. Qed.
620
621Lemma limit_min_l l1 l2 : l1 ≤ l2 → l1 `min` l2 = l1.
622Proof. apply limit_min_eq_l. Qed.
623Lemma limit_min_r l1 l2 : l2 ≤ l1 → l1 `min` l2 = l2.
624Proof. apply limit_min_eq_r. Qed.
625
626Lemma limit_lt_le_trans {l1} l2 {l3} : l1 < l2 → l2 ≤ l3 → l1 < l3.
627Proof. by intros Hlt12 [->|Hlt23]%limit_le_cases; last etrans. Qed.
628
629Instance period_union : Union period :=
630 λ '[s1, e1) '[s2, e2), [s1 `min` s2, e1 `max` e2).
631
632Lemma limit_min_le l1 l2 l3 :
633 l1 ≤ l3 ∨ l2 ≤ l3 ↔
634 l1 `min` l2 ≤ l3.
635Proof.
636 unfold limit_min. case_decide; split.
637 - by intros [H13|H23]; last trans l2.
638 - intros H13. by left.
639 - apply not_limit_le in H. intros [H13|H23]; last done.
640 trans l1; last done.
641 apply limit_le_cases. by right.
642 - intros H23. by right.
643Qed.
644
645Lemma limit_le_min l1 l2 l3 :
646 l1 ≤ l2 ∧ l1 ≤ l3 ↔
647 l1 ≤ l2 `min` l3.
648Proof.
649 unfold limit_min. case_decide; split.
650 - by intros [H12 _].
651 - intros ?. by split; last trans l2.
652 - by intros [_ H13].
653 - intros ?. split; last done.
654 apply not_limit_le in H.
655 trans l3; first done.
656 apply limit_le_cases. by right.
657Qed.
658
659Lemma period_union_lem_1 t (p1 p2 : period) :
660 t ∈ p1 ∨ t ∈ p2 → t ∈ p1 ∪ p2.
661Proof.
662 destruct p1 as [s1 e1], p2 as [s2 e2].
663 unfold union, period_union.
664 intros [Ht|Ht]; split.
665 - apply limit_min_le. left. apply Ht.
666 - apply limit_lt_max. left. apply Ht.
667 - apply limit_min_le. right. apply Ht.
668 - apply limit_lt_max. right. apply Ht.
669Qed.
670
671Definition unifiable '[s1, e1) '[s2, e2) :=
672 s2 ≤ e1 ∧ s1 ≤ e2.
673
674Instance unifiable_dec : RelDecision unifiable.
675Proof. intros [] []. solve_decision. Qed.
676
677Lemma not_limit_le_lt l1 l2 l3 :
678 ¬ l1 ≤ l2 < l3 ↔ l2 < l1 ∨ l3 ≤ l2.
679Proof.
680 split.
681 - intros H123.
682 destruct (decide (l2 < l1)) as [?|H21%not_limit_lt]; first by left.
683 destruct (decide (l3 ≤ l2)) as [?|H32%not_limit_le]; first by right.
684 exfalso. by apply H123.
685 - intros [H21|H32] contra.
686 + eapply not_limit_le; [apply H21|apply contra].
687 + eapply not_limit_lt; [apply H32|apply contra].
688Qed.
689
690Lemma limit_lt_le l1 l2 : l1 < l2 → l1 ≤ l2.
691Proof. intros Hlt. apply limit_le_cases. by right. Qed.
692
693Lemma period_union_lem_2 t (p1 p2 : period) :
694 unifiable p1 p2 →
695 t ∈ p1 ∪ p2 → t ∈ p1 ∨ t ∈ p2.
696Proof.
697 intros Hunif Hunion.
698 destruct (decide (t ∈ p1)) as [?|Ht1]; first by left.
699 destruct (decide (t ∈ p2)) as [?|Ht2]; first by right.
700 exfalso.
701
702 destruct p1 as [s1 e1], p2 as [s2 e2].
703 unfold elem_of, period_elem_of in *.
704 simpl in *. destruct Hunif as [Hunif1 Hunif2].
705
706 (* If t is not in p1, then it must be in p2 *)
707 apply Ht2. clear Ht2.
708 apply not_limit_le_lt in Ht1.
709 destruct Ht1 as [Ht1|Ht1].
710 - (* t is not in p1 because it is before p1 (where p2 must hence be) *)
711 destruct Hunion as [Hunion1 Hunion2].
712 apply limit_min_le in Hunion1 as [[->|contra]%limit_le_cases | Hunion1].
713 { exfalso. by eapply (_ : Irreflexive limit_lt). }
714 { exfalso. by eapply (asymmetry (R:=limit_lt)). }
715 split; first done. by eapply limit_lt_le_trans.
716 - destruct Hunion as [Hunion1 Hunion2].
717 apply limit_lt_max in Hunion2 as [Hunion2 | Hunion2].
718 + apply limit_le_cases in Ht1 as [->|contra].
719 { exfalso. by eapply (_ : Irreflexive limit_lt). }
720 { exfalso. by eapply (asymmetry (R:=limit_lt)). }
721 + split; last done. by trans e1.
722Qed.
723
724Instance period_union_comm : Comm (=) period_union.
725Proof.
726 unfold period_union. intros [s1 e1] [s2 e2].
727 by rewrite limit_min_comm limit_max_comm.
728Qed.
729
730Instance period_singleton : Singleton timestamp period :=
731 λ t, [t, TsLimit (Z.succ t)).
732Lemma period_singleton_lem_1 t : t ∈ ({[t]} : period).
733Proof. by split; simpl; last lia. Qed.
734Lemma period_singleton_lem_2 t t' : t' ∈ ({[t]} : period) → t' = t.
735Proof.
736 unfold singleton, period_singleton.
737 intros [H11 H12]. destruct t, t'; try done; simpl in *; lia.
738Qed.
739Lemma period_singleton_nonempty t : period_nonempty {[t]}.
740Proof.
741 apply period_nonempty_alt_iff.
742 exists t. apply period_singleton_lem_1.
743Qed.
744
745Lemma unifiable_period_union p1 p2 p3 :
746 unifiable p1 p2 → unifiable p2 p3 →
747 unifiable (p1 ∪ p2) p3.
748Proof.
749 destruct p1 as [s1 e1], p2 as [s2 e2], p3 as [s3 e3].
750 intros [Hunif11 Hunif12] [Hunif21 Hunif22]. simpl. split.
751 + apply limit_le_max. by right.
752 + apply limit_min_le. by right.
753Qed.
754
755Instance unifiable_symm : Symmetric unifiable.
756Proof. by intros [] [] []. Qed.
757
758Definition Σlift {A} {Φ : A → Prop} (R : relation A) : relation {x : A | Φ x} :=
759 λ '(x↾_) '(y↾_), R x y.
760
761Instance Σlift_symm {A Φ} `{!Symmetric R} : Symmetric (@Σlift A Φ R).
762Proof. intros [x Hx] [y Hy] HR. simpl in *. by apply symmetry. Qed.
763
764(* TODO: probably unused? *)
765Instance Σlift_dec {A Φ} `{!RelDecision R} : RelDecision (@Σlift A Φ R).
766Proof. intros [x Hx] [y Hy]. by simpl. Qed.
767
768Definition ne_period_unifiable : relation ne_period := Σlift unifiable.
769
770Lemma period_unifiable_not_before p1 p2 : ne_period_unifiable p1 p2 → ¬ period_before p1 p2.
771Proof.
772 destruct p1 as [[s1 e1] Hne1], p2 as [[s2 e2] Hne2]. simpl in *.
773 intros [Hunif1 Hunif2] Hbefore.
774 apply limit_le_cases in Hunif1 as [->|contra].
775 - by eapply (_ : Irreflexive limit_lt).
776 - by eapply (asymmetry (R:=limit_lt)).
777Qed.
778
779(* TODO: define total relation on Σperiod_nonempty, p1 p2 := unifiable p1 p2 ∨ p1 < p2.
780 (Then have [AntiSymm unifiable (≤@{Σperiod_nonempty})].)
781 Show decidability, perform mergesort.
782 Then make the rest of normalization consist in unification of the periods.
783 *)
784
785Definition ne_period_le p1 p2 := ne_period_unifiable p1 p2 ∨ period_before p1 p2.
786
787Instance ne_period_le_antisymm : AntiSymm ne_period_unifiable ne_period_le.
788Proof.
789 intros p1 p2 [H12|H12] [H21|H21]; [done|done|..].
790 - exfalso. apply symmetry in H21.
791 by eapply period_unifiable_not_before.
792 - exfalso. by eapply asymmetry.
793Qed.
794
795Lemma ne_period_neither_before_unifiable p1 p2 :
796 ¬ period_before p1 p2 → ¬ period_before p2 p1 →
797 ne_period_unifiable p1 p2.
798Proof.
799 destruct p1 as [[s1 e1] Hne1], p2 as [[s2 e2] Hne2].
800 simpl in *. by intros ?%not_limit_lt ?%not_limit_lt.
801Qed.
802
803Instance period_before_dec : RelDecision period_before.
804Proof.
805 intros [[s1 e1] ?] [[s2 e2] ?]. simpl in *.
806 solve_decision.
807Qed.
808
809Lemma ne_period_not_unifiable p1 p2 :
810 ¬ ne_period_unifiable p1 p2 →
811 period_before p1 p2 ∨ period_before p2 p1.
812Proof.
813 intros Hnunif.
814 destruct (decide (period_before p1 p2)) as [?|H12]; first by left.
815 destruct (decide (period_before p2 p1)) as [?|H21]; first by right.
816 exfalso. by apply Hnunif, ne_period_neither_before_unifiable.
817Qed.
818
819Instance ne_period_le_total : Total ne_period_le.
820Proof.
821 intros p1 p2.
822 destruct (decide (ne_period_unifiable p1 p2)) as [Hunif|Hnunif].
823 - (* which one we pick does not matter *)
824 by do 2 left.
825 - apply ne_period_not_unifiable in Hnunif as [H12|H21].
826 + left. by right.
827 + right. by right.
828Qed.
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 @@
1From stdpp Require Import numbers option sorting ssreflect.
2From stdpp Require Import options.
3From routemon Require Import period util.
4
5(* This setup would require the proof irrelevance stuff
6
7Record period_seq :=
8 PeriodSeq
9 { periods : list period
10 ; Hnonempty : Forall period_nonempty periods
11 ; Hsorted : Sorted period_before periods
12 }.
13*)
14
15Definition period_seq := list ne_period.
16
17Definition period_seq_nf (ps : period_seq) :=
18 Sorted period_before ps.
19
20Instance period_seq_elem_of : ElemOf timestamp period_seq :=
21 λ t, Exists (λ p, t ∈ p).
22Instance period_seq_elem_of_dec t (ps : period_seq) : Decision (t ∈ ps).
23Proof.
24 induction ps as [|p ps].
25 - right. inv 1.
26 - destruct IHps.
27 + left. by apply Exists_cons_tl.
28 + destruct (decide (t ∈ p)).
29 * left. by apply Exists_cons_hd.
30 * right. by inv 1.
31Qed.
32
33Instance period_seq_equiv : Equiv period_seq :=
34 λ ps1 ps2, ∀ t, t ∈ ps1 ↔ t ∈ ps2.
35
36Definition ne_period_intersection (p1 p2 : ne_period) :=
37 let p := `p1 ∩ `p2 in
38 match decide (period_nonempty p) with
39 | left H => Some (p ↾ H)
40 | right _ => None
41 end.
42
43Definition ne_period_start (p : ne_period) :=
44 period_start (`p).
45Definition ne_period_end (p : ne_period) :=
46 period_end (`p).
47
48Definition period_seq_intersection_1 go ps1 ps2 :=
49 match ps1, ps2 with
50 | p1 :: ps1', p2 :: ps2' =>
51 let mp12 := ne_period_intersection p1 p2 in
52 let rest := if decide (ne_period_end p1 < ne_period_end p2)%lim then go ps1' ps2 else go ps1 ps2' in
53 match mp12 with
54 | Some p12 => p12 :: rest
55 | None => rest
56 end
57 | _, _ => []
58 end.
59Fixpoint period_seq_intersection_aux n :=
60 match n with
61 | 0 => const (const [])
62 | S n => period_seq_intersection_1 (period_seq_intersection_aux n)
63 end.
64Instance period_seq_intersection : Intersection period_seq :=
65 λ ps1 ps2, period_seq_intersection_aux (S (length ps1 + length ps2)) ps1 ps2.
66
67Lemma period_seq_intersection_eq ps1 ps2 :
68 period_seq_intersection ps1 ps2 =
69 match ps1, ps2 with
70 | p1 :: ps1', p2 :: ps2' =>
71 let mp12 := ne_period_intersection p1 p2 in
72 let rest := if decide (ne_period_end p1 < ne_period_end p2)%lim
73 then period_seq_intersection ps1' ps2
74 else period_seq_intersection ps1 ps2' in
75 match mp12 with
76 | Some p12 => p12 :: rest
77 | None => rest
78 end
79 | _, _ => []
80 end.
81Proof.
82 destruct ps1 as [|p1 ps1], ps2 as [|p2 ps2]; [done..|].
83 have Hlen1 : S (S (length ps1 + length ps2)) = S (length (p1 :: ps1) + length ps2) by simpl; lia.
84 have Hlen2 : S (S (length ps1 + length ps2)) = S (length ps1 + length (p2 :: ps2)) by simpl; lia.
85 by rewrite
86 /period_seq_intersection /period_seq_intersection_aux
87 !length_cons Nat.add_succ_l Nat.add_succ_r -/period_seq_intersection_aux.
88Qed.
89
90Opaque period_seq_intersection.
91
92Lemma period_seq_nf_cons p ps :
93 period_seq_nf (p :: ps) ↔
94 period_seq_nf ps ∧
95 Forall (λ q, ne_period_end p < ne_period_start q)%lim ps.
96Proof.
97 split.
98 - intros HSort%Sorted_StronglySorted; last apply _.
99 inv HSort. repeat split; try done.
100 + by apply StronglySorted_Sorted.
101 + eapply Forall_impl; first done.
102 intros [[sq eq] Hq] Hbef.
103 by destruct p as [[sp ep] Hp].
104 - intros (Hnf & Hlt).
105 constructor; first done. destruct ps as [|q ps]; constructor.
106 inv Hlt. destruct p as [[sp ep] Hp], q as [[sq eq] Hq]. by simpl in *.
107Qed.
108
109(*
110Lemma list_elem_of_cons_inv `{!EqDecision A} (x y : A) (l : list A) :
111 x ∈ y :: l ↔ x = y ∨ x ≠ y ∧ x ∈ l.
112Proof.
113 split.
114 - destruct (decide (x = y)) as [<-|H].
115 + intros _. by left.
116 + inv 1. by right.
117 - by intros [<-|[_ H]]; constructor.
118Qed.
119*)
120
121Lemma list_elem_of_cons_inv {A} (x y : A) (l : list A) :
122 x ∈ y :: l ↔ x = y ∨ x ∈ l.
123Proof.
124 split.
125 - by inv 1; [left|right].
126 - by intros [<-|H]; constructor.
127Qed.
128
129Lemma Sorted_list_elem_of_R_trans {A} `{!Transitive R} (x y z : A) (l : list A) :
130 Sorted R (y :: l) → z ∈ y :: l → R x y → R x z.
131Proof.
132 intros [HSort Hyl]%Sorted_inv.
133 revert y Hyl.
134 induction HSort as [|y' l' HSort IH Hy'l']; intros y.
135 - intros _. by inv 1; last inv H2.
136 - intros Hyy'%HdRel_inv.
137 intros [->|Hz]%list_elem_of_cons_inv; first done.
138 intros Hxy.
139 have : R x y' by eapply (_ : Transitive R).
140 by apply IH.
141Qed.
142
143Lemma Sorted_list_elem_of_cons_inv {A} `{!Transitive R} (x y : A) (l : list A) :
144 Sorted R (y :: l) →
145 x ∈ y :: l → x = y ∧ Forall (R x) l ∨ R y x ∧ x ∈ l.
146Proof.
147 intros HSort [->|H%list_elem_of_In]%list_elem_of_In%in_inv.
148 - left. by apply Sorted_StronglySorted in HSort as [_ ?]%StronglySorted_inv.
149 - right. inv HSort. inv H3; first inv H.
150 by split; first eapply Sorted_list_elem_of_R_trans.
151Qed.
152
153Lemma period_seq_nf_elem_of_cons_inv (p1 p2 : ne_period) (ps : period_seq) :
154 period_seq_nf (p2 :: ps) →
155 p1 ∈ p2 :: ps → p1 = p2 ∧ Forall (period_before p1) ps ∨
156 period_before p2 p1 ∧ p1 ∈ ps.
157Proof. apply Sorted_list_elem_of_cons_inv. Qed.
158
159Inductive option_Exists {A} (Φ : A → Prop) : option A → Prop :=
160 | Exists_Some (x : A) : Φ x → option_Exists Φ (Some x).
161
162Lemma option_Exists_from_option {A} Φ (mx : option A) :
163 option_Exists Φ mx ↔ from_option Φ False mx.
164Proof. split; by [inv 1 | destruct mx]. Qed.
165
166Lemma period_seq_intersect_lem_aux (p1 p2 : ne_period) (ps1 ps2 : period_seq) :
167 is_Some (ne_period_intersection p1 p2) →
168 period_seq_nf ps1 → period_seq_nf ps2 →
169 p1 ∈ ps1 → p2 ∈ ps2 →
170 option_Exists (.∈ ps1 ∩ ps2) (ne_period_intersection p1 p2).
171Proof.
172 intros Hne. revert ps2.
173 induction ps1 as [|[s1 e1] ps1]; first inv 3.
174 intros ps2 Hnf1 Hnf2 H1 H2. revert ps2 Hnf2 H2.
175 induction ps2 as [|[s2 e2] ps2]; first inv 2.
176 intros Hnf2 H2.
177
178 apply option_Exists_from_option.
179 rewrite /intersection period_seq_intersection_eq /=.
180 apply period_seq_nf_elem_of_cons_inv in H1 as [[-> Hp1]|[Hlt1 H1]]; last done.
181 + apply period_seq_nf_elem_of_cons_inv in H2 as [[-> Hp2]|[Hlt2 H2]]; last done.
182 * unfold ne_period_intersection.
183 case_decide.
184 -- exfalso. simpl in Hne.
185 apply limit_le_cases in H as [contra|contra].
186 ++ rewrite contra in Hne. by eapply (_ : Irreflexive limit_lt).
187 ++ by apply asymmetry in Hne.
188 -- constructor.
189 * case_decide.
190 -- case_decide.
191 ++ (* we need to show that [s1, e1) ## p2 *)
192 exfalso. assert ([s1, e1) ## p2).
193 { unfold disjoint, period_disjoint, period_empty.
194 destruct p2 as [s3 e3]. simpl.
195 destruct Hlt2 as [Hne2 [Hne3 Hlt2]].
196 simpl in Hlt2.
197
198 trans (e1 `min` e2)%lim.
199 { apply limit_le_cases. left.
200 trans e1.
201 - apply limit_min_eq_l, limit_le_cases. right.
202 by trans e2; last trans s3.
203 - apply symmetry, limit_min_eq_l, limit_le_cases. by right. }
204 etrans; first done.
205 apply limit_max_le.
206 split.
207 - apply limit_le_max. by left.
208 - apply limit_le_max. right.
209 apply limit_le_cases. right. by trans e2. }
210 by eapply period_empty_not_nonempty.
211 ++ by apply IHps2; first apply period_seq_nf_cons in Hnf2 as [_ [? _]].
212 -- case_decide.
213 ++ apply not_limit_le in H.
214 (* [s1, e1) ## p2 since e1 < e2 and e2 < p2, but [s1, e1) ∩ p2 ≠ ∅ in hyp *)
215 exfalso. assert ([s1, e1) ## p2).
216 { unfold disjoint, period_disjoint, period_empty.
217 destruct p2 as [s3 e3]. simpl.
218 destruct Hlt2 as [Hne2 [Hne3 Hlt2]].
219 simpl in Hlt2.
220
221 rewrite limit_min_l; last first.
222 { apply limit_le_cases. right.
223 by trans e2; last trans s3. }
224 apply limit_le_max. right.
225 apply limit_le_cases. right.
226 by trans e2. }
227 by eapply period_empty_not_nonempty.
228 ++ constructor. by apply IHps2; first apply period_seq_nf_cons in Hnf2 as (_ & ? & _).
229 + apply period_seq_nf_elem_of_cons_inv in H2 as [[-> Hp2]|[Hlt2 H2]]; last done.
230 * case_decide.
231 -- case_decide.
232 ++ apply IHps1; try done.
233 ** by apply period_seq_nf_cons in Hnf1 as (_ & ? & _).
234 ** by constructor.
235 ++ apply not_limit_lt in H0. exfalso. assert (p1 ## [s2, e2)).
236 { unfold disjoint, period_disjoint, period_empty.
237 destruct p1 as [s3 e3]. simpl.
238 destruct Hlt1 as [Hne1 [Hne3 Hlt1]].
239 simpl in Hlt1.
240
241 trans (e1 `min` e2)%lim.
242 { apply limit_le_cases. left.
243 trans e2.
244 - apply limit_min_eq_r. trans e1; first done.
245 apply limit_le_cases. right. by trans s3.
246 - by apply symmetry, limit_min_eq_r. }
247 etrans; first done.
248 apply limit_max_le.
249 split.
250 - apply limit_le_max. left.
251 apply limit_le_cases. right. by trans e1.
252 - apply limit_le_max. by right. }
253 by eapply period_empty_not_nonempty.
254 -- case_decide.
255 ++ constructor. apply IHps1; try done.
256 ** by apply period_seq_nf_cons in Hnf1 as (_ & ? & _).
257 ** by constructor.
258 ++ apply not_limit_lt in H0. apply not_limit_le in H.
259 exfalso. assert (p1 ## [s2, e2)).
260 { unfold disjoint, period_disjoint, period_empty.
261 destruct p1 as [s3 e3]. simpl.
262 destruct Hlt1 as [Hne1 [Hne3 Hlt1]].
263 simpl in Hlt1.
264
265 rewrite limit_min_r; last first.
266 { trans e1; first done.
267 apply limit_le_cases. right.
268 by trans s3. }
269 trans e1; first done.
270 apply limit_le_max. left.
271 apply limit_le_cases. by right. }
272 by eapply period_empty_not_nonempty.
273 * case_decide.
274 -- case_decide.
275 ++ apply IHps1; try done.
276 ** by apply period_seq_nf_cons in Hnf1 as (_ & ? & _).
277 ** by constructor.
278 ++ by apply IHps2; first apply period_seq_nf_cons in Hnf2 as (_ & ? & _).
279 -- case_decide; constructor.
280 ++ apply IHps1; try done.
281 ** by apply period_seq_nf_cons in Hnf1 as (_ & ? & _).
282 ** by constructor.
283 ++ by apply IHps2; first apply period_seq_nf_cons in Hnf2 as (_ & ? & _).
284Qed.
285
286Lemma period_seq_intersection_inv (p : period) (ps1 ps2 : period_seq) :
287 period_seq_nf ps1 → period_seq_nf ps2 → p ∈ ps1 ∩ ps2 →
288 ∃ p1 p2, p1 ∈ ps1 ∧ p2 ∈ ps2 ∧ p = p1 ∩ p2.
289Proof.
290 intros Hnf1. revert ps2.
291 induction ps1; first inv 2.
292 induction ps2.
293 { intros _ contra.
294 rewrite period_seq_intersection_eq in contra.
295 destruct a. inv contra. }
296 destruct a as [s1 e1], a0 as [s2 e2].
297 intros Hnf2 Hint.
298 rewrite period_seq_intersection_eq in Hint.
299 simpl in Hint. case_decide; case_decide.
300 - apply IHps1 in Hint as (q1 & q2 & Hq1 & Hq2 & ->); last done.
301 + exists q1, q2. by repeat split; first constructor.
302 + by apply period_seq_nf_cons in Hnf1 as (_ & ? & _).
303 - apply IHps2 in Hint as (q1 & q2 & Hq1 & Hq2 & ->).
304 + exists q1, q2. by repeat split; last constructor.
305 + by apply period_seq_nf_cons in Hnf2 as (_ & ? & _).
306 - inv Hint.
307 + exists [s1, e1), [s2, e2). repeat split; constructor.
308 + apply IHps1 in H3 as (q1 & q2 & Hq1 & Hq2 & ->); last done.
309 * exists q1, q2. by repeat split; first constructor.
310 * by apply period_seq_nf_cons in Hnf1 as (_ & ? & _).
311 - inv Hint.
312 + exists [s1, e1), [s2, e2). repeat split; constructor.
313 + apply IHps2 in H3 as (q1 & q2 & Hq1 & Hq2 & ->).
314 * exists q1, q2. by repeat split; last constructor.
315 * by apply period_seq_nf_cons in Hnf2 as (_ & ? & _).
316Qed.
317
318Lemma period_seq_intersection_lem t (ps1 ps2 : period_seq) :
319 period_seq_nf ps1 → period_seq_nf ps2 →
320 t ∈ ps1 ∧ t ∈ ps2 ↔ t ∈ ps1 ∩ ps2.
321Proof.
322 intros Hnf1 Hnf2.
323 split.
324 - intros [H1 H2].
325 unfold elem_of, period_seq_elem_of in H1, H2.
326 apply Exists_exists in H1 as (p1 & Hp1 & Ht1).
327 apply Exists_exists in H2 as (p2 & Hp2 & Ht2).
328 assert (Ht : t ∈ p1 ∩ p2). { by apply intersect_and. }
329 clear Ht1 Ht2.
330 unfold elem_of, period_seq_elem_of.
331 apply Exists_exists. exists (p1 ∩ p2).
332 split; first apply period_seq_intersect_lem_aux; try done.
333 apply period_nonempty_alt_iff. by exists t.
334 - intros (p & Hp & Ht)%Exists_exists.
335 apply period_seq_intersection_inv in Hp as (p1 & p2 & Hp1 & Hp2 & ->); try done.
336 apply intersect_and in Ht as [Ht1 Ht2].
337 split; apply Exists_exists; by eexists.
338Qed.
339
340Definition period_seq_extent (ps : period_seq) : period :=
341 match head ps, last ps with
342 | Some [s, _), Some [_, e) => [s, e)
343 | _, _ => ∅
344 end.
345
346(*
347Lemma period_seq_extent_hd ps :
348 period_seq_nf ps →
349 Forall (period_start (period_seq_extent ps)
350
351Lemma period_seq_extent_spec t ps :
352 period_seq_nf ps → t ∈ ps →
353 t ∈ period_seq_extent ps.
354Proof.
355 Search StronglySorted.
356 induction ps as [|p ps]; first inv 2.
357 intros Hnf. inv 1.
358 -
359
360Qed.
361*)
362
363(*
364Definition period_seq_intersection_extent (ps1 ps2 : period_seq) :
365 period_seq_nf ps1 → period_seq_nf ps2 →
366 period_seq_extent (ps1 ∩ ps2) = period_seq_extent ps1 ∩ period_seq_extent ps2.
367Proof.
368 intros Hnf1 Hnf2.
369 destruct (decide (period_empty (period_seq_extent (ps1 ∩ ps2)))).
370 - admit.
371 - apply period_empty_not_nonempty in n.
372 apply period_nonempty_equiv_L; first done.
373 + admit.
374 + intros t.
375 Search period equiv eq.
376*)
377
378(* The intersection preserves normal forms *)
379Lemma period_seq_intersection_nf (ps1 ps2 : period_seq) :
380 period_seq_nf ps1 → period_seq_nf ps2 → period_seq_nf (ps1 ∩ ps2).
381Proof.
382 intros Hnf1. revert ps2.
383 induction ps1 as [|[s1 e1] ps1]; induction ps2 as [|[s2 e2] ps2]; [done..|].
384 intros Hnf2. rewrite period_seq_intersection_eq /=.
385 case_decide.
386 - case_decide.
387 + by apply IHps1; first apply period_seq_nf_cons in Hnf1 as (_ & ? & _).
388 + apply IHps2. by apply period_seq_nf_cons in Hnf2 as (_ & ? & _).
389 - case_decide.
390 + apply IHps1 in Hnf2 as Hnf2'; last by apply period_seq_nf_cons in Hnf1 as (_ & ? & _).
391 destruct Hnf2' as [Hne HSort]. split.
392 * by constructor; first apply period_empty_not_nonempty.
393 * constructor; first done.
394 rewrite {1}/intersection /period_intersection.
395 apply period_seq_nf_cons in Hnf1 as (Hne1 & Hnf1 & Hlt1).
396 destruct (ps1 ∩ ([s2, e2) :: ps2)) as [|[sq eq] qs] eqn:Hqs; constructor.
397 assert (Hq : [sq, eq) ∈ ps1 ∩ ([s2, e2) :: ps2)).
398 { rewrite Hqs. constructor. }
399 unfold period_before. repeat split.
400 -- by apply period_empty_not_nonempty.
401 -- by eapply Forall_forall; first apply Hne.
402 -- specialize (IHps1 Hnf1).
403 apply period_seq_intersection_inv in Hq as ([sq1 eq1] & [sq2 eq2] & Hq1%list_elem_of_In & Hq2 & Hq); [|done..].
404 apply (proj1 (List.Forall_forall _ _) Hlt1) in Hq1.
405 injection Hq as -> ->.
406 simplify_eq/=.
407 apply limit_min_lt. left.
408 apply limit_lt_max. by left.
409 + apply IHps1 in Hnf2 as Hnf2'; last by apply period_seq_nf_cons in Hnf1 as (_ & ? & _).
410 destruct Hnf2' as [Hne HSort].
411 apply not_limit_lt in H0. split.
412 * constructor.
413 -- by apply period_empty_not_nonempty.
414 -- apply IHps2. by apply period_seq_nf_cons in Hnf2 as (_ & ? & _).
415 * constructor.
416 -- apply IHps2. by apply period_seq_nf_cons in Hnf2 as (_ & ? & _).
417 -- rewrite {1}/intersection /period_intersection.
418 apply period_seq_nf_cons in Hnf1 as Hnf1'.
419 destruct Hnf1' as (Hp1 & Hnf1' & Hne1).
420 apply period_seq_nf_cons in Hnf2 as (Hne2 & Hnf2 & Hlt2).
421 apply IHps2 in Hnf2 as Hnf2'.
422 destruct (([s1, e1) :: ps1) ∩ ps2) as [|[sq eq] qs] eqn:Hqs; constructor.
423 assert (Hq : [sq, eq) ∈ ([s1, e1) :: ps1) ∩ ps2).
424 { rewrite Hqs. constructor. }
425 unfold period_before. repeat split.
426 ++ by apply period_empty_not_nonempty.
427 ++ by eapply Forall_forall; first apply Hnf2'.
428 ++ apply period_seq_intersection_inv in Hq as ([sq1 eq1] & [sq2 eq2] & Hq1 & Hq2%list_elem_of_In & Hq); [|done..].
429 apply (proj1 (List.Forall_forall _ _) Hlt2) in Hq2.
430 injection Hq as -> ->.
431 simplify_eq/=.
432 apply limit_min_lt. right.
433 apply limit_lt_max. by right.
434Qed.
435
436Definition period_seq_intersection_comm_equiv ps1 ps2 :
437 period_seq_nf ps1 → period_seq_nf ps2 →
438 ps1 ∩ ps2 ≡ ps2 ∩ ps1.
439Proof.
440 intros Hnf1 Hnf2 t.
441 split; by intros [H2 H1]%period_seq_intersection_lem;
442 first apply period_seq_intersection_lem.
443Qed.
444
445Lemma period_seq_nf_cons_equiv_inv_start_1 p1 ps1 p2 ps2:
446 period_seq_nf (p1 :: ps1) →
447 period_seq_nf (p2 :: ps2) →
448 p1 :: ps1 ≡ p2 :: ps2 →
449 ¬ (period_start p1 < period_start p2)%lim.
450Proof.
451 intros Hnf1 Hnf2 Hequiv Hp12.
452 apply period_seq_nf_cons in Hnf1 as (Hne1 & Hnf1 & Hlt1), Hnf2 as (Hne2 & Hnf2 & Hlt2).
453 destruct p1 as [s1 e1], p2 as [s2 e2]. simpl in Hp12.
454 destruct s2 as [|s2|]; [by destruct s1| |done].
455 destruct s1 as [|s1|]; last done.
456 - destruct e1 as [|e1|]; first done.
457 + assert (Z.pred (s2 `min` e1) ∈ [-∞, e1) :: ps1).
458 { constructor. by split; [|simpl; lia]. }
459 apply Hequiv in H. inv H.
460 * destruct H1 as [H1 _]. simpl in H1. lia.
461 * apply Exists_exists in H1 as ([sp ep] & Hp & Hs2).
462 rewrite Forall_forall in Hlt2.
463 apply Hlt2 in Hp. simpl in Hp.
464 destruct Hs2 as [Hs21 Hs22].
465 assert (contra : (s2 < s2)%lim).
466 { trans e2; first done.
467 apply (limit_lt_le_trans sp); first done.
468 etrans; first apply Hs21. simpl. lia. }
469 by eapply (_ : Irreflexive limit_lt).
470 + assert (Z.pred s2 ∈ [-∞, +∞) :: ps1).
471 { by constructor. }
472 apply Hequiv in H. inv H.
473 * destruct H1 as [H1 _]. simpl in H1. lia.
474 * apply Exists_exists in H1 as ([sp ep] & Hp & Hs2).
475 rewrite Forall_forall in Hlt2.
476 apply Hlt2 in Hp. simpl in Hp.
477 destruct Hs2 as [Hs21 Hs22].
478 assert (contra : (s2 < s2)%lim).
479 { trans e2; first done.
480 apply (limit_lt_le_trans sp); first done.
481 etrans; first apply Hs21. simpl. lia. }
482 by eapply (_ : Irreflexive limit_lt).
483 - assert (s1 ∈ [s1, e1) :: ps1).
484 { by constructor. }
485 apply Hequiv in H. inv H.
486 + destruct H1 as [[[= ->]|H1]%limit_le_cases _].
487 * by eapply (_ : Irreflexive limit_lt).
488 * by eapply (asymmetry (R:=limit_lt)).
489 + apply Exists_exists in H1 as ([sp ep] & Hp & Hs1).
490 rewrite Forall_forall in Hlt2.
491 apply Hlt2 in Hp. simpl in Hp.
492 assert (contra : (s1 < s1)%lim).
493 { trans s2; first done.
494 trans e2; first done.
495 by apply (limit_lt_le_trans sp); last apply Hs1. }
496 by eapply (_ : Irreflexive limit_lt).
497Qed.
498
499Instance period_seq_equiv_trans : Transitive (≡@{period_seq}).
500Proof.
501 intros ps1 ps2 ps3 Heq12 Heq23 t. split.
502 - by intros Ht%Heq12%Heq23.
503 - by intros Ht%Heq23%Heq12.
504Qed.
505
506Instance period_seq_equiv_symm : Symmetric (≡@{period_seq}).
507Proof. intros ps1 ps2 Heq12 t. split; by intros Ht%Heq12. Qed.
508
509Lemma period_seq_nf_cons_equiv_inv_start p1 ps1 p2 ps2:
510 period_seq_nf (p1 :: ps1) →
511 period_seq_nf (p2 :: ps2) →
512 p1 :: ps1 ≡ p2 :: ps2 →
513 period_start p1 = period_start p2.
514Proof.
515 intros Hnf1 Hnf2 Hequiv.
516 destruct (decide (period_start p1 < period_start p2)%lim) as [Hs12|Hs21].
517 - exfalso. by eapply period_seq_nf_cons_equiv_inv_start_1 in Hs12.
518 - apply not_limit_lt, limit_le_cases in Hs21 as [Hs21|Hs21]; first done.
519 exfalso. by eapply period_seq_nf_cons_equiv_inv_start_1 in Hs21.
520Qed.
521
522Lemma period_seq_nf_cons_equiv_inv_end_1 p1 ps1 p2 ps2:
523 period_seq_nf (p1 :: ps1) →
524 period_seq_nf (p2 :: ps2) →
525 p1 :: ps1 ≡ p2 :: ps2 →
526 ¬ (period_end p1 < period_end p2)%lim.
527Proof.
528 intros Hnf1 Hnf2 Hequiv Hp12.
529 assert (Hs : period_start p1 = period_start p2).
530 { by eapply period_seq_nf_cons_equiv_inv_start. }
531 apply period_seq_nf_cons in Hnf1 as (Hne1 & Hnf1 & Hlt1), Hnf2 as (Hne2 & Hnf2 & Hlt2).
532 destruct p1 as [s1 e1], p2 as [s2 e2]. simpl in Hs, Hp12.
533 rewrite <-Hs in *. rename s1 into s. clear Hs s2.
534 destruct e1 as [|e1|]; [by destruct s| |done].
535 assert (e1 ∈ [s, e2) :: ps2).
536 { constructor. by split; [apply limit_le_cases; right|]. }
537 apply Hequiv in H. inv H.
538 + destruct H1 as [_ H12]. by eapply (_ : Irreflexive limit_lt).
539 + apply Exists_exists in H1 as (p & Hp & He1).
540 rewrite Forall_forall in Hlt1.
541 apply Hlt1 in Hp.
542 destruct p as [sp ep].
543 unfold period_end, period_start in Hp.
544 assert (contra : (e1 < e1)%lim).
545 { by eapply limit_lt_le_trans; last apply He1. }
546 by eapply (_ : Irreflexive limit_lt).
547Qed.
548
549Lemma period_seq_nf_cons_equiv_inv_end p1 ps1 p2 ps2:
550 period_seq_nf (p1 :: ps1) →
551 period_seq_nf (p2 :: ps2) →
552 p1 :: ps1 ≡ p2 :: ps2 →
553 period_end p1 = period_end p2.
554Proof.
555 intros Hnf1 Hnf2 Hequiv.
556 destruct (decide (period_end p1 < period_end p2)%lim) as [He12|He21].
557 - exfalso. by eapply period_seq_nf_cons_equiv_inv_end_1 in He12.
558 - apply not_limit_lt, limit_le_cases in He21 as [He21|He21]; first done.
559 exfalso. by eapply period_seq_nf_cons_equiv_inv_end_1 in He21.
560Qed.
561
562Lemma period_seq_nf_cons_equiv_inv p1 ps1 p2 ps2:
563 period_seq_nf (p1 :: ps1) →
564 period_seq_nf (p2 :: ps2) →
565 p1 :: ps1 ≡ p2 :: ps2 →
566 p1 = p2.
567Proof.
568 intros Hnf1 Hnf2 Hequiv.
569 trans [period_start p1, period_end p1); first by destruct p1.
570 trans [period_start p2, period_end p2); last by destruct p2.
571 erewrite period_seq_nf_cons_equiv_inv_start; try done.
572 by erewrite period_seq_nf_cons_equiv_inv_end.
573Qed.
574
575Lemma period_seq_nf_equiv_L ps1 ps2 :
576 period_seq_nf ps1 →
577 period_seq_nf ps2 →
578 ps1 ≡ ps2 → ps1 = ps2.
579Proof.
580 intros Hnf1. revert ps2.
581 induction ps1 as [|p1 ps1]; intros ps2 Hnf2 Hequiv.
582 - destruct ps2; first done.
583 assert (period_nonempty p) as [t Ht]%period_nonempty_alt_iff.
584 { inv Hnf2. by inv H. }
585 assert (t ∈ p :: ps2) as contra%Hequiv.
586 { by apply Exists_cons_hd. }
587 inv contra.
588 - destruct ps2 as [|p2 ps2].
589 + assert (period_nonempty p1) as [t Ht]%period_nonempty_alt_iff.
590 { inv Hnf1. by inv H. }
591 assert (t ∈ p1 :: ps1) as contra%Hequiv.
592 { by apply Exists_cons_hd. }
593 inv contra.
594 + assert (p1 = p2) as <-.
595 { by eapply period_seq_nf_cons_equiv_inv. }
596 rename p1 into p.
597 apply period_seq_nf_cons in Hnf1 as (Hne1 & Hnf1 & Hlt1), Hnf2 as (Hne2 & Hnf2 & Hlt2).
598 f_equal. apply IHps1; [done..|].
599 intros t. split; intros Ht.
600 * assert (t ∈ p :: ps1) as H%Hequiv.
601 { by apply Exists_cons_tl. }
602 inv H; last done.
603 apply Exists_exists in Ht as ([sq eq] & Hp & Ht).
604 rewrite Forall_forall in Hlt1.
605 apply Hlt1 in Hp.
606 exfalso. destruct p as [s e].
607 simpl in *.
608 assert (contra : (t < t)%lim).
609 { trans e; first apply H1.
610 by eapply limit_lt_le_trans; last apply Ht. }
611 by eapply (_ : Irreflexive limit_lt).
612 * assert (t ∈ p :: ps2) as H%Hequiv.
613 { by apply Exists_cons_tl. }
614 inv H; last done.
615 apply Exists_exists in Ht as ([sq eq] & Hp & Ht).
616 rewrite Forall_forall in Hlt2.
617 apply Hlt2 in Hp.
618 exfalso. destruct p as [s e].
619 simpl in *.
620 assert (contra : (t < t)%lim).
621 { trans e; first apply H1.
622 by eapply limit_lt_le_trans; last apply Ht. }
623 by eapply (_ : Irreflexive limit_lt).
624Qed.
625
626Definition period_seq_intersection_comm ps1 ps2 :
627 period_seq_nf ps1 → period_seq_nf ps2 →
628 ps1 ∩ ps2 = ps2 ∩ ps1.
629Proof.
630 intros Hnf1 Hnf2.
631 apply period_seq_nf_equiv_L.
632 - by apply period_seq_intersection_nf.
633 - by apply period_seq_intersection_nf.
634 - by apply period_seq_intersection_comm_equiv.
635Qed.
636
637Instance period_seq_equiv_refl : Reflexive (≡@{period_seq}).
638Proof. done. Qed.
639
640Instance period_seq_equiv_equivalence : Equivalence (≡@{period_seq}).
641Proof. split; apply _. Qed.
642
643Variant bound :=
644 | LtBound of limit
645 | GeBound of limit.
646
647Definition bound_le b1 b2 :=
648 match b1, b2 with
649 | GeBound l1, GeBound l2 => (l1 ≤ l2)%lim
650 | GeBound _, LtBound _ => True
651 | LtBound l1, LtBound l2 => (l1 ≤ l2)%lim
652 | LtBound _, GeBound _ => False
653 end.
654Instance bound_lt_dec : RelDecision bound_le.
655Proof. intros [l1|l1] [l2|l2]; simpl; solve_decision. Qed.
656
657Instance bound_le_refl : Reflexive bound_le.
658Proof. by intros []; simpl. Qed.
659
660Instance bound_le_trans : Transitive bound_le.
661Proof. intros [] [] [] ? ?; simpl in *; done || by etrans. Qed.
662
663Instance bound_le_preorder : PreOrder bound_le.
664Proof. split; apply _. Qed.
665
666Instance bound_le_antisymm : AntiSymm (=) bound_le.
667Proof. intros [] [] ? ?; simpl in *; done || f_equal; by eapply (_ : AntiSymm (=) limit_le). Qed.
668
669Instance bound_le_partial_order : PartialOrder bound_le.
670Proof. split; apply _. Qed.
671
672Instance bound_le_trichotomy : Trichotomy (strict bound_le).
673Proof.
674 intros [] []; simpl in *.
675 - destruct (trichotomy _ l l0) as [?|[?|?]].
676 + left. split; simpl.
677 * apply limit_le_cases. by right.
678 * by apply not_limit_le.
679 + right. left. by subst.
680 + right. right. split; simpl.
681 * apply limit_le_cases. by right.
682 * by apply not_limit_le.
683 - right. right. split; simpl; [done|by intros ?].
684 - left. split; simpl; [done|by intros ?].
685 - destruct (trichotomy _ l l0) as [?|[?|?]].
686 + left. split; simpl.
687 * apply limit_le_cases. by right.
688 * by apply not_limit_le.
689 + right. left. by subst.
690 + right. right. split; simpl.
691 * apply limit_le_cases. by right.
692 * by apply not_limit_le.
693Qed.
694
695Instance bound_le_total_order : TotalOrder bound_le.
696Proof. split; apply _. Qed.
697
698Definition period_bounds '[s, e) :=
699 if decide (period_nonempty [s, e)) then [GeBound s; LtBound e] else [].
700
701Definition period_seq_bounds (ps : period_seq) :=
702 ps ≫= period_bounds.
703
704Definition period_seq_bounds_sorted (ps : period_seq) :=
705 merge_sort bound_le (period_seq_bounds ps).
706
707Variant window_filter_action :=
708 KickLeft | KickRight | NoAction.
709Fixpoint window_filter_aux {A} (f : A → A → window_filter_action) (x : A) (l : list A) :=
710 match l with
711 | [] => [x]
712 | y :: l' =>
713 match f x y with
714 | KickLeft => window_filter_aux f y l'
715 | KickRight => window_filter_aux f x l'
716 | NoAction => x :: window_filter_aux f y l'
717 end
718 end.
719Definition window_filter {A} (f : A → A → window_filter_action) (l : list A) :=
720 match l with
721 | [] => []
722 | x :: l' => window_filter_aux f x l'
723 end.
724
725Definition period_seq_bounds_clean (ps : period_seq) :=
726 window_filter (λ b1 b2, match b1, b2 with
727 | GeBound _, LtBound _ => NoAction
728 | GeBound _, GeBound _ => KickRight
729 | LtBound _, GeBound _ => NoAction
730 | LtBound _, LtBound _ => KickLeft
731 end)
732 (period_seq_bounds_sorted ps).
733
734Fixpoint period_seq_from_bounds (bs : list bound) : period_seq :=
735 match bs with
736 | GeBound s :: LtBound e :: bs' => [s, e) :: period_seq_from_bounds bs'
737 | _ => []
738 end.
739
740Definition period_seq_normalize (ps : period_seq) :=
741 period_seq_from_bounds (period_seq_bounds_clean ps).
742
743
744Lemma period_seq_normalize_lem_1 (ps : period_seq) :
745 period_seq_normalize ps ≡ ps.
746Proof.
747 Search merge_sort.
748 Search Total Trichotomy.
749
750
751(* TODO: continue here *) Admitted.
752
753Lemma period_seq_normalize_lem_2 (ps : period_seq) :
754 period_seq_nf (period_seq_normalize ps).
755Proof. (* TODO: and here *) Admitted.
756
757Definition period_seq_union (ps1 ps2 : period_seq) :=
758 period_seq_normalize (ps1 ++ ps2).
759Lemma period_seq_union_lem t ps1 ps2 :
760 t ∈ period_seq_union ps1 ps2 ↔ t ∈ ps1 ∨ t ∈ ps2.
761Proof.
762 split.
763 - intros Ht%(period_seq_normalize_lem_1 (ps1 ++ ps2)).
764 apply Exists_app in Ht as [Ht|Ht]; by [left|right].
765 - intros [Ht|Ht]; apply period_seq_normalize_lem_1, Exists_app; by [left|right].
766Qed.
767Lemma period_seq_union_nf ps1 ps2 :
768 period_seq_nf (period_seq_union ps1 ps2).
769Proof. apply period_seq_normalize_lem_2. Qed.
770
771Definition nf_period_seq := sig period_seq_nf.
772
773Instance period_seq_nf_pi ps : ProofIrrel (period_seq_nf ps).
774Proof.
775 unfold period_seq_nf. intros [P11 P12] [P21 P22].
776 f_equal; [apply Forall_pi | apply Sorted_pi]; apply _.
777Qed.
778
779Instance period_seq_empty : Empty period_seq := [].
780Lemma period_seq_empty_nf : period_seq_nf ∅.
781Proof. done. Qed.
782
783Instance period_seq_singleton : Singleton timestamp period_seq :=
784 λ t, [{[t]}].
785Lemma period_seq_singleton_lem_1 t : t ∈ ({[t]} : period_seq).
786Proof.
787 unfold singleton, period_seq_singleton.
788 constructor. apply period_singleton_lem_1.
789Qed.
790Lemma period_seq_singleton_lem_2 t t' : t' ∈ ({[t]} : period_seq) → t' = t.
791Proof.
792 unfold singleton, period_seq_singleton.
793 inv 1; last inv H1.
794 by apply period_singleton_lem_2.
795Qed.
796Lemma period_seq_singleton_nf t : period_seq_nf {[t]}.
797Proof.
798 unfold singleton, period_seq_singleton.
799 split.
800 - constructor; last constructor.
801 apply period_singleton_nonempty.
802 - constructor; constructor.
803Qed.
804
805Instance nf_period_seq_elem_of : ElemOf timestamp nf_period_seq :=
806 λ t ps, t ∈ `ps.
807Instance nf_period_seq_empty : Empty nf_period_seq :=
808 ∅ ↾ period_seq_empty_nf.
809Instance nf_period_seq_union : Union nf_period_seq :=
810 λ '(ps1↾_) '(ps2↾_), period_seq_union ps1 ps2 ↾ (period_seq_union_nf ps1 ps2).
811Instance nf_period_seq_singleton : Singleton timestamp nf_period_seq :=
812 λ t, {[t]} ↾ period_seq_singleton_nf t.
813
814Instance nf_period_seq_semiset : SemiSet timestamp nf_period_seq.
815Proof.
816 split.
817 - intros t Ht. inv Ht.
818 - split.
819 + apply period_seq_singleton_lem_2.
820 + intros <-. apply period_seq_singleton_lem_1.
821 - intros [ps1 Hnf1] [ps2 Hnf2] t.
822 unfold union, nf_period_seq_union, elem_of, nf_period_seq_elem_of.
823 simpl. apply period_seq_union_lem.
824Qed.
825
826Instance nf_period_seq_intersection : Intersection nf_period_seq :=
827 λ '(ps1↾Hnf1) '(ps2↾Hnf2), (ps1 ∩ ps2) ↾ (period_seq_intersection_nf ps1 ps2 Hnf1 Hnf2).
828
829(* TODO: difference!
830
831Instance nf_period_seq_set : Set_ timestamp nf_period_seq.
832Proof. (* TODO *) Qed.
833
834*)
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 @@
1From stdpp Require Import numbers option sorting ssreflect.
2From stdpp Require Import options.
3
4Definition transportf {X} (P : X → Type) {x x' : X} : x = x' → P x → P x'.
5Proof. by induction 1. Defined.
6
7Instance HdRel_pi {A} (R : relation A) `{!EqDecision A} `{!∀ x y, ProofIrrel (R x y)} a l : ProofIrrel (HdRel R a l).
8Proof.
9 intros HR1 HR2.
10 assert (Hnil : ∀ xs (Hxs : [] = xs) (HR : HdRel R a xs),
11 HR = transportf _ Hxs (HdRel_nil R a)).
12 { intros. destruct HR; last done.
13 by replace Hxs with (eq_refl ([] : list A)); last apply eq_pi, list_eq_dec. }
14 assert (Hcons : ∀ xs x y xs' (Hxs : y :: xs' = xs) (HR : HdRel R x xs) (Hxy : R x y),
15 HR = transportf (HdRel R x) Hxs (HdRel_cons R x y xs' Hxy)).
16 { intros. destruct HR; first done.
17 injection Hxs as <- <-.
18 replace Hxs with (eq_refl (y :: xs')); last apply eq_pi, list_eq_dec.
19 simpl.
20 by replace r with Hxy by apply H. }
21 destruct l.
22 - trans (transportf (HdRel R a) eq_refl (HdRel_nil R a)).
23 + apply Hnil.
24 + symmetry. apply Hnil.
25 - apply HdRel_inv in HR1 as Haa0.
26 trans (transportf (HdRel R a) eq_refl (HdRel_cons R a a0 l Haa0)).
27 + apply Hcons.
28 + symmetry. apply Hcons.
29Qed.
30
31Instance Sorted_pi {A} (R : relation A) `{!EqDecision A} `{!∀ x y, ProofIrrel (R x y)} l : ProofIrrel (Sorted R l).
32Proof.
33 intros HS1 HS2.
34 assert (Hbase : ∀ xs (Hxs : [] = xs) (HS : Sorted R xs), HS = transportf _ Hxs (Sorted_nil R)).
35 { intros. destruct HS; last done.
36 by replace Hxs with (eq_refl ([] : list A)); last apply eq_pi, list_eq_dec. }
37 assert (Hind : ∀ xs x xs'
38 (Hxs : x :: xs' = xs) (HS : Sorted R xs)
39 (Hx : HdRel R x xs') (HS' : Sorted R xs')
40 (IH : ∀ HS1' HS2' : Sorted R xs', HS1' = HS2'),
41 HS = transportf _ Hxs (Sorted_cons HS' Hx)).
42 { intros. destruct HS; first done.
43 injection Hxs as <- <-.
44 replace Hxs with (eq_refl (x :: xs')); last apply eq_pi, list_eq_dec.
45 simpl.
46 replace h with Hx by apply: HdRel_pi.
47 by replace HS with HS' by apply IH. }
48 induction l.
49 - trans (transportf _ eq_refl (Sorted_nil R)).
50 + apply Hbase.
51 + symmetry. apply Hbase.
52 - destruct (Sorted_inv HS1) as [Hl Hal].
53 trans (transportf _ eq_refl (Sorted_cons Hl Hal)).
54 + apply Hind, IHl.
55 + symmetry. apply Hind, IHl.
56Qed.
57
58Instance Forall_pi {A} (P : A → Prop) (l : list A) `{!EqDecision A} `{!∀ a, ProofIrrel (P a)} : ProofIrrel (Forall P l).
59Proof.
60 intros HF1 HF2.
61 assert (Hbase : ∀ xs (Hxs : [] = xs) (HF : Forall P xs), HF = transportf (Forall P) Hxs (ListDef.Forall_nil P)).
62 { intros xs Hxs HF. destruct HF; last done.
63 by replace Hxs with (eq_refl ([] : list A)); last apply eq_pi, list_eq_dec. }
64 assert (Hind : ∀ xs x xs'
65 (Hxs : x :: xs' = xs) (HF : Forall P xs)
66 (Hx : P x) (HF' : Forall P xs')
67 (IH : ∀ HF1' HF2' : Forall P xs', HF1' = HF2'),
68 HF = transportf _ Hxs (ListDef.Forall_cons P x xs' Hx HF')).
69 { intros. destruct HF; first done.
70 injection Hxs as <- <-.
71 replace Hxs with (eq_refl (x :: xs')); last apply eq_pi, list_eq_dec.
72 simpl.
73 replace p with Hx by apply H.
74 by replace HF with HF' by apply IH. }
75 induction l.
76 - trans (transportf _ eq_refl (ListDef.Forall_nil P)).
77 + apply Hbase.
78 + symmetry. apply Hbase.
79 - apply Forall_inv in HF1 as Ha.
80 apply Forall_inv_tail in HF1 as Hl.
81 trans (transportf _ eq_refl (ListDef.Forall_cons P a l Ha Hl)).
82 + apply Hind, IHl.
83 + symmetry. apply Hind, IHl.
84Qed.
85
86Instance ex_pi {A} {B : A → Prop} `{!ProofIrrel A} `{!∀ x, ProofIrrel (B x)} :
87 ProofIrrel (∃ (x : A), B x).
88Proof.
89 intros [x Hx] [y Hy].
90 assert (y = x) by apply proof_irrel. subst.
91 assert (Hx = Hy) by apply proof_irrel. by subst.
92Qed.
generated by cgit v1.3 (git 2.53.0) at 2026-09-10 13:11:39 +0000