]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/nlibrary/overlap/o-algebra.ma
fork for Matita version B
[helm.git] / matitaB / matita / nlibrary / overlap / o-algebra.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "sets/categories2.ma".
16
17 (*
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 ?).
22
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}.
27
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).
32 *)
33
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] := {
38   oa_P :> setoid1;
39   oa_leq : unary_morphism1 oa_P (unary_morphism1_setoid1 oa_P CPROP); (*CSC: dovrebbe essere CProp bug refiner*)
40   oa_overlap: unary_morphism1 oa_P (unary_morphism1_setoid1 oa_P CPROP);
41   binary_meet: unary_morphism1 oa_P (unary_morphism1_setoid1 oa_P oa_P);
42 (*CSC:  oa_join: ∀I:setoid.unary_morphism1 (setoid1_of_setoid … I ⇒ oa_P) oa_P;*)
43   oa_one: oa_P;
44   oa_zero: 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);
53 (*CSC:  oa_join_split:
54       ∀I:SET.∀p.∀q:I ⇒ oa_P.
55        oa_overlap p (oa_join I q) = (∃i:I.oa_overlap p (q i));*)
56   (*oa_base : setoid;
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
61   *)
62   oa_density: 
63       ∀p,q.(∀r.oa_overlap p r → oa_overlap q r) → oa_leq p q
64 }.
65
66 interpretation "o-algebra leq" 'leq a b = (fun11 ?? (fun11 ?? (oa_leq ?) a) b).
67
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 = (fun11 ?? (fun11 ?? (oa_overlap ?) a) b).
71
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) }.
76
77 (*notation > "hovbox(∧ f)" non associative with precedence 60
78 for @{ 'oa_meet $f }.
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 ?)).
83 *)
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) }.
88
89 (*CSC
90 notation > "hovbox(∨ f)" non associative with precedence 60
91 for @{ 'oa_join $f }.
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 ?)).
96 *)
97 (*definition binary_meet : ∀O:OAlgebra. binary_morphism1 O O O.
98 intros; split;
99 [ intros (p q); 
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' });
104    | apply Hletin;]
105   intro x; simplify; cases x; simplify; assumption;]
106 qed.*)
107
108 interpretation "o-algebra binary meet" 'and a b = 
109   (fun11 ?? (fun11 ?? (binary_meet ?) a) b).
110
111 (*
112 prefer coercion Type1_OF_OAlgebra.
113
114 definition binary_join : ∀O:OAlgebra. binary_morphism1 O O O.
115 intros; split;
116 [ intros (p q); 
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' });
121    | apply Hletin;]
122   intro x; simplify; cases x; simplify; assumption;]
123 qed.
124
125 interpretation "o-algebra binary join" 'or a b = 
126   (fun21 ??? (binary_join ?) a b).
127 *)
128 (*
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;
135 qed.
136 *)
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 ]) }.
143
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)) }.
148
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 ?)).
153 *)
154 nrecord ORelation (P,Q : OAlgebra) : Type[1] ≝ {
155   or_f :> P ⇒ Q;
156   or_f_minus_star : P ⇒ Q;
157   or_f_star : Q ⇒ P;
158   or_f_minus : Q ⇒ P;
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)
162 }.
163  
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}.
166
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}.
169
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}.
172
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).
176
177
178 ndefinition ORelation_setoid : OAlgebra → OAlgebra → setoid1.
179 #P; #Q; @ (ORelation P Q); @
180  [ napply (λp,q.p = q)
181  | #x; napply refl1
182  | #x; #y; napply sym1
183  | #x; #y; #z; napply trans1 ]
184 nqed.
185
186 unification hint 0 ≔ P, Q ;
187   R ≟ (ORelation_setoid P Q)
188 (* -------------------------- *) ⊢
189     carr1 R ≡ ORelation P Q.
190
191 ndefinition or_f_morphism1: ∀P,Q:OAlgebra.unary_morphism1 (ORelation_setoid P Q)
192  (unary_morphism1_setoid1 P Q).
193  #P; #Q; @
194   [ napply or_f
195   | #a; #a'; #e; nassumption]
196 nqed.
197
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.
202
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'? *)
210  napply (. ?‡#)
211   [##2: napply (a r)
212   | napply (e^-1); //]
213  napply (. (or_prop3 …));
214  napply oa_overlap_sym;
215  nassumption.
216 nqed.
217
218 nlemma ORelation_eq2:
219  ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
220   r=r' → r⎻ = r'⎻.
221  #P; #Q; #a; #a'; #e; #x; #x'; #Hx; napply (.= †Hx);
222  napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_minus_
223   [ napply e | napply (e^-1)]
224 nqed.
225
226 ndefinition or_f_minus_morphism1: ∀P,Q:OAlgebra.unary_morphism1 (ORelation_setoid P Q)
227  (unary_morphism1_setoid1 Q P).
228  #P; #Q; @
229   [ napply or_f_minus
230   | napply ORelation_eq2]
231 nqed.
232
233 unification hint 0 ≔ P, Q, r;
234  R ≟ (mk_unary_morphism1 … (or_f_minus …) (prop11 … (or_f_minus_morphism1 …)))
235 (* ------------------------ *) ⊢
236   fun11 … R r ≡ or_f_minus P Q r.
237   
238 naxiom daemon : False.
239
240 nlemma ORelation_eq_respects_leq_or_f_star_:
241  ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
242   r=r' → ∀x. r* x ≤ r'* x.
243  #P; #Q; #a; #a'; #e; #x; (*CSC: una schifezza *)
244  ncases daemon.
245  (*
246  ngeneralize in match (. (or_prop1 P Q a' (a* x) x)^-1) in ⊢ %; #H; napply H;
247  nchange with (or_f P Q a' (a* x) ≤ x);
248  napply (. ?‡#)
249   [##2: napply (a (a* x))
250   | ngeneralize in match (a* x);
251     nchange with (or_f P Q a' = or_f P Q a);
252     napply (.= †e^-1); napply #]
253  napply (. (or_prop1 …));
254  napply oa_leq_refl.*)
255 nqed.
256
257 nlemma ORelation_eq3:
258  ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
259   r=r' → r* = r'*.
260  #P; #Q; #a; #a'; #e; #x; #x'; #Hx; napply (.= †Hx);
261  napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_star_
262   [ napply e | napply (e^-1)]
263 nqed.
264
265 ndefinition or_f_star_morphism1: ∀P,Q:OAlgebra.unary_morphism1 (ORelation_setoid P Q)
266  (unary_morphism1_setoid1 Q P).
267  #P; #Q; @
268   [ napply or_f_star
269   | napply ORelation_eq3] 
270 nqed.
271
272 unification hint 0 ≔ P, Q, r;
273  R ≟ (mk_unary_morphism1 … (or_f_star …) (prop11 … (or_f_star_morphism1 …)))
274 (* ------------------------ *) ⊢
275   fun11 … R r ≡ or_f_star P Q r.
276
277 nlemma ORelation_eq_respects_leq_or_f_minus_star_:
278  ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
279   r=r' → ∀x. r⎻* x ≤ r'⎻* x.
280  #P; #Q; #a; #a'; #e; #x; (*CSC: una schifezza *)
281  ncases daemon. (*
282  ngeneralize in match (. (or_prop2 P Q a' (a⎻* x) x)^-1) in ⊢ %; #H; napply H;
283  nchange with (or_f_minus P Q a' (a⎻* x) ≤ x);
284  napply (. ?‡#)
285   [##2: napply (a⎻ (a⎻* x))
286   | ngeneralize in match (a⎻* x);
287     nchange with (a'⎻ = a⎻);
288     napply (.= †e^-1); napply #]
289  napply (. (or_prop2 …));
290  napply oa_leq_refl.*)
291 nqed.
292
293 nlemma ORelation_eq4:
294  ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
295   r=r' → r⎻* = r'⎻*.
296  #P; #Q; #a; #a'; #e; #x; #x'; #Hx; napply (.= †Hx);
297  napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_minus_star_
298   [ napply e | napply (e^-1)]
299 nqed.
300
301 ndefinition or_f_minus_star_morphism1:
302  ∀P,Q:OAlgebra.unary_morphism1 (ORelation_setoid P Q) (unary_morphism1_setoid1 P Q).
303  #P; #Q; @
304   [ napply or_f_minus_star
305   | napply ORelation_eq4]
306 nqed.
307
308
309 unification hint 0 ≔ P, Q, r;
310  R ≟ (mk_unary_morphism1 … (or_f_minus_star …) (prop11 … (or_f_minus_star_morphism1 …)))
311 (* ------------------------ *) ⊢
312   fun11 … R r ≡ or_f_minus_star P Q r.
313   
314 (* qui la notazione non va *)
315 (*CSC
316 nlemma leq_to_eq_join: ∀S:OAlgebra.∀p,q:S. p ≤ q → q = (binary_join ? p q).
317  intros;
318  apply oa_leq_antisym;
319   [ apply oa_density; intros;
320     apply oa_overlap_sym;
321     unfold binary_join; simplify;
322     apply (. (oa_join_split : ?));
323     exists; [ apply false ]
324     apply oa_overlap_sym;
325     assumption
326   | unfold binary_join; simplify;
327     apply (. (oa_join_sup : ?)); intro;
328     cases i; whd in ⊢ (? ? ? ? ? % ?);
329      [ assumption | apply oa_leq_refl ]]
330 qed.
331
332 nlemma overlap_monotone_left: ∀S:OAlgebra.∀p,q,r:S. p ≤ q → p >< r → q >< r.
333  #S; #p; #q; #r; #H1; #H2;
334  apply (. (leq_to_eq_join : ?)‡#);
335   [ apply f;
336   | skip
337   | apply oa_overlap_sym;
338     unfold binary_join; simplify;
339     apply (. (oa_join_split : ?));
340     exists [ apply true ]
341     apply oa_overlap_sym;
342     assumption; ]
343 qed.*)
344
345 (* Part of proposition 9.9 *)
346 nlemma f_minus_image_monotone: ∀S,T.∀R:ORelation S T.∀p,q. p ≤ q → R⎻ p ≤ R⎻ q.
347  #S; #T; #R; #p; #q; #H;
348  napply (. (or_prop2 …));
349  napply oa_leq_trans; ##[##2: napply H; ##| ##skip |
350   napply (. (or_prop2 … q …)^ -1);(*CSC: why q?*) napply oa_leq_refl]
351 nqed.
352  
353 (* Part of proposition 9.9 *)
354 nlemma f_minus_star_image_monotone: ∀S,T.∀R:ORelation S T.∀p,q. p ≤ q → R⎻* p ≤ R⎻* q.
355  #S; #T; #R; #p; #q; #H;
356  napply (. (or_prop2 … (R⎻* p) q)^ -1); (*CSC: why ?*)
357  napply oa_leq_trans; ##[##3: napply H; ##| ##skip | napply (. (or_prop2 …)); napply oa_leq_refl]
358 nqed.
359
360 (* Part of proposition 9.9 *)
361 nlemma f_image_monotone: ∀S,T.∀R:ORelation S T.∀p,q. p ≤ q → R p ≤ R q.
362  #S; #T; #R; #p; #q; #H;
363  napply (. (or_prop1 …));
364  napply oa_leq_trans; ##[##2: napply H; ##| ##skip | napply (. (or_prop1 … q …)^ -1); napply oa_leq_refl]
365 nqed.
366
367 (* Part of proposition 9.9 *)
368 nlemma f_star_image_monotone: ∀S,T.∀R:ORelation S T.∀p,q. p ≤ q → R* p ≤ R* q.
369  #S; #T; #R; #p; #q; #H;
370  napply (. (or_prop1 … (R* p) q)^ -1);
371  napply oa_leq_trans; ##[##3: napply H; ##| ##skip | napply (. (or_prop1 …)); napply oa_leq_refl]
372 nqed.
373
374 nlemma lemma_10_2_a: ∀S,T.∀R:ORelation S T.∀p. p ≤ R⎻* (R⎻ p).
375  #S; #T; #R; #p;
376  napply (. (or_prop2 … p …)^-1);
377  napply oa_leq_refl.
378 nqed.
379
380 nlemma lemma_10_2_b: ∀S,T.∀R:ORelation S T.∀p. R⎻ (R⎻* p) ≤ p.
381  #S; #T; #R; #p;
382  napply (. (or_prop2 …));
383  napply oa_leq_refl.
384 nqed.
385
386 nlemma lemma_10_2_c: ∀S,T.∀R:ORelation S T.∀p. p ≤ R* (R p).
387  #S; #T; #R; #p;
388  napply (. (or_prop1 … p …)^-1);
389  napply oa_leq_refl.
390 nqed.
391
392 nlemma lemma_10_2_d: ∀S,T.∀R:ORelation S T.∀p. R (R* p) ≤ p.
393  #S; #T; #R; #p;
394  napply (. (or_prop1 …));
395  napply oa_leq_refl.
396 nqed.
397
398 nlemma lemma_10_3_a: ∀S,T.∀R:ORelation S T.∀p. R⎻ (R⎻* (R⎻ p)) = R⎻ p.
399  #S; #T; #R; #p; napply oa_leq_antisym
400   [ napply lemma_10_2_b
401   | napply f_minus_image_monotone;
402     napply lemma_10_2_a ]
403 nqed.
404
405 nlemma lemma_10_3_b: ∀S,T.∀R:ORelation S T.∀p. R* (R (R* p)) = R* p.
406  #S; #T; #R; #p; napply oa_leq_antisym
407   [ napply f_star_image_monotone;
408     napply (lemma_10_2_d ?? R p)
409   | napply lemma_10_2_c ]
410 nqed.
411
412 nlemma lemma_10_3_c: ∀S,T.∀R:ORelation S T.∀p. R (R* (R p)) = R p.
413  #S; #T; #R; #p; napply oa_leq_antisym
414   [ napply lemma_10_2_d
415   | napply f_image_monotone;
416     napply (lemma_10_2_c ?? R p) ]
417 nqed.
418
419 nlemma lemma_10_3_d: ∀S,T.∀R:ORelation S T.∀p. R⎻* (R⎻ (R⎻* p)) = R⎻* p.
420  #S; #T; #R; #p; napply oa_leq_antisym
421   [ napply f_minus_star_image_monotone;
422     napply (lemma_10_2_b ?? R p)
423   | napply lemma_10_2_a ]
424 nqed.
425
426 nlemma lemma_10_4_a: ∀S,T.∀R:ORelation S T.∀p. R⎻* (R⎻ (R⎻* (R⎻ p))) = R⎻* (R⎻ p).
427  #S; #T; #R; #p; napply (†(lemma_10_3_a …)).
428 nqed.
429
430 nlemma lemma_10_4_b: ∀S,T.∀R:ORelation S T.∀p. R (R* (R (R* p))) = R (R* p).
431  #S; #T; #R; #p; napply (†(lemma_10_3_b …));
432 nqed.
433
434 nlemma oa_overlap_sym': ∀o:OAlgebra.∀U,V:o. (U >< V) = (V >< U).
435  #o; #U; #V; @; #H; napply oa_overlap_sym; nassumption.
436 nqed.
437
438 (******************* CATEGORIES **********************)
439
440 ninductive one : Type[0] ≝ unit : one.
441
442 ndefinition force : ∀S:Type[2]. S → ∀T:Type[2]. T → one → Type[2] ≝   
443  λS,s,T,t,lock. match lock with [ unit => S ].
444
445 ndefinition enrich_as : 
446  ∀S:Type[2].∀s:S.∀T:Type[2].∀t:T.∀lock:one.force S s T t lock ≝ 
447  λS,s,T,t,lock. match lock return λlock.match lock with [ unit ⇒ S ] 
448                     with [ unit ⇒ s ].
449
450 ncoercion enrich_as : ∀S:Type[2].∀s:S.∀T:Type[2].∀t:T.∀lock:one. force S s T t lock
451  ≝ enrich_as on t: ? to force ? ? ? ? ?.
452
453 (* does not work here 
454 nlemma foo : ∀A,B,C:setoid1.∀f:B ⇒ C.∀g:A ⇒ B. unary_morphism1 A C.
455 #A; #B; #C; #f; #g; napply(f \circ g).
456 nqed.*)
457
458 (* This precise hint does not leave spurious metavariables *)
459 unification hint 0 ≔ A,B,C : setoid1, f:B ⇒ C, g: A ⇒ B;
460    lock ≟ unit
461 (* --------------------------------------------------------------- *) ⊢
462   (unary_morphism1 A C)
463  ≡
464   (force (unary_morphism1 A C) (comp1_unary_morphisms A B C f g)
465    (carr1 A → carr1 C) (composition1 A B C f g)  lock)
466   .
467
468 (* This uniform hint opens spurious metavariables
469 unification hint 0 ≔ A,B,C : setoid1, f:B ⇒ C, g: A ⇒ B, X;
470    lock ≟ unit
471 (* --------------------------------------------------------------- *) ⊢
472   (unary_morphism1 A C)
473  ≡
474   (force (unary_morphism1 A C) X (carr1 A → carr1 C) (fun11 … X)  lock)
475   .
476 *)
477
478 nlemma foo : ∀A,B,C:setoid1.∀f:B ⇒ C.∀g:A ⇒ B. unary_morphism1 A C.
479 #A; #B; #C; #f; #g; napply(f ∘ g).
480 nqed.
481
482 (*
483
484 ndefinition uffa: ∀A,B. ∀U: unary_morphism1 A B. (A → B) → CProp[0].
485  #A;#B;#_;#_; napply True.
486 nqed.
487 ndefinition mk_uffa: ∀A,B.∀U: unary_morphism1 A B. ∀f: (A → B). uffa A B U f.
488  #A; #B; #U; #f; napply I.
489 nqed.
490
491 ndefinition coerc_to_unary_morphism1:
492  ∀A,B. ∀U: unary_morphism1 A B. uffa A B U (fun11 … U) → unary_morphism1 A B.
493  #A; #B; #U; #_; nassumption.
494 nqed.
495
496 ncheck (λA,B,C,f,g.coerc_to_unary_morphism1 ??? (mk_uffa ??? (composition1 A B C f g))). 
497 *)
498 ndefinition ORelation_composition : ∀P,Q,R. 
499   unary_morphism1 (ORelation_setoid P Q)
500    (unary_morphism1_setoid1 (ORelation_setoid Q R) (ORelation_setoid P R)).
501 #P; #Q; #R; napply mk_binary_morphism1
502 [ #F; #G; @
503   [ napply (G ∘ F) (* napply (comp1_unary_morphisms … G F) (*CSC: was (G ∘ F);*) *)
504   | napply (G⎻* ∘ F⎻* ) (* napply (comp1_unary_morphisms … G⎻* F⎻* ) (*CSC: was (G⎻* ∘ F⎻* );*)*)
505   | napply (comp1_unary_morphisms … F* G* ) (*CSC: was (F* ∘ G* );*)
506   | napply (comp1_unary_morphisms … F⎻ G⎻) (*CSC: was (F⎻ ∘ G⎻);*)
507   | #p; #q; nnormalize;
508     napply (.= (or_prop1 … G …)); (*CSC: it used to understand without G *)
509     napply (or_prop1 …)
510   | #p; #q; nnormalize;
511     napply (.= (or_prop2 … F …));
512     napply or_prop2
513   | #p; #q; nnormalize;
514     napply (.= (or_prop3 … G …));
515     napply or_prop3
516   ]
517 ##| nnormalize; /3/]
518 nqed.
519
520 (*
521 ndefinition OA : category2.
522 split;
523 [ apply (OAlgebra);
524 | intros; apply (ORelation_setoid o o1);
525 | intro O; split;
526   [1,2,3,4: apply id2;
527   |5,6,7:intros; apply refl1;] 
528 | apply ORelation_composition;
529 | intros (P Q R S F G H); split;
530    [ change with (H⎻* ∘ G⎻* ∘ F⎻* = H⎻* ∘ (G⎻* ∘ F⎻* ));
531      apply (comp_assoc2 ????? (F⎻* ) (G⎻* ) (H⎻* ));
532    | apply ((comp_assoc2 ????? (H⎻) (G⎻) (F⎻))^-1);
533    | apply ((comp_assoc2 ????? F G H)^-1);
534    | apply ((comp_assoc2 ????? H* G* F* ));]
535 | intros; split; unfold ORelation_composition; simplify; apply id_neutral_left2;
536 | intros; split; unfold ORelation_composition; simplify; apply id_neutral_right2;]
537 qed.
538
539 definition OAlgebra_of_objs2_OA: objs2 OA → OAlgebra ≝ λx.x.
540 coercion OAlgebra_of_objs2_OA.
541
542 definition ORelation_setoid_of_arrows2_OA: 
543   ∀P,Q. arrows2 OA P Q → ORelation_setoid P Q ≝ λP,Q,c.c.
544 coercion ORelation_setoid_of_arrows2_OA.
545
546 prefer coercion Type_OF_objs2.
547 *)
548 (* alias symbol "eq" = "setoid1 eq". *)