matita/matita/lib/lambda-delta/ground.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "basics/list.ma".
  13 include "lambda-delta/xoa_defs.ma".
  14 include "lambda-delta/xoa_notation.ma".
  15
  16 (* ARITHMETICAL PROPERTIES **************************************************)
  17
  18 lemma plus_plus_comm_23: ∀m,n,p. m + n + p = m + p + n.
  19 // qed.
  20
  21 lemma minus_plus_comm: ∀a,b,c. a - b - c = a - (c + b).
  22 // qed.
  23
  24 lemma arith8: ∀a,b. a < a + b + 1.
  25 // qed.
  26
  27 lemma arith9: ∀a,b,c. c < a + (b + c + 1) + 1.
  28 // qed.
  29
  30 lemma minus_le: ∀m,n. m - n ≤ m.
  31 /2/ qed.
  32
  33 lemma plus_plus_minus_m_m: ∀e1,e2,d. e1 ≤ e2 → d + e1 + (e2 - e1) = d + e2.
  34 /2/ qed.
  35
  36 lemma le_O_to_eq_O: ∀n. n ≤ 0 → n = 0.
  37 /2/ qed.
  38
  39 lemma plus_le_minus: ∀a,b,c. a + b ≤ c → a ≤ c - b.
  40 /2/ qed.
  41
  42 lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → (m + n) - p = (m - p) + n.
  43 #n #m #p #lepm @plus_to_minus <associative_plus
  44 >(commutative_plus p) <plus_minus_m_m //
  45 qed.
  46
  47 lemma le_plus_minus: ∀a,b,c. c ≤ b → a + b - c = a + (b - c).
  48 /2/ qed.
  49
  50 lemma minus_le_minus_minus_comm: ∀m,p,n.
  51                                  p ≤ m → m - p ≤ n → n + p - m = n - (m - p).
  52 #m elim m -m
  53 [ #p #n #H >(le_O_to_eq_O … H) -H //
  54 | #m #IHm #p elim p -p //
  55   #p #_ #n #Hpm <plus_n_Sm @IHm /2/
  56 ]
  57 qed.
  58
  59 lemma lt_refl_false: ∀n. n < n → False.
  60 #n #H elim (lt_to_not_eq … H) -H /2/
  61 qed.
  62
  63 lemma lt_zero_false: ∀n. n < 0 → False.
  64 #n #H elim (lt_to_not_le … H) -H /2/
  65 qed.
  66
  67 lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
  68 #m #n elim (decidable_lt m n) /3/
  69 qed.
  70
  71 lemma plus_lt_false: ∀m,n. m + n < m → False.
  72 #m #n #H1 lapply (le_plus_n_r n m) #H2
  73 lapply (le_to_lt_to_lt … H2 H1) -H2 H1 #H
  74 elim (lt_refl_false … H)
  75 qed.
  76
  77 lemma plus_S_eq_O_false: ∀n,m. n + S m = 0 → False.
  78 #n #m <plus_n_Sm #H destruct
  79 qed.
  80
  81 lemma minus_minus_comm: ∀a,b,c. a - b - c = a - c - b.
  82 /3/ qed.
  83
  84 lemma arith1: ∀n,h,m,p. n + h + m ≤ p + h → n + m ≤ p.
  85 /2/ qed.
  86
  87 lemma arith6: ∀m,n. m < n → n - (n - m - 1) = m + 1.
  88 #m #n #H >minus_plus <minus_minus //
  89 qed.
  90
  91 lemma arith4: ∀h,d,e1,e2. d ≤ e1 + e2 → d + h ≤ e1 + h + e2.
  92 /2/ qed.
  93
  94 lemma arith5: ∀i,h,d. i + h ≤ d → d - i - h + (i + h) = d.
  95 /2/ qed.
  96
  97 lemma arith7: ∀i,d. i ≤ d → d - i + i = d.
  98 /2/ qed.
  99
 100 lemma arith2: ∀j,i,e,d. d + e ≤ i → d ≤ i - e + j.
 101 /3/ qed.
 102
 103 lemma arith3: ∀m,n,p. p ≤ m → m + n - (m - p + n) = p.
 104 /3/ qed.
 105