matita/matita/contribs/lambdadelta/ground/arith/ynat_le_lminus_plus.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/arith/nat_le_minus_plus.ma".
  16 include "ground/arith/ynat_lminus_plus.ma".
  17 include "ground/arith/ynat_le_plus.ma".
  18 include "ground/arith/ynat_le_lminus.ma".
  19
  20 (* ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY ****************************)
  21
  22 (* Constructions with ylminus and yplus *************************************)
  23
  24 (*** yle_plus1_to_minus_inj2 *)
  25 lemma yle_plus_sn_dx_lminus_dx (n) (x) (z):
  26       x + yinj_nat n ≤ z → x ≤ z - n.
  27 #n #x #z #H
  28 lapply (yle_lminus_bi_dx n … H) -H //
  29 qed.
  30
  31 (*** yle_plus1_to_minus_inj1 *)
  32 lemma yle_plus_sn_sn_lminus_dx (n) (x) (z):
  33       yinj_nat n + x ≤ z → x ≤ z - n.
  34 /2 width=1 by yle_plus_sn_dx_lminus_dx/ qed.
  35
  36 (*** yle_plus2_to_minus_inj2 *)
  37 lemma yle_plus_dx_dx_lminus_sn (o) (x) (y):
  38       x ≤ y + yinj_nat o → x - o ≤ y.
  39 /2 width=1 by yle_lminus_bi_dx/ qed.
  40
  41 (*** yle_plus2_to_minus_inj1 *)
  42 lemma yle_plus_dx_sn_lminus_sn (o) (x) (y):
  43       x ≤ yinj_nat o + y → x - o ≤ y.
  44 /2 width=1 by yle_plus_dx_dx_lminus_sn/ qed.
  45
  46 (* Destructions with ylminus and yplus **************************************)
  47
  48 (*** yplus_minus_comm_inj *)
  49 lemma ylminus_plus_comm_23 (n) (x) (z):
  50       yinj_nat n ≤ x → x - n + z = x + z - n.
  51 #n #x @(ynat_split_nat_inf … x) -x //
  52 #m #z #Hnm @(ynat_split_nat_inf … z) -z
  53 [ #o <ylminus_inj_sn <yplus_inj_bi <yplus_inj_bi <ylminus_inj_sn
  54   <nminus_plus_comm_23 /2 width=1 by yle_inv_inj_bi/
  55 | <yplus_inf_dx <yplus_inf_dx //
  56 ]
  57 qed-.
  58
  59 (*** yplus_minus_assoc_inj *)
  60 lemma yplus_lminus_assoc (o) (x) (y):
  61       yinj_nat o ≤ y → x + y - o = x + (y - o).
  62 #o #x @(ynat_split_nat_inf … x) -x //
  63 #m #y @(ynat_split_nat_inf … y) -y
  64 [ #n #Hon <ylminus_inj_sn <yplus_inj_bi <yplus_inj_bi
  65   <nplus_minus_assoc /2 width=1 by yle_inv_inj_bi/
  66 | #_ <ylminus_inf_sn //
  67 ]
  68 qed-.
  69
  70 (*** yplus_minus_assoc_comm_inj *)
  71 lemma ylminus_assoc_comm_23 (n) (o) (x):
  72       n ≤ o → x + yinj_nat n - o = x - (o - n).
  73 #n #o #x @(ynat_split_nat_inf … x) -x
  74 [ #m #Hno <ylminus_inj_sn <yplus_inj_bi <ylminus_inj_sn
  75   <nminus_assoc_comm_23 //
  76 | #_ <ylminus_inf_sn <yplus_inf_sn //
  77 ]
  78 qed-.
  79
  80 (* Inversions with ylminus and yplus ****************************************)
  81
  82 (*** yminus_plus *)
  83 lemma yplus_lminus_sn_refl_sn (n) (x):
  84       yinj_nat n ≤ x → x = x - n + yinj_nat n.
  85 /2 width=1 by ylminus_plus_comm_23/ qed-.
  86
  87 lemma yplus_lminus_dx_refl_sn (n) (x):
  88       yinj_nat n ≤ x → x = yinj_nat n + (x - n).
  89 /2 width=1 by yplus_lminus_sn_refl_sn/ qed-.
  90
  91 (*** yplus_inv_minus *)
  92 lemma eq_inv_yplus_bi_inj_md (n1) (m2) (x1) (y2):
  93       yinj_nat n1 ≤ x1 → x1 + yinj_nat m2 = yinj_nat n1 + y2 →
  94       ∧∧ x1 - n1 = y2 - m2 & yinj_nat m2 ≤ y2.
  95 #n1 #m2 #x1 #y2 #Hnx1 #H12
  96 lapply (yle_plus_bi_dx (yinj_nat m2) … Hnx1) >H12 #H
  97 lapply (yle_inv_plus_bi_sn_inj … H) -H #Hmy2
  98 generalize in match H12; -H12 (* * rewrite in hyp *)
  99 >(yplus_lminus_sn_refl_sn … Hmy2) in ⊢ (%→?); <yplus_assoc #H
 100 lapply (eq_inv_yplus_bi_dx_inj … H) -H
 101 >(yplus_lminus_dx_refl_sn … Hnx1) in ⊢ (%→?); -Hnx1 #H
 102 lapply (eq_inv_yplus_bi_sn_inj … H) -H #H12
 103 /2 width=1 by conj/
 104 qed-.
 105
 106 (*** yle_inv_plus_inj2 yle_inv_plus_inj_dx *)
 107 lemma yle_inv_plus_sn_inj_dx (n) (x) (z):
 108       x + yinj_nat n ≤ z →
 109       ∧∧ x ≤ z - n & yinj_nat n ≤ z.
 110 /3 width=3 by yle_plus_sn_dx_lminus_dx, yle_trans, conj/
 111 qed-.
 112
 113 (*** yle_inv_plus_inj1 *)
 114 lemma yle_inv_plus_sn_inj_sn (n) (x) (z):
 115       yinj_nat n + x ≤ z →
 116       ∧∧ x ≤ z - n & yinj_nat n ≤ z.
 117 /2 width=1 by yle_inv_plus_sn_inj_dx/ qed-.