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