Work in Progress: Who needs binary_morphisms? Curryfication is your friend.

But...

 1) the hints are uglier
 2) you really need to apply mk_binary_morphism to prove a curryfied binary
    morphism if you want to remain sane...

Note: with non uniform coercions everywhere we should be able to finally get
a beautiful script. Yet to be done.

diff --git a/helm/software/matita/nlibrary/logic/cprop.ma b/helm/software/matita/nlibrary/logic/cprop.ma
index 0302264c690a7575a63cce643fd9940933d23a12..47ccef5d008927f5278b1c2310e8056a574866b5 100644 (file)
--- a/helm/software/matita/nlibrary/logic/cprop.ma
+++ b/helm/software/matita/nlibrary/logic/cprop.ma
@@ -42,40 +42,50 @@ nqed.
 notation ". r" with precedence 50 for @{'fi $r}.
 interpretation "fi" 'fi r = (fi' ?? r).
 
-ndefinition and_morphism: binary_morphism1 CPROP CPROP CPROP.
- napply mk_binary_morphism1
-  [ napply And
-  | #a; #a'; #b; #b'; *; #H1; #H2; *; #H3; #H4; napply mk_iff; *; #K1; #K2; napply conj
-     [ napply (H1 K1)
-     | napply (H3 K2)
-     | napply (H2 K1)
-     | napply (H4 K2)]##]
+ndefinition and_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP).
+ napply (mk_binary_morphism1 … And);
+ #a; #a'; #b; #b'; #Ha; #Hb; @; *; #x; #y; @
+  [ napply (. Ha^-1) | napply (. Hb^-1) | napply (. Ha) | napply (. Hb)] //.
 nqed.
 
