refactoring: helena sources are now in a dedicated directory

[helm.git] / helm / software / matita / nlibrary / re / re-setoids.ma

diff --git a/helm/software/matita/nlibrary/re/re-setoids.ma b/helm/software/matita/nlibrary/re/re-setoids.ma
index 0b4c3365a40932d43236debf28cd7c3634066bd4..28332fbffa74bccccd122ae632992e758c271350 100644 (file)
--- a/helm/software/matita/nlibrary/re/re-setoids.ma
+++ b/helm/software/matita/nlibrary/re/re-setoids.ma
@@ -322,16 +322,50 @@ ndefinition ex_morph : ∀S:setoid. (S ⇒_1 CPROP) ⇒_1 CPROP.
 *; #x; #H; @ x; nlapply (E x x ?); //; *; /2/;
 nqed.
  
-nlemma d : ∀S:Alpha.
- ∀ee: (setoid1_of_setoid (list S)) ⇒_1 (setoid1_of_setoid (list S)) ⇒_1 CPROP.
- ∀x,y:list S.x = y →
+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;
  nletin F ≝ (comp1_unary_morphisms ??? (ex_morph (list S)) ee);
  
  nnormalize;
- nlapply (exists_is_morph (list S) (list S) ? ?? E);
+  nchange in E with (eq_rel1 ? (eq1 (setoid1_of_setoid (LIST S))) x y);
+
+ ncheck (exists_is_morph (LIST S) (LIST S) ? ?? (E‡#)).
+ nletin xxx ≝ (exists_is_morph); (LIST S)); (LIST S) ee x y E);
  
  nchange with (F x = F y);
  nchange in E with (eq_rel1 ? (eq1 (setoid1_of_setoid (LIST S))) x y);