First tests for paramodulation (pretty printer, unification)

[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 6c7e161f68d6ea8692024d874e9f697ffdd057a1..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)).
@@ -22,7 +23,7 @@ nletin pippo ≝ (S m) in H: % ⊢ (???%);
 #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) ⊢ (nat → eq nat __1 (pippo+m) → pippo=S pippo); *)
+ 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: (?%? (?%?));
@@ -30,7 +31,7 @@ nwhd in H: (?%? (?%?));
 nchange in match (S ?) in H:(??%?) ⊢ (??%%) with (pred (S ?));
 ngeneralize in match H;
 napply (? H);
-nelim m in ⊢ (???(?%?) → %); (*SBAGLIA UNIFICATORE*)
+nelim m in ⊢ (???(?%?) → %);
 nnormalize;
  ##[ ncases x in H ⊢ (? → % → ?);
  ##|