matita/library_auto/auto/nat/le_arith.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/le_arith".
  16
  17 include "auto/nat/times.ma".
  18 include "auto/nat/orders.ma".
  19
  20 (* plus *)
  21 theorem monotonic_le_plus_r:
  22 \forall n:nat.monotonic nat le (\lambda m.n + m).
  23 simplify.intros.
  24 elim n;simplify
  25 [ assumption
  26 | auto
  27   (*apply le_S_S.assumption*)
  28 ]
  29 qed.
  30
  31 theorem le_plus_r: \forall p,n,m:nat. n \le m \to p + n \le p + m
  32 \def monotonic_le_plus_r.
  33
  34 theorem monotonic_le_plus_l:
  35 \forall m:nat.monotonic nat le (\lambda n.n + m).
  36 simplify.intros.
  37  (*rewrite < sym_plus.
  38  rewrite < (sym_plus m).*)
  39  applyS le_plus_r.
  40  assumption.
  41 qed.
  42
  43 (* IN ALTERNATIVA:
  44
  45 theorem monotonic_le_plus_l:
  46 \forall m:nat.monotonic nat le (\lambda n.n + m).
  47 simplify.intros.
  48  rewrite < sym_plus.
  49  rewrite < (sym_plus m).
  50  auto.
  51 qed.
  52 *)
  53 theorem le_plus_l: \forall p,n,m:nat. n \le m \to n + p \le m + p
  54 \def monotonic_le_plus_l.
  55
  56 theorem le_plus: \forall n1,n2,m1,m2:nat. n1 \le n2  \to m1 \le m2
  57 \to n1 + m1 \le n2 + m2.
  58 intros.
  59 auto.
  60 (*apply (trans_le ? (n2 + m1)).
  61 apply le_plus_l.assumption.
  62 apply le_plus_r.assumption.*)
  63 qed.
  64
  65 theorem le_plus_n :\forall n,m:nat. m \le n + m.
  66 intros.
  67 change with (O+m \le n+m).
  68 auto.
  69 (*apply le_plus_l.
  70   apply le_O_n.*)
  71 qed.
  72
  73 theorem eq_plus_to_le: \forall n,m,p:nat.n=m+p \to m \le n.
  74 intros.
  75 rewrite > H.
  76 rewrite < sym_plus.
  77 apply le_plus_n. (* a questo punto funziona anche: auto.*)
  78 qed.
  79
  80 (* times *)
  81 theorem monotonic_le_times_r:
  82 \forall n:nat.monotonic nat le (\lambda m. n * m).
  83 simplify.intros.elim n;simplify
  84 [ apply le_O_n.
  85 | auto.
  86 (*apply le_plus;
  87   assumption. *) (* chiudo entrambi i goal attivi in questo modo*)
  88 ]
  89 qed.
  90
  91 theorem le_times_r: \forall p,n,m:nat. n \le m \to p*n \le p*m
  92 \def monotonic_le_times_r.
  93
  94 theorem monotonic_le_times_l:
  95 \forall m:nat.monotonic nat le (\lambda n.n*m).
  96 simplify.intros.
  97 (*rewrite < sym_times.
  98   rewrite < (sym_times m).
  99 *)
 100 applyS le_times_r.
 101 assumption.
 102 qed.
 103
 104 (* IN ALTERNATIVA:
 105 theorem monotonic_le_times_l:
 106 \forall m:nat.monotonic nat le (\lambda n.n*m).
 107 simplify.intros.
 108 rewrite < sym_times.
 109 rewrite < (sym_times m).
 110 auto.
 111 qed.
 112 *)
 113
 114 theorem le_times_l: \forall p,n,m:nat. n \le m \to n*p \le m*p
 115 \def monotonic_le_times_l.
 116
 117 theorem le_times: \forall n1,n2,m1,m2:nat. n1 \le n2  \to m1 \le m2
 118 \to n1*m1 \le n2*m2.
 119 intros.
 120 auto.
 121 (*apply (trans_le ? (n2*m1)).
 122 apply le_times_l.assumption.
 123 apply le_times_r.assumption.*)
 124 qed.
 125
 126 theorem le_times_n: \forall n,m:nat.(S O) \le n \to m \le n*m.
 127 intros.elim H;simplify
 128 [ auto
 129   (*elim (plus_n_O ?).
 130   apply le_n....*)
 131 | auto
 132   (*rewrite < sym_plus.
 133   apply le_plus_n.*)
 134 ]
 135 qed.