matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le.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/ynat_le.ma".
  16 include "ground/arith/ynat_lt.ma".
  17
  18 (* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
  19
  20 (* Constructions with yle ***************************************************)
  21
  22 (*** yle_split_eq *)
  23 lemma yle_split_lt_eq (x) (y):
  24       x ≤ y → ∨∨ x < y | x = y.
  25 #x #y * -x -y
  26 [ #m #n #Hmn elim (nle_split_lt_eq … Hmn) -Hmn
  27   /3 width=1 by or_introl, ylt_inj/
  28 | #x @(ynat_split_nat_inf … x) -x
  29  /2 width=1 by or_introl, ylt_inf/
  30 ]
  31 qed-.
  32
  33 (*** ylt_split *)
  34 lemma ynat_split_lt_ge (x) (y): ∨∨ x < y | y ≤ x.
  35 #x #y elim (ynat_split_le_ge x y) /2 width=1 by or_intror/
  36 #H elim (yle_split_lt_eq … H) -H /2 width=1 by or_introl, or_intror/
  37 qed-.
  38
  39 (*** ylt_split_eq *)
  40 lemma ynat_split_lt_eq_gt (x) (y): ∨∨ x < y | y = x | y < x.
  41 #x #y elim (ynat_split_lt_ge x y) /2 width=1 by or3_intro0/
  42 #H elim (yle_split_lt_eq … H) -H /2 width=1 by or3_intro1, or3_intro2/
  43 qed-.
  44
  45 (*** ylt_yle_trans *)
  46 lemma ylt_yle_trans (x) (y) (z): y ≤ z → x < y → x < z.
  47 #x #y #z * -y -z
  48 [ #n #o #Hno #H elim (ylt_inv_inj_dx … H) -H
  49   #m #Hmn #H destruct /3 width=3 by ylt_inj, nlt_nle_trans/
  50 | #y /2 width=2 by ylt_des_lt_inf_dx/
  51 ]
  52 qed-.
  53
  54 (*** yle_ylt_trans *)
  55 lemma yle_ylt_trans (x) (y) (z): y < z → x ≤ y → x < z.
  56 #x #y #z * -y -z
  57 [ #n #o #Hno #H elim (yle_inv_inj_dx … H) -H
  58   #m #Hmn #H destruct /3 width=3 by ylt_inj, nle_nlt_trans/
  59 | #n #H elim (yle_inv_inj_dx … H) -H #m #_ #H destruct //
  60 ]
  61 qed-.
  62
  63 (*** le_ylt_trans *)
  64 lemma nle_ylt_trans (m) (n) (z):
  65       m ≤ n → yinj_nat n < z → yinj_nat m < z.
  66 /3 width=3 by yle_ylt_trans, yle_inj/ qed-.
  67
  68 (* Inversions with yle ******************************************************)
  69
  70 (*** ylt_yle_false *)
  71 lemma ylt_ge_false (x) (y): x < y → y ≤ x → ⊥.
  72 /3 width=4 by yle_ylt_trans, ylt_inv_refl/ qed-.
  73
  74 (* Destructions with yle ****************************************************)
  75
  76 (*** ylt_fwd_le *)
  77 lemma ylt_des_le (x) (y): x < y → x ≤ y.
  78 #x #y * -x -y
  79 /3 width=1 by nlt_des_le, yle_inj/
  80 qed-.
  81
  82 (* Eliminations *************************************************************)
  83
  84 (*** ynat_ind_lt_le_aux *)
  85 lemma ynat_ind_lt_le_inj_dx (Q:predicate …):
  86       (∀y. (∀x. x < y → Q x) → Q y) →
  87       ∀n,x. x ≤ yinj_nat n → Q x.
  88 #Q #IH #n #x #H
  89 elim (yle_inv_inj_dx … H) -H #m #Hmn #H destruct
  90 @(nat_ind_lt_le … Hmn) -Hmn #n0 #IH0
  91 @IH -IH #x #H
  92 elim (ylt_inv_inj_dx … H) -H #m0 #Hmn0 #H destruct
  93 /2 width=1 by/
  94 qed-.
  95
  96 (*** ynat_ind_lt_aux *)
  97 lemma ynat_ind_lt_inj (Q:predicate …):
  98       (∀y. (∀x. x < y → Q x) → Q y) →
  99       ∀n. Q (yinj_nat n).
 100 /4 width=2 by ynat_ind_lt_le_inj_dx/ qed-.
 101
 102 (*** ynat_ind_lt *)
 103 lemma ynat_ind_lt (Q:predicate …):
 104       (∀y. (∀x. x < y → Q x) → Q y) →
 105       ∀y. Q y.
 106 #Q #IH #y @(ynat_split_nat_inf … y) -y
 107 [ /4 width=1 by ynat_ind_lt_inj/
 108 | @IH #x #H
 109   elim (ylt_des_gen_sn … H) -H #m #H destruct
 110   /4 width=1 by ynat_ind_lt_inj/
 111 ]
 112 qed-.