From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 8 Sep 2010 13:30:32 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~2840
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=070b44c9c2344967ca8c4531909614a0d4da2fbe;p=helm.git

...
---

diff --git a/helm/software/matita/nlibrary/re/re-setoids.ma b/helm/software/matita/nlibrary/re/re-setoids.ma
index 28332fbff..06791066a 100644
--- a/helm/software/matita/nlibrary/re/re-setoids.ma
+++ b/helm/software/matita/nlibrary/re/re-setoids.ma
@@ -25,9 +25,8 @@ ninductive list (A:Type[0]) : Type[0] ≝
   
 nlet rec eq_list (A : setoid) (l1, l2 : list A) on l1 : CProp[0] ≝ 
 match l1 with
-[ nil ⇒ match l2 return λ_.CProp[0] with [ nil ⇒ ? | _ ⇒ ? ]
-| cons x xs ⇒ match l2 with [ nil ⇒ ? | cons y ys ⇒ x = y ∧ eq_list ? xs ys]].
-##[ napply True|napply False|napply False]nqed.
+[ nil ⇒ match l2 return λ_.CProp[0] with [ nil ⇒ True | _ ⇒ False ]
+| cons x xs ⇒ match l2 with [ nil ⇒ False | cons y ys ⇒ x = y ∧ eq_list ? xs ys]].
    
 ndefinition LIST : setoid → setoid.
 #S; @(list S); @(eq_list S); ncases admit; nqed.  
@@ -322,14 +321,41 @@ ndefinition ex_morph : ∀S:setoid. (S ⇒_1 CPROP) ⇒_1 CPROP.
 *; #x; #H; @ x; nlapply (E x x ?); //; *; /2/;
 nqed.
  
-nlemma Sig: ∀S,T:setoid.∀P: S → (T → CProp[0]).
+nlemma Sig: ∀S,T:setoid.∀P: S → (T → CPROP).
   ∀y,z:T.y = z → (∀x.y=z → P x y = P x z)  → (Ex S (λx.P x y)) =_1 (Ex S (λx.P x z)).
 #S T P y z Q E; @; *; #x Px; @x; nlapply (E x Q); *; /2/; nqed.
 
+(* desiderata : Σ(λx.H‡#)
+   ottenute   : Σ H (λx,H.H‡#) -- quindi monoriscrittura. H toplevel permette inferenza di y e z in Sig
+*)
 
 nlemma test : ∀S:setoid. ∀ee: S ⇒_1 S ⇒_1 CPROP.
  ∀x,y:setoid1_of_setoid S.x =_1 y → (Ex S (λw.ee x w ∧ True)) =_1 (Ex S (λw.ee y w ∧ True)).
 #S m x y E;
+
+napply (trans1 ????? (Sig ????? E (λw,H.
+  (prop11 ?(unary_morphism1_setoid1 ??)??? 
+    (prop11 ?(unary_morphism1_setoid1 ??)??? 
+       H 
+       ?? (refl ???))
+    ?? (refl1 ???))))).
+napply refl1.
+nqed.
+
+nlemma test2 : ∀S:setoid. ∀ee: S ⇒_1 S ⇒_1 CPROP.
+ ∀x,y:setoid1_of_setoid S.x =_1 y → 
+   (True ∧ (Ex S (λw.ee x w ∧ True))) =_1 (True ∧ (Ex S (λw.ee y w ∧ True))).
+#S m x y E;
+napply (trans1 ????? 
+(#‡
+ (Sig ????? E (λw,H.
+  (prop11 ?(unary_morphism1_setoid1 ??)??? 
+    (prop11 ?(unary_morphism1_setoid1 ??)??? 
+       H 
+       ?? (refl ???))
+    ?? (refl1 ???)))))).
+napply refl1.
+
 alias symbol "trans" (instance 1) = "trans1".
 alias symbol "refl" (instance 5) = "refl".
 alias symbol "prop2" (instance 3) = "prop21".
@@ -349,7 +375,37 @@ alias symbol "prop2" (instance 3) = "prop21".
      la E astratta nella prova è solo per fargli inferire x e y, se Sig
      lo si riformula in modo più naturale (senza y=z) allora bisogna passare
      x e y esplicitamente. *)  
-napply (.= (Sig ? S (λw,x.(m x w) ∧ True) ?? E (λw,E.(E‡#)‡#))); 
+alias symbol "trans" (instance 1) = "trans1".
+alias symbol "prop2" (instance 3) = "prop21".
+alias symbol "trans" (instance 1) = "trans1".
+alias symbol "prop2" (instance 3) = "prop21".
+
+alias symbol "trans" (instance 1) = "trans1".
+alias symbol "prop2" (instance 3) = "prop21".
+(*napply (.= (Sig ? S (λw,x. m x w ∧ True) ?? E (λw,H.(H‡#)‡#))); *)
+
+(* OK *)
+napply (.= (Sig ? ? (?) ?? E (λw,H.
+  (prop11 ?(unary_morphism1_setoid1 ??)??? 
+    (prop11 ?(unary_morphism1_setoid1 ??)??? 
+       H 
+       ?? (refl ???))
+    ?? (refl1 ???))))).
+napply refl1.
+
+  (prop11 (setoid1_of_setoid ?) (ext_powerclass_setoid ?) ? ? ???? 
+                                                (prop11 (setoid1_of_setoid ?) (ext_powerclass_setoid ?) ? ? ???? 
+                                                   H
+                                                   (refl ??))
+                                              (refl ? True))))).
+
+prop11 ???????? (prop11 ???????? H (refl ??)) (refl ??)))); 
+
+napply (.= (Sig ? S (λw,x. m x w ∧ True) ?? E (λw,H.(H‡#)‡#))); 
+
+
+napply (.= (Sig ? S (λw,x.?) ?? E (λw,H.(H‡#)‡#))); 
+(Ex S (λx.?P x y)) ==?== 
 //; nqed.
 STOP
 napply (λw:S.(.= ((E‡#)‡#)) #); ##[##2: napply w| napply m. #H; napply H;