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 (*CSC: the URI must disappear: there is a bug now *)
  27 interpretation "natural times" 'times x y = (cic:/matita/nat/times/times.con x y).
  28
  29 theorem times_n_O: \forall n:nat. O = n*O.
  30 intros.elim n.
  31 simplify.reflexivity.
  32 simplify.assumption.
  33 qed.
  34
  35 theorem times_n_Sm :
  36 \forall n,m:nat.n+n*m = n*(S m).
  37 intros.elim n.
  38 simplify.reflexivity.
  39 simplify.apply eq_f.rewrite < H.
  40 transitivity ((n1+m)+n1*m).symmetry.apply assoc_plus.
  41 transitivity ((m+n1)+n1*m).
  42 apply eq_f2.
  43 apply sym_plus.
  44 reflexivity.
  45 apply assoc_plus.
  46 qed.
  47
  48 (* same problem with symmetric: see plus
  49 theorem symmetric_times : symmetric nat times. *)
  50
  51 theorem sym_times :
  52 \forall n,m:nat.n*m = m*n.
  53 intros.elim n.
  54 simplify.apply times_n_O.
  55 simplify.rewrite > H.apply times_n_Sm.
  56 qed.
  57
  58 theorem distributive_times_plus : distributive nat times plus.
  59 simplify.
  60 intros.elim x.
  61 simplify.reflexivity.
  62 simplify.rewrite > H. rewrite > assoc_plus.rewrite > assoc_plus.
  63 apply eq_f.rewrite < assoc_plus. rewrite < sym_plus ? z.
  64 rewrite > assoc_plus.reflexivity.
  65 qed.
  66
  67 variant times_plus_distr: \forall n,m,p:nat. n*(m+p)=n*m+n*p
  68 \def distributive_times_plus.
  69