From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 16 Sep 2009 09:02:16 +0000 (+0000)
Subject: New interesting coercion.
X-Git-Tag: make_still_working~3462
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a9d1332496548ff921db655f4b9430a0b2b6e92d;p=helm.git

New interesting coercion.
---

diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index f140ef770..8ee6ea1ae 100644
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -129,15 +129,28 @@ nlemma subseteq_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_s
         [ nassumption | napply (subseteq_trans … b'); nassumption ] ##]
 nqed.
 
+(* hints can pass under mem *) (* ??? XXX why is it needed? *)
+unification hint 0 ≔ A,B,x ;
+           C ≟ B
+ (*---------------------*) ⊢ 
+   mem A B x ≡ mem A C x.
+
+unification hint 0 ≔ A,a,a'
+ (*---------------------*) ⊢
+  eq_rel ? (eq A) a a' ≡ eq_rel1 ? (eq1 (setoid1_of_setoid A)) a a'.
+
 nlemma intersect_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) (qpowerclass_setoid A).
  #A; @
   [ #S; #S'; @
      [ napply (S ∩ S')
-     | #a; #a'; #Ha; nwhd in ⊢ (? ? ? % %); @; *; #H1; #H2; @
-        [##1,2: napply (. (mem_ok' …)^-1) [##3,6: nassumption |##2,5: nassumption |##*: ##skip]
-      ##|##3,4: napply (. (mem_ok' …)) [##1,3,4,6: nassumption |##*: ##skip]##]##]
+     | #a; #a'; #Ha;
+       (*napply (.= #‡#);*)
+        nwhd in ⊢ (? ? ? % %); @; *; #H1; #H2; @
+        [##1,2: napply (. Ha^-1‡#); nassumption;
+      ##|##3,4: napply (. Ha‡#); nassumption]##]
  ##| #a; #a'; #b; #b'; #Ha; #Hb; nwhd; @; #x; nwhd in ⊢ (% → %); #H
-      [ napply (. ((#‡Ha^-1)‡(#‡Hb^-1))); nassumption
+      [ alias symbol "invert" = "setoid1 symmetry".
+        napply (. ((#‡Ha^-1)‡(#‡Hb^-1))); nassumption
       | napply (. ((#‡Ha)‡(#‡Hb))); nassumption ]##]
 nqed.
 
@@ -147,12 +160,6 @@ unification hint 0 ≔
   A : setoid, B,C : qpowerclass A ⊢ 
     pc A (intersect_ok A B C) ≡ intersect ? (pc ? B) (pc ? C).
 
-(* hints can pass under mem *) (* ??? XXX why is it needed? *)
-unification hint 0 ≔ A,B,x ;
-           C ≟ B
- (*---------------------*) ⊢ 
-   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; napply (. (H^-1‡#)); nassumption.
 nqed.
@@ -187,7 +194,8 @@ ndefinition eqrel_of_morphism:
   [ @
      [ napply (λx,y. f x = f y)
      | #x; napply refl | #x; #y; napply sym | #x; #y; #z; napply trans]
-##| #x; #x'; #H; nwhd; napply (.= (†H)); napply refl ]
+##| #x; #x'; #H; nwhd; alias symbol "prop1" = "prop1".
+napply (.= (†H)); napply refl ]
 nqed.
 
 ndefinition canonical_proj: ∀A,R. unary_morphism A (quotient A R).