-unification hint 0 ≔ A,B ⊢ fun21 … (mk_binary_morphism1 … And (prop21 … and_morphism)) A B ≡ And A B.
-
-(*nlemma test: ∀A,A',B: CProp[0]. A=A' → (B ∨ A) = B → (B ∧ A) ∧ B.
- #A; #A'; #B; #H1; #H2;
- napply (. ((#‡H1)‡H2^-1)); nnormalize;
-nqed.*)
-
-ndefinition or_morphism: binary_morphism1 CPROP CPROP CPROP.
- napply mk_binary_morphism1
-  [ napply Or
-  | #a; #a'; #b; #b'; *; #H1; #H2; *; #H3; #H4; napply mk_iff; *; #H;
-     ##[##1,3: napply or_introl |##*: napply or_intror ]
-   ##[ napply (H1 H)
-     | napply (H2 H)
-     | napply (H3 H)
-     | napply (H4 H)]##]
+unification hint 0 ≔ A,B ⊢
+ mk_unary_morphism1 …
+  (λX.mk_unary_morphism1 … (And X) (prop11 … (and_morphism X)))
+  (prop11 … and_morphism)
+   A B ≡ And A B.
+
+(*
+naxiom daemon: False.
+
+nlemma test: ∀A,A',B: CProp[0]. A=A' → (B ∨ A) = B → (B ∧ A) ∧ B.
+ #A; #A'; #B; #H1; #H2; napply (. (#‡H1)‡H2^-1); nelim daemon.
+nqed.
+
+CSC: ugly proof term
+ncheck test.
+*)
+
+ndefinition or_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP).
+ napply (mk_binary_morphism1 … Or);
+ #a; #a'; #b; #b'; #Ha; #Hb; @; *; #x
+  [ @1; napply (. Ha^-1) | @2; napply (. Hb^-1) | @1; napply (. Ha) | @2; napply (. Hb)] //.
 nqed.
 
-unification hint 0 ≔ A,B ⊢ fun21 … (mk_binary_morphism1 … Or (prop21 … or_morphism)) A B ≡ Or A B.
+unification hint 0 ≔ A,B ⊢
+ mk_unary_morphism1 …
+  (λX.mk_unary_morphism1 … (Or X) (prop11 … (or_morphism X)))
+  (prop11 … or_morphism)
+  A B ≡ Or A B.
 
-ndefinition if_morphism: binary_morphism1 CPROP CPROP CPROP.
- napply mk_binary_morphism1
-  [ napply (λA,B. A → B)
-  | #a; #a'; #b; #b'; #H1; #H2; napply mk_iff; #H; #w
-     [ napply (if … H2); napply H; napply (fi … H1); nassumption
-     | napply (fi … H2); napply H; napply (if … H1); nassumption]##]
+ndefinition if_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP).
+ napply (mk_binary_morphism1 … (λA,B:CProp[0]. A → B));
+ #a; #a'; #b; #b'; #Ha; #Hb; @; #H; #x
+  [ napply (. Hb^-1); napply H; napply (. Ha) | napply (. Hb); napply H; napply (. Ha^-1)]
+ //.
 nqed.
+
+unification hint 0 ≔ A,B ⊢
+ mk_unary_morphism1 …
+  (λX:CProp[0].mk_unary_morphism1 … (λY:CProp[0]. X → Y) (prop11 … (if_morphism X)))
+  (prop11 … if_morphism)
+  A B ≡ A → B.
\ No newline at end of file

diff --git a/helm/software/matita/nlibrary/sets/setoids.ma b/helm/software/matita/nlibrary/sets/setoids.ma
index dac7b1375ac3f93fcafcfea033b5d39db1a69170..f9fcfd0202591711cb85951a89ba095b46a626bc 100644 (file)
--- a/helm/software/matita/nlibrary/sets/setoids.ma
+++ b/helm/software/matita/nlibrary/sets/setoids.ma
@@ -45,38 +45,34 @@ nrecord unary_morphism (A,B: setoid) : Type[0] ≝
    prop1: ∀a,a'. eq ? a a' → eq ? (fun1 a) (fun1 a')
  }.
 
-nrecord binary_morphism (A,B,C:setoid) : Type[0] ≝
- { fun2:2> A → B → C;
-   prop2: ∀a,a',b,b'. eq ? a a' → eq ? b b' → eq ? (fun2 a b) (fun2 a' b')
- }.
-
 notation "† c" with precedence 90 for @{'prop1 $c }.
 notation "l ‡ r" with precedence 90 for @{'prop2 $l $r }.
 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 …)); ##]
+##[ #f; #g; napply (∀x,x'. x=x' → f x = g x');
+##| #f; #x; #x'; #Hx; napply (.= †Hx); napply #;
+##| #f; #g; #H; #x; #x'; #Hx; napply ((H … Hx^-1)^-1);
+##| #f; #g; #h; #H1; #H2; #x; #x'; #Hx; 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)).
-*)
+
+interpretation "prop2" 'prop2 l r = (prop1 ? (unary_morph_setoid ??) ? ?? l ?? r).
+
+nlemma unary_morph_eq: ∀A,B.∀f,g: unary_morphism A B. (∀x. f x = g x) → f=g.
+/3/. nqed.
+
+nlemma mk_binary_morphism:
+ ∀A,B,C: setoid. ∀f: A → B → C. (∀a,a',b,b'. a=a' → b=b' → f a b = f a' b') →
+  unary_morphism A (unary_morph_setoid B C).
+ #A; #B; #C; #f; #H; @ [ #x; @ (f x) ] #a; #a'; #Ha [##2: napply unary_morph_eq; #y]
+ /2/.
+nqed.
 
 ndefinition composition ≝
  λo1,o2,o3:Type[0].λf:o2 → o3.λg: o1 → o2.λx.f (g x).
@@ -96,7 +92,8 @@ unification hint 0 ≔ o1,o2,o3:setoid,f:unary_morphism o2 o3,g:unary_morphism o
         (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)
@@ -106,3 +103,4 @@ ndefinition comp_binary_morphisms:
  | #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 49d259d5dd46ddb0d7efff2f0bf532794d8589df..fa615c8e4d74600903d6e1cdd845eb3524ad6f3f 100644 (file)
--- a/helm/software/matita/nlibrary/sets/setoids1.ma
+++ b/helm/software/matita/nlibrary/sets/setoids1.ma
@@ -56,21 +56,15 @@ nrecord unary_morphism1 (A,B: setoid1) : Type[1] ≝
    prop11: ∀a,a'. eq1 ? a a' → eq1 ? (fun11 a) (fun11 a')
  }.
 
-nrecord binary_morphism1 (A,B,C:setoid1) : Type[1] ≝
- { fun21:2> A → B → C;
-   prop21: ∀a,a',b,b'. eq1 ? a a' → eq1 ? b b' → eq1 ? (fun21 a b) (fun21 a' b')
- }.
-
 interpretation "prop11" 'prop1 c = (prop11 ????? c).
-interpretation "prop21" 'prop2 l r = (prop21 ???????? l r).
 interpretation "refl1" 'refl = (refl1 ???).
 
 ndefinition unary_morphism1_setoid1: setoid1 → setoid1 → setoid1.
  #s; #s1; @ (unary_morphism1 s s1); @
-     [ #f; #g; napply (∀a:s. f a = g a)
-     | #x; #a; napply refl1
-     | #x; #y; #H; #a; napply sym1; //
-     | #x; #y; #z; #H1; #H2; #a; napply trans1; ##[##2: napply H1 | ##skip | napply H2]##]
+     [ #f; #g; napply (∀a,a':s. a=a' → f a = g a')
+     | #x; #a; #a'; #Ha; napply (.= †Ha); napply refl1
+     | #x; #y; #H; #a; #a'; #Ha; napply (.= †Ha); napply sym1; /2/
+     | #x; #y; #z; #H1; #H2; #a; #a'; #Ha; napply (.= †Ha); napply trans1; ##[##2: napply H1 | ##skip | napply H2]//;##]
 nqed.
 
 unification hint 0 ≔ S, T ;
@@ -78,6 +72,18 @@ unification hint 0 ≔ S, T ;
 (* --------------------------------- *) ⊢
    carr1 R ≡ unary_morphism1 S T.
 
+interpretation "prop21" 'prop2 l r = (prop11 ? (unary_morphism1_setoid1 ??) ? ?? l ?? r).
+
+nlemma unary_morph1_eq1: ∀A,B.∀f,g: unary_morphism1 A B. (∀x. f x = g x) → f=g.
+/3/. nqed.
+
+nlemma mk_binary_morphism1:
+ ∀A,B,C: setoid1. ∀f: A → B → C. (∀a,a',b,b'. a=a' → b=b' → f a b = f a' b') →
+  unary_morphism1 A (unary_morphism1_setoid1 B C).
+ #A; #B; #C; #f; #H; @ [ #x; @ (f x) ] #a; #a'; #Ha [##2: napply unary_morph1_eq1; #y]
+ /2/.
+nqed.
+
 ndefinition composition1 ≝
  λo1,o2,o3:Type[1].λf:o2 → o3.λg: o1 → o2.λx.f (g x).
  
@@ -98,6 +104,7 @@ unification hint 0 ≔ o1,o2,o3:setoid1,f:unary_morphism1 o2 o3,g:unary_morphism
  (* -------------------------------------------------------------------- *) ⊢
                               fun11 ?? R ≡ (composition1 … f g).
                               
+(*
 ndefinition comp_binary_morphisms:
  ∀o1,o2,o3.
   binary_morphism1 (unary_morphism1_setoid1 o2 o3) (unary_morphism1_setoid1 o1 o2)
@@ -107,3 +114,4 @@ ndefinition comp_binary_morphisms:
  | #a; #a'; #b; #b'; #ea; #eb; #x; nnormalize;
    napply (.= †(eb x)); napply ea.
 nqed.
+*)

diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index 241282c1acde3865a377f1fea26436d4e0fa85ce..c66b51e2dbb6a98efa6bf7249e8817aaf6b529b0 100644 (file)
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -107,38 +107,40 @@ unification hint 0 ≔ A;
   (* ----------------------------------------------------- *) ⊢  
                  carr1 R ≡ ext_powerclass A.
 
+(*
 interpretation "prop21 mem" 'prop2 l r = (prop21 (setoid1_of_setoid ?) (ext_powerclass_setoid ?) ? ? ???? l r).
-      
+*)
+    
 (*
 ncoercion ext_carr' : ∀A.∀x:ext_powerclass_setoid A. Ω^A ≝ ext_carr 
 on _x : (carr1 (ext_powerclass_setoid ?)) to (Ω^?). 
 *)
 
 nlemma mem_ext_powerclass_setoid_is_morph: 
- ∀A. binary_morphism1 (setoid1_of_setoid A) (ext_powerclass_setoid A) CPROP.
- #A; @
-  [ napply (λx,S. x ∈ S)
-  | #a; #a'; #b; #b'; #Ha; *; #Hb1; #Hb2; @; #H;
-     ##[ napply Hb1; napply (. (ext_prop … Ha^-1)); nassumption;
-     ##| napply Hb2; napply (. (ext_prop … Ha)); nassumption;
-     ##]
-  ##]
+ ∀A. unary_morphism1 (setoid1_of_setoid A) (unary_morphism1_setoid1 (ext_powerclass_setoid A) CPROP).
+ #A; napply (mk_binary_morphism1 … (λx:setoid1_of_setoid A.λS: 𝛀^A. x ∈ S));
+ #a; #a'; #b; #b'; #Ha; *; #Hb1; #Hb2; @; #H
+  [ napply (. (ext_prop … Ha^-1)) | napply (. (ext_prop … Ha)) ] /2/.
 nqed.
 
 unification hint 0 ≔  A:setoid, x, S;  
      SS ≟ (ext_carr ? S),
-     TT ≟ (mk_binary_morphism1 ??? 
-             (λx:setoid1_of_setoid ?.λS:ext_powerclass_setoid ?. x ∈ S) 
-             (prop21 ??? (mem_ext_powerclass_setoid_is_morph A))),
+     TT ≟ (mk_unary_morphism1 … 
+             (λx:setoid1_of_setoid ?.
+               mk_unary_morphism1 …
+                 (λS:ext_powerclass_setoid ?. x ∈ S)
+                 (prop11 … (mem_ext_powerclass_setoid_is_morph A x)))
+             (prop11 … (mem_ext_powerclass_setoid_is_morph A))),
      XX ≟ (ext_powerclass_setoid A)
   (*-------------------------------------*) ⊢ 
-      fun21 (setoid1_of_setoid A) XX CPROP TT x S 
+      fun11 (setoid1_of_setoid A)
+       (unary_morphism1_setoid1 XX CPROP) TT x S 
     ≡ mem A SS x.
 
-nlemma subseteq_is_morph: ∀A. binary_morphism1 (ext_powerclass_setoid A) (ext_powerclass_setoid A) CPROP.
- #A; @
-  [ napply (λS,S'. S ⊆ S')
-  | #a; #a'; #b; #b'; *; #Ha1; #Ha2; *;/4/]
+nlemma subseteq_is_morph: ∀A. unary_morphism1 (ext_powerclass_setoid A)
+ (unary_morphism1_setoid1 (ext_powerclass_setoid A) CPROP).
+ #A; napply (mk_binary_morphism1 … (λS,S':𝛀^A. S ⊆ S'));
+ #a; #a'; #b; #b'; *; #H1; #H2; *; /4/.
 nqed.
 
 unification hint 0 ≔ A,a,a'
@@ -160,9 +162,9 @@ unification hint 0 ≔
   (* ------------------------------------------*)  ⊢ 
     ext_carr A R ≡ intersect ? (ext_carr ? B) (ext_carr ? C).
 
-nlemma intersect_is_morph: 
- ∀A. binary_morphism1 (powerclass_setoid A) (powerclass_setoid A) (powerclass_setoid A).
- #A; @ (λS,S'. S ∩ S');
+nlemma intersect_is_morph:
+ ∀A. unary_morphism1 (powerclass_setoid A) (unary_morphism1_setoid1 (powerclass_setoid A) (powerclass_setoid A)).
+ #A; napply (mk_binary_morphism1 … (λS,S'. S ∩ S'));
  #a; #a'; #b; #b'; *; #Ha1; #Ha2; *; #Hb1; #Hb2; @; #x; nnormalize; *;/3/.
 nqed.