matita/tests/decl.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15
  16
  17 include "nat/times.ma".
  18 include "nat/orders.ma".
  19
  20 theorem easy: ∀n,m. n * m = O → n = O ∨ m = O.
  21  assume n: nat.
  22  assume m: nat.
  23  (* base case *)
  24  by (refl_eq ? O) we proved (O = O) (trivial).
  25  by or_introl we proved (O = O ∨ m = O) (trivial2).
  26  using (λ_.trivial2) we proved (O*m=O → O=O ∨ m=O) (base_case).
  27  (* inductive case *)
  28  we need to prove
  29   (∀n1. (n1 * m = O → n1 = O ∨ m = O) → (S n1) * m = O → (S n1) = O ∨ m = O)
  30   (inductive_case).
  31    assume n1: nat.
  32    suppose (n1 * m = O → n1 = O ∨ m = O) (inductive_hyp).
  33    (* base case *)
  34    by or_intror we proved (S n1 = O ∨ O = O) (pre_base_case2).
  35    using (λ_.pre_base_case2) we proved (S n1*O = O → S n1 = O ∨ O = O) (base_case2).
  36    (* inductive case *)
  37    we need to prove
  38     (∀m1. (S n1 * m1 = O → S n1 = O ∨ m1 = O) →
  39       (S n1 * S m1 = O → S n1 = O ∨ S m1 = O)) (inductive_hyp2).
  40      assume m1: nat.
  41      suppose (S n1 * m1 = O → S n1 = O ∨ m1 = O) (useless).
  42      suppose (S n1 * S m1 = O) (absurd_hyp).
  43      simplify in absurd_hyp.
  44      by sym_eq we proved (O = S (m1+n1*S m1)) (absurd_hyp').
  45      by not_eq_O_S we proved False (the_absurd).
  46      by (False_ind ? the_absurd)
  47    done.
  48    (* the induction *)
  49    using (nat_ind (λm.S n1 * m = O → S n1 = O ∨ m = O) base_case2 inductive_hyp2 m)
  50  done.
  51  (* the induction *)
  52  using (nat_ind (λn.n*m=O → n=O ∨ m=O) base_case inductive_case n)
  53 done.
  54 qed.
  55
  56 theorem easy2: ∀n,m. n * m = O → n = O ∨ m = O.
  57  intros 2.
  58  elim n 0
  59   [ intro;
  60     left;
  61     reflexivity
  62   | intro;
  63     elim m 0
  64     [ intros;
  65       right;
  66       reflexivity
  67     | intros;
  68       simplify in H2;
  69       lapply (sym_eq ? ? ? H2);
  70       elim (not_eq_O_S ? Hletin)
  71     ]
  72   ]
  73 qed.
  74
  75 theorem easy15: ∀n,m. n * m = O → n = O ∨ m = O.
  76  assume n: nat.
  77  assume m: nat.
  78  (* base case *)
  79  we proved (O = O) (trivial).
  80  we proved (O = O ∨ m = O) (trivial2).
  81  we proved (O*m=O → O=O ∨ m=O) (base_case).
  82  (* inductive case *)
  83  we need to prove
  84   (∀n1. (n1 * m = O → n1 = O ∨ m = O) → (S n1) * m = O → (S n1) = O ∨ m = O)
  85   (inductive_case).
  86    assume n1: nat.
  87    suppose (n1 * m = O → n1 = O ∨ m = O) (inductive_hyp).
  88    (* base case *)
  89    we proved (S n1 = O ∨ O = O) (pre_base_case2).
  90    we proved (S n1*O = O → S n1 = O ∨ O = O) (base_case2).
  91    (* inductive case *)
  92    we need to prove
  93     (∀m1. (S n1 * m1 = O → S n1 = O ∨ m1 = O) →
  94       (S n1 * S m1 = O → S n1 = O ∨ S m1 = O)) (inductive_hyp2).
  95      assume m1: nat.
  96      suppose (S n1 * m1 = O → S n1 = O ∨ m1 = O) (useless).
  97      suppose (S n1 * S m1 = O) (absurd_hyp).
  98      simplify in absurd_hyp.
  99      we proved (O = S (m1+n1*S m1)) (absurd_hyp').
 100      we proved False (the_absurd).
 101      we proceed by cases on the_absurd to prove (S n1=O ∨ S m1=O).
 102    (* the induction *)
 103    using (nat_ind (λm.S n1 * m = O → S n1 = O ∨ m = O) base_case2 inductive_hyp2 m)
 104  done.
 105  (* the induction *)
 106  using (nat_ind (λn.n*m=O → n=O ∨ m=O) base_case inductive_case n)
 107 done.
 108 qed.
 109
 110 theorem easy3: ∀A:Prop. (A ∧ ∃n:nat.n ≠ n) → True.
 111  assume P: Prop.
 112  suppose (P ∧ ∃m:nat.m ≠ m) (H).
 113  by H we have P (H1) and (∃x:nat.x≠x) (H2).
 114  by H2 let q:nat such that (q ≠ q) (Ineq).
 115  by I done.
 116 qed.
 117
 118 theorem easy4: ∀n,m,p. n = m → S m = S p → n = S p → S n = n.
 119 assume n: nat.
 120 assume m:nat.
 121 assume p:nat.
 122 suppose (n=m) (H).
 123 suppose (S m = S p) (K).
 124 suppose (n = S p) (L).
 125 conclude (S n) = (S m) by H.
 126              = (S p) by K.
 127              = n by L
 128 done.
 129 qed.
 130
 131 theorem easy45: ∀n,m,p. n = m → S m = S p → n = S p → S n = n.
 132 assume n: nat.
 133 assume m:nat.
 134 assume p:nat.
 135 suppose (n=m) (H).
 136 suppose (S m = S p) (K).
 137 suppose (n = S p) (L).
 138 conclude (S n) = (S m).
 139              = (S p).
 140              = n
 141 done.
 142 qed.
 143
 144 theorem easy5: ∀n:nat. n*O=O.
 145 assume n: nat.
 146 (* Bug here: False should be n*0=0 *)
 147 we proceed by induction on n to prove False.
 148  case O.
 149    the thesis becomes (O*O=O).
 150    done.
 151  case S (m:nat).
 152   by induction hypothesis we know (m*O=O) (I).
 153   the thesis becomes (S m * O = O).
 154   (* Bug here: missing that is equivalent to *)
 155   simplify.
 156   by I done.
 157 qed.
 158
 159 inductive tree : Type ≝
 160    Empty: tree
 161  | Node: tree → tree → tree.
 162
 163 let rec size t ≝
 164  match t with
 165   [ Empty ⇒ O
 166   | (Node t1 t2) ⇒ S ((size t1) + (size t2))
 167   ].
 168
 169 theorem easy6: ∀t. O ≮ O → O < size t → t ≠ Empty.
 170  assume t: tree.
 171  suppose (O ≮ O) (trivial).
 172  (*Bug here: False should be something else *)
 173  we proceed by induction on t to prove False.
 174   case Empty.
 175     the thesis becomes (O < size Empty → Empty ≠ Empty).
 176      suppose (O < size Empty) (absurd)
 177      that is equivalent to (O < O).
 178      (* Here the "natural" language is not natural at all *)
 179      we proceed by induction on (trivial absurd) to prove False.
 180   (*Bug here: this is what we want
 181   case Node (t1:tree) (t2:tree).
 182      by induction hypothesis we know (O < size t1 → t1 ≠ Empty) (Ht1).
 183      by induction hypothesis we know (O < size t2 → t2 ≠ Empty) (Ht2). *)
 184   (*This is the best we can do right now*)
 185   case Node.
 186    assume t1: tree.
 187    by induction hypothesis we know (O < size t1 → t1 ≠ Empty) (Ht1).
 188    assume t2: tree.
 189    by induction hypothesis we know (O < size t2 → t2 ≠ Empty) (Ht2).
 190    suppose (O < size (Node t1 t2)) (useless).
 191    we need to prove (Node t1 t2 ≠ Empty) (final)
 192    or equivalently (Node t1 t2 = Empty → False).
 193      suppose (Node t1 t2 = Empty) (absurd).
 194      (* Discriminate should really generate a theorem to be useful with
 195         declarative tactics *)
 196      destruct absurd.
 197      by final
 198    done.
 199 qed.