From a580ff5c627c4148cdd3649ead20f4fac0f78be8 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 2 Jan 2010 19:40:58 +0000
Subject: [PATCH] 1) stuff moved from categories.ma to setoids*.ma 2) we are
 now ready to define the category of o-algebras

---
 .../matita/nlibrary/overlap/o-algebra.ma      | 39 +++++++-------
 .../matita/nlibrary/sets/categories.ma        | 31 +++--------
 helm/software/matita/nlibrary/sets/setoids.ma | 51 +++++++++++++++++++
 .../software/matita/nlibrary/sets/setoids1.ma | 32 +++++++++++-
 4 files changed, 105 insertions(+), 48 deletions(-)

diff --git a/helm/software/matita/nlibrary/overlap/o-algebra.ma b/helm/software/matita/nlibrary/overlap/o-algebra.ma
index ce922a38a..227ef0451 100644
--- 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);
diff --git a/helm/software/matita/nlibrary/sets/categories.ma b/helm/software/matita/nlibrary/sets/categories.ma
index 80f3b4cf6..310aa709e 100644
--- a/helm/software/matita/nlibrary/sets/categories.ma
+++ b/helm/software/matita/nlibrary/sets/categories.ma
@@ -1,31 +1,15 @@
 
 include "sets/sets.ma".
 
