helm/matita/library/nat/times.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/nat/times".
  16
  17 include "logic/equality.ma".
  18 include "nat/nat.ma".
  19 include "nat/plus.ma".
  20
  21 let rec times n m \def
  22  match n with
  23  [ O \Rightarrow O
  24  | (S p) \Rightarrow (m+(times p m)) ].
  25
  26 interpretation "natural times" 'times x y = (cic:/matita/nat/times/times.con x y).
  27
  28 theorem times_n_O: \forall n:nat. O = n*O.
  29 intros.elim n.
  30 simplify.reflexivity.
  31 simplify.assumption.
  32 qed.
  33
  34 theorem times_n_Sm :
  35 \forall n,m:nat.n+n*m = n*(S m).
  36 intros.elim n.
  37 simplify.reflexivity.
  38 simplify.apply eq_f.rewrite < H.
  39 transitivity ((n1+m)+n1*m).symmetry.apply assoc_plus.
  40 transitivity ((m+n1)+n1*m).
  41 apply eq_f2.
  42 apply sym_plus.
  43 reflexivity.
  44 apply assoc_plus.
  45 qed.
  46
  47 (* same problem with symmetric: see plus
  48 theorem symmetric_times : symmetric nat times. *)
  49
  50 theorem sym_times :
  51 \forall n,m:nat.n*m = m*n.
  52 intros.elim n.
  53 simplify.apply times_n_O.
  54 simplify.rewrite > H.apply times_n_Sm.
  55 qed.
  56
  57 theorem distributive_times_plus : distributive nat times plus.
  58 simplify.
  59 intros.elim x.
  60 simplify.reflexivity.
  61 simplify.rewrite > H. rewrite > assoc_plus.rewrite > assoc_plus.
  62 apply eq_f.rewrite < assoc_plus. rewrite < sym_plus ? z.
  63 rewrite > assoc_plus.reflexivity.
  64 qed.
  65
  66 variant times_plus_distr: \forall n,m,p:nat. n*(m+p)=n*m+n*p
  67 \def distributive_times_plus.
  68