helm/software/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 set "baseuri" "cic:/matita/test/decl".
  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 ? ? trivial) we proved (O = O ∨ m = O) (trivial2).
  26  by (λ_.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 ? ? trivial) we proved (S n1 = O ∨ O = O) (pre_base_case2).
  35    by (λ_.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 ? ? ? absurd_hyp) we proved (O = S (m1+n1*S m1)) (absurd_hyp').
  45      by (not_eq_O_S ? absurd_hyp') we proved False (the_absurd).
  46      by (False_ind ? the_absurd)
  47    done.
  48    (* the induction *)
  49    by (nat_ind (λm.S n1 * m = O → S n1 = O ∨ m = O) base_case2 inductive_hyp2 m)
  50  done.
  51  (* the induction *)
  52  by (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