]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/arith/ynat_lt.ma
update in delayed_updating
[helm.git] / 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-.