Experiment...

diff --git a/helm/software/matita/nlibrary/logic/cprop.ma b/helm/software/matita/nlibrary/logic/cprop.ma
index d857ba6a72942fabd1898feff2934a0b832c1e72..0302264c690a7575a63cce643fd9940933d23a12 100644 (file)
--- a/helm/software/matita/nlibrary/logic/cprop.ma
+++ b/helm/software/matita/nlibrary/logic/cprop.ma
@@ -52,7 +52,6 @@ ndefinition and_morphism: binary_morphism1 CPROP CPROP CPROP.
      | napply (H4 K2)]##]
 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.
 
 (*nlemma test: ∀A,A',B: CProp[0]. A=A' → (B ∨ A) = B → (B ∧ A) ∧ B.
@@ -60,14 +59,6 @@ unification hint 0 ≔ A,B ⊢ fun21 … (mk_binary_morphism1 … And (prop21 
  napply (. ((#‡H1)‡H2^-1)); nnormalize;
 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).*)
-
 ndefinition or_morphism: binary_morphism1 CPROP CPROP CPROP.
  napply mk_binary_morphism1
   [ napply Or
@@ -79,9 +70,7 @@ ndefinition or_morphism: binary_morphism1 CPROP CPROP CPROP.
      | napply (H4 H)]##]
 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 ⊢ fun21 … (mk_binary_morphism1 … Or (prop21 … or_morphism)) A B ≡ Or A B.
 
 ndefinition if_morphism: binary_morphism1 CPROP CPROP CPROP.
  napply mk_binary_morphism1
@@ -89,4 +78,4 @@ ndefinition if_morphism: binary_morphism1 CPROP CPROP CPROP.
   | #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
+nqed.

diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma
index 61173c78e34215c0081b4d0a3a29f49bbd0db564..93f9cd6b5d3e014121adf9ff04042816848cb5a6 100644 (file)
--- a/helm/software/matita/nlibrary/sets/partitions.ma
+++ b/helm/software/matita/nlibrary/sets/partitions.ma
@@ -24,6 +24,7 @@ alias symbol "eq" = "setoid1 eq".
 alias symbol "eq" = "setoid eq".
 alias symbol "eq" = "setoid eq".
 alias symbol "eq" = "setoid1 eq".
+alias symbol "eq" = "setoid eq".
 nrecord partition (A: setoid) : Type[1] ≝ 
  { support: setoid;
    indexes: qpowerclass support;
@@ -146,25 +147,25 @@ nlemma partition_splits_card:
      | #a; #a'; #H; nrewrite < H; napply refl ]
 ##| #x; #Hx; nwhd; napply I
 ##| #y; #_;
-    ngeneralize in match (covers ? P) in ⊢ ?; *; #_; #Hc;
-    ngeneralize in match (Hc y I) in ⊢ ?; *; #index; *; #Hi1; #Hi2;
-    ngeneralize in match (f_sur ???? f ? Hi1) in ⊢ ?; *; #nindex; *; #Hni1; #Hni2;
-    ngeneralize in match (f_sur ???? (fi nindex) y ?) in ⊢ ?
-     [##2: alias symbol "refl" = "refl".
+    nlapply (covers ? P); *; #_; #Hc;
+    nlapply (Hc y I); *; #index; *; #Hi1; #Hi2;
+    nlapply (f_sur ???? f ? Hi1); *; #nindex; *; #Hni1; #Hni2;
+    nlapply (f_sur ???? (fi nindex) y ?)
+     [ alias symbol "refl" = "refl".
 alias symbol "prop1" = "prop11".
 napply (. #‡(†?));##[##2: napply Hni2 |##1: ##skip | nassumption]##]
     *; #nindex2; *; #Hni21; #Hni22;
     nletin xxx ≝ (plus (big_plus (minus n nindex) (λi.λ_.s (S (plus i nindex)))) nindex2);
-    napply (ex_intro … xxx); napply conj
+    @ xxx; @
      [ napply iso_nat_nat_union_pre [ napply le_S_S_to_le; nassumption | nassumption ]
    ##| nwhd in ⊢ (???%%); napply (.= ?) [##3: nassumption|##skip]
-       ngeneralize in match (iso_nat_nat_union_char n s xxx ?) in ⊢ ?
-        [##2: napply iso_nat_nat_union_pre [ napply le_S_S_to_le; nassumption | nassumption]##]
+       nlapply (iso_nat_nat_union_char n s xxx ?)
+        [napply iso_nat_nat_union_pre [ napply le_S_S_to_le; nassumption | nassumption]##]
        *; *; #K1; #K2; #K3;
-       ngeneralize in match
+       nlapply
         (iso_nat_nat_union_uniq n s nindex (fst … (iso_nat_nat_union s xxx n))
-          nindex2 (snd … (iso_nat_nat_union s xxx n)) ?????) in ⊢ ?
-        [ *; #E1; #E2; nrewrite > E1; nrewrite > E2; napply refl
+          nindex2 (snd … (iso_nat_nat_union s xxx n)) ?????)
+        [##2: *; #E1; #E2; nrewrite > E1; nrewrite > E2; napply refl
         | napply le_S_S_to_le; nassumption
         |##*: nassumption]##]
 ##| #x; #x'; nnormalize in ⊢ (? → ? → %); #Hx; #Hx'; #E;

diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index 4e7418fd93bcc17f4777d3bb30a293d674bc43c3..c4fc89f210b0c90f5a049d80442f0cf6b7222e11 100644 (file)
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -71,7 +71,7 @@ nqed.
 include "hints_declaration.ma". 
 
 alias symbol "hint_decl" = "hint_decl_Type2".
-unification hint 0 ≔ A ⊢ carr1 (powerclass_setoid A) ≡ Ω^A.
+unification hint 0 ≔ A ⊢ carr1 (mk_setoid1 (Ω^A) (eq1 (powerclass_setoid A))) ≡ Ω^A.
 
 (************ SETS OVER SETOIDS ********************)
 
@@ -106,6 +106,10 @@ nqed.
 unification hint 0 ≔ A ⊢  
   carr1 (qpowerclass_setoid A) ≡ qpowerclass A.
 
+(*CSC: non va!  
+unification hint 0 ≔ A ⊢  
+  carr1 (mk_setoid1 (qpowerclass A) (eq1 (qpowerclass_setoid A))) ≡ qpowerclass A.*)
+
 nlemma mem_ok: ∀A. binary_morphism1 (setoid1_of_setoid A) (qpowerclass_setoid A) CPROP.
  #A; @
   [ napply (λx,S. x ∈ S) 
@@ -116,10 +120,15 @@ nlemma mem_ok: ∀A. binary_morphism1 (setoid1_of_setoid A) (qpowerclass_setoid
   ##]
 nqed.
 
+(*CSC: bug qui se metto x o S al posto di ?
+nlemma foo: True.
+nletin xxx ≝ (λA:setoid.λx,S. let SS ≝ pc ? S in
+    fun21 ??? (mk_binary_morphism1 ??? (λx.λS. ? ∈ ?) (prop21 ??? (mem_ok A))) x S);
+*)
 unification hint 0 ≔  A:setoid, x, S;  
          SS ≟ (pc ? S)
   (*-------------------------------------*) ⊢ 
-    fun21 ??? (mem_ok A) x S ≡ mem A SS x.
+    fun21 ??? (mk_binary_morphism1 ??? (λx,S. x ∈ S) (prop21 ??? (mem_ok A))) x S ≡ mem A SS x.
 
 nlemma subseteq_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) CPROP.
  #A; @