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

diff --git a/helm/software/matita/nlibrary/overlap/o-algebra.ma b/helm/software/matita/nlibrary/overlap/o-algebra.ma
index eae842c44..bf320c1e1 100644
--- a/helm/software/matita/nlibrary/overlap/o-algebra.ma
+++ b/helm/software/matita/nlibrary/overlap/o-algebra.ma
@@ -237,11 +237,15 @@ unification hint 0 ≔ P, Q, r;
  R ≟ (mk_unary_morphism1 … (or_f_minus …) (prop11 … (or_f_minus_morphism1 …)))
 (* ------------------------ *) ⊢
   fun11 … R r ≡ or_f_minus P Q r.
+  
+naxiom daemon : False.
 
 nlemma ORelation_eq_respects_leq_or_f_star_:
  ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
   r=r' → ∀x. r* x ≤ r'* x.
  #P; #Q; #a; #a'; #e; #x; (*CSC: una schifezza *)
+ ncases daemon.
+ (*
  ngeneralize in match (. (or_prop1 P Q a' (a* x) x)^-1) in ⊢ %; #H; napply H;
  nchange with (or_f P Q a' (a* x) ≤ x);
  napply (. ?‡#)
@@ -250,7 +254,7 @@ nlemma ORelation_eq_respects_leq_or_f_star_:
     nchange with (or_f P Q a' = or_f P Q a);
     napply (.= †e^-1); napply #]
  napply (. (or_prop1 …));
- napply oa_leq_refl.
+ napply oa_leq_refl.*)
 nqed.
 
 nlemma ORelation_eq3:
@@ -277,6 +281,7 @@ nlemma ORelation_eq_respects_leq_or_f_minus_star_:
  ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
   r=r' → ∀x. r⎻* x ≤ r'⎻* x.
  #P; #Q; #a; #a'; #e; #x; (*CSC: una schifezza *)
+ ncases daemon. (*
  ngeneralize in match (. (or_prop2 P Q a' (a⎻* x) x)^-1) in ⊢ %; #H; napply H;
  nchange with (or_f_minus P Q a' (a⎻* x) ≤ x);
  napply (. ?‡#)
@@ -285,7 +290,7 @@ nlemma ORelation_eq_respects_leq_or_f_minus_star_:
     nchange with (a'⎻ = a⎻);
     napply (.= †e^-1); napply #]
  napply (. (or_prop2 …));
- napply oa_leq_refl.
+ napply oa_leq_refl.*)
 nqed.
 
 nlemma ORelation_eq4:
@@ -303,39 +308,93 @@ ndefinition or_f_minus_star_morphism1:
   | napply ORelation_eq4]
 nqed.
 
+
 unification hint 0 ≔ P, Q, r;
  R ≟ (mk_unary_morphism1 … (or_f_minus_star …) (prop11 … (or_f_minus_star_morphism1 …)))
 (* ------------------------ *) ⊢
   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.
 
-(*CSC:
+(*
+
+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);
-  | apply rule (G⎻* ∘ F⎻* );
-  | apply (F* ∘ G* );
-  | apply (F⎻ ∘ G⎻);
-  | intros; 
-    change with ((G (F p) ≤ q) = (p ≤ (F* (G* q))));
-    apply (.= (or_prop1 :?));
-    apply (or_prop1 :?);
-  | intros;
-    change with ((F⎻ (G⎻ p) ≤ q) = (p ≤ (G⎻* (F⎻* q))));
-    apply (.= (or_prop2 :?));
-    apply or_prop2 ; 
-  | intros; change with ((G (F (p)) >< q) = (p >< (F⎻ (G⎻ q))));
-    apply (.= (or_prop3 :?));
-    apply or_prop3;
+  [ 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
   ]
-| intros; split; simplify; 
-   [3: unfold arrows1_of_ORelation_setoid; apply ((†e)‡(†e1));
-   |1: apply ((†e)‡(†e1));
-   |2,4: apply ((†e1)‡(†e));]]
-qed.
+##| #a;#a';#b;#b';#e;#e1;#x;nnormalize;napply (.= †(e x));napply e1]
+nqed.
 
-definition OA : category2.
+(*
+ndefinition OA : category2.
 split;
 [ apply (OAlgebra);
 | intros; apply (ORelation_setoid o o1);
@@ -430,60 +489,60 @@ nlemma lemma_10_2_a: ∀S,T.∀R:ORelation S T.∀p. p ≤ R⎻* (R⎻ p).
  napply oa_leq_refl.
 nqed.
 
-lemma lemma_10_2_b: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻ (R⎻* p) ≤ p.
- intros;
- apply (. (or_prop2 : ?));
- apply oa_leq_refl.
-qed.
+nlemma lemma_10_2_b: ∀S,T.∀R:ORelation S T.∀p. R⎻ (R⎻* p) ≤ p.
+ #S; #T; #R; #p;
+ napply (. (or_prop2 …));
+ napply oa_leq_refl.
+nqed.
 
-lemma lemma_10_2_c: ∀S,T.∀R:arrows2 OA S T.∀p. p ≤ R* (R p).
- intros;
- apply (. (or_prop1 : ?)^-1);
- apply oa_leq_refl.
-qed.
+nlemma lemma_10_2_c: ∀S,T.∀R:ORelation S T.∀p. p ≤ R* (R p).
+ #S; #T; #R; #p;
+ napply (. (or_prop1 … p …)^-1);
+ napply oa_leq_refl.
+nqed.
 
-lemma lemma_10_2_d: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* p) ≤ p.
- intros;
- apply (. (or_prop1 : ?));
- apply oa_leq_refl.
-qed.
+nlemma lemma_10_2_d: ∀S,T.∀R:ORelation S T.∀p. R (R* p) ≤ p.
+ #S; #T; #R; #p;
+ napply (. (or_prop1 …));
+ napply oa_leq_refl.
+nqed.
 
-lemma lemma_10_3_a: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻ (R⎻* (R⎻ p)) = R⎻ p.
- intros; apply oa_leq_antisym;
-  [ apply lemma_10_2_b;
-  | apply f_minus_image_monotone;
-    apply lemma_10_2_a; ]
-qed.
+nlemma lemma_10_3_a: ∀S,T.∀R:ORelation S T.∀p. R⎻ (R⎻* (R⎻ p)) = R⎻ p.
+ #S; #T; #R; #p; napply oa_leq_antisym
+  [ napply lemma_10_2_b
+  | napply f_minus_image_monotone;
+    napply lemma_10_2_a ]
+nqed.
 
-lemma lemma_10_3_b: ∀S,T.∀R:arrows2 OA S T.∀p. R* (R (R* p)) = R* p.
- intros; apply oa_leq_antisym;
-  [ apply f_star_image_monotone;
-    apply (lemma_10_2_d ?? R p);
-  | apply lemma_10_2_c; ]
-qed.
+nlemma lemma_10_3_b: ∀S,T.∀R:ORelation S T.∀p. R* (R (R* p)) = R* p.
+ #S; #T; #R; #p; napply oa_leq_antisym
+  [ napply f_star_image_monotone;
+    napply (lemma_10_2_d ?? R p)
+  | napply lemma_10_2_c ]
+nqed.
 
-lemma lemma_10_3_c: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* (R p)) = R p.
- intros; apply oa_leq_antisym;
-  [ apply lemma_10_2_d;
-  | apply f_image_monotone;
-    apply (lemma_10_2_c ?? R p); ]
-qed.
+nlemma lemma_10_3_c: ∀S,T.∀R:ORelation S T.∀p. R (R* (R p)) = R p.
+ #S; #T; #R; #p; napply oa_leq_antisym
+  [ napply lemma_10_2_d
+  | napply f_image_monotone;
+    napply (lemma_10_2_c ?? R p) ]
+nqed.
 
-lemma lemma_10_3_d: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻* (R⎻ (R⎻* p)) = R⎻* p.
- intros; apply oa_leq_antisym;
-  [ apply f_minus_star_image_monotone;
-    apply (lemma_10_2_b ?? R p);
-  | apply lemma_10_2_a; ]
-qed.
+nlemma lemma_10_3_d: ∀S,T.∀R:ORelation S T.∀p. R⎻* (R⎻ (R⎻* p)) = R⎻* p.
+ #S; #T; #R; #p; napply oa_leq_antisym
+  [ napply f_minus_star_image_monotone;
+    napply (lemma_10_2_b ?? R p)
+  | napply lemma_10_2_a ]
+nqed.
 
-lemma lemma_10_4_a: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻* (R⎻ (R⎻* (R⎻ p))) = R⎻* (R⎻ p).
- intros; apply (†(lemma_10_3_a ?? R p));
-qed.
+nlemma lemma_10_4_a: ∀S,T.∀R:ORelation S T.∀p. R⎻* (R⎻ (R⎻* (R⎻ p))) = R⎻* (R⎻ p).
+ #S; #T; #R; #p; napply (†(lemma_10_3_a …)).
+nqed.
 
-lemma lemma_10_4_b: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* (R (R* p))) = R (R* p).
-intros; unfold in ⊢ (? ? ? % %); apply (†(lemma_10_3_b ?? R p));
-qed.
+nlemma lemma_10_4_b: ∀S,T.∀R:ORelation S T.∀p. R (R* (R (R* p))) = R (R* p).
+ #S; #T; #R; #p; napply (†(lemma_10_3_b …));
+nqed.
 
-lemma oa_overlap_sym': ∀o:OA.∀U,V:o. (U >< V) = (V >< U).
- intros; split; intro; apply oa_overlap_sym; assumption.
-qed.
\ No newline at end of file
+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