X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Ftests%2Fdecl.ma;h=a0d3a0bd610f62962e0ffb73ea4d718985f49a21;hb=9a81424c15d8b80a50f62ffe5f5b3ced32dfa463;hp=8ff56dde87398e467896aee5d7c3d58b8266e829;hpb=31d3422a07ed889dff7bda3a28884caff30cba07;p=helm.git

diff --git a/matita/tests/decl.ma b/matita/tests/decl.ma
index 8ff56dde8..a0d3a0bd6 100644
--- a/matita/tests/decl.ma
+++ b/matita/tests/decl.ma
@@ -72,6 +72,43 @@ theorem easy2: ∀n,m. n * m = O → n = O ∨ m = O.
   ]
 qed.
 
+theorem easy15: ∀n,m. n * m = O → n = O ∨ m = O.
+ assume n: nat.
+ assume m: nat.
+ (* base case *)
+ by _ we proved (O = O) (trivial).
+ by _ we proved (O = O ∨ m = O) (trivial2).
+ by _ we proved (O*m=O → O=O ∨ m=O) (base_case).
+ (* inductive case *)
+ we need to prove
+  (∀n1. (n1 * m = O → n1 = O ∨ m = O) → (S n1) * m = O → (S n1) = O ∨ m = O)
+  (inductive_case).
+   assume n1: nat.
+   suppose (n1 * m = O → n1 = O ∨ m = O) (inductive_hyp).
+   (* base case *)
+   by _ we proved (S n1 = O ∨ O = O) (pre_base_case2).
+   by _ we proved (S n1*O = O → S n1 = O ∨ O = O) (base_case2).
+   (* inductive case *)
+   we need to prove
+    (∀m1. (S n1 * m1 = O → S n1 = O ∨ m1 = O) →
+      (S n1 * S m1 = O → S n1 = O ∨ S m1 = O)) (inductive_hyp2).
+     assume m1: nat.
+     suppose (S n1 * m1 = O → S n1 = O ∨ m1 = O) (useless).
+     suppose (S n1 * S m1 = O) (absurd_hyp).
+     simplify in absurd_hyp.
+     by _ we proved (O = S (m1+n1*S m1)) (absurd_hyp').
+     (* BUG: automation failure *)
+     by (not_eq_O_S ? absurd_hyp') we proved False (the_absurd).
+     (* BUG: automation failure *)
+     by (False_ind ? the_absurd)
+   done.
+   (* the induction *)
+   by (nat_ind (λm.S n1 * m = O → S n1 = O ∨ m = O) base_case2 inductive_hyp2 m)
+ done.
+ (* the induction *)
+ by (nat_ind (λn.n*m=O → n=O ∨ m=O) base_case inductive_case n)
+done.
+qed.
 
 theorem easy3: ∀A:Prop. (A ∧ ∃n:nat.n ≠ n) → True.
  assume P: Prop.
@@ -98,6 +135,19 @@ obtain (S n) = (S m) by (eq_f ? ? ? ? ? H).
 done.
 qed.
 
+theorem easy45: ∀n,m,p. n = m → S m = S p → n = S p → S n = n.
+assume n: nat.
+assume m:nat.
+assume p:nat.
+suppose (n=m) (H).
+suppose (S m = S p) (K).
+suppose (n = S p) (L).
+obtain (S n) = (S m) by _.
+             = (S p) by _.
+             = n by _
+done.
+qed.
+
 theorem easy5: ∀n:nat. n*O=O.
 assume n: nat.
 (* Bug here: False should be n*0=0 *)
@@ -130,9 +180,8 @@ theorem easy6: ∀t. O ≮ O → O < size t → t ≠ Empty.
  we proceed by induction on t to prove False.
   case Empty.
     the thesis becomes (O < size Empty → Empty ≠ Empty).
-     suppose (O < size Empty) (absurd).
-     (*Bug here: missing that is equivalent to *)
-     simplify in absurd.
+     suppose (O < size Empty) (absurd)
+     that is equivalent to (O < O).
      (* Here the "natural" language is not natural at all *)
      we proceed by induction on (trivial absurd) to prove False.
   (*Bug here: this is what we want
@@ -145,11 +194,13 @@ theorem easy6: ∀t. O ≮ O → O < size t → t ≠ Empty.
    by induction hypothesis we know (O < size t1 → t1 ≠ Empty) (Ht1).
    assume t2: tree.
    by induction hypothesis we know (O < size t2 → t2 ≠ Empty) (Ht2).
-   suppose (O < size (Node t1 t2)) (Hyp).
-   (*BUG: that is equivalent to missed here *)
-   unfold Not.
-   suppose (Node t1 t2 = Empty) (absurd).
-   (* Discriminate should really generate a theorem to be useful with
-      declarative tactics *)
-   discriminate absurd.
+   suppose (O < size (Node t1 t2)) (useless).
+   we need to prove (Node t1 t2 ≠ Empty) (final)
+   or equivalently (Node t1 t2 = Empty → False).
+     suppose (Node t1 t2 = Empty) (absurd).
+     (* Discriminate should really generate a theorem to be useful with
+        declarative tactics *)
+     discriminate absurd.
+     by final
+   done.
 qed.
\ No newline at end of file