X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Ftests%2Fng_tactics.ma;h=6c7e161f68d6ea8692024d874e9f697ffdd057a1;hb=a9c8d96d47a5895c99bca2fe93decf464bca62c3;hp=629c9990920b6d32c370c731d30a54323fe874f3;hpb=eff920e57112c3eaee889384d435602e41951a36;p=helm.git

diff --git a/helm/software/matita/tests/ng_tactics.ma b/helm/software/matita/tests/ng_tactics.ma
index 629c99909..6c7e161f6 100644
--- a/helm/software/matita/tests/ng_tactics.ma
+++ b/helm/software/matita/tests/ng_tactics.ma
@@ -21,29 +21,28 @@ nletin pippo ≝ (S m) in H: % ⊢ (???%);
             nassert m:nat pippo : nat ≝ (S m) ⊢ (m = pippo + m → S m = S pippo);
 #H; nchange in match pippo in H:% with (pred (S pippo));
  nassert m:nat pippo : nat ≝ (S m) H:(m = pred (S pippo) + m) ⊢ (S m = S pippo);
-ngeneralize in match m in ⊢ %; (* BUG *)
+ngeneralize in match m in H:(??%?) ⊢ %;
+(* nassert m:nat pippo : nat ≝ (S m) ⊢ (nat → eq nat __1 (pippo+m) → pippo=S pippo); *)
+#x; #H;
+ nassert m:nat pippo : nat ≝ (S m) x: nat H:(x = pred (S pippo) + m) ⊢ (S x = S pippo);
+nwhd in H: (?%? (?%?));
+           nassert m:nat pippo:nat≝(S m) x:nat H:(x=S m + m) ⊢ (S x = S pippo);
+nchange in match (S ?) in H:(??%?) ⊢ (??%%) with (pred (S ?));
+ngeneralize in match H;
+napply (? H);
+nelim m in ⊢ (???(?%?) → %); (*SBAGLIA UNIFICATORE*)
+nnormalize;
+ ##[ ncases x in H ⊢ (? → % → ?);
+ ##|
+ ##]
 STOP;
 
-nwhd in H:(???%); 
-nchange in match (S ?) in H:% ⊢ (? → %) with (pred (S ?));  
-ntaint;
-
-ngeneralize in match m in ⊢ %;   in ⊢ (???% → ??%?);
-STOP 
-ncases (O) in m : % (*H : (??%?)*) ⊢ (???%);
-nelim (S m) in H : (??%?) ⊢ (???%);
-STOP;
 axiom A : Prop.
 axiom B : Prop.
 axiom C : Prop.
 axiom a: A.
 axiom b: B.
 
-include "nat/plus.ma".
-(*
-ntheorem foo: ∀n. n+n=n → n=n → n=n.
- #n; #H; #K; nrewrite < H in (*K: (???%) ⊢*) ⊢ (??%?); napply (eq_ind ????? H);
-*)
 include "logic/connectives.ma".
 
 definition xxx ≝ A.
@@ -52,9 +51,7 @@ notation "†" non associative with precedence 90 for @{ 'sharp }.
 interpretation "a" 'sharp = a.
 interpretation "b" 'sharp = b.
 
-include "nat/plus.ma".
-
-(*ntheorem foo: ∀n:nat. match n with [ O ⇒ n | S m ⇒ m + m ] = n.*)
+ntheorem foo: ∀n:nat. match n with [ O ⇒ n | S m ⇒ m + m ] = n.
 
 (*ntheorem prova : ((A ∧ A → A) → (A → B) → C) → C.
 # H; nassert H: ((A ∧ A → A) → (A → B) → C) ⊢ C;