claudio, please have a look at this

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

diff --git a/helm/software/matita/tests/decl.ma b/helm/software/matita/tests/decl.ma
index 138e37e71fbbd941ad9c48559796071d5d7d0135..3e1bdd3747fdd4b3cb7b5f217351746252b35aea 100644 (file)
--- a/helm/software/matita/tests/decl.ma
+++ b/helm/software/matita/tests/decl.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/test/decl".
+
 
 include "nat/times.ma".
 include "nat/orders.ma".
@@ -22,8 +22,8 @@ theorem easy: ∀n,m. n * m = O → n = O ∨ m = O.
  assume m: nat.
  (* base case *)
  by (refl_eq ? O) we proved (O = O) (trivial).
- by (or_introl ? ? trivial) we proved (O = O ∨ m = O) (trivial2).
- by (λ_.trivial2) we proved (O*m=O → O=O ∨ m=O) (base_case).
+ by or_introl we proved (O = O ∨ m = O) (trivial2).
+ using (λ_.trivial2) 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)
@@ -31,8 +31,8 @@ theorem easy: ∀n,m. n * m = O → n = O ∨ m = O.
    assume n1: nat.
    suppose (n1 * m = O → n1 = O ∨ m = O) (inductive_hyp).
    (* base case *)
-   by (or_intror ? ? trivial) we proved (S n1 = O ∨ O = O) (pre_base_case2).
-   by (λ_.pre_base_case2) we proved (S n1*O = O → S n1 = O ∨ O = O) (base_case2).
+   by or_intror we proved (S n1 = O ∨ O = O) (pre_base_case2).
+   using (λ_.pre_base_case2) 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) →
@@ -41,15 +41,15 @@ theorem easy: ∀n,m. n * m = O → n = O ∨ m = O.
      suppose (S n1 * m1 = O → S n1 = O ∨ m1 = O) (useless).
      suppose (S n1 * S m1 = O) (absurd_hyp).
      simplify in absurd_hyp.
-     by (sym_eq ? ? ? absurd_hyp) we proved (O = S (m1+n1*S m1)) (absurd_hyp').
-     by (not_eq_O_S ? absurd_hyp') we proved False (the_absurd).
+     by sym_eq we proved (O = S (m1+n1*S m1)) (absurd_hyp').
+     by not_eq_O_S we proved False (the_absurd).
      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)
+   using (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)
+ using (nat_ind (λn.n*m=O → n=O ∨ m=O) base_case inductive_case n)
 done.
 qed.
  
@@ -76,9 +76,9 @@ 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).
+ we proved (O = O) (trivial).
+ we proved (O = O ∨ m = O) (trivial2).
+ 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)
@@ -86,8 +86,8 @@ theorem easy15: ∀n,m. n * m = O → n = O ∨ m = O.
    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).
+   we proved (S n1 = O ∨ O = O) (pre_base_case2).
+   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) →
@@ -96,17 +96,14 @@ theorem easy15: ∀n,m. n * m = O → n = O ∨ m = O.
      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.
+     we proved (O = S (m1+n1*S m1)) (absurd_hyp').
+     we proved False (the_absurd).
+     we proceed by cases on the_absurd to prove (S n1=O ∨ S m1=O).
    (* the induction *)
-   by (nat_ind (λm.S n1 * m = O → S n1 = O ∨ m = O) base_case2 inductive_hyp2 m)
+   using (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)
+ using (nat_ind (λn.n*m=O → n=O ∨ m=O) base_case inductive_case n)
 done.
 qed.
 
@@ -114,11 +111,7 @@ theorem easy3: ∀A:Prop. (A ∧ ∃n:nat.n ≠ n) → True.
  assume P: Prop.
  suppose (P ∧ ∃m:nat.m ≠ m) (H).
  by H we have P (H1) and (∃x:nat.x≠x) (H2).
- (*BUG:
  by H2 let q:nat such that (q ≠ q) (Ineq).
- *)
- (* the next line is wrong, but for the moment it does the job *)
- by H2 let q:nat such that False (Ineq).
  by I done.
 qed.
 
@@ -129,9 +122,9 @@ assume p:nat.
 suppose (n=m) (H).
 suppose (S m = S p) (K).
 suppose (n = S p) (L).
-obtain (S n) = (S m) by (eq_f ? ? ? ? ? H).
+conclude (S n) = (S m) by H.
              = (S p) by K.
-             = n by (sym_eq ? ? ? L)
+             = n by L
 done.
 qed.
 
@@ -142,9 +135,9 @@ 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 _
+conclude (S n) = (S m).
+             = (S p).
+             = n
 done.
 qed.
 
@@ -154,7 +147,7 @@ assume n: nat.
 we proceed by induction on n to prove False. 
  case O.
    the thesis becomes (O*O=O).
-   by (refl_eq ? O) done.
+   done.
  case S (m:nat).
   by induction hypothesis we know (m*O=O) (I).
   the thesis becomes (S m * O = O).
@@ -203,4 +196,4 @@ theorem easy6: ∀t. O ≮ O → O < size t → t ≠ Empty.
      destruct absurd.
      by final
    done.
-qed.
\ No newline at end of file
+qed.