helm/software/matita/contribs/library_auto/auto/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/library_autobatch/nat/times".
  16
  17 include "auto/nat/plus.ma".
  18
  19 let rec times n m \def
  20  match n with
  21  [ O \Rightarrow O
  22  | (S p) \Rightarrow m+(times p m) ].
  23
  24 interpretation "natural times" 'times x y = (times x y).
  25
  26 theorem times_n_O: \forall n:nat. O = n*O.
  27 intros.elim n
  28 [ autobatch
  29   (*simplify.
  30   reflexivity.*)
  31 | simplify.  (* qui autobatch non funziona: Uncaught exception: Invalid_argument ("List.map2")*)
  32   assumption.
  33 ]
  34 qed.
  35
  36 theorem times_n_Sm :
  37 \forall n,m:nat. n+(n*m) = n*(S m).
  38 intros.elim n
  39 [ autobatch.
  40   (*simplify.reflexivity.*)
  41 | simplify.
  42   autobatch
  43   (*apply eq_f.
  44   rewrite < H.
  45   transitivity ((n1+m)+n1*m)
  46  [ symmetry.
  47    apply assoc_plus.
  48  | transitivity ((m+n1)+n1*m)
  49    [ apply eq_f2.
  50      apply sym_plus.
  51      reflexivity.
  52    | apply assoc_plus.
  53    ]
  54  ]*)
  55 ]
  56 qed.
  57
  58 (* NOTA:
  59    se non avessi semplificato con autobatch tutto il secondo ramo della tattica
  60    elim n, avrei comunque potuto risolvere direttamente con autobatch entrambi
  61    i rami generati dalla prima applicazione della tattica transitivity
  62    (precisamente transitivity ((n1+m)+n1*m)
  63  *)
  64
  65 theorem times_n_SO : \forall n:nat. n = n * S O.
  66 intros.
  67 rewrite < times_n_Sm.
  68 autobatch paramodulation. (*termina la dim anche solo con autobatch*)
  69 (*rewrite < times_n_O.
  70 rewrite < plus_n_O.
  71 reflexivity.*)
  72 qed.
  73
  74 theorem times_SSO_n : \forall n:nat. n + n = S (S O) * n.
  75 intros.
  76 simplify.
  77 autobatch paramodulation. (* termina la dim anche solo con autobatch*)
  78 (*rewrite < plus_n_O.
  79 reflexivity.*)
  80 qed.
  81
  82 theorem symmetric_times : symmetric nat times.
  83 unfold symmetric.
  84 intros.elim x
  85 [ autobatch
  86   (*simplify.apply times_n_O.*)
  87 | simplify.
  88   autobatch
  89   (*rewrite > H.apply times_n_Sm.*)
  90 ]
  91 qed.
  92
  93 variant sym_times : \forall n,m:nat. n*m = m*n \def
  94 symmetric_times.
  95
  96 theorem distributive_times_plus : distributive nat times plus.
  97 unfold distributive.
  98 intros.elim x;simplify
  99 [ reflexivity.
 100 | autobatch
 101   (*rewrite > H.
 102   rewrite > assoc_plus.
 103   rewrite > assoc_plus.
 104   apply eq_f.
 105   rewrite < assoc_plus.
 106   rewrite < (sym_plus ? z).
 107   rewrite > assoc_plus.
 108   reflexivity.*)
 109 ]
 110 qed.
 111
 112 variant distr_times_plus: \forall n,m,p:nat. n*(m+p) = n*m + n*p
 113 \def distributive_times_plus.
 114
 115 theorem associative_times: associative nat times.
 116 unfold associative.intros.
 117 elim x;simplify
 118 [ apply refl_eq
 119 | autobatch
 120   (*rewrite < sym_times.
 121   rewrite > distr_times_plus.
 122   rewrite < sym_times.
 123   rewrite < (sym_times (times n y) z).
 124   rewrite < H.
 125   apply refl_eq.*)
 126 ]
 127 qed.
 128
 129 variant assoc_times: \forall n,m,p:nat. (n*m)*p = n*(m*p) \def
 130 associative_times.