...

diff --git a/helm/software/matita/tests/ng_elim.ma b/helm/software/matita/tests/ng_elim.ma
index b67401fde0a32273ccabdcdf6e3b19c1ab1f2834..dfded53ee2ed82759aa93e1b078c40c0d9018806 100644 (file)
--- a/helm/software/matita/tests/ng_elim.ma
+++ b/helm/software/matita/tests/ng_elim.ma
@@ -64,10 +64,12 @@ nlet rec le_rec (n:nat) (Q: ∀D1:nat.∀D2: P D1. le n D1 D2 → Type) (p1: ?)
  ## ]
 nqed.*)
 
-include "list/list.ma".
+ninductive list (A:Type) : nat → Type ≝
+   nil: list A O
+ | cons: ∀n. A → list A n → list A (S n).
 
 ninductive ii: Type ≝
- kk: list ii → ii.
+ kk: list ii O → ii.
 
 nlet rec ii_rect (Q_: (∀(x_16: ii).Type)) H_kknil H_kkcons x_16 on x_16: (Q_ x_16) ≝
  (match x_16 with

diff --git a/helm/software/matita/tests/ng_tactics.ma b/helm/software/matita/tests/ng_tactics.ma
index 629c9990920b6d32c370c731d30a54323fe874f3..6c7e161f68d6ea8692024d874e9f697ffdd057a1 100644 (file)
--- 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;