-ndefinition binary_morph_setoid : setoid → setoid → setoid → setoid.
-#S1; #S2; #T; @ (binary_morphism S1 S2 T); @;
-##[ #f; #g; napply (∀x,y. f x y = g x y);
-##| #f; #x; #y; napply #;
-##| #f; #g; #H; #x; #y; napply ((H x y)^-1);
-##| #f; #g; #h; #H1; #H2; #x; #y; napply (trans … (H1 …) (H2 …)); ##]
-nqed.
-
-ndefinition unary_morph_setoid : setoid → setoid → setoid.
-#S1; #S2; @ (unary_morphism S1 S2); @;
-##[ #f; #g; napply (∀x. f x = g x);
-##| #f; #x; napply #;
-##| #f; #g; #H; #x; napply ((H x)^-1);
-##| #f; #g; #h; #H1; #H2; #x; napply (trans … (H1 …) (H2 …)); ##]
-nqed.
-
 nrecord category : Type[2] ≝
  { objs:> Type[1];
    arrows: objs → objs → setoid;
    id: ∀o:objs. arrows o o;
-   comp: ∀o1,o2,o3. binary_morphism (arrows o1 o2) (arrows o2 o3) (arrows o1 o3);
-   comp_assoc: ∀o1,o2,o3,o4. ∀a12,a23,a34.
-    comp o1 o3 o4 (comp o1 o2 o3 a12 a23) a34 = comp o1 o2 o4 a12 (comp o2 o3 o4 a23 a34);
-   id_neutral_left: ∀o1,o2. ∀a: arrows o1 o2. comp ??? (id o1) a = a;
-   id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o2) = a
+   comp: ∀o1,o2,o3. binary_morphism (arrows o2 o3) (arrows o1 o2) (arrows o1 o3);
+   comp_assoc: ∀o1,o2,o3,o4. ∀a34,a23,a12.
+    comp o1 o3 o4 a34 (comp o1 o2 o3 a23 a12) = comp o1 o2 o4 (comp o2 o3 o4 a34 a23) a12;
+   id_neutral_left: ∀o1,o2. ∀a: arrows o1 o2. comp ??? (id o2) a = a;
+   id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o1) = a
  }.
 
 notation "hvbox(A break ⇒ B)" right associative with precedence 50 for @{ 'arrows $A $B }.
@@ -42,10 +26,7 @@ ndefinition SETOID : category.
 ##[ napply setoid;
 ##| napply unary_morph_setoid;
 ##| #o; @ (λx.x); #a; #b; #H; napply H;
-##| #o1; #o2; #o3; @; 
-    ##[ #f; #g; @(λx.g (f x)); #a; #b; #H; napply (.= (††H)); napply #;
-    ##| #f; #g; #f'; #g'; #H1; #H2; nwhd; #x; napply (.= (H2 (f x)));
-        napply (.= (†(H1 x))); napply #; ##]
+##| napply comp_binary_morphisms; (*CSC: why not ∘?*)
 ##| #o1; #o2; #o3; #o4; #f; #g; #h; nwhd; #x; napply #;
 ##|##6,7: #o1; #o2; #f; nwhd; #x; napply #; ##]
 nqed.
diff --git a/helm/software/matita/nlibrary/sets/setoids.ma b/helm/software/matita/nlibrary/sets/setoids.ma
index 28761806f..dac7b1375 100644
--- a/helm/software/matita/nlibrary/sets/setoids.ma
+++ b/helm/software/matita/nlibrary/sets/setoids.ma
@@ -14,6 +14,7 @@
 
 include "logic/connectives.ma".
 include "properties/relations.ma".
+include "hints_declaration.ma".
 
 (*
 notation "hvbox(a break = \sub \ID b)" non associative with precedence 45
@@ -55,3 +56,53 @@ notation "#" with precedence 90 for @{'refl}.
 interpretation "prop1" 'prop1 c  = (prop1 ????? c).
 interpretation "prop2" 'prop2 l r = (prop2 ???????? l r).
 interpretation "refl" 'refl = (refl ???).
+
+ndefinition binary_morph_setoid : setoid → setoid → setoid → setoid.
+#S1; #S2; #T; @ (binary_morphism S1 S2 T); @;
+##[ #f; #g; napply (∀x,y. f x y = g x y);
+##| #f; #x; #y; napply #;
+##| #f; #g; #H; #x; #y; napply ((H x y)^-1);
+##| #f; #g; #h; #H1; #H2; #x; #y; napply (trans … (H1 …) (H2 …)); ##]
+nqed.
+
+ndefinition unary_morph_setoid : setoid → setoid → setoid.
+#S1; #S2; @ (unary_morphism S1 S2); @;
+##[ #f; #g; napply (∀x. f x = g x);
+##| #f; #x; napply #;
+##| #f; #g; #H; #x; napply ((H x)^-1);
+##| #f; #g; #h; #H1; #H2; #x; napply (trans … (H1 …) (H2 …)); ##]
+nqed.
+
+(*
+unification hint 0
+ (∀o1,o2. (λx,y:Type[0].True) (carr (unary_morph_setoid o1 o2)) (unary_morphism o1 o2)).
+*)
+
+ndefinition composition ≝
+ λo1,o2,o3:Type[0].λf:o2 → o3.λg: o1 → o2.λx.f (g x).
+ 
+interpretation "function composition" 'compose f g = (composition ??? f g).
+
+ndefinition comp_unary_morphisms:
+ ∀o1,o2,o3:setoid.
+  unary_morphism o2 o3 → unary_morphism o1 o2 →
+   unary_morphism o1 o3.
+#o1; #o2; #o3; #f; #g; @ (f ∘ g);
+ #a; #a'; #e; nnormalize; napply (.= †(†e)); napply #.
+nqed.
+
+unification hint 0 ≔ o1,o2,o3:setoid,f:unary_morphism o2 o3,g:unary_morphism o1 o2;
+   R ≟ (mk_unary_morphism ?? (composition … f g)
+        (prop1 ?? (comp_unary_morphisms o1 o2 o3 f g)))
+ (* -------------------------------------------------------------------- *) ⊢
+                              fun1 ?? R ≡ (composition … f g).
+                              
+ndefinition comp_binary_morphisms:
+ ∀o1,o2,o3.
+  binary_morphism (unary_morph_setoid o2 o3) (unary_morph_setoid o1 o2)
+   (unary_morph_setoid o1 o3).
+#o1; #o2; #o3; @
+ [ #f; #g; napply (comp_unary_morphisms … f g) (*CSC: why not ∘?*)
+ | #a; #a'; #b; #b'; #ea; #eb; #x; nnormalize;
+   napply (.= †(eb x)); napply ea.
+nqed.
diff --git a/helm/software/matita/nlibrary/sets/setoids1.ma b/helm/software/matita/nlibrary/sets/setoids1.ma
index 6d6b68743..115d1f643 100644
--- a/helm/software/matita/nlibrary/sets/setoids1.ma
+++ b/helm/software/matita/nlibrary/sets/setoids1.ma
@@ -76,4 +76,34 @@ nqed.
 unification hint 0 ≔ S, T ;
  R ≟ (unary_morphism1_setoid1 S T)
 (* --------------------------------- *) ⊢
-   carr1 R ≡ unary_morphism1 S T.
\ No newline at end of file
+   carr1 R ≡ unary_morphism1 S T.
+
+ndefinition composition1 ≝
+ λo1,o2,o3:Type[1].λf:o2 → o3.λg: o1 → o2.λx.f (g x).
+ 
+interpretation "function composition" 'compose f g = (composition ??? f g).
+interpretation "function composition1" 'compose f g = (composition1 ??? f g).
+
+ndefinition comp1_unary_morphisms:
+ ∀o1,o2,o3:setoid1.
+  unary_morphism1 o2 o3 → unary_morphism1 o1 o2 →
+   unary_morphism1 o1 o3.
+#o1; #o2; #o3; #f; #g; @ (f ∘ g);
+ #a; #a'; #e; nnormalize; napply (.= †(†e)); napply #.
+nqed.
+
+unification hint 0 ≔ o1,o2,o3:setoid1,f:unary_morphism1 o2 o3,g:unary_morphism1 o1 o2;
+   R ≟ (mk_unary_morphism1 ?? (composition1 … f g)
+        (prop11 ?? (comp1_unary_morphisms o1 o2 o3 f g)))
+ (* -------------------------------------------------------------------- *) ⊢
+                              fun11 ?? R ≡ (composition1 … f g).
+                              
+ndefinition comp_binary_morphisms:
+ ∀o1,o2,o3.
+  binary_morphism1 (unary_morphism1_setoid1 o2 o3) (unary_morphism1_setoid1 o1 o2)
+   (unary_morphism1_setoid1 o1 o3).
+#o1; #o2; #o3; @
+ [ #f; #g; napply (comp1_unary_morphisms … f g) (*CSC: why not ∘?*)
+ | #a; #a'; #b; #b'; #ea; #eb; #x; nnormalize;
+   napply (.= †(eb x)); napply ea.
+nqed.
-- 
2.39.2