1) stuff moved from categories.ma to setoids*.ma

[helm.git] / helm / software / matita / nlibrary / overlap / o-algebra.ma

diff --git a/helm/software/matita/nlibrary/overlap/o-algebra.ma b/helm/software/matita/nlibrary/overlap/o-algebra.ma
index eae842c44e150cf71d2a1dc8399da1e8f93f734d..227ef04517d4d65f92121d066d3240606928e7d6 100644 (file)
--- a/helm/software/matita/nlibrary/overlap/o-algebra.ma
+++ b/helm/software/matita/nlibrary/overlap/o-algebra.ma
@@ -308,34 +308,29 @@ unification hint 0 ≔ P, Q, r;
 (* ------------------------ *) ⊢
   fun11 … R r ≡ or_f_minus_star P Q r.
 
-(*CSC:
 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 (comp1_unary_morphisms … G F) (*CSC: was (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 +425,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