matita/matita/contribs/lambdadelta/ground/arith/ynat_lt.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_lt.ma".
  16 include "ground/arith/ynat_nat.ma".
  17
  18 (* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
  19
  20 (*** ylt *)
  21 inductive ylt: relation ynat ≝
  22 | ylt_inj: ∀m,n. m < n → ylt (yinj_nat m) (yinj_nat n)
  23 | ylt_inf: ∀m. ylt (yinj_nat m) (∞)
  24 .
  25
  26 interpretation
  27   "less (non-negative integers with infinity)"
  28   'lt x y = (ylt x y).
  29
  30 (* Basic destructions *******************************************************)
  31
  32 (* ylt_fwd_gen ylt_inv_Y2 *)
  33 lemma ylt_des_gen_sn (x) (y):
  34       x < y → ∃m. x = yinj_nat m.
  35 #x #y * -x -y
  36 /2 width=2 by ex_intro/
  37 qed-.
  38
  39 lemma ylt_des_lt_inf_dx (x) (y): x < y → x < ∞.
  40 #x #y #H
  41 elim (ylt_des_gen_sn … H) -y #m #H destruct //
  42 qed-.
  43
  44 (*** ylt_fwd_lt_O1 *)
  45 lemma ylt_des_lt_zero_sn (x) (y): x < y → 𝟎 < y.
  46 #x #y * -x -y
  47 /3 width=2 by ylt_inf, ylt_inj, nlt_des_lt_zero_sn/
  48 qed-.
  49
  50 (* Basic inversions *********************************************************)
  51
  52 (*** ylt_inv_inj2 *)
  53 lemma ylt_inv_inj_dx (x) (n):
  54       x < yinj_nat n →
  55       ∃∃m. m < n & x = yinj_nat m.
  56 #x #n0 @(insert_eq_1 … (yinj_nat n0))
  57 #y * -x -y
  58 [ #m #n #Hmn #H >(eq_inv_yinj_nat_bi … H) -n0
  59   /2 width=3 by ex2_intro/
  60 | #m0 #H elim (eq_inv_yinj_nat_inf … H)
  61 ]
  62 qed-.
  63
  64 (*** ylt_inv_inj *)
  65 lemma ylt_inv_inj_bi (m) (n):
  66       yinj_nat m < yinj_nat n → m < n.
  67 #m #n #H elim (ylt_inv_inj_dx … H) -H
  68 #x #Hx #H >(eq_inv_yinj_nat_bi … H) -m //
  69 qed-.
  70
  71 (*** ylt_inv_Y1 *)
  72 lemma ylt_inv_inf_sn (y): ∞ < y → ⊥.
  73 #y #H elim (ylt_des_gen_sn … H) -H
  74 #n #H elim (eq_inv_inf_yinj_nat … H)
  75 qed-.
  76
  77 lemma ylt_inv_refl (x): x < x → ⊥.
  78 #x @(ynat_split_nat_inf … x) -x
  79 /3 width=2 by ylt_inv_inf_sn, ylt_inv_inj_bi, nlt_inv_refl/
  80 qed-.
  81
  82 (* Main constructions *******************************************************)
  83
  84 (*** ylt_trans *)
  85 theorem ylt_trans: Transitive … ylt.
  86 #x #y * -x -y
  87 [ #m #n #Hxy #z @(ynat_split_nat_inf … z) -z
  88   /4 width=3 by ylt_inv_inj_bi, ylt_inj, nlt_trans/
  89 | #m #z #H elim (ylt_inv_inf_sn … H)
  90 ]
  91 qed-.
  92
  93 (*** lt_ylt_trans *)
  94 lemma lt_ylt_trans (m) (n) (z):
  95       m < n → yinj_nat n < z → yinj_nat m < z.
  96 /3 width=3 by ylt_trans, ylt_inj/
  97 qed-.