claudio, please have a look at this

[helm.git] / helm / software / matita / tests / ng_tactics.ma

diff --git a/helm/software/matita/tests/ng_tactics.ma b/helm/software/matita/tests/ng_tactics.ma
index 629c9990920b6d32c370c731d30a54323fe874f3..882bdcbeb1e89856ea2954c81875382ef463a2de 100644 (file)
--- a/helm/software/matita/tests/ng_tactics.ma
+++ b/helm/software/matita/tests/ng_tactics.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ng_pts.ma".
 include "nat/plus.ma".
 
 ntheorem test1 : ∀n:nat.n = S n + n → S n = (S (S n)).
@@ -21,29 +22,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) ⊢ (∀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.
@@ -52,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;