X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Foverlap%2Fo-algebra.ma;h=40b2f72bb5dab9c2d53b979059e9b88bf0b7c063;hb=d1c9cdb2de96aa2dda6a7b25a4c4959b82b08f6c;hp=bf320c1e1f58051d41b61b8123338de371318e5c;hpb=cb731a63dfd801c15047e0d18b644794ac63fe03;p=helm.git

diff --git a/helm/software/matita/nlibrary/overlap/o-algebra.ma b/helm/software/matita/nlibrary/overlap/o-algebra.ma
index bf320c1e1..40b2f72bb 100644
--- a/helm/software/matita/nlibrary/overlap/o-algebra.ma
+++ b/helm/software/matita/nlibrary/overlap/o-algebra.ma
@@ -36,9 +36,9 @@ interpretation "unary morphism1 comprehension with proof" 'comprehension_by s \e
 (* USARE L'ESISTENZIALE DEBOLE *)
 nrecord OAlgebra : Type[2] := {
   oa_P :> setoid1;
-  oa_leq : binary_morphism1 oa_P oa_P CPROP; (*CSC: dovrebbe essere CProp bug refiner*)
-  oa_overlap: binary_morphism1 oa_P oa_P CPROP;
-  binary_meet: binary_morphism1 oa_P oa_P oa_P;
+  oa_leq : unary_morphism1 oa_P (unary_morphism1_setoid1 oa_P CPROP); (*CSC: dovrebbe essere CProp bug refiner*)
+  oa_overlap: unary_morphism1 oa_P (unary_morphism1_setoid1 oa_P CPROP);
+  binary_meet: unary_morphism1 oa_P (unary_morphism1_setoid1 oa_P oa_P);
 (*CSC:  oa_join: ∀I:setoid.unary_morphism1 (setoid1_of_setoid … I ⇒ oa_P) oa_P;*)
   oa_one: oa_P;
   oa_zero: oa_P;
@@ -63,11 +63,11 @@ nrecord OAlgebra : Type[2] := {
       ∀p,q.(∀r.oa_overlap p r → oa_overlap q r) → oa_leq p q
 }.
 
-interpretation "o-algebra leq" 'leq a b = (fun21 ??? (oa_leq ?) a b).
+interpretation "o-algebra leq" 'leq a b = (fun11 ?? (fun11 ?? (oa_leq ?) a) b).
 
 notation "hovbox(a mpadded width -150% (>)< b)" non associative with precedence 45
 for @{ 'overlap $a $b}.
-interpretation "o-algebra overlap" 'overlap a b = (fun21 ??? (oa_overlap ?) a b).
+interpretation "o-algebra overlap" 'overlap a b = (fun11 ?? (fun11 ?? (oa_overlap ?) a) b).
 
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (\emsp) \nbsp term 90 p)" 
 non associative with precedence 50 for @{ 'oa_meet $p }.
@@ -106,7 +106,7 @@ intros; split;
 qed.*)
 
 interpretation "o-algebra binary meet" 'and a b = 
-  (fun21 ??? (binary_meet ?) a b).
+  (fun11 ?? (fun11 ?? (binary_meet ?) a) b).
 
 (*
 prefer coercion Type1_OF_OAlgebra.
@@ -209,10 +209,7 @@ nlemma ORelation_eq_respects_leq_or_f_minus_:
  napply (. (or_prop3 … a' …)^-1); (*CSC: why a'? *)
  napply (. ?‡#)
   [##2: napply (a r)
-  | ngeneralize in match r in ⊢ %;
-    nchange with (or_f … a' = or_f … a);
-    napply (.= †e^-1);
-    napply #]
+  | napply (e^-1); //]
  napply (. (or_prop3 …));
  napply oa_overlap_sym;
  nassumption.
@@ -221,9 +218,9 @@ nqed.
 nlemma ORelation_eq2:
  ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
   r=r' → r⎻ = r'⎻.
- #P; #Q; #a; #a'; #e; #x;
+ #P; #Q; #a; #a'; #e; #x; #x'; #Hx; napply (.= †Hx);
  napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_minus_
-  [ napply e | napply e^-1]
+  [ napply e | napply (e^-1)]
 nqed.
 
 ndefinition or_f_minus_morphism1: ∀P,Q:OAlgebra.unary_morphism1 (ORelation_setoid P Q)
@@ -260,9 +257,9 @@ nqed.
 nlemma ORelation_eq3:
  ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
   r=r' → r* = r'*.
- #P; #Q; #a; #a'; #e; #x;
+ #P; #Q; #a; #a'; #e; #x; #x'; #Hx; napply (.= †Hx);
  napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_star_
-  [ napply e | napply e^-1]
+  [ napply e | napply (e^-1)]
 nqed.
 
 ndefinition or_f_star_morphism1: ∀P,Q:OAlgebra.unary_morphism1 (ORelation_setoid P Q)
@@ -296,9 +293,9 @@ nqed.
 nlemma ORelation_eq4:
  ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
   r=r' → r⎻* = r'⎻*.
- #P; #Q; #a; #a'; #e; #x;
+ #P; #Q; #a; #a'; #e; #x; #x'; #Hx; napply (.= †Hx);
  napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_minus_star_
-  [ napply e | napply e^-1]
+  [ napply e | napply (e^-1)]
 nqed.
 
 ndefinition or_f_minus_star_morphism1:
@@ -314,115 +311,6 @@ unification hint 0 ≔ P, Q, r;
 (* ------------------------ *) ⊢
   fun11 … R r ≡ or_f_minus_star P Q r.
   
-ninductive one : Type[0] ≝ unit : one.
-
-ndefinition force : ∀S:Type[2]. S → ∀T:Type[2]. T → one → Type[2] ≝   
- λS,s,T,t,lock. match lock with [ unit => S ].
-
-ndefinition enrich_as : 
- ∀S:Type[2].∀s:S.∀T:Type[2].∀t:T.∀lock:one.force S s T t lock ≝ 
- λS,s,T,t,lock. match lock return λlock.match lock with [ unit ⇒ S ] 
-                    with [ unit ⇒ s ].
-
-ncoercion enrich_as : ∀S:Type[2].∀s:S.∀T:Type[2].∀t:T.∀lock:one. force S s T t lock
- ≝ enrich_as on t: ? to force ? ? ? ? ?.
-
-(* does not work here 
-nlemma foo : ∀A,B,C:setoid1.∀f:B ⇒ C.∀g:A ⇒ B. unary_morphism1 A C.
-#A; #B; #C; #f; #g; napply(f \circ g).
-nqed.*)
-
-(* This precise hint does not leave spurious metavariables *)
-unification hint 0 ≔ A,B,C : setoid1, f:B ⇒ C, g: A ⇒ B;
-   lock ≟ unit
-(* --------------------------------------------------------------- *) ⊢
-  (unary_morphism1 A C)
- ≡
-  (force (unary_morphism1 A C) (comp1_unary_morphisms A B C f g)
-   (carr1 A → carr1 C) (composition1 A B C f g)  lock)
-  .
-
-(* This uniform hint opens spurious metavariables
-unification hint 0 ≔ A,B,C : setoid1, f:B ⇒ C, g: A ⇒ B, X;
-   lock ≟ unit
-(* --------------------------------------------------------------- *) ⊢
-  (unary_morphism1 A C)
- ≡
-  (force (unary_morphism1 A C) X (carr1 A → carr1 C) (fun11 … X)  lock)
-  .
-*)
-
-nlemma foo : ∀A,B,C:setoid1.∀f:B ⇒ C.∀g:A ⇒ B. unary_morphism1 A C.
-#A; #B; #C; #f; #g; napply(f ∘ g).
-nqed.
-
-(*
-
-ndefinition uffa: ∀A,B. ∀U: unary_morphism1 A B. (A → B) → CProp[0].
- #A;#B;#_;#_; napply True.
-nqed.
-ndefinition mk_uffa: ∀A,B.∀U: unary_morphism1 A B. ∀f: (A → B). uffa A B U f.
- #A; #B; #U; #f; napply I.
-nqed.
-
-ndefinition coerc_to_unary_morphism1:
- ∀A,B. ∀U: unary_morphism1 A B. uffa A B U (fun11 … U) → unary_morphism1 A B.
- #A; #B; #U; #_; nassumption.
-nqed.
-
-ncheck (λA,B,C,f,g.coerc_to_unary_morphism1 ??? (mk_uffa ??? (composition1 A B C f g))). 
-*)
-ndefinition ORelation_composition : ∀P,Q,R. 
-  binary_morphism1 (ORelation_setoid P Q) (ORelation_setoid Q R) (ORelation_setoid P R).
-#P; #Q; #R; @
-[ #F; #G; @
-  [ napply (G ∘ F) (* napply (comp1_unary_morphisms … G F) (*CSC: was (G ∘ F);*) *)
-  | napply (G⎻* ∘ F⎻* ) (* napply (comp1_unary_morphisms … G⎻* F⎻* ) (*CSC: was (G⎻* ∘ F⎻* );*)*)
-  | napply (comp1_unary_morphisms … F* G* ) (*CSC: was (F* ∘ G* );*)
-  | napply (comp1_unary_morphisms … F⎻ G⎻) (*CSC: was (F⎻ ∘ G⎻);*)
-  | #p; #q; nnormalize;
-    napply (.= (or_prop1 … G …)); (*CSC: it used to understand without G *)
-    napply (or_prop1 …)
-  | #p; #q; nnormalize;
-    napply (.= (or_prop2 … F …));
-    napply or_prop2
-  | #p; #q; nnormalize;
-    napply (.= (or_prop3 … G …));
-    napply or_prop3
-  ]
-##| #a;#a';#b;#b';#e;#e1;#x;nnormalize;napply (.= †(e x));napply e1]
-nqed.
-
-(*
-ndefinition OA : category2.
-split;
-[ apply (OAlgebra);
-| intros; apply (ORelation_setoid o o1);
-| intro O; split;
-  [1,2,3,4: apply id2;
-  |5,6,7:intros; apply refl1;] 
-| apply ORelation_composition;
-| intros (P Q R S F G H); split;
-   [ change with (H⎻* ∘ G⎻* ∘ F⎻* = H⎻* ∘ (G⎻* ∘ F⎻* ));
-     apply (comp_assoc2 ????? (F⎻* ) (G⎻* ) (H⎻* ));
-   | apply ((comp_assoc2 ????? (H⎻) (G⎻) (F⎻))^-1);
-   | apply ((comp_assoc2 ????? F G H)^-1);
-   | apply ((comp_assoc2 ????? H* G* F* ));]
-| intros; split; unfold ORelation_composition; simplify; apply id_neutral_left2;
-| intros; split; unfold ORelation_composition; simplify; apply id_neutral_right2;]
-qed.
-
-definition OAlgebra_of_objs2_OA: objs2 OA → OAlgebra ≝ λx.x.
-coercion OAlgebra_of_objs2_OA.
-
-definition ORelation_setoid_of_arrows2_OA: 
-  ∀P,Q. arrows2 OA P Q → ORelation_setoid P Q ≝ λP,Q,c.c.
-coercion ORelation_setoid_of_arrows2_OA.
-
-prefer coercion Type_OF_objs2.
-*)
-(* alias symbol "eq" = "setoid1 eq". *)
-
 (* qui la notazione non va *)
 (*CSC
 nlemma leq_to_eq_join: ∀S:OAlgebra.∀p,q:S. p ≤ q → q = (binary_join ? p q).
@@ -545,4 +433,116 @@ nqed.
 
 nlemma oa_overlap_sym': ∀o:OAlgebra.∀U,V:o. (U >< V) = (V >< U).
  #o; #U; #V; @; #H; napply oa_overlap_sym; nassumption.
-nqed.
\ No newline at end of file
+nqed.
+
+(******************* CATEGORIES **********************)
+
+ninductive one : Type[0] ≝ unit : one.
+
+ndefinition force : ∀S:Type[2]. S → ∀T:Type[2]. T → one → Type[2] ≝   
+ λS,s,T,t,lock. match lock with [ unit => S ].
+
+ndefinition enrich_as : 
+ ∀S:Type[2].∀s:S.∀T:Type[2].∀t:T.∀lock:one.force S s T t lock ≝ 
+ λS,s,T,t,lock. match lock return λlock.match lock with [ unit ⇒ S ] 
+                    with [ unit ⇒ s ].
+
+ncoercion enrich_as : ∀S:Type[2].∀s:S.∀T:Type[2].∀t:T.∀lock:one. force S s T t lock
+ ≝ enrich_as on t: ? to force ? ? ? ? ?.
+
+(* does not work here 
+nlemma foo : ∀A,B,C:setoid1.∀f:B ⇒ C.∀g:A ⇒ B. unary_morphism1 A C.
+#A; #B; #C; #f; #g; napply(f \circ g).
+nqed.*)
+
+(* This precise hint does not leave spurious metavariables *)
+unification hint 0 ≔ A,B,C : setoid1, f:B ⇒ C, g: A ⇒ B;
+   lock ≟ unit
+(* --------------------------------------------------------------- *) ⊢
+  (unary_morphism1 A C)
+ ≡
+  (force (unary_morphism1 A C) (comp1_unary_morphisms A B C f g)
+   (carr1 A → carr1 C) (composition1 A B C f g)  lock)
+  .
+
+(* This uniform hint opens spurious metavariables
+unification hint 0 ≔ A,B,C : setoid1, f:B ⇒ C, g: A ⇒ B, X;
+   lock ≟ unit
+(* --------------------------------------------------------------- *) ⊢
+  (unary_morphism1 A C)
+ ≡
+  (force (unary_morphism1 A C) X (carr1 A → carr1 C) (fun11 … X)  lock)
+  .
+*)
+
+nlemma foo : ∀A,B,C:setoid1.∀f:B ⇒ C.∀g:A ⇒ B. unary_morphism1 A C.
+#A; #B; #C; #f; #g; napply(f ∘ g).
+nqed.
+
+(*
+
+ndefinition uffa: ∀A,B. ∀U: unary_morphism1 A B. (A → B) → CProp[0].
+ #A;#B;#_;#_; napply True.
+nqed.
+ndefinition mk_uffa: ∀A,B.∀U: unary_morphism1 A B. ∀f: (A → B). uffa A B U f.
+ #A; #B; #U; #f; napply I.
+nqed.
+
+ndefinition coerc_to_unary_morphism1:
+ ∀A,B. ∀U: unary_morphism1 A B. uffa A B U (fun11 … U) → unary_morphism1 A B.
+ #A; #B; #U; #_; nassumption.
+nqed.
+
+ncheck (λA,B,C,f,g.coerc_to_unary_morphism1 ??? (mk_uffa ??? (composition1 A B C f g))). 
+*)
+ndefinition ORelation_composition : ∀P,Q,R. 
+  unary_morphism1 (ORelation_setoid P Q)
+   (unary_morphism1_setoid1 (ORelation_setoid Q R) (ORelation_setoid P R)).
+#P; #Q; #R; napply mk_binary_morphism1
+[ #F; #G; @
+  [ napply (G ∘ F) (* napply (comp1_unary_morphisms … G F) (*CSC: was (G ∘ F);*) *)
+  | napply (G⎻* ∘ F⎻* ) (* napply (comp1_unary_morphisms … G⎻* F⎻* ) (*CSC: was (G⎻* ∘ F⎻* );*)*)
+  | napply (comp1_unary_morphisms … F* G* ) (*CSC: was (F* ∘ G* );*)
+  | napply (comp1_unary_morphisms … F⎻ G⎻) (*CSC: was (F⎻ ∘ G⎻);*)
+  | #p; #q; nnormalize;
+    napply (.= (or_prop1 … G …)); (*CSC: it used to understand without G *)
+    napply (or_prop1 …)
+  | #p; #q; nnormalize;
+    napply (.= (or_prop2 … F …));
+    napply or_prop2
+  | #p; #q; nnormalize;
+    napply (.= (or_prop3 … G …));
+    napply or_prop3
+  ]
+##| nnormalize; /3/]
+nqed.
+
+(*
+ndefinition OA : category2.
+split;
+[ apply (OAlgebra);
+| intros; apply (ORelation_setoid o o1);
+| intro O; split;
+  [1,2,3,4: apply id2;
+  |5,6,7:intros; apply refl1;] 
+| apply ORelation_composition;
+| intros (P Q R S F G H); split;
+   [ change with (H⎻* ∘ G⎻* ∘ F⎻* = H⎻* ∘ (G⎻* ∘ F⎻* ));
+     apply (comp_assoc2 ????? (F⎻* ) (G⎻* ) (H⎻* ));
+   | apply ((comp_assoc2 ????? (H⎻) (G⎻) (F⎻))^-1);
+   | apply ((comp_assoc2 ????? F G H)^-1);
+   | apply ((comp_assoc2 ????? H* G* F* ));]
+| intros; split; unfold ORelation_composition; simplify; apply id_neutral_left2;
+| intros; split; unfold ORelation_composition; simplify; apply id_neutral_right2;]
+qed.
+
+definition OAlgebra_of_objs2_OA: objs2 OA → OAlgebra ≝ λx.x.
+coercion OAlgebra_of_objs2_OA.
+
+definition ORelation_setoid_of_arrows2_OA: 
+  ∀P,Q. arrows2 OA P Q → ORelation_setoid P Q ≝ λP,Q,c.c.
+coercion ORelation_setoid_of_arrows2_OA.
+
+prefer coercion Type_OF_objs2.
+*)
+(* alias symbol "eq" = "setoid1 eq". *)