From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 4 Aug 2009 21:22:30 +0000 (+0000)
Subject: More Gonthierism. Are they the right solution?
X-Git-Tag: make_still_working~3571
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3807c5d0fa5abceccbc67f40edb9939b353ead0e;p=helm.git

More Gonthierism. Are they the right solution?
---

diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma
index d4a650c5e..103d17557 100644
--- a/helm/software/matita/nlibrary/algebra/magmas.ma
+++ b/helm/software/matita/nlibrary/algebra/magmas.ma
@@ -63,12 +63,12 @@ ndefinition mm_counter_image:
            nrewrite < Hy1;
            napply (mmprop … f)]##]
 nqed.
+*)
 
 ndefinition m_intersect: ∀A. magma A → magma A → magma A.
  #A; #M1; #M2;
  napply (mk_magma …)
-  [ napply (M1 ∩ M2)
+  [ napply (intersects_ok ? M1 M2)
   | #x; #y; nwhd in ⊢ (% → % → %); *; #Hx1; #Hx2; *; #Hy1; #Hy2;
     napply conj; napply op_closed; nassumption ]
-nqed.
-*)
\ No newline at end of file
+nqed.
\ No newline at end of file
diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index 20065cec4..f4b924dcc 100644
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -14,7 +14,7 @@
 
 include "logic/cprop.ma".
 
-nrecord powerset (A: setoid) : Type[1] ≝ { mem_op: unary_morphism1 A CPROP }.
+nrecord powerset (A: setoid) : Type[1] ≝ { mem_op:> unary_morphism1 A CPROP }.
 
 interpretation "powerset" 'powerset A = (powerset A).
 
@@ -67,13 +67,30 @@ ndefinition overlaps ≝ λA.λU,V:Ω \sup A.∃x:A.x ∈ U ∧ x ∈ V.
 
 interpretation "overlaps" 'overlaps U V = (overlaps ? U V).
 
-ndefinition intersects ≝ λA.λU,V:Ω \sup A. {x | x ∈ U ∧ x ∈ V }.
- #a; #a'; #H; napply mk_iff; *; #H1; #H2
-  [ napply (. ((H^-1‡#)‡(H^-1‡#))); nwhd; napply conj; nassumption
-  | napply (. ((H‡#)‡(H‡#))); nwhd; napply conj; nassumption]
+ndefinition intersects ≝ λA:Type[0].λU,V:A → CProp[0]. λx. U x ∧ V x.
+
+interpretation "intersects" 'intersects U V = (intersects ? U V).
+
+(* dovrebbe essere un binario? *)
+ndefinition intersects_ok: ∀A. Ω \sup A → Ω \sup A → Ω \sup A.
+ #A; #U; #V; napply mk_powerset; napply mk_unary_morphism1
+  [ napply (intersects ? (mem_op ? U) (mem_op ? V))
+  | #a; #a'; #H; napply mk_iff; *; #H1; #H2
+    [ nwhd; napply (. ((H^-1‡#)‡(H^-1‡#))); nwhd; napply conj; nassumption
+    | nwhd; napply (. ((H‡#)‡(H‡#))); nwhd; napply conj; nassumption]
+nqed.
+
+unification hint 0 (∀A.∀U,V: Ω \sup A.∀w.(λx,y.True)
+ (intersects A U V w) (fun11 ?? (mem_op ? (intersects_ok A U V)) w)).
+
+nlemma test: ∀A. ∀U,V: Ω \sup A. ∀x,x':A. x=x' → (U ∩ V) x → (U ∩ V) x'.
+ #A; #U; #V; #x; #x'; #H; #p;
+ nwhd in ⊢ (? ? % % ?);
+ (* l'unification hint non funziona *)
+  nchange with (? ∈ (intersects_ok ? ? ?));
+  napply (. (†H^-1));
+  nassumption.
 nqed.
-  
-(*interpretation "intersects" 'intersects U V = (intersects ? U V).*)
 
 (*
 ndefinition union ≝ λA.λU,V:Ω \sup A. {x | x ∈ U ∨ x ∈ V }.