1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "sets/categories2.ma".
18 interpretation "unary morphism comprehension with no proof" 'comprehension T P =
19 (mk_unary_morphism T ? P ?).
20 interpretation "unary morphism1 comprehension with no proof" 'comprehension T P =
21 (mk_unary_morphism1 T ? P ?).
23 notation > "hvbox({ ident i ∈ s | term 19 p | by })" with precedence 90
24 for @{ 'comprehension_by $s (λ${ident i}. $p) $by}.
25 notation < "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
26 for @{ 'comprehension_by $s (λ${ident i}:$_. $p) $by}.
28 interpretation "unary morphism comprehension with proof" 'comprehension_by s \eta.f p =
29 (mk_unary_morphism s ? f p).
30 interpretation "unary morphism1 comprehension with proof" 'comprehension_by s \eta.f p =
31 (mk_unary_morphism1 s ? f p).
34 (* per il set-indexing vedere capitolo BPTools (foundational tools), Sect. 0.3.4 complete
35 lattices, Definizione 0.9 *)
36 (* USARE L'ESISTENZIALE DEBOLE *)
37 nrecord OAlgebra : Type[2] := {
39 oa_leq : binary_morphism1 oa_P oa_P CPROP; (*CSC: dovrebbe essere CProp bug refiner*)
40 oa_overlap: binary_morphism1 oa_P oa_P CPROP;
41 binary_meet: binary_morphism1 oa_P oa_P oa_P;
42 (*CSC: oa_join: ∀I:setoid.unary_morphism1 (setoid1_of_setoid … I ⇒ oa_P) oa_P;*)
45 oa_leq_refl: ∀a:oa_P. oa_leq a a;
46 oa_leq_antisym: ∀a,b:oa_P.oa_leq a b → oa_leq b a → a = b;
47 oa_leq_trans: ∀a,b,c:oa_P.oa_leq a b → oa_leq b c → oa_leq a c;
48 oa_overlap_sym: ∀a,b:oa_P.oa_overlap a b → oa_overlap b a;
49 (*CSC: oa_join_sup: ∀I:setoid.∀p_i:I ⇒ oa_P.∀p:oa_P.oa_leq (oa_join I p_i) p = (∀i:I.oa_leq (p_i i) p);*)
50 oa_zero_bot: ∀p:oa_P.oa_leq oa_zero p;
51 oa_one_top: ∀p:oa_P.oa_leq p oa_one;
52 oa_overlap_preservers_meet: ∀p,q:oa_P.oa_overlap p q → oa_overlap p (binary_meet p q);
54 ∀I:SET.∀p.∀q:I ⇒ oa_P.
55 oa_overlap p (oa_join I q) = (∃i:I.oa_overlap p (q i));*)
57 1) enum non e' il nome giusto perche' non e' suriettiva
58 2) manca (vedere altro capitolo) la "suriettivita'" come immagine di insiemi di oa_base
59 oa_enum : ums oa_base oa_P;
60 oa_density: ∀p,q.(∀i.oa_overlap p (oa_enum i) → oa_overlap q (oa_enum i)) → oa_leq p q
63 ∀p,q.(∀r.oa_overlap p r → oa_overlap q r) → oa_leq p q
66 interpretation "o-algebra leq" 'leq a b = (fun21 ??? (oa_leq ?) a b).
68 notation "hovbox(a mpadded width -150% (>)< b)" non associative with precedence 45
69 for @{ 'overlap $a $b}.
70 interpretation "o-algebra overlap" 'overlap a b = (fun21 ??? (oa_overlap ?) a b).
72 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (\emsp) \nbsp term 90 p)"
73 non associative with precedence 50 for @{ 'oa_meet $p }.
74 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (ident i ∈ I) break term 90 p)"
75 non associative with precedence 50 for @{ 'oa_meet_mk (λ${ident i}:$I.$p) }.
77 (*notation > "hovbox(∧ f)" non associative with precedence 60
79 interpretation "o-algebra meet" 'oa_meet f =
80 (fun12 ?? (oa_meet ??) f).
81 interpretation "o-algebra meet with explicit function" 'oa_meet_mk f =
82 (fun12 ?? (oa_meet ??) (mk_unary_morphism ?? f ?)).
84 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (\emsp) \nbsp term 90 p)"
85 non associative with precedence 50 for @{ 'oa_join $p }.
86 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (ident i ∈ I) break term 90 p)"
87 non associative with precedence 50 for @{ 'oa_join_mk (λ${ident i}:$I.$p) }.
90 notation > "hovbox(∨ f)" non associative with precedence 60
92 interpretation "o-algebra join" 'oa_join f =
93 (fun12 ?? (oa_join ??) f).
94 interpretation "o-algebra join with explicit function" 'oa_join_mk f =
95 (fun12 ?? (oa_join ??) (mk_unary_morphism ?? f ?)).
97 (*definition binary_meet : ∀O:OAlgebra. binary_morphism1 O O O.
100 apply (∧ { x ∈ BOOL | match x with [ true ⇒ p | false ⇒ q ] | IF_THEN_ELSE_p ? p q });
101 | intros; lapply (prop12 ? O (oa_meet O BOOL));
102 [2: apply ({ x ∈ BOOL | match x with [ true ⇒ a | false ⇒ b ] | IF_THEN_ELSE_p ? a b });
103 |3: apply ({ x ∈ BOOL | match x with [ true ⇒ a' | false ⇒ b' ] | IF_THEN_ELSE_p ? a' b' });
105 intro x; simplify; cases x; simplify; assumption;]
108 interpretation "o-algebra binary meet" 'and a b =
109 (fun21 ??? (binary_meet ?) a b).
112 prefer coercion Type1_OF_OAlgebra.
114 definition binary_join : ∀O:OAlgebra. binary_morphism1 O O O.
117 apply (∨ { x ∈ BOOL | match x with [ true ⇒ p | false ⇒ q ] | IF_THEN_ELSE_p ? p q });
118 | intros; lapply (prop12 ? O (oa_join O BOOL));
119 [2: apply ({ x ∈ BOOL | match x with [ true ⇒ a | false ⇒ b ] | IF_THEN_ELSE_p ? a b });
120 |3: apply ({ x ∈ BOOL | match x with [ true ⇒ a' | false ⇒ b' ] | IF_THEN_ELSE_p ? a' b' });
122 intro x; simplify; cases x; simplify; assumption;]
125 interpretation "o-algebra binary join" 'or a b =
126 (fun21 ??? (binary_join ?) a b).
129 lemma oa_overlap_preservers_meet: ∀O:OAlgebra.∀p,q:O.p >< q → p >< (p ∧ q).
130 (* next change to avoid universe inconsistency *)
131 change in ⊢ (?→%→%→?) with (Type1_OF_OAlgebra O);
132 intros; lapply (oa_overlap_preserves_meet_ O p q f);
133 lapply (prop21 O O CPROP (oa_overlap O) p p ? (p ∧ q) # ?);
134 [3: apply (if ?? (Hletin1)); apply Hletin;|skip] apply refl1;
137 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (\emsp) \nbsp term 90 p)"
138 non associative with precedence 49 for @{ 'oa_join $p }.
139 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (ident i ∈ I) break term 90 p)"
140 non associative with precedence 49 for @{ 'oa_join_mk (λ${ident i}:$I.$p) }.
141 notation < "hovbox(a ∨ b)" left associative with precedence 49
142 for @{ 'oa_join_mk (λ${ident i}:$_.match $i with [ true ⇒ $a | false ⇒ $b ]) }.
144 notation > "hovbox(∨ f)" non associative with precedence 59
145 for @{ 'oa_join $f }.
146 notation > "hovbox(a ∨ b)" left associative with precedence 49
147 for @{ 'oa_join (mk_unary_morphism BOOL ? (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) (IF_THEN_ELSE_p ? $a $b)) }.
149 (*interpretation "o-algebra join" 'oa_join f =
150 (fun12 ?? (oa_join ??) f).
151 interpretation "o-algebra join with explicit function" 'oa_join_mk f =
152 (fun12 ?? (oa_join ??) (mk_unary_morphism ?? f ?)).
154 nrecord ORelation (P,Q : OAlgebra) : Type[1] ≝ {
156 or_f_minus_star : P ⇒ Q;
159 or_prop1 : ∀p,q. (or_f p ≤ q) = (p ≤ or_f_star q);
160 or_prop2 : ∀p,q. (or_f_minus p ≤ q) = (p ≤ or_f_minus_star q);
161 or_prop3 : ∀p,q. (or_f p >< q) = (p >< or_f_minus q)
164 notation "r \sup *" non associative with precedence 90 for @{'OR_f_star $r}.
165 notation > "r *" non associative with precedence 90 for @{'OR_f_star $r}.
167 notation "r \sup (⎻* )" non associative with precedence 90 for @{'OR_f_minus_star $r}.
168 notation > "r⎻*" non associative with precedence 90 for @{'OR_f_minus_star $r}.
170 notation "r \sup ⎻" non associative with precedence 90 for @{'OR_f_minus $r}.
171 notation > "r⎻" non associative with precedence 90 for @{'OR_f_minus $r}.
173 interpretation "o-relation f⎻*" 'OR_f_minus_star r = (or_f_minus_star ? ? r).
174 interpretation "o-relation f⎻" 'OR_f_minus r = (or_f_minus ? ? r).
175 interpretation "o-relation f*" 'OR_f_star r = (or_f_star ? ? r).
178 ndefinition ORelation_setoid : OAlgebra → OAlgebra → setoid1.
179 #P; #Q; @ (ORelation P Q); @
180 [ napply (λp,q.p = q)
182 | #x; #y; napply sym1
183 | #x; #y; #z; napply trans1 ]
186 unification hint 0 ≔ P, Q ;
187 R ≟ (ORelation_setoid P Q)
188 (* -------------------------- *) ⊢
189 carr1 R ≡ ORelation P Q.
191 ndefinition or_f_morphism1: ∀P,Q:OAlgebra.unary_morphism1 (ORelation_setoid P Q)
192 (unary_morphism1_setoid1 P Q).
195 | #a; #a'; #e; nassumption]
198 unification hint 0 ≔ P, Q, r;
199 R ≟ (mk_unary_morphism1 … (or_f …) (prop11 … (or_f_morphism1 …)))
200 (* ------------------------ *) ⊢
201 fun11 … R r ≡ or_f P Q r.
203 nlemma ORelation_eq_respects_leq_or_f_minus_:
204 ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
205 r=r' → ∀x. r⎻ x ≤ r'⎻ x.
206 #P; #Q; #a; #a'; #e; #x;
207 napply oa_density; #r; #H;
208 napply oa_overlap_sym;
209 napply (. (or_prop3 … a' …)^-1); (*CSC: why a'? *)
212 | ngeneralize in match r in ⊢ %;
213 nchange with (or_f … a' = or_f … a);
216 napply (. (or_prop3 …));
217 napply oa_overlap_sym;
221 nlemma ORelation_eq2:
222 ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
224 #P; #Q; #a; #a'; #e; #x;
225 napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_minus_
226 [ napply e | napply e^-1]
229 ndefinition or_f_minus_morphism1: ∀P,Q:OAlgebra.unary_morphism1 (ORelation_setoid P Q)
230 (unary_morphism1_setoid1 Q P).
233 | napply ORelation_eq2]
236 unification hint 0 ≔ P, Q, r;
237 R ≟ (mk_unary_morphism1 … (or_f_minus …) (prop11 … (or_f_minus_morphism1 …)))
238 (* ------------------------ *) ⊢
239 fun11 … R r ≡ or_f_minus P Q r.
241 nlemma ORelation_eq_respects_leq_or_f_star_:
242 ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
243 r=r' → ∀x. r* x ≤ r'* x.
244 #P; #Q; #a; #a'; #e; #x; (*CSC: una schifezza *)
245 ngeneralize in match (. (or_prop1 P Q a' (a* x) x)^-1) in ⊢ %; #H; napply H;
246 nchange with (or_f P Q a' (a* x) ≤ x);
248 [##2: napply (a (a* x))
249 | ngeneralize in match (a* x);
250 nchange with (or_f P Q a' = or_f P Q a);
251 napply (.= †e^-1); napply #]
252 napply (. (or_prop1 …));
256 nlemma ORelation_eq3:
257 ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
259 #P; #Q; #a; #a'; #e; #x;
260 napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_star_
261 [ napply e | napply e^-1]
264 ndefinition or_f_star_morphism1: ∀P,Q:OAlgebra.unary_morphism1 (ORelation_setoid P Q)
265 (unary_morphism1_setoid1 Q P).
268 | napply ORelation_eq3]
271 unification hint 0 ≔ P, Q, r;
272 R ≟ (mk_unary_morphism1 … (or_f_star …) (prop11 … (or_f_star_morphism1 …)))
273 (* ------------------------ *) ⊢
274 fun11 … R r ≡ or_f_star P Q r.
276 nlemma ORelation_eq_respects_leq_or_f_minus_star_:
277 ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
278 r=r' → ∀x. r⎻* x ≤ r'⎻* x.
279 #P; #Q; #a; #a'; #e; #x; (*CSC: una schifezza *)
280 ngeneralize in match (. (or_prop2 P Q a' (a⎻* x) x)^-1) in ⊢ %; #H; napply H;
281 nchange with (or_f_minus P Q a' (a⎻* x) ≤ x);
283 [##2: napply (a⎻ (a⎻* x))
284 | ngeneralize in match (a⎻* x);
285 nchange with (a'⎻ = a⎻);
286 napply (.= †e^-1); napply #]
287 napply (. (or_prop2 …));
291 nlemma ORelation_eq4:
292 ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
294 #P; #Q; #a; #a'; #e; #x;
295 napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_minus_star_
296 [ napply e | napply e^-1]
299 ndefinition or_f_minus_star_morphism1:
300 ∀P,Q:OAlgebra.unary_morphism1 (ORelation_setoid P Q) (unary_morphism1_setoid1 P Q).
302 [ napply or_f_minus_star
303 | napply ORelation_eq4]
306 unification hint 0 ≔ P, Q, r;
307 R ≟ (mk_unary_morphism1 … (or_f_minus_star …) (prop11 … (or_f_minus_star_morphism1 …)))
308 (* ------------------------ *) ⊢
309 fun11 … R r ≡ or_f_minus_star P Q r.
312 ndefinition ORelation_composition : ∀P,Q,R.
313 binary_morphism1 (ORelation_setoid P Q) (ORelation_setoid Q R) (ORelation_setoid P R).
317 | apply rule (G⎻* ∘ F⎻* );
321 change with ((G (F p) ≤ q) = (p ≤ (F* (G* q))));
322 apply (.= (or_prop1 :?));
325 change with ((F⎻ (G⎻ p) ≤ q) = (p ≤ (G⎻* (F⎻* q))));
326 apply (.= (or_prop2 :?));
328 | intros; change with ((G (F (p)) >< q) = (p >< (F⎻ (G⎻ q))));
329 apply (.= (or_prop3 :?));
332 | intros; split; simplify;
333 [3: unfold arrows1_of_ORelation_setoid; apply ((†e)‡(†e1));
334 |1: apply ((†e)‡(†e1));
335 |2,4: apply ((†e1)‡(†e));]]
338 definition OA : category2.
341 | intros; apply (ORelation_setoid o o1);
344 |5,6,7:intros; apply refl1;]
345 | apply ORelation_composition;
346 | intros (P Q R S F G H); split;
347 [ change with (H⎻* ∘ G⎻* ∘ F⎻* = H⎻* ∘ (G⎻* ∘ F⎻* ));
348 apply (comp_assoc2 ????? (F⎻* ) (G⎻* ) (H⎻* ));
349 | apply ((comp_assoc2 ????? (H⎻) (G⎻) (F⎻))^-1);
350 | apply ((comp_assoc2 ????? F G H)^-1);
351 | apply ((comp_assoc2 ????? H* G* F* ));]
352 | intros; split; unfold ORelation_composition; simplify; apply id_neutral_left2;
353 | intros; split; unfold ORelation_composition; simplify; apply id_neutral_right2;]
356 definition OAlgebra_of_objs2_OA: objs2 OA → OAlgebra ≝ λx.x.
357 coercion OAlgebra_of_objs2_OA.
359 definition ORelation_setoid_of_arrows2_OA:
360 ∀P,Q. arrows2 OA P Q → ORelation_setoid P Q ≝ λP,Q,c.c.
361 coercion ORelation_setoid_of_arrows2_OA.
363 prefer coercion Type_OF_objs2.
365 (* alias symbol "eq" = "setoid1 eq". *)
367 (* qui la notazione non va *)
369 nlemma leq_to_eq_join: ∀S:OAlgebra.∀p,q:S. p ≤ q → q = (binary_join ? p q).
371 apply oa_leq_antisym;
372 [ apply oa_density; intros;
373 apply oa_overlap_sym;
374 unfold binary_join; simplify;
375 apply (. (oa_join_split : ?));
376 exists; [ apply false ]
377 apply oa_overlap_sym;
379 | unfold binary_join; simplify;
380 apply (. (oa_join_sup : ?)); intro;
381 cases i; whd in ⊢ (? ? ? ? ? % ?);
382 [ assumption | apply oa_leq_refl ]]
385 nlemma overlap_monotone_left: ∀S:OAlgebra.∀p,q,r:S. p ≤ q → p >< r → q >< r.
386 #S; #p; #q; #r; #H1; #H2;
387 apply (. (leq_to_eq_join : ?)‡#);
390 | apply oa_overlap_sym;
391 unfold binary_join; simplify;
392 apply (. (oa_join_split : ?));
393 exists [ apply true ]
394 apply oa_overlap_sym;
398 (* Part of proposition 9.9 *)
399 nlemma f_minus_image_monotone: ∀S,T.∀R:ORelation S T.∀p,q. p ≤ q → R⎻ p ≤ R⎻ q.
400 #S; #T; #R; #p; #q; #H;
401 napply (. (or_prop2 …));
402 napply oa_leq_trans; ##[##2: napply H; ##| ##skip |
403 napply (. (or_prop2 … q …)^ -1);(*CSC: why q?*) napply oa_leq_refl]
406 (* Part of proposition 9.9 *)
407 nlemma f_minus_star_image_monotone: ∀S,T.∀R:ORelation S T.∀p,q. p ≤ q → R⎻* p ≤ R⎻* q.
408 #S; #T; #R; #p; #q; #H;
409 napply (. (or_prop2 … (R⎻* p) q)^ -1); (*CSC: why ?*)
410 napply oa_leq_trans; ##[##3: napply H; ##| ##skip | napply (. (or_prop2 …)); napply oa_leq_refl]
413 (* Part of proposition 9.9 *)
414 nlemma f_image_monotone: ∀S,T.∀R:ORelation S T.∀p,q. p ≤ q → R p ≤ R q.
415 #S; #T; #R; #p; #q; #H;
416 napply (. (or_prop1 …));
417 napply oa_leq_trans; ##[##2: napply H; ##| ##skip | napply (. (or_prop1 … q …)^ -1); napply oa_leq_refl]
420 (* Part of proposition 9.9 *)
421 nlemma f_star_image_monotone: ∀S,T.∀R:ORelation S T.∀p,q. p ≤ q → R* p ≤ R* q.
422 #S; #T; #R; #p; #q; #H;
423 napply (. (or_prop1 … (R* p) q)^ -1);
424 napply oa_leq_trans; ##[##3: napply H; ##| ##skip | napply (. (or_prop1 …)); napply oa_leq_refl]
427 nlemma lemma_10_2_a: ∀S,T.∀R:ORelation S T.∀p. p ≤ R⎻* (R⎻ p).
429 napply (. (or_prop2 … p …)^-1);
433 nlemma lemma_10_2_b: ∀S,T.∀R:ORelation S T.∀p. R⎻ (R⎻* p) ≤ p.
435 napply (. (or_prop2 …));
439 nlemma lemma_10_2_c: ∀S,T.∀R:ORelation S T.∀p. p ≤ R* (R p).
441 napply (. (or_prop1 … p …)^-1);
445 nlemma lemma_10_2_d: ∀S,T.∀R:ORelation S T.∀p. R (R* p) ≤ p.
447 napply (. (or_prop1 …));
451 nlemma lemma_10_3_a: ∀S,T.∀R:ORelation S T.∀p. R⎻ (R⎻* (R⎻ p)) = R⎻ p.
452 #S; #T; #R; #p; napply oa_leq_antisym
453 [ napply lemma_10_2_b
454 | napply f_minus_image_monotone;
455 napply lemma_10_2_a ]
458 nlemma lemma_10_3_b: ∀S,T.∀R:ORelation S T.∀p. R* (R (R* p)) = R* p.
459 #S; #T; #R; #p; napply oa_leq_antisym
460 [ napply f_star_image_monotone;
461 napply (lemma_10_2_d ?? R p)
462 | napply lemma_10_2_c ]
465 nlemma lemma_10_3_c: ∀S,T.∀R:ORelation S T.∀p. R (R* (R p)) = R p.
466 #S; #T; #R; #p; napply oa_leq_antisym
467 [ napply lemma_10_2_d
468 | napply f_image_monotone;
469 napply (lemma_10_2_c ?? R p) ]
472 nlemma lemma_10_3_d: ∀S,T.∀R:ORelation S T.∀p. R⎻* (R⎻ (R⎻* p)) = R⎻* p.
473 #S; #T; #R; #p; napply oa_leq_antisym
474 [ napply f_minus_star_image_monotone;
475 napply (lemma_10_2_b ?? R p)
476 | napply lemma_10_2_a ]
479 nlemma lemma_10_4_a: ∀S,T.∀R:ORelation S T.∀p. R⎻* (R⎻ (R⎻* (R⎻ p))) = R⎻* (R⎻ p).
480 #S; #T; #R; #p; napply (†(lemma_10_3_a …)).
483 nlemma lemma_10_4_b: ∀S,T.∀R:ORelation S T.∀p. R (R* (R (R* p))) = R (R* p).
484 #S; #T; #R; #p; napply (†(lemma_10_3_b …));
487 nlemma oa_overlap_sym': ∀o:OAlgebra.∀U,V:o. (U >< V) = (V >< U).
488 #o; #U; #V; @; #H; napply oa_overlap_sym; nassumption.