X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Ftests%2Fng_tactics.ma;h=882bdcbeb1e89856ea2954c81875382ef463a2de;hb=b6afef7e73324824025a6d7f313129d55b72cfc6;hp=a9cb8557787d1c5669ce54a66a988419af8e18e9;hpb=901ee87aad4ae08a19399f8bf925dfdffd92aee1;p=helm.git

diff --git a/helm/software/matita/tests/ng_tactics.ma b/helm/software/matita/tests/ng_tactics.ma
index a9cb85577..882bdcbeb 100644
--- a/helm/software/matita/tests/ng_tactics.ma
+++ b/helm/software/matita/tests/ng_tactics.ma
@@ -12,35 +12,38 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ng_pts.ma".
 include "nat/plus.ma".
 
 ntheorem test1 : ∀n:nat.n = S n + n → S n = (S (S n)).
 #m; #H;
                                  nassert m:nat H: (m=S m + m) ⊢ (S m = S (S m));
 nletin pippo ≝ (S m) in H: % ⊢ (???%);
- nassert m:nat pippo : nat ≝ (S m) ⊢ (m = pippo + m → (S m) = (S pippo));
+            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 H:(??%?) ⊢ %;
+ nassert m:nat pippo : nat ≝ (S m) ⊢ (∀n:nat. n=(pred (S pippo)+m) → (S n)=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 ⊢ (???(?%?) → %);
+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.
@@ -49,9 +52,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;