X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Flogic%2Fcprop.ma;h=47ccef5d008927f5278b1c2310e8056a574866b5;hb=1439ced76cb62f9c5f5e638c53a005c3843870ae;hp=d857ba6a72942fabd1898feff2934a0b832c1e72;hpb=68cadaa38277ea16ce97b3ed24884420c19eac20;p=helm.git

diff --git a/helm/software/matita/nlibrary/logic/cprop.ma b/helm/software/matita/nlibrary/logic/cprop.ma
index d857ba6a7..47ccef5d0 100644
--- a/helm/software/matita/nlibrary/logic/cprop.ma
+++ b/helm/software/matita/nlibrary/logic/cprop.ma
@@ -42,51 +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 … and_morphism A B ≡ And A B.*)
-unification hint 0 ≔ A,B ⊢ fun21 … (mk_binary_morphism1 … And (prop21 … and_morphism)) A B ≡ And A B.
+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.
 
-(*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.*)
+(*
+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.
 
-(*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.*)
-
-(*interpretation "and_morphism" 'and a b = (fun21 ??? and_morphism a b).*)
+CSC: ugly proof term
+ncheck test.
+*)
 
-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)]##]
+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 … or_morphism A B ≡ Or A B.
-
-(*interpretation "or_morphism" 'or a b = (fun21 ??? or_morphism 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: 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.
 
-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]##]
-nqed.
\ No newline at end of file
+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