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

[helm.git] / helm / software / matita / nlibrary / logic / cprop.ma

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