matita/matita/contribs/lambda_delta/Ground_2/arith.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "arithmetics/nat.ma".
  16 include "Ground_2/star.ma".
  17
  18 (* ARITHMETICAL PROPERTIES **************************************************)
  19
  20 (* equations ****************************************************************)
  21
  22 lemma plus_plus_comm_23: ∀x,y,z. x + y + z = x + z + y.
  23 // qed.
  24
  25 lemma le_plus_minus: ∀m,n,p. p ≤ n → m + n - p = m + (n - p).
  26 /2 by plus_minus/ qed.
  27
  28 lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → m + n - p = m - p + n.
  29 /2 by plus_minus/ qed.
  30
  31 lemma minus_minus_comm: ∀a,b,c. a - b - c = a - c - b.
  32  /3 by monotonic_le_minus_l, le_to_le_to_eq/ qed.
  33
  34 lemma minus_le_minus_minus_comm: ∀b,c,a. c ≤ b → a - (b - c) = a + c - b.
  35 #b elim b -b
  36 [ #c #a #H >(le_n_O_to_eq … H) -H //
  37 | #b #IHb #c elim c -c //
  38   #c #_ #a #Hcb
  39   lapply (le_S_S_to_le … Hcb) -Hcb #Hcb
  40   <plus_n_Sm normalize /2 width=1/
  41 ]
  42 qed.
  43
  44 lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b.
  45 #a #b #c1 #H >minus_plus /3 width=1/
  46 qed.
  47
  48 lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b.
  49 #a #b #c1 #c2 #H >minus_plus >minus_plus >minus_plus /2 width=1/
  50 qed.
  51
  52 lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b.
  53 /3 by monotonic_le_minus_l, le_to_le_to_eq, le_n/ qed.
  54
  55 lemma arith_h1: ∀a1,a2,b,c1. c1 ≤ a1 → c1 ≤ b →
  56                 a1 - c1 + a2 - (b - c1) = a1 + a2 - b.
  57 #a1 #a2 #b #c1 #H1 #H2 >plus_minus // /2 width=1/
  58 qed.
  59
  60 (* inversion & forward lemmas ***********************************************)
  61
  62 axiom eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2).
  63
  64 axiom lt_dec: ∀n1,n2. Decidable (n1 < n2).
  65
  66 lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
  67 #m #n elim (decidable_lt m n) /2 width=1/ /3 width=1/
  68 qed-.
  69
  70 lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m.
  71 #m elim m -m
  72 [ * /2 width=1/
  73 | #m #IHm * /2 width=1/
  74   #n elim (IHm n) -IHm #H
  75   [ @or3_intro0 | @or3_intro1 destruct | @or3_intro2 ] // /2 width=1/ (**) (* /3 width=1/ is slow *)
  76 qed-.
  77
  78 lemma le_inv_plus_plus_r: ∀x,y,z. x + z ≤ y + z → x ≤ y.
  79 /2 by le_plus_to_le/ qed-.
  80
  81 lemma le_inv_plus_l: ∀x,y,z. x + y ≤ z → x ≤ z - y ∧ y ≤ z.
  82 /3 width=2/ qed-.
  83
  84 lemma lt_refl_false: ∀n. n < n → False.
  85 #n #H elim (lt_to_not_eq … H) -H /2 width=1/
  86 qed-.
  87
  88 lemma lt_zero_false: ∀n. n < 0 → False.
  89 #n #H elim (lt_to_not_le … H) -H /2 width=1/
  90 qed-.
  91
  92 lemma plus_S_eq_O_false: ∀n,m. n + S m = 0 → False.
  93 #n #m <plus_n_Sm #H destruct
  94 qed-.
  95
  96 lemma plus_lt_false: ∀m,n. m + n < m → False.
  97 #m #n #H1 lapply (le_plus_n_r n m) #H2
  98 lapply (le_to_lt_to_lt … H2 H1) -H2 -H1 #H
  99 elim (lt_refl_false … H)
 100 qed-.
 101
 102 lemma false_lt_to_le: ∀x,y. (x < y → False) → y ≤ x.
 103 #x #y #H elim (decidable_lt x y) /2 width=1/
 104 #Hxy elim (H Hxy)
 105 qed-.
 106
 107 lemma le_fwd_plus_plus_ge: ∀m1,m2. m2 ≤ m1 → ∀n1,n2. m1 + n1 ≤ m2 + n2 → n1 ≤ n2.
 108 #m1 #m2 #H elim H -m1
 109 [ /2 width=2/
 110 | #m1 #_ #IHm1 #n1 #n2 #H @IHm1 /2 width=3/
 111 ]
 112 qed-.