From 742913ecf0e021372665974e4b4e3a203a3428ab Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 10 Sep 2009 10:37:10 +0000
Subject: [PATCH] more stuff fixed

---
 .../matita/nlibrary/hints_declaration.ma      | 16 +++++-----
 helm/software/matita/nlibrary/sets/sets.ma    | 31 +++++++++++--------
 2 files changed, 26 insertions(+), 21 deletions(-)

diff --git a/helm/software/matita/nlibrary/hints_declaration.ma b/helm/software/matita/nlibrary/hints_declaration.ma
index 29d17382b..5c189f63a 100644
--- a/helm/software/matita/nlibrary/hints_declaration.ma
+++ b/helm/software/matita/nlibrary/hints_declaration.ma
@@ -13,16 +13,16 @@
 (**************************************************************************)
 
 include "logic/pts.ma".
-ndefinition hint_declaration_Type0  ≝  λA:Type[0] .λa,b:A.a.
-ndefinition hint_declaration_Type1  ≝  λA:Type[1].λa,b:A.a.
-ndefinition hint_declaration_Type2  ≝  λa,b:Type[1].a.
-ndefinition hint_declaration_CProp0 ≝  λA:CProp[0].λa,b:A.a.
-ndefinition hint_declaration_CProp1 ≝  λA:CProp[1].λa,b:A.a.
-ndefinition hint_declaration_CProp2 ≝  λa,b:CProp[1].a.
+ndefinition hint_declaration_Type0  ≝  λA:Type[0] .λa,b:A.Prop.
+ndefinition hint_declaration_Type1  ≝  λA:Type[1].λa,b:A.Prop.
+ndefinition hint_declaration_Type2  ≝  λa,b:Type[1].Prop.
+ndefinition hint_declaration_CProp0 ≝  λA:CProp[0].λa,b:A.Prop.
+ndefinition hint_declaration_CProp1 ≝  λA:CProp[1].λa,b:A.Prop.
+ndefinition hint_declaration_CProp2 ≝  λa,b:CProp[1].Prop.
   
-notation > "≔ (list0 (ident x : T )sep ,) ⊢ term 19 Px ≡ term 19 Py"
+notation > "≔ (list0 (ident x : T ) sep ,) ⊢ term 19 Px ≡ term 19 Py"
   with precedence 90
-  for @{ ${ fold right @{'hint_decl $Px $Py} rec acc @{ ∀${ident x}:$T.$acc } } }.      
+  for @{ ${ fold right @{'hint_decl $Px $Py} rec acc @{ ∀${ident x}:$T.$acc } } }.
 
 interpretation "hint_decl_Type2"  'hint_decl a b = (hint_declaration_Type2 a b).
 interpretation "hint_decl_CProp2" 'hint_decl a b = (hint_declaration_CProp2 a b).
diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index 2f0725d85..348332441 100644
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -1,4 +1,3 @@
-
 (**************************************************************************)
 (*       ___                                                              *)
 (*      ||M||                                                             *)
@@ -65,7 +64,7 @@ include "sets/setoids1.ma".
 
 ndefinition powerclass_setoid: Type[0] → setoid1.
  #A; napply mk_setoid1
-  [ napply (Ω \sup A)
+  [ napply (Ω^A)
   | napply seteq ]
 nqed.
 
@@ -79,7 +78,9 @@ unification hint 0 ≔ A : ? ⊢ carr1 (powerclass_setoid A) ≡ Ω^A.
 include "logic/cprop.ma".
 
 nrecord qpowerclass (A: setoid) : Type[1] ≝
- { pc:> Ω^A;
+ { pc:> Ω^A; (* qui pc viene dichiarato con un target preciso... 
+                forse lo si vorrebbe dichiarato con un target più lasco 
+                ma la sintassi :> non lo supporta *)
    mem_ok': ∀x,x':A. x=x' → (x ∈ pc) = (x' ∈ pc) 
  }.
 
@@ -91,7 +92,7 @@ nqed.
 
 ndefinition qseteq: ∀A. equivalence_relation1 (qpowerclass A).
  #A; napply mk_equivalence_relation1
-  [ napply (λS,S':qpowerclass A. S = S')
+  [ napply (λS,S'. S = S')
   | #S; napply (refl1 ? (seteq A))
   | #S; #S'; napply (sym1 ? (seteq A))
   | #S; #T; #U; napply (trans1 ? (seteq A))]
@@ -107,7 +108,7 @@ unification hint 0 ≔ A : ? ⊢  carr1 (qpowerclass_setoid A) ≡ qpowerclass A
 
 nlemma mem_ok: ∀A. binary_morphism1 (setoid1_of_setoid A) (qpowerclass_setoid A) CPROP.
  #A; napply mk_binary_morphism1
-  [ #x; napply (λS: qpowerclass_setoid ?. x ∈ S) (* ERROR CSC: ??? *)
+  [ napply (λx,S. x ∈ S) 
   | #a; #a'; #b; #b'; #Ha; *; #Hb1; #Hb2; napply mk_iff; #H;
      ##[ napply Hb1; napply (. (mem_ok' …)); ##[##3: napply H| napply Ha^-1;##]
      ##| napply Hb2; napply (. (mem_ok' …)); ##[##3: napply H| napply Ha;##]
@@ -120,7 +121,7 @@ unification hint 0 ≔
   
 nlemma subseteq_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) CPROP.
  #A; napply mk_binary_morphism1
-  [ napply (λS,S': qpowerclass_setoid ?. S ⊆ S')
+  [ napply (λS,S'. S ⊆ S')
   | #a; #a'; #b; #b'; *; #Ha1; #Ha2; *; #Hb1; #Hb2; napply mk_iff; #H
      [ napply (subseteq_trans … a)
         [ nassumption | napply (subseteq_trans … b); nassumption ]
@@ -140,16 +141,20 @@ nlemma intersect_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_
       | napply (. ((#‡Ha)‡(#‡Hb))); nassumption ]##]
 nqed.
 
-(*
+(* unfold if intersect, exposing fun21 *)
+alias symbol "hint_decl" = "hint_decl_Type1".
 unification hint 0 ≔ 
-   A : setoid, U : qpowerclass_setoid A, V : ? ⊢ (intersect_ok A) U V ≡ U ∩ V.
-  *)
+  A : setoid, B : qpowerclass A, C : qpowerclass A ⊢ 
+    pc A (fun21 ???  (intersect_ok A) B C) ≡ intersect ? (pc ? B) (pc ? C).
+
+(* hints can pass under mem *)
+unification hint 0 ( 
+  ∀A,B,x.
+   let C ≝ B in 
+    (λa,b.Prop) (mem A B x) (mem A C x)).
 
 nlemma test: ∀A:setoid. ∀U,V:qpowerclass A. ∀x,x':setoid1_of_setoid A. x=x' → x ∈ U ∩ V → x' ∈ U ∩ V.
- #A; #U; #V; #x; #x'; #H; #p;
-  (* CSC: senza la change non funziona! *)
-  nchange with (x' ∈ (fun21 ??? (intersect_ok A) U V));
-  napply (. (H^-1‡#)); nassumption.
+ #A; #U; #V; #x; #x'; #H; #p; napply (. (H^-1‡#)); nassumption.
 nqed.
 
 (*
-- 
2.39.2