...

diff --git a/helm/software/matita/nlibrary/re/re-setoids.ma b/helm/software/matita/nlibrary/re/re-setoids.ma
index 06791066ab1d21f3d486bc26ff943bc46deeebb7..dcd9a226d3e5fb46b51fb23ad3c8d8bdded3020c 100644 (file)
--- a/helm/software/matita/nlibrary/re/re-setoids.ma
+++ b/helm/software/matita/nlibrary/re/re-setoids.ma
@@ -293,9 +293,10 @@ notation "𝐋\sub(\p) term 70 E" non associative with precedence 75 for @{'L_pi
 interpretation "in_pl" 'L_pi E = (L_pi ? E).
 
 unification hint 0 ≔ S,a,b;
-   R ≟ LIST S
+   R ≟ LIST S,
+   L ≟ (list S)
 (* -------------------------------------------- *) ⊢
-   eq_list S a b ≡ eq_rel (list S) (eq0 R) a b.
+   eq_list S a b ≡ eq_rel L (eq0 R) a b.
 
 notation > "B ⇒_0 C" right associative with precedence 72 for @{'umorph0 $B $C}.
 notation > "B ⇒_1 C" right associative with precedence 72 for @{'umorph1 $B $C}.
@@ -329,187 +330,51 @@ nlemma Sig: ∀S,T:setoid.∀P: S → (T → CPROP).
    ottenute   : Σ H (λx,H.H‡#) -- quindi monoriscrittura. H toplevel permette inferenza di y e z in Sig
 *)
 
+notation "∑" non associative with precedence 90 for @{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.
+napply (.=_1 (∑ E (λw,H.(H ╪_1 #)╪_1 #))).
+napply #.
 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".
-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. *)  
-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;
-
- 
- 
- 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;
-  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);
- napply (.= † E);
- napply #.
-nqed.
-
-
-E : w = w2
-  
-  
-  Σ(λx.(#‡E)‡#) : ∃x.x = w ∧ m → ∃x.x = w2 ∧ m 
-  λx.(#‡E)‡#    : ∀x.x = w ∧ m → x = w2 ∧ m 
-
-
-w;
-F ≟ ex_moprh ∘ G
-g ≟ fun11 G
-------------------------------
-ex (λx.g w x) ==?== fun11 F w
-
-x ⊢ fun11 ?h ≟ λw. ?g w x
-?G ≟ morphism_leibniz (T → S) ∘ ?h 
-------------------------------
-(λw. (λx:T.?g w x)) ==?== fun11 ?G
-
-...
-x ⊢ fun11 ?h ==?== λw. eq x w ∧ m [w] 
-(λw,x.eq x w ∧ m[w]) ==?== fun11 ?G
-ex (λx.?g w x) ==?== ex (λx.x = w ∧ m[w])
-
-ndefinition ex_morph : ∀S:setoid. (S ⇒_1 CPROP) ⇒_1 CPROP.
-#S; @; ##[ #P; napply (Ex ? P); ##| ncases admit. ##] nqed.
-
-ndefinition ex_morph1 : ∀S:setoid. (S ⇒_1 CPROP) ⇒_1 CPROP.
-#S; @; ##[ #P; napply (Ex ? (λx.P); ##| ncases admit. ##] 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 →
- 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;
- 
- nchange with (F x = F y);
- nchange in E with (eq_rel1 ? (eq1 (setoid1_of_setoid (LIST S))) x y);
- napply (.= † E);
- napply #.
+napply (.=_1 #‡(∑ E (λw,H.(H ╪_1 #) ╪_1 #))).
+napply #.
 nqed.
 
+nlemma ex_setoid : ∀S:setoid.(S ⇒_1 CPROP) → setoid.
+#T P; @ (Ex T (λx:T.P x)); @;
+##[ #H1 H2; ncases H1; ncases H2; #x Px y Py; napply (x = y);
+##| #H; napply (?:?); ncases H; nelim H;  nnormalize;
 
-nlemma d : ∀S:Alpha.∀ee: (setoid1_of_setoid (list S)) ⇒_1 (setoid1_of_setoid (list S)) ⇒_1 CPROP.∀x,y:list S.x = y →
- 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;
- 
- nchange with (F x = F y);
- nchange in E with (eq_rel1 ? (eq1 (setoid1_of_setoid (LIST S))) x y);
- napply (.= † E);
- napply #.
+nlemma test3 : ∀S:setoid. ∀ee: S ⇒_1 S ⇒_1 CPROP.
+ ∀x,y:setoid1_of_setoid S.x =_1 y → 
+   ((Ex S (λw.ee x w ∧ True) ∨ True)) =_1 ((Ex S (λw.ee y w ∧ True) ∨ True)).
+#S m x y E;
+napply (. (? ‡ #));
+napply (.=_1 (∑ E (λw,H.(H ╪_1 #) ╪_1 #)) ╪_1 #).
+napply #.
 nqed.
- 
-  
-nlemma d : ∀S:Alpha.(setoid1_of_setoid (list S)) ⇒_1 CPROP.
- #S; napply (comp1_unary_morphisms ??? (ex_morph (list S)) ?);
- napply (eq1).
-  
-  
-  
-(*
-ndefinition comp_ex : ∀X,S,T,K.∀P:X ⇒_1 (S ⇒_1 T).∀Pc : (S ⇒_1 T) ⇒_1 K. X ⇒_1 K.
- *)
 
 ndefinition L_pi_ext : ∀S:Alpha.∀r:pitem S.Elang S.
-#S r; @(𝐋\p r); #w1 w2 E; nelim r; /2/;
-##[ #x; @; #H; ##[ nchange in H ⊢ % with ([?]=?); napply ((.= H) E)]
-    nchange in H ⊢ % with ([?]=?); napply ((.= H) E^-1);
+#S r; @(𝐋\p r); #w1 w2 E; nelim r; 
+##[ /2/;
+##| /2/;
+##| #x; @; *;
+##| #x; @; #H; nchange in H with ([?] =_0 ?); ##[ napply ((.=_0 H) E); ##]
+    napply ((.=_0 H) E^-1);
 ##| #e1 e2 H1 H2; 
     nchange in match (w1 ∈ 𝐋\p (?·?)) with ((∃_.?)∨?);
+    nchange in match (w2 ∈ 𝐋\p (?·?)) with ((∃_.?)∨?);
     napply (.= (#‡H2));
-    napply (.= (Eexists ?? ? w1 w2 E)‡#);
+    napply (. (?‡#)); 
+    nlapply (.=_1 (∑ E (λx,H.?))╪_1 #);
+    napply (.=_1 (∑ E (λx,H.#))╪_1 #);
     
     
     nchange in match (w2 ∈ 𝐋\p (?·?)) with (?∨?);