matita/matita/contribs/lambdadelta/ground/lib/arith_2a.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 "ground/lib/arith.ma".
  16
  17 (* ARITHMETICAL PROPERTIES FOR λδ-2B ****************************************)
  18
  19 (* Equalities ***************************************************************)
  20
  21 lemma plus_n_2: ∀n. n + 2 = n + 1 + 1.
  22 // qed.
  23
  24 lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b.
  25 #a #b #c1 #H >minus_minus_comm >minus_le_minus_minus_comm //
  26 qed-.
  27
  28 lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b.
  29 #a #b #c1 #c2 #H >minus_plus >minus_plus >minus_plus /2 width=1 by arith_b1/
  30 qed-.
  31
  32 lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b.
  33 /3 by monotonic_le_minus_l, le_to_le_to_eq, le_n/ qed.
  34
  35 lemma arith_h1: ∀a1,a2,b,c1. c1 ≤ a1 → c1 ≤ b →
  36                 a1 - c1 + a2 - (b - c1) = a1 + a2 - b.
  37 #a1 #a2 #b #c1 #H1 #H2 >plus_minus /2 width=1 by arith_b2/
  38 qed-.
  39
  40 lemma arith_i: ∀x,y,z. y < x → x+z-y-1 = x-y-1+z.
  41 /2 width=1 by plus_minus/ qed-.
  42
  43 (* Properties ***************************************************************)
  44
  45 fact le_repl_sn_conf_aux: ∀x,y,z:nat. x ≤ z → x = y → y ≤ z.
  46 // qed-.
  47
  48 fact le_repl_sn_trans_aux: ∀x,y,z:nat. x ≤ z → y = x → y ≤ z.
  49 // qed-.
  50
  51 lemma arith_j: ∀x,y,z. x-y-1 ≤ x-(y-z)-1.
  52 /3 width=1 by monotonic_le_minus_l, monotonic_le_minus_r/ qed.
  53
  54 lemma arith_k_sn: ∀z,x,y,n. z < x → x+n ≤ y → x-z-1+n ≤ y-z-1.
  55 #z #x #y #n #Hzx #Hxny
  56 >plus_minus [2: /2 width=1 by monotonic_le_minus_r/ ]
  57 >plus_minus [2: /2 width=1 by lt_to_le/ ]
  58 /2 width=1 by monotonic_le_minus_l2/
  59 qed.
  60
  61 lemma arith_k_dx: ∀z,x,y,n. z < x → y ≤ x+n → y-z-1 ≤ x-z-1+n.
  62 #z #x #y #n #Hzx #Hyxn
  63 >plus_minus [2: /2 width=1 by monotonic_le_minus_r/ ]
  64 >plus_minus [2: /2 width=1 by lt_to_le/ ]
  65 /2 width=1 by monotonic_le_minus_l2/
  66 qed.
  67
  68 (* Inversion & forward lemmas ***********************************************)
  69
  70 lemma lt_plus_SO_to_le: ∀x,y. x < y + 1 → x ≤ y.
  71 /2 width=1 by monotonic_pred/ qed-.
  72
  73 (* Iterators ****************************************************************)
  74
  75 lemma iter_SO: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^(l+1) b = f (f^l b).
  76 #B #f #b #l >commutative_plus //
  77 qed.