From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 17 May 2009 19:11:00 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~3973
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6e3edeedb090d7406c2383d57d14755a55b43946;p=helm.git

...
---

diff --git a/helm/software/matita/tests/ng_elim.ma b/helm/software/matita/tests/ng_elim.ma
index b67401fde..dfded53ee 100644
--- 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 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;