From 839b5aa6fe82b39eaaca34e6f99fe3a4f58658c4 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 22 Jul 2010 08:05:23 +0000
Subject: [PATCH] some work on \exists

---
 .../software/matita/nlibrary/re/re-setoids.ma | 36 +++++++++++++++++--
 1 file changed, 34 insertions(+), 2 deletions(-)

diff --git a/helm/software/matita/nlibrary/re/re-setoids.ma b/helm/software/matita/nlibrary/re/re-setoids.ma
index a495413f5..28332fbff 100644
--- a/helm/software/matita/nlibrary/re/re-setoids.ma
+++ b/helm/software/matita/nlibrary/re/re-setoids.ma
@@ -322,8 +322,40 @@ ndefinition ex_morph : ∀S:setoid. (S ⇒_1 CPROP) ⇒_1 CPROP.
 *; #x; #H; @ x; nlapply (E x x ?); //; *; /2/;
 nqed.
  
-nlemma d : ∀S:setoid1. ∀ee: S ⇒_1 S ⇒_1 CPROP.
- ∀x,y:S.x =_1 y → (Ex1 S (λw.ee x w)) =_1 (Ex1 S (λw.ee y w)).
+nlemma Sig: ∀S,T:setoid.∀P: S → (T → CProp[0]).
+  ∀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.
+
+
+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;
+alias symbol "trans" (instance 1) = "trans1".
+alias symbol "refl" (instance 5) = "refl".
+alias symbol "prop2" (instance 3) = "prop21".
+alias symbol "trans" (instance 1) = "trans1".
+alias symbol "prop2" (instance 3) = "prop21".
+(* super bug 1+1: 
+     eseguire senza modificare per ottenrere degli alias, fare back di 1 passo
+     e ri-eseguire. Se riesegue senza aggiungere altri alias allora hai gli 
+     alias giusti (ma se fate back di più passi, gli alias non vanno più bene...).
+     ora (m x w) e True possono essere sostituiti da ?, se invece 
+     si toglie anche l'∧, allora un super bug si scatena (meta contesto locale
+     scazzato, con y al posto di x, unificata con se stessa ma col contesto
+     locale corretto...). lo stesso (o simile) bug salta fuori se esegui
+     senza gli alias giusti con ? al posto di True o (m x w). 
+     
+     bug a parte, pare inferisca tutto lui...
+     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‡#)‡#))); 
+//; nqed.
+STOP
+napply (λw:S.(.= ((E‡#)‡#)) #); ##[##2: napply w| napply m. #H; napply H;
+
+ 
+ 
  let form ≝ comp1_unary_morphisms ??? (ex_morph (list S)) ee in
   form x = form y.
  #S ee x y E;
-- 
2.39.2