+++ /dev/null
-(* Equalities ***************************************************************)
-
-(*** plus_minus_plus_plus_l *) (**)
-lemma plus_minus_plus_plus_l: ∀z,x,y,h. z + (x + h) - (y + h) = z + x - y.
-#H1 #H2 #H3 #H4
-<nplus_assoc <nminus_plus_dx_bi // qed-.
-
-fact plus_minus_minus_be_aux: ∀i,x,y,z. y ≤ z → z ≤ x → i = z - y → x - z + i = x - y.
-/2 width=1 by plus_minus_minus_be/ qed-.
-
-(* Properties ***************************************************************)
-
-(*** lt_plus_Sn_r *) (**)
-lemma lt_plus_Sn_r: ∀a,x,n. a < a + x + ↑n.
-/2 width=1/ qed-.
-
-lemma monotonic_le_minus_l2: ∀x1,x2,y,z. x1 ≤ x2 → x1 - y - z ≤ x2 - y - z.
-/3 width=1 by monotonic_le_minus_l/ qed.
-
-(* Inversion & forward lemmas ***********************************************)
-
-lemma le_plus_xySz_x_false: ∀y,z,x. x + y + S z ≤ x → ⊥.
-#y #z #x elim x -x /3 width=1 by le_S_S_to_le/
-#H elim (le_plus_xSy_O_false … H)
-qed-.
-
-lemma plus_xySz_x_false: ∀z,x,y. x + y + S z = x → ⊥.
-/2 width=4 by le_plus_xySz_x_false/ qed-.
-
-lemma nat_elim_le_sn (Q:relation …):
- (∀m1,m2. (∀m. m < m2-m1 → Q (m2-m) m2) → m1 ≤ m2 → Q m1 m2) →
- ∀n1,n2. n1 ≤ n2 → Q n1 n2.
-#Q #IH #n1 #n2 #Hn
-<(minus_minus_m_m … Hn) -Hn
-lapply (minus_le n2 n1)
-let d ≝ (n2-n1)
-@(nat_elim1 … d) -d -n1 #d
-@pull_2 #Hd
-<(minus_minus_m_m … Hd) in ⊢ (%→?); -Hd
-let n1 ≝ (n2-d) #IHd
-@IH -IH [| // ] #m #Hn
-/4 width=3 by lt_to_le, lt_to_le_to_lt/
-qed-.
-
-(* Decidability of predicates ***********************************************)
-
-lemma dec_lt (R:predicate nat):
- (∀n. Decidable … (R n)) →
- ∀n. Decidable … (∃∃m. m < n & R m).
-#R #HR #n elim n -n [| #n * ]
-[ @or_intror * /2 width=2 by lt_zero_false/
-| * /4 width=3 by lt_S, or_introl, ex2_intro/
-| #H0 elim (HR n) -HR
- [ /3 width=3 by or_introl, ex2_intro/
- | #Hn @or_intror * #m #Hmn #Hm
- elim (le_to_or_lt_eq … Hmn) -Hmn #H destruct [ -Hn | -H0 ]
- /4 width=3 by lt_S_S_to_lt, ex2_intro/
- ]
-]
-qed-.
-
-lemma dec_min (R:predicate nat):
- (∀n. Decidable … (R n)) → ∀n. R n →
- ∃∃m. m ≤ n & R m & (∀p. p < m → R p → ⊥).
-#R #HR #n
-@(nat_elim1 n) -n #n #IH #Hn
-elim (dec_lt … HR n) -HR [ -Hn | -IH ]
-[ * #p #Hpn #Hp
- elim (IH … Hpn Hp) -IH -Hp #m #Hmp #Hm #HNm
- @(ex3_intro … Hm HNm) -HNm
- /3 width=3 by lt_to_le, le_to_lt_to_lt/
-| /4 width=4 by ex3_intro, ex2_intro/
-]
-qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/notation/functions/two_0.ma".
+include "ground/arith/nat_le_minus_plus.ma".
+include "ground/arith/nat_lt.ma".
+
+(* ARITHMETICAL PROPERTIES FOR λδ-2A ****************************************)
+
+interpretation
+ "zero (non-negative integers)"
+ 'Two = (ninj (psucc punit)).
+
+(* Equalities ***************************************************************)
+
+lemma plus_n_2: ∀n. (n + 𝟐) = n + 𝟏 + 𝟏.
+// qed.
+
+lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b.
+#a #b #c1 #H >nminus_comm <nminus_assoc_comm_23 //
+qed-.
+
+lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b.
+#a #b #c1 #c2 #H
+>(nminus_plus_assoc ? c1 c2) >(nminus_plus_assoc ? c1 c2)
+/2 width=1 by arith_b1/
+qed-.
+
+lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b.
+#x #a #b #c1
+<nplus_plus_comm_23 //
+qed.
+
+lemma arith_h1: ∀a1,a2,b,c1. c1 ≤ a1 → c1 ≤ b →
+ a1 - c1 + a2 - (b - c1) = a1 + a2 - b.
+#a1 #a2 #b #c1 #H1 #H2
+>nminus_plus_comm_23
+/2 width=1 by arith_b1/
+qed-.
+
+lemma arith_i: ∀x,y,z. y < x → x+z-y-(𝟏) = x-y-(𝟏)+z.
+/2 width=1 by nminus_plus_comm_23/ qed-.
+
+(* Constructions ************************************************************)
+
+fact le_repl_sn_conf_aux: ∀x,y,z:nat. x ≤ z → x = y → y ≤ z.
+// qed-.
+
+fact le_repl_sn_trans_aux: ∀x,y,z:nat. x ≤ z → y = x → y ≤ z.
+// qed-.
+
+lemma monotonic_le_minus_l2: ∀x1,x2,y,z. x1 ≤ x2 → x1 - y - z ≤ x2 - y - z.
+/3 width=1 by nle_minus_bi_dx/ qed.
+
+lemma arith_j: ∀x,y,z. x-y-(𝟏) ≤ x-(y-z)-𝟏.
+/3 width=1 by nle_minus_bi_dx, nle_minus_bi_sn/ qed.
+
+lemma arith_k_sn: ∀z,x,y,n. z < x → x+n ≤ y → x-z-(𝟏)+n ≤ y-z-𝟏.
+#z #x #y #n #Hzx #Hxny
+>nminus_plus_comm_23 [2: /2 width=1 by nle_minus_bi_sn/ ]
+>nminus_plus_comm_23 [2: /2 width=1 by nlt_des_le/ ]
+/2 width=1 by monotonic_le_minus_l2/
+qed.
+
+lemma arith_k_dx: ∀z,x,y,n. z < x → y ≤ x+n → y-z-(𝟏) ≤ x-z-(𝟏)+n.
+#z #x #y #n #Hzx #Hyxn
+>nminus_plus_comm_23 [2: /2 width=1 by nle_minus_bi_sn/ ]
+>nminus_plus_comm_23 [2: /2 width=1 by nlt_des_le/ ]
+/2 width=1 by monotonic_le_minus_l2/
+qed.
+
+(* Inversions ***************************************************************)
+
+lemma lt_plus_SO_to_le: ∀x,y. x < y + (𝟏) → x ≤ y.
+/2 width=1 by nle_inv_succ_bi/ qed-.
+
+(* Iterators ****************************************************************)
+
+lemma iter_SO: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^(l+𝟏) b = f (f^l b).
+#B #f #b #l
+<niter_succ //
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_le_minus_plus.ma".
+
+(* ARITHMETICAL PROPERTIES FOR λδ-2B ****************************************)
+
+lemma arith_l4 (m11) (m12) (m21) (m22):
+ m21+m22-(m11+m12) = m21-m11-m12+(m22-(m11-m21)-(m12-(m21-m11))).
+#m11 #m12 #m21 #m22 >nminus_plus_assoc
+elim (nat_split_le_ge (m11+m12) m21) #Hm1121
+[ lapply (nle_trans m11 ??? Hm1121) // #Hm121
+ lapply (nle_minus_dx_dx … Hm1121) #Hm12211
+ <nminus_plus_comm_23 // @eq_f2 // <(nle_inv_eq_zero_minus m11 ?) // <(nle_inv_eq_zero_minus m12 ?) //
+| <(nle_inv_eq_zero_minus m21 ?) // <nplus_zero_sn <nminus_plus_assoc <nplus_comm
+ elim (nat_split_le_ge m11 m21) #Hm121
+ [ lapply (nle_minus_sn_dx … Hm1121) #Hm2112
+ <(nle_inv_eq_zero_minus m11 ?) // >nplus_minus_assoc // >nminus_assoc_comm_23 //
+ | <(nle_inv_eq_zero_minus m21 ?) // >nminus_assoc_comm_23 //
+ ]
+]
+qed.
+
+lemma arith_l3 (m) (n1) (n2): n1+n2-m = n1-m+(n2-(m-n1)).
+// qed.
+
+lemma arith_l2 (n1) (n2): ↑n2-n1 = 𝟏-n1+(n2-(n1-𝟏)).
+#n1 #n2 <arith_l3 //
+qed.
+
+lemma arith_l1 (n): ninj (𝟏) = 𝟏-n+(n-(n-𝟏)).
+#n <arith_l2 //
+qed.
--- /dev/null
+(* Equalities ***************************************************************)
+
+(*** plus_minus_plus_plus_l *) (**)
+lemma plus_minus_plus_plus_l: ∀z,x,y,h. z + (x + h) - (y + h) = z + x - y.
+#H1 #H2 #H3 #H4
+<nplus_assoc <nminus_plus_dx_bi // qed-.
+
+fact plus_minus_minus_be_aux: ∀i,x,y,z. y ≤ z → z ≤ x → i = z - y → x - z + i = x - y.
+/2 width=1 by plus_minus_minus_be/ qed-.
+
+(* Properties ***************************************************************)
+
+(*** lt_plus_Sn_r *) (**)
+lemma lt_plus_Sn_r: ∀a,x,n. a < a + x + ↑n.
+/2 width=1/ qed-.
+
+(* Inversion & forward lemmas ***********************************************)
+
+lemma le_plus_xySz_x_false: ∀y,z,x. x + y + S z ≤ x → ⊥.
+#y #z #x elim x -x /3 width=1 by le_S_S_to_le/
+#H elim (le_plus_xSy_O_false … H)
+qed-.
+
+lemma plus_xySz_x_false: ∀z,x,y. x + y + S z = x → ⊥.
+/2 width=4 by le_plus_xySz_x_false/ qed-.
+
+lemma nat_elim_le_sn (Q:relation …):
+ (∀m1,m2. (∀m. m < m2-m1 → Q (m2-m) m2) → m1 ≤ m2 → Q m1 m2) →
+ ∀n1,n2. n1 ≤ n2 → Q n1 n2.
+#Q #IH #n1 #n2 #Hn
+<(minus_minus_m_m … Hn) -Hn
+lapply (minus_le n2 n1)
+let d ≝ (n2-n1)
+@(nat_elim1 … d) -d -n1 #d
+@pull_2 #Hd
+<(minus_minus_m_m … Hd) in ⊢ (%→?); -Hd
+let n1 ≝ (n2-d) #IHd
+@IH -IH [| // ] #m #Hn
+/4 width=3 by lt_to_le, lt_to_le_to_lt/
+qed-.
+
+(* Decidability of predicates ***********************************************)
+
+lemma dec_lt (R:predicate nat):
+ (∀n. Decidable … (R n)) →
+ ∀n. Decidable … (∃∃m. m < n & R m).
+#R #HR #n elim n -n [| #n * ]
+[ @or_intror * /2 width=2 by lt_zero_false/
+| * /4 width=3 by lt_S, or_introl, ex2_intro/
+| #H0 elim (HR n) -HR
+ [ /3 width=3 by or_introl, ex2_intro/
+ | #Hn @or_intror * #m #Hmn #Hm
+ elim (le_to_or_lt_eq … Hmn) -Hmn #H destruct [ -Hn | -H0 ]
+ /4 width=3 by lt_S_S_to_lt, ex2_intro/
+ ]
+]
+qed-.
+
+lemma dec_min (R:predicate nat):
+ (∀n. Decidable … (R n)) → ∀n. R n →
+ ∃∃m. m ≤ n & R m & (∀p. p < m → R p → ⊥).
+#R #HR #n
+@(nat_elim1 n) -n #n #IH #Hn
+elim (dec_lt … HR n) -HR [ -Hn | -IH ]
+[ * #p #Hpn #Hp
+ elim (IH … Hpn Hp) -IH -Hp #m #Hmp #Hm #HNm
+ @(ex3_intro … Hm HNm) -HNm
+ /3 width=3 by lt_to_le, le_to_lt_to_lt/
+| /4 width=4 by ex3_intro, ex2_intro/
+]
+qed-.
+++ /dev/null
-"cic:/matita/arithmetics/nat/nat_discr.con"
-"cic:/matita/arithmetics/nat/times.con"
-"cic:/matita/arithmetics/nat/times_n_1.con"
-"cic:/matita/arithmetics/nat/times_Sn_m.con"
-"cic:/matita/arithmetics/nat/leb.con"
-"cic:/matita/arithmetics/nat/leb_elim.con"
-"cic:/matita/arithmetics/nat/le_to_leb_true.con"
-"cic:/matita/arithmetics/nat/not_le_to_leb_false.con"
--- /dev/null
+"cic:/matita/arithmetics/nat/nat_discr.con"
+"cic:/matita/arithmetics/nat/times.con"
+"cic:/matita/arithmetics/nat/times_n_1.con"
+"cic:/matita/arithmetics/nat/times_Sn_m.con"
+"cic:/matita/arithmetics/nat/leb.con"
+"cic:/matita/arithmetics/nat/leb_elim.con"
+"cic:/matita/arithmetics/nat/le_to_leb_true.con"
+"cic:/matita/arithmetics/nat/not_le_to_leb_false.con"
lemma niter_zero (A) (f) (a): a = (f^{A}𝟎) a.
// qed.
-lemma niter_inj (A) (f) (p) (a): f^p a = f^{A}(ninj p) a.
+lemma niter_inj (A) (f) (p): f^p ≐ f^{A}(ninj p).
// qed.
(* Advanced constructions ***************************************************)
(*** iter_n_Sm *)
-lemma niter_appl (A) (f) (n) (a): f (f^n a) = f^{A}n (f a).
+lemma niter_appl (A) (f) (n): f ∘ f^n ≐ f^{A}n ∘ f.
#A #f * //
-#p #a <niter_inj <niter_inj <piter_appl //
+#p @exteq_repl
+/2 width=5 by piter_appl, compose_repl_fwd_dx/
+qed.
+
+lemma niter_compose (A) (B) (f) (g) (h) (n):
+ h ∘ f ≐ g ∘ h → h ∘ (f^{A}n) ≐ (g^{B}n) ∘ h.
+#A #B #f #g #h * //
+#p #H @exteq_repl
+/2 width=5 by piter_compose, compose_repl_fwd_dx/
qed.
(* *)
(**************************************************************************)
-include "ground/insert_eq/insert_eq_0.ma".
+include "ground/insert_eq/insert_eq_1.ma".
include "ground/arith/nat_succ.ma".
(* ORDER FOR NON-NEGATIVE INTEGERS ******************************************)
qed.
(*** le_or_ge *)
-lemma nle_ge_dis (m) (n): ∨∨ m ≤ n | n ≤ m.
+lemma nat_split_le_ge (m) (n): ∨∨ m ≤ n | n ≤ m.
#m #n @(nat_ind_2_succ … m n) -m -n
[ /2 width=1 by or_introl/
| /2 width=1 by or_intror/
(*** le_S_S_to_le *)
lemma nle_inv_succ_bi (m) (n): ↑m ≤ ↑n → m ≤ n.
-#m #n @(insert_eq_0 … (↑n))
+#m #n @(insert_eq_1 … (↑n))
#x * -x
[ #H >(eq_inv_nsucc_bi … H) -n //
| #o #Ho #H >(eq_inv_nsucc_bi … H) -n
(*** le_n_O_to_eq *)
lemma nle_inv_zero_dx (m): m ≤ 𝟎 → 𝟎 = m.
-#m @(insert_eq_0 … (𝟎))
+#m @(insert_eq_1 … (𝟎))
#y * -y
[ #H destruct //
| #y #_ #H elim (eq_inv_zero_nsucc … H)
(*** decidable_le le_dec *)
lemma nle_dec (m) (n): Decidable … (m ≤ n).
-#m #n elim (nle_ge_dis m n) [ /2 width=1 by or_introl/ ]
+#m #n elim (nat_split_le_ge m n) [ /2 width=1 by or_introl/ ]
#Hnm elim (eq_nat_dec m n) [ #H destruct /2 width=1 by nle_refl, or_introl/ ]
/4 width=1 by nle_antisym, or_intror/
qed-.
// qed.
(*** inv_eq_minus_O *)
-lemma nle_eq_minus_O (m) (n): 𝟎 = m - n → m ≤ n.
+lemma nle_eq_zero_minus (m) (n): 𝟎 = m - n → m ≤ n.
#m #n @(nat_ind_2_succ … m n) //
/3 width=1 by nle_succ_bi/
qed.
(*** monotonic_le_minus_l *)
-lemma nle_minus_sn_bi (m) (n) (o): m ≤ n → m-o ≤ n-o.
+lemma nle_minus_bi_dx (m) (n) (o): m ≤ n → m-o ≤ n-o.
#m #n #o @(nat_ind_succ … o) -o //
#o #IH #Hmn /3 width=1 by nle_pred_bi/
qed.
(*** monotonic_le_minus_r *)
-lemma nle_minus_dx_bi (m) (n) (o): m ≤ n → o-n ≤ o-m.
+lemma nle_minus_bi_sn (m) (n) (o): m ≤ n → o-n ≤ o-m.
#m #n #o #H elim H -n //
#n #_ #IH /2 width=3 by nle_trans/
qed.
(* Inversions with nminus ***************************************************)
(*** eq_minus_O *)
-lemma nle_inv_eq_minus_O (m) (n): m ≤ n → 𝟎 = m - n.
+lemma nle_inv_eq_zero_minus (m) (n): m ≤ n → 𝟎 = m - n.
#m #n #H elim H -n //
qed-.
(*** le_plus_to_minus *)
lemma nle_minus_sn_sn (o) (m) (n): m ≤ n + o → m - o ≤ n.
-/2 width=1 by nle_minus_sn_bi/ qed.
+/2 width=1 by nle_minus_bi_dx/ qed.
(*** le_plus_to_minus_comm *)
lemma nle_minus_sn_dx (o) (m) (n): m ≤ o + n → m - o ≤ n.
-/2 width=1 by nle_minus_sn_bi/ qed.
+/2 width=1 by nle_minus_bi_dx/ qed.
(*** le_plus_to_minus_r *)
lemma nle_minus_dx_sn (o) (m) (n): m + o ≤ n → m ≤ n - o.
#o #m #n #H >(nminus_plus_sn_refl_sn m o)
-/2 width=1 by nle_minus_sn_bi/
+/2 width=1 by nle_minus_bi_dx/
qed.
(*** le_plus_to_minus_l *)
lemma nle_minus_dx_dx (o) (m) (n): o + m ≤ n → m ≤ n - o.
#o #m #n #H >(nminus_plus_sn_refl_dx m o)
-/2 width=1 by nle_minus_sn_bi/
+/2 width=1 by nle_minus_bi_dx/
qed.
(*** le_inv_plus_l *)
qed-.
(*** minus_le_minus_minus_comm *)
-theorem minus_assoc_comm_23 (m1) (m2) (m3):
+theorem nminus_assoc_comm_23 (m1) (m2) (m3):
m3 ≤ m2 → m1 + m3 - m2 = m1 - (m2 - m3).
#m1 #m2 #m3 #Hm
>(nplus_minus_sn_refl_sn … Hm) in ⊢ (??%?); //
lemma nle_plus_dx_sn_refl (m) (n): m ≤ n + m.
/2 width=1 by nle_plus_bi_sn/ qed.
-(*** le_plus_b *)
-lemma nle_plus_dx_dx (m) (n) (o): n + o ≤ m → n ≤ m.
-/2 width=3 by nle_trans/ qed.
-
(*** le_plus_a *)
lemma nle_plus_dx_sn (m) (n) (o): n ≤ m → n ≤ o + m.
/2 width=3 by nle_trans/ qed.
(* Inversions with nplus ****************************************************)
+(*** le_plus_b *)
+lemma nle_inv_plus_sn_dx (m) (n) (o): n + o ≤ m → n ≤ m.
+/2 width=3 by nle_trans/ qed.
+
(*** plus_le_0 *)
lemma nle_inv_plus_zero (m) (n): m + n ≤ 𝟎 → ∧∧ 𝟎 = m & 𝟎 = n.
/3 width=1 by nle_inv_zero_dx, eq_inv_zero_nplus/ qed-.
lemma nlt_refl_succ (n): n < ↑n.
// qed.
+lemma nlt_succ_dx (m) (n): m ≤ n → m < ↑n.
+/2 width=1 by nle_succ_bi/ qed.
+
(*** lt_S *)
-lemma nlt_succ_dx (m) (n): m < n → m < ↑n.
+lemma nlt_succ_dx_trans (m) (n): m < n → m < ↑n.
/2 width=1 by nle_succ_dx/ qed.
(*** lt_O_S *)
/2 width=1 by nle_succ_bi/ qed.
(*** le_to_or_lt_eq *)
-lemma nle_lt_eq_dis (m) (n): m ≤ n → ∨∨ m < n | m = n.
+lemma nle_split_lt_eq (m) (n): m ≤ n → ∨∨ m < n | m = n.
#m #n * -n /3 width=1 by nle_succ_bi, or_introl/
qed-.
(*** eq_or_gt *)
-lemma eq_gt_dis (n): ∨∨ 𝟎 = n | 𝟎 < n.
-#n elim (nle_lt_eq_dis (𝟎) n ?)
+lemma nat_split_zero_gt (n): ∨∨ 𝟎 = n | 𝟎 < n.
+#n elim (nle_split_lt_eq (𝟎) n ?)
/2 width=1 by or_introl, or_intror/
qed-.
(*** lt_or_ge *)
-lemma nlt_ge_dis (m) (n): ∨∨ m < n | n ≤ m.
-#m #n elim (nle_ge_dis m n) /2 width=1 by or_intror/
-#H elim (nle_lt_eq_dis … H) -H /2 width=1 by nle_refl, or_introl, or_intror/
+lemma nat_split_lt_ge (m) (n): ∨∨ m < n | n ≤ m.
+#m #n elim (nat_split_le_ge m n) /2 width=1 by or_intror/
+#H elim (nle_split_lt_eq … H) -H /2 width=1 by nle_refl, or_introl, or_intror/
qed-.
(*** lt_or_eq_or_gt *)
-lemma nlt_eq_gt_dis (m) (n): ∨∨ m < n | n = m | n < m.
-#m #n elim (nlt_ge_dis m n) /2 width=1 by or3_intro0/
-#H elim (nle_lt_eq_dis … H) -H /2 width=1 by or3_intro1, or3_intro2/
+lemma nat_split_lt_eq_gt (m) (n): ∨∨ m < n | n = m | n < m.
+#m #n elim (nat_split_lt_ge m n) /2 width=1 by or3_intro0/
+#H elim (nle_split_lt_eq … H) -H /2 width=1 by or3_intro1, or3_intro2/
qed-.
(*** not_le_to_lt *)
lemma le_false_nlt (m) (n): (n ≤ m → ⊥) → m < n.
-#m #n elim (nlt_ge_dis m n) [ // ]
+#m #n elim (nat_split_lt_ge m n) [ // ]
#H #Hn elim Hn -Hn //
qed.
(*** lt_to_le_to_lt *)
-lemma nlt_le_trans (o) (m) (n): m < o → o ≤ n → m < n.
+lemma nlt_nle_trans (o) (m) (n): m < o → o ≤ n → m < n.
/2 width=3 by nle_trans/ qed-.
(*** le_to_lt_to_lt *)
-lemma le_nlt_trans (o) (m) (n): m ≤ o → o < n → m < n.
+lemma nle_nlt_trans (o) (m) (n): m ≤ o → o < n → m < n.
/3 width=3 by nle_succ_bi, nle_trans/ qed-.
(* Basic inversions *********************************************************)
+lemma nlt_inv_succ_dx (m) (n): m < ↑n → m ≤ n.
+/2 width=1 by nle_inv_succ_bi/ qed-.
+
(*** lt_S_S_to_lt *)
lemma nlt_inv_succ_bi (m) (n): ↑m < ↑n → m < n.
/2 width=1 by nle_inv_succ_bi/ qed-.
(*** lt_to_not_le lt_le_false *)
lemma nlt_ge_false (m) (n): m < n → n ≤ m → ⊥.
-/3 width=4 by nle_inv_succ_sn_refl, nlt_le_trans/ qed-.
+/3 width=4 by nle_inv_succ_sn_refl, nlt_nle_trans/ qed-.
(*** lt_to_not_eq lt_refl_false *)
lemma nlt_inv_refl (m): m < m → ⊥.
/2 width=3 by nle_trans/ qed-.
(*** ltn_to_ltO *)
-lemma nlt_des_lt_O_sn (m) (n): m < n → 𝟎 < n.
-/3 width=3 by le_nlt_trans/ qed-.
+lemma nlt_des_lt_zero_sn (m) (n): m < n → 𝟎 < n.
+/3 width=3 by nle_nlt_trans/ qed-.
(* Main constructions *******************************************************)
(*** transitive_lt *)
theorem nlt_trans: Transitive … nlt.
-/3 width=3 by nlt_des_le, nlt_le_trans/ qed-.
+/3 width=3 by nlt_des_le, nlt_nle_trans/ qed-.
(* Advanced eliminations ****************************************************)
#Q #H1 #n @(nat_ind_succ … n) -n
[ #m #H <(nle_inv_zero_dx … H) -m
@H1 -H1 #o #H elim (nlt_inv_zero_dx … H)
-| /5 width=3 by nlt_le_trans, nle_inv_succ_bi/
+| /5 width=3 by nlt_nle_trans, nle_inv_succ_bi/
]
qed-.
(* Constructions with nminus ************************************************)
(*** monotonic_lt_minus_l *)
-lemma nlt_minus_sn_bi (o) (m) (n): o ≤ m → m < n → m - o < n - o.
+lemma nlt_minus_bi_dx (o) (m) (n): o ≤ m → m < n → m - o < n - o.
#o #m #n #Hom #Hmn
-lapply (nle_minus_sn_bi … o Hmn) -Hmn
+lapply (nle_minus_bi_dx … o Hmn) -Hmn
<(nminus_succ_sn … Hom) //
qed.
(*** monotonic_lt_minus_r *)
-lemma nlt_minus_dx_bi (o) (m) (n):
+lemma nlt_minus_bi_sn (o) (m) (n):
m < o -> m < n → o-n < o-m.
#o #m #n #Ho #H
-lapply (nle_minus_dx_bi … o H) -H #H
-@(le_nlt_trans … H) -n
+lapply (nle_minus_bi_sn … o H) -H #H
+@(nle_nlt_trans … H) -n
@nlt_i >(nminus_succ_sn … Ho) //
qed.
+(* Inversions with nminus ***************************************************)
+
+lemma nlt_inv_minus_bi_dx (o) (m) (n):
+ m - o < n - o → m < n.
+#o @(nat_ind_succ … o) -o
+/3 width=1 by nlt_inv_pred_bi/
+qed-.
+
(* Destructions with nminus *************************************************)
(*** minus_pred_pred *)
lemma nlt_des_minus_dx (o) (m) (n): m < n - o → o < n.
#o @(nat_ind_succ … o) -o
[ #m #n <nminus_zero_dx
- /2 width=3 by le_nlt_trans/
+ /2 width=3 by nle_nlt_trans/
| #o #IH #m #n <nminus_succ_dx_pred_sn #H
/3 width=2 by nlt_inv_pred_dx/
]
(*** lt_inv_plus_l *)
lemma nlt_minus_dx_full (o) (m) (n): m + o < n → ∧∧ o < n & m < n - o.
-/3 width=3 by nlt_minus_dx, le_nlt_trans, conj/ qed-.
+/3 width=3 by nlt_minus_dx, nle_nlt_trans, conj/ qed-.
(* Inversions with nminus and nplus *****************************************)
lemma nlt_inv_pred_dx (m) (n): m < ↓n → ↑m < n.
#m #n #H >(nlt_des_gen (𝟎) n)
[ /2 width=1 by nlt_succ_bi/
-| /3 width=3 by le_nlt_trans, nlt_le_trans/
+| /3 width=3 by nle_nlt_trans, nlt_nle_trans/
]
qed-.
+lemma nlt_inv_pred_bi (m) (n):
+ ↓m < ↓n → m < n.
+/3 width=3 by nlt_inv_pred_dx, nle_nlt_trans/
+qed-.
+
(* Constructions with npred *************************************************)
lemma nlt_zero_sn (n): n = ↑↓n → 𝟎 < n.
λm,n. npred^n m.
interpretation
- "minus (positive integers)"
+ "minus (non-negative integers)"
'minus m n = (nminus m n).
(* Basic constructions ******************************************************)
theorem nminus_plus_assoc (o) (m) (n): o-m-n = o-(m+n).
#o #m #n @(nat_ind_succ … n) -n //
#n #IH <nplus_succ_dx <nminus_succ_dx <nminus_succ_dx //
-qed-.
+qed.
(*** minus_plus_plus_l *)
lemma nminus_plus_dx_bi (m) (n) (o): m - n = (m + o) - (n + o).
λm,n. nsucc^n m.
interpretation
- "plus (positive integers)"
+ "plus (non-negative integers)"
'plus m n = (nplus m n).
(* Basic constructions ******************************************************)
(* Constructions with niter *************************************************)
(*** iter_plus *)
-lemma niter_plus (A) (f) (a) (n1) (n2):
- f^n1 (f^n2 a) = f^{A}(n1+n2) a.
-#A #f #a #n1 #n2 @(nat_ind_succ … n2) -n2 //
-#n2 #IH <nplus_succ_dx <niter_succ <niter_succ <niter_appl //
+lemma niter_plus (A) (f) (n1) (n2):
+ f^n2 ∘ f^n1 ≐ f^{A}(n1+n2).
+#A #f #n1 #n2 @(nat_ind_succ … n2) -n2 //
+#n2 #IH <nplus_succ_dx
+@exteq_repl
+/3 width=5 by compose_repl_fwd_sn, compose_repl_fwd_dx/
qed.
(* Advanved constructions (semigroup properties) ****************************)
(**************************************************************************)
include "ground/notation/functions/downarrow_1.ma".
-include "ground/arith/pnat_dis.ma".
+include "ground/arith/pnat_split.ma".
include "ground/arith/nat.ma".
(* PREDECESSOR FOR NON-NEGATIVE INTEGERS ************************************)
(*** pred *)
definition npred (m): nat ≝ match m with
[ nzero ⇒ 𝟎
-| ninj p ⇒ pdis … (𝟎) ninj p
+| ninj p ⇒ psplit … (𝟎) ninj p
].
interpretation
(* Inversion with nsucc *****************************************************)
(*** nat_split *)
-lemma nat_split (n): ∨∨ 𝟎 = n | n = ↑↓n.
+lemma nat_split_zero_pos (n): ∨∨ 𝟎 = n | n = ↑↓n.
#n @(nat_ind_succ … n) -n
/2 width=1 by or_introl, or_intror/
qed-.
(* SUCCESSOR FOR NON-NEGATIVE INTEGERS **************************************)
-definition nsucc: nat → nat ≝ λm. match m with
-[ nzero ⇒ ninj (𝟏)
-| ninj p ⇒ ninj (↑p)
+definition nsucc_pos (m): pnat ≝
+match m with
+[ nzero ⇒ 𝟏
+| ninj p ⇒ ↑p
].
+interpretation
+ "positive successor (non-negative integers)"
+ 'UpArrow m = (nsucc_pos m).
+
+definition nsucc (m): nat ≝
+ ninj (↑m).
+
interpretation
"successor (non-negative integers)"
'UpArrow m = (nsucc m).
(* Constructions with niter *************************************************)
(*** iter_S *)
-lemma niter_succ (A) (f) (n) (a): f (f^n a) = f^{A}(↑n) a.
+lemma niter_succ (A) (f) (n): f ∘ f^n ≐ f^{A}(↑n).
#A #f * //
qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground/arith/pnat.ma".
-
-(* DISCRIMINATOR FOR POSITIVE INTEGERS **************************************)
-
-definition pdis (A:Type[0]) (a) (f) (p): A ≝
-match p with
-[ punit ⇒ a
-| psucc q ⇒ f q
-].
(**************************************************************************)
include "ground/notation/functions/exp_3.ma".
+include "ground/lib/exteq.ma".
include "ground/arith/pnat.ma".
(* ITERATED FUNCTION FOR POSITIVE INTEGERS **********************************)
(* Basic constructions ******************************************************)
-lemma piter_unit (A) (f) (a): f a = (f^{A}𝟏) a.
+lemma piter_unit (A) (f): f ≐ f^{A}𝟏.
// qed.
-lemma piter_succ (A) (f) (p) (a): f (f^p a) = f^{A}(↑p) a.
+lemma piter_succ (A) (f) (p): f ∘ f^p ≐ f^{A}(↑p).
// qed.
(* Advanced constructions ***************************************************)
-lemma piter_appl (A) (f) (p) (a): f (f^p a) = f^{A}p (f a).
+lemma piter_appl (A) (f) (p): f ∘ f^p ≐ f^{A}p ∘ f.
#A #f #p elim p -p //
-#p #IH #a <piter_succ <piter_succ //
+#p #IH @exteq_repl
+/3 width=5 by compose_repl_fwd_dx, compose_repl_fwd_sn, exteq_canc_dx/
+qed.
+
+lemma piter_compose (A) (B) (f) (g) (h) (p):
+ h ∘ f ≐ g ∘ h → h ∘ (f^{A}p) ≐ (g^{B}p) ∘ h.
+#A #B #f #g #h #p elim p -p
+[ #H @exteq_repl
+ /2 width=5 by compose_repl_fwd_sn, compose_repl_fwd_dx/
+| #p #IH #H @exteq_repl
+ [4: @compose_repl_fwd_dx [| @piter_succ ]
+ |5: @compose_repl_fwd_sn [| @piter_succ ]
+ |1,2: skip
+ ]
+ @exteq_trans [2: @compose_assoc |1: skip ]
+ @exteq_trans [2: @(compose_repl_fwd_sn … H) | 1:skip ]
+ @exteq_canc_sn [2: @compose_assoc |1: skip ]
+ /3 width=1 by compose_repl_fwd_dx/
+]
qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/pnat.ma".
+
+(* DISCRIMINATOR FOR POSITIVE INTEGERS **************************************)
+
+definition psplit (A:Type[0]) (a) (f) (p): A ≝
+match p with
+[ punit ⇒ a
+| psucc q ⇒ f q
+].
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_lt.ma".
+
+(* WELL-FOUNDED INDUCTION ***************************************************)
+
+fact wf1_ind_nlt_aux (A1) (f:A1→nat) (Q:predicate …):
+ (∀n. (∀a1. f a1 < n → Q a1) → ∀a1. f a1 = n → Q a1) →
+ ∀n,a1. f a1 = n → Q a1.
+#A1 #f #Q #H #n @(nat_ind_lt … n) -n /3 width=3 by/
+qed-.
+
+(*** f_ind *)
+lemma wf1_ind_nlt (A1) (f:A1→nat) (Q:predicate …):
+ (∀n. (∀a1. f a1 < n → Q a1) → ∀a1. f a1 = n → Q a1) →
+ ∀a1. Q a1.
+#A #f #Q #H #a1 @(wf1_ind_nlt_aux … H) -H //
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/ynat_lt_le.ma".
+
+(* WELL-FOUNDED INDUCTION ***************************************************)
+
+(*** ynat_f_ind_aux *)
+fact wf1_ind_ylt_aux (A1) (f:A1→ynat) (Q:predicate …):
+ (∀y. (∀a1. f a1 < y → Q a1) → ∀a1. f a1 = y → Q a1) →
+ ∀y,a1. f a1 = y → Q a1.
+#A1 #f #Q #H #y @(ynat_ind_lt … y) -y /3 width=3 by/
+qed-.
+
+(*** ynat_f_ind *)
+lemma wf1_ind_ylt (A1) (f:A1→ynat) (Q:predicate …):
+ (∀y. (∀a1. f a1 < y → Q a1) → ∀a1. f a1 = y → Q a1) →
+ ∀a1. Q a1.
+#A #f #Q #H #a1 @(wf1_ind_ylt_aux … H) -H //
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_lt.ma".
+
+(* WELL-FOUNDED INDUCTION ***************************************************)
+
+fact wf2_ind_nlt_aux (A1) (A2) (f:A1→A2→nat) (Q:relation2 …):
+ (∀n. (∀a1,a2. f a1 a2 < n → Q a1 a2) → ∀a1,a2. f a1 a2 = n → Q a1 a2) →
+ ∀n,a1,a2. f a1 a2 = n → Q a1 a2.
+#A1 #A2 #f #Q #H #n @(nat_ind_lt … n) -n /3 width=3 by/
+qed-.
+
+(*** f2_ind *)
+lemma wf2_ind_nlt (A1) (A2) (f:A1→A2→nat) (Q:relation2 …):
+ (∀n. (∀a1,a2. f a1 a2 < n → Q a1 a2) → ∀a1,a2. f a1 a2 = n → Q a1 a2) →
+ ∀a1,a2. Q a1 a2.
+#A1 #A2 #f #Q #H #a1 #a2 @(wf2_ind_nlt_aux … H) -H //
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_lt.ma".
+
+(* WELL-FOUNDED INDUCTION ***************************************************)
+
+fact wf3_ind_nlt_aux (A1) (A2) (A3) (f:A1→A2→A3→nat) (Q:relation3 …):
+ (∀n. (∀a1,a2,a3. f a1 a2 a3 < n → Q a1 a2 a3) → ∀a1,a2,a3. f a1 a2 a3 = n → Q a1 a2 a3) →
+ ∀n,a1,a2,a3. f a1 a2 a3 = n → Q a1 a2 a3.
+#A1 #A2 #A3 #f #Q #H #n @(nat_ind_lt … n) -n /3 width=3 by/
+qed-.
+
+(*** f3_ind *)
+lemma wf3_ind_nlt (A1) (A2) (A3) (f:A1→A2→A3→nat) (Q:relation3 …):
+ (∀n. (∀a1,a2,a3. f a1 a2 a3 < n → Q a1 a2 a3) → ∀a1,a2,a3. f a1 a2 a3 = n → Q a1 a2 a3) →
+ ∀a1,a2,a3. Q a1 a2 a3.
+#A1 #A2 #A3 #f #Q #H #a1 #a2 #a3 @(wf3_ind_nlt_aux … H) -H //
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/pnat.ma".
+include "ground/notation/functions/zero_0.ma".
+include "ground/notation/functions/infinity_0.ma".
+
+(* NON-NEGATIVE INTEGERS WITH INFINITY **************************************)
+
+(*** ynat *)
+inductive ynat: Type[0] ≝
+| yzero: ynat
+| yinj : pnat → ynat
+| yinf : ynat
+.
+
+coercion yinj.
+
+interpretation
+ "zero (non-negative integers with infinity)"
+ 'Zero = yzero.
+
+interpretation
+ "infinity (non-negative integers with infinity)"
+ 'Infinity = yinf.
+
+(* Inversion lemmas *********************************************************)
+
+(* Note: destruct *)
+(*** yinj_inj *)
+lemma eq_inv_yinj_bi (y1) (y2): yinj y1 = yinj y2 → y1 = y2.
+#x #y #H destruct //
+qed-.
+
+(* Basic properties *********************************************************)
+
+(*** eq_ynat_dec *)
+lemma eq_ynat_dec (y1,y2:ynat): Decidable (y1 = y2).
+* [| #p1 |] *
+[1,9: /2 width=1 by or_introl/ |2,5,8: #p2 ]
+[2: elim (eq_pnat_dec p1 p2)
+ /4 width=1 by eq_inv_yinj_bi, or_intror, or_introl/
+|*: @or_intror #H destruct
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_le.ma".
+include "ground/arith/ynat_nat.ma".
+
+(* ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY ****************************)
+
+(*** yle *)
+inductive yle: relation ynat ≝
+| yle_inj: ∀m,n. m ≤ n → yle (yinj_nat m) (yinj_nat n)
+| yle_inf: ∀x. yle x (∞)
+.
+
+interpretation
+ "less equal (non-negative integers with infinity)"
+ 'leq x y = (yle x y).
+
+(* Basic inversions *********************************************************)
+
+(*** yle_inv_inj2 *)
+lemma yle_inv_inj_dx (x) (n):
+ x ≤ yinj_nat n →
+ ∃∃m. m ≤ n & x = yinj_nat m.
+#x #n0 @(insert_eq_1 … (yinj_nat n0))
+#y #H elim H -x -y
+[ #m #n #Hmn #H
+ lapply (eq_inv_yinj_nat_bi … H) -H #H destruct
+ /2 width=3 by ex2_intro/
+| #x #H
+ elim (eq_inv_yinj_nat_inf … H)
+]
+qed-.
+
+(*** yle_inv_inj *)
+lemma yle_inv_inj_bi (m) (n):
+ yinj_nat m ≤ yinj_nat n → m ≤ n.
+#m #n #H
+elim (yle_inv_inj_dx … H) -H #x #Hxn #H
+lapply (eq_inv_yinj_nat_bi … H) -H #H destruct //
+qed-.
+
+(*** yle_inv_O2 *)
+lemma yle_inv_zero_dx (x):
+ x ≤ 𝟎 → 𝟎 = x.
+#x #H
+elim (yle_inv_inj_dx ? (𝟎) H) -H #m #Hm #H destruct
+<(nle_inv_zero_dx … Hm) -m //
+qed-.
+
+(*** yle_inv_Y1 *)
+lemma yle_inv_inf_sn (y): ∞ ≤ y → ∞ = y.
+#y @(insert_eq_1 … (∞))
+#x #H elim H -x -y //
+#m #n #_ #H
+elim (eq_inv_inf_yinj_nat … H)
+qed-.
+
+(*** yle_antisym *)
+lemma yle_antisym (x) (y):
+ x ≤ y → y ≤ x → x = y.
+#x #y #H elim H -x -y
+[ /4 width=1 by yle_inv_inj_bi, nle_antisym, eq_f/
+| /2 width=1 by yle_inv_inf_sn/
+]
+qed-.
+
+(* Basic constructions ******************************************************)
+
+(*** le_O1 *)
+lemma yle_zero_sn (y): 𝟎 ≤ y.
+#y @(ynat_split_nat_inf … y) -y
+/2 width=1 by yle_inj/
+qed.
+
+(*** yle_refl *)
+lemma yle_refl: reflexive … yle.
+#x @(ynat_split_nat_inf … x) -x
+/2 width=1 by yle_inj, yle_inf, nle_refl/
+qed.
+
+(*** yle_split *)
+lemma ynat_split_le_ge (x) (y):
+ ∨∨ x ≤ y | y ≤ x.
+#x @(ynat_split_nat_inf … x) -x
+[| /2 width=1 by or_intror/ ]
+#m #y @(ynat_split_nat_inf … y) -y
+[| /3 width=1 by yle_inf, or_introl/ ]
+#n elim (nat_split_le_ge m n)
+/3 width=1 by yle_inj, or_introl, or_intror/
+qed-.
+
+(* Main constructions *******************************************************)
+
+(*** yle_trans *)
+theorem yle_trans: Transitive … yle.
+#x #y * -x -y
+[ #m #n #Hxy #z @(ynat_split_nat_inf … z) -z //
+ /4 width=3 by yle_inv_inj_bi, nle_trans, yle_inj/
+| #x #z #H <(yle_inv_inf_sn … H) -H //
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_le_minus.ma".
+include "ground/arith/ynat_minus1.ma".
+include "ground/arith/ynat_le.ma".
+
+(* ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY ****************************)
+
+(* Constructions with yminus1 ***********************************************)
+
+(*** yle_minus_sn *)
+lemma yle_minus1_sn_refl_sn (x) (n): x - n ≤ x.
+#x @(ynat_split_nat_inf … x) -x //
+#m #n /2 width=1 by yle_inj/
+qed.
+
+(*** monotonic_yle_minus_dx *)
+lemma yle_minus1_bi_dx (o) (x) (y):
+ x ≤ y → x - o ≤ y - o.
+#o #x #y *
+/3 width=1 by nle_minus_bi_dx, yle_inj, yle_inf/
+qed.
+
+(*** yminus_to_le *)
+lemma yle_eq_zero_minus1 (x) (n): 𝟎 = x - n → x ≤ yinj_nat n.
+#x @(ynat_split_nat_inf … x) -x
+[ #m #n <yminus1_inj_sn >yinj_nat_zero #H
+ /4 width=1 by nle_eq_zero_minus, yle_inj, eq_inv_yinj_nat_bi/
+| #n <yminus1_inf_sn #H destruct
+]
+qed.
+
+(* Inversions with yminus1 **************************************************)
+
+(*** yle_to_minus *)
+lemma yle_inv_eq_zero_minus1 (x) (n):
+ x ≤ yinj_nat n → 𝟎 = x - n.
+#x @(ynat_split_nat_inf … x) -x
+[ #m #n #H <yminus1_inj_sn
+ /4 width=1 by nle_inv_eq_zero_minus, yle_inv_inj_bi, eq_f/
+| #n #H
+ lapply (yle_inv_inf_sn … H) -H #H
+ elim (eq_inv_inf_yinj_nat … H)
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_le_minus_plus.ma".
+include "ground/arith/ynat_minus1_plus.ma".
+include "ground/arith/ynat_le_plus.ma".
+include "ground/arith/ynat_le_minus1.ma".
+
+(* ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY ****************************)
+
+(* Constructions with yminus and yplus **************************************)
+
+(*** yle_plus1_to_minus_inj2 *)
+lemma yle_plus_sn_dx_minus1_dx (n) (x) (z):
+ x + yinj_nat n ≤ z → x ≤ z - n.
+#n #x #z #H
+lapply (yle_minus1_bi_dx n … H) -H //
+qed.
+
+(*** yle_plus1_to_minus_inj1 *)
+lemma yle_plus_sn_sn_minus1_dx (n) (x) (z):
+ yinj_nat n + x ≤ z → x ≤ z - n.
+/2 width=1 by yle_plus_sn_dx_minus1_dx/ qed.
+
+(*** yle_plus2_to_minus_inj2 *)
+lemma yle_plus_dx_dx_minus1_sn (o) (x) (y):
+ x ≤ y + yinj_nat o → x - o ≤ y.
+/2 width=1 by yle_minus1_bi_dx/ qed.
+
+(*** yle_plus2_to_minus_inj1 *)
+lemma yle_plus_dx_sn_minus1_sn (o) (x) (y):
+ x ≤ yinj_nat o + y → x - o ≤ y.
+/2 width=1 by yle_plus_dx_dx_minus1_sn/ qed.
+
+(* Destructions with yminus and yplus ***************************************)
+
+(*** yplus_minus_comm_inj *)
+lemma yminus1_plus_comm_23 (n) (x) (z):
+ yinj_nat n ≤ x → x - n + z = x + z - n.
+#n #x @(ynat_split_nat_inf … x) -x //
+#m #z #Hnm @(ynat_split_nat_inf … z) -z
+[ #o <yminus1_inj_sn <yplus_inj_bi <yplus_inj_bi <yminus1_inj_sn
+ <nminus_plus_comm_23 /2 width=1 by yle_inv_inj_bi/
+| <yplus_inf_dx <yplus_inf_dx //
+]
+qed-.
+
+(*** yplus_minus_assoc_inj *)
+lemma yplus_minus1_assoc (o) (x) (y):
+ yinj_nat o ≤ y → x + y - o = x + (y - o).
+#o #x @(ynat_split_nat_inf … x) -x //
+#m #y @(ynat_split_nat_inf … y) -y
+[ #n #Hon <yminus1_inj_sn <yplus_inj_bi <yplus_inj_bi
+ <nplus_minus_assoc /2 width=1 by yle_inv_inj_bi/
+| #_ <yminus1_inf_sn //
+]
+qed-.
+
+(*** yplus_minus_assoc_comm_inj *)
+lemma yminus1_assoc_comm_23 (n) (o) (x):
+ n ≤ o → x + yinj_nat n - o = x - (o - n).
+#n #o #x @(ynat_split_nat_inf … x) -x
+[ #m #Hno <yminus1_inj_sn <yplus_inj_bi <yminus1_inj_sn
+ <nminus_assoc_comm_23 //
+| #_ <yminus1_inf_sn <yplus_inf_sn //
+]
+qed-.
+
+(* Inversions with yminus and yplus *****************************************)
+
+(*** yminus_plus *)
+lemma yplus_minus1_sn_refl_sn (n) (x):
+ yinj_nat n ≤ x → x = x - n + yinj_nat n.
+/2 width=1 by yminus1_plus_comm_23/ qed-.
+
+lemma yplus_minus1_dx_refl_sn (n) (x):
+ yinj_nat n ≤ x → x = yinj_nat n + (x - n).
+/2 width=1 by yplus_minus1_sn_refl_sn/ qed-.
+
+(*** yplus_inv_minus *)
+lemma eq_inv_yplus_bi_inj_md (n1) (m2) (x1) (y2):
+ yinj_nat n1 ≤ x1 → x1 + yinj_nat m2 = yinj_nat n1 + y2 →
+ ∧∧ x1 - n1 = y2 - m2 & yinj_nat m2 ≤ y2.
+#n1 #m2 #x1 #y2 #Hnx1 #H12
+lapply (yle_plus_bi_dx (yinj_nat m2) … Hnx1) >H12 #H
+lapply (yle_inv_plus_bi_sn_inj … H) -H #Hmy2
+generalize in match H12; -H12 (**) (* rewrite in hyp *)
+>(yplus_minus1_sn_refl_sn … Hmy2) in ⊢ (%→?); <yplus_assoc #H
+lapply (eq_inv_yplus_bi_dx_inj … H) -H
+>(yplus_minus1_dx_refl_sn … Hnx1) in ⊢ (%→?); -Hnx1 #H
+lapply (eq_inv_yplus_bi_sn_inj … H) -H #H12
+/2 width=1 by conj/
+qed-.
+
+(*** yle_inv_plus_inj2 yle_inv_plus_inj_dx *)
+lemma yle_inv_plus_sn_inj_dx (n) (x) (z):
+ x + yinj_nat n ≤ z →
+ ∧∧ x ≤ z - n & yinj_nat n ≤ z.
+/3 width=3 by yle_plus_sn_dx_minus1_dx, yle_trans, conj/
+qed-.
+
+(*** yle_inv_plus_inj1 *)
+lemma yle_inv_plus_sn_inj_sn (n) (x) (z):
+ yinj_nat n + x ≤ z →
+ ∧∧ x ≤ z - n & yinj_nat n ≤ z.
+/2 width=1 by yle_inv_plus_sn_inj_dx/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/ynat_succ.ma".
+include "ground/arith/ynat_le_minus1.ma".
+
+(* ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY ****************************)
+
+(* Constructions with yminus1 and ysucc *************************************)
+
+(*** yminus_succ1_inj *)
+lemma yminus1_succ_sn (x) (n):
+ yinj_nat n ≤ x → ↑(x - n) = ↑x - n.
+#x @(ynat_split_nat_inf … x) -x //
+#m #n #Hnm
+<yminus1_inj_sn <ysucc_inj <ysucc_inj <yminus1_inj_sn
+/4 width=1 by yle_inv_inj_bi, nminus_succ_sn, eq_f/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_le_plus.ma".
+include "ground/arith/ynat_plus.ma".
+include "ground/arith/ynat_le_succ.ma".
+
+(* ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY ****************************)
+
+(* Constructions with yplus *************************************************)
+
+(*** monotonic_yle_plus *)
+lemma yle_plus_bi (x1) (x2) (y1) (y2):
+ x1 ≤ y1 → x2 ≤ y2 → x1 + x2 ≤ y1 + y2.
+#x1 #x2 #y1 #y2 * //
+#m1 #n1 #Hmn1 * //
+#m2 #n2 #Hmn2 /3 width=1 by nle_plus_bi, yle_inj/
+qed.
+
+(*** monotonic_yle_plus_dx *)
+lemma yle_plus_bi_dx (z) (x) (y):
+ x ≤ y → x + z ≤ y + z.
+/2 width=1 by yle_plus_bi/ qed.
+
+(*** monotonic_yle_plus_sn *)
+lemma yle_plus_bi_sn (z) (x) (y):
+ x ≤ y → z + x ≤ z + y.
+/2 width=1 by yle_plus_bi/ qed.
+
+(*** yle_plus_dx1_trans *)
+lemma yle_plus_dx_dx (z) (x) (y):
+ z ≤ x → z ≤ x + y.
+/2 width=1 by yle_plus_bi/ qed.
+
+(*** yle_plus_dx2_trans *)
+lemma yle_plus_dx_sn (z) (x) (y):
+ z ≤ y → z ≤ x + y.
+#z #x #y <yplus_comm
+/2 width=3 by yle_plus_dx_dx/
+qed.
+
+(*** yle_plus_dx1 *)
+lemma yle_plus_dx_dx_refl (x) (y): x ≤ x + y.
+/2 width=1 by yle_plus_dx_dx/ qed.
+
+(*** yle_plus_dx2 *)
+lemma yle_plus_dx_sn_refl (x) (y): y ≤ x + y.
+// qed-.
+
+(* Inversions with yplus ****************************************************)
+
+(*** yle_inv_monotonic_plus_dx_inj *)
+lemma yle_inv_plus_bi_dx_inj (o) (x) (y):
+ x + yinj_nat o ≤ y + yinj_nat o → x ≤ y.
+#o @(nat_ind_succ … o) -o //
+#o #IH #x #y >ysucc_inj <yplus_succ_dx <yplus_succ_dx #H
+/3 width=1 by yle_inv_succ_bi/
+qed-.
+
+(*** yle_inv_monotonic_plus_sn_inj *)
+lemma yle_inv_plus_bi_sn_inj (o) (x) (y):
+ yinj_nat o + x ≤ yinj_nat o + y → x ≤ y.
+/2 width=2 by yle_inv_plus_bi_dx_inj/ qed-.
+
+(* Destructions with yplus **************************************************)
+
+(*** yle_fwd_plus_sn2 *)
+lemma yle_des_plus_sn_sn (x) (y) (z):
+ x + y ≤ z → y ≤ z.
+/2 width=3 by yle_trans/ qed-.
+
+(*** yle_fwd_plus_sn1 *)
+lemma yle_des_plus_sn_dx (x) (y) (z):
+ x + y ≤ z → x ≤ z.
+/2 width=3 by yle_trans/ qed-.
+
+(*** yle_fwd_plus_ge *)
+lemma yle_des_plus_bi_sn_inj_bi (m) (n) (x) (y):
+ n ≤ m → yinj_nat m + x ≤ yinj_nat n + y → x ≤ y.
+#m #n #x #y #Hnm #H
+lapply (yle_inj … Hnm) -Hnm #Hnm
+lapply (yle_plus_bi … Hnm … H) -Hnm -H
+<yplus_assoc <yplus_inj_bi <yplus_assoc <yplus_inj_bi #H
+/2 width=2 by yle_inv_plus_bi_sn_inj/
+qed-.
+
+(*** yle_fwd_plus_ge_inj *)
+lemma yle_des_plus_bi_sn_inj_sn (o) (z) (x) (y):
+ z ≤ yinj_nat o → yinj_nat o + x ≤ z + y → x ≤ y.
+#m #z #x #y #H elim (yle_inv_inj_dx … H) -H
+#n #Hnm #H destruct
+/2 width=4 by yle_des_plus_bi_sn_inj_bi/
+qed-.
+
+(*** yle_fwd_plus_yge *)
+lemma yle_des_plus_bi_sn_inj_md (m1) (m2) (y1) (y2):
+ yinj_nat m2 ≤ y1 → y1 + yinj_nat m1 ≤ yinj_nat m2 + y2 → yinj_nat m1 ≤ y2.
+#m1 #m2 #y1 #y2 @(ynat_split_nat_inf … y2) -y2 //
+#n2 @(ynat_split_nat_inf … y1) -y1
+/2 width=4 by yle_des_plus_bi_sn_inj_sn/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_le_pred.ma".
+include "ground/arith/ynat_pred.ma".
+include "ground/arith/ynat_le.ma".
+
+(* ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY ****************************)
+
+(* Constructions with ypred *************************************************)
+
+(*** yle_pred_sn *)
+lemma yle_pred_sn_trans (x) (y): x ≤ y → ↓x ≤ y.
+#x #y * -x -y
+/3 width=3 by yle_inj, nle_trans/
+qed.
+
+(*** yle_refl_pred_sn *)
+lemma yle_pred_sn_refl (x): ↓x ≤ x.
+/2 width=1 by yle_pred_sn_trans, yle_refl/ qed.
+
+(*** yle_pred *)
+lemma yle_pred_bi (x) (y): x ≤ y → ↓x ≤ ↓y.
+#x #y * -x -y
+/3 width=1 by yle_inj, nle_pred_bi/
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/ynat_succ.ma".
+include "ground/arith/ynat_le_pred.ma".
+
+(* ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY ****************************)
+
+(* Constructions with ypred and ysucc ***************************************)
+
+(*** yle_refl_SP_dx *)
+lemma yle_succ_pred_dx_refl (x): x ≤ ↑↓x.
+#x @(ynat_split_nat_inf … x) -x
+/2 width=1 by yle_inj/
+qed.
+
+(*** yle_inv_succ2 *)
+lemma yle_pred_sn (x) (y): x ≤ ↑y → ↓x ≤ y.
+#x #y0 @(insert_eq_1 … (↑y0))
+#y * -x -y
+[ #m #n0 #Hmn #H
+ elim (eq_inv_ysucc_inj … H) -H #n #H1 #H2 destruct
+ /3 width=1 by yle_inj, nle_pred_sn/
+| #x0 #H <(eq_inv_ysucc_inf … H) -y0 //
+]
+qed.
+
+(* Inversions with ypred and ysucc ******************************************)
+
+(*** yle_succ2 *)
+lemma yle_inv_pred_sn (x) (y): ↓x ≤ y → x ≤ ↑y.
+#x0 #y @(insert_eq_1 … (↓x0))
+#x * -x -y // #m0 #n #Hmn #H
+elim (eq_inv_ypred_inj … H) -H #m #H1 #H2 destruct
+/3 width=1 by yle_inj, nle_inv_pred_sn/
+qed-.
+
+(*** yle_inv_succ1 *)
+lemma yle_inv_succ_sn (x) (y):
+ ↑x ≤ y → ∧∧ x ≤ ↓y & y = ↑↓y.
+#x0 #y @(insert_eq_1 … (↑x0))
+#x * -x -y
+[ #m0 #n #Hmn #H
+ elim (eq_inv_ysucc_inj … H) -H #m #H1 #H2 destruct
+ elim (nle_inv_succ_sn … Hmn) -Hmn #Hmn #Hn
+ /3 width=1 by yle_inj, conj/
+| /2 width=1 by yle_inf, conj/
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/ynat_succ.ma".
+include "ground/arith/ynat_le.ma".
+
+(* ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY ****************************)
+
+(* Constructions with ysucc *************************************************)
+
+(*** yle_succ *)
+lemma yle_succ_bi (x) (y): x ≤ y → ↑x ≤ ↑y.
+#x #y * -x -y
+/3 width=1 by yle_inj, yle_inf, nle_succ_bi/
+qed.
+
+(*** yle_succ_dx *)
+lemma yle_succ_dx (x) (y): x ≤ y → x ≤ ↑y.
+#x #y * -x -y
+/3 width=1 by yle_inj, yle_inf, nle_succ_dx/
+qed.
+
+(*** yle_refl_S_dx *)
+lemma yle_succ_dx_refl (x): x ≤ ↑x.
+/2 width=1 by yle_succ_dx/ qed.
+
+(* Inversions with ysucc ****************************************************)
+
+(*** yle_inv_succ *)
+lemma yle_inv_succ_bi (x) (y): ↑x ≤ ↑y → x ≤ y.
+#x #y @(ynat_split_nat_inf … y) -y //
+#n <ysucc_inj #H
+elim (yle_inv_inj_dx … H) -H #o #Hmn #H
+elim (eq_inv_ysucc_inj … H) -H #m #H1 #H2 destruct
+/3 width=1 by yle_inj, nle_inv_succ_bi/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_lt.ma".
+include "ground/arith/ynat_nat.ma".
+
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
+
+(*** ylt *)
+inductive ylt: relation ynat ≝
+| ylt_inj: ∀m,n. m < n → ylt (yinj_nat m) (yinj_nat n)
+| ylt_inf: ∀m. ylt (yinj_nat m) (∞)
+.
+
+interpretation
+ "less (non-negative integers with infinity)"
+ 'lt x y = (ylt x y).
+
+(* Basic destructions *******************************************************)
+
+(* ylt_fwd_gen ylt_inv_Y2 *)
+lemma ylt_des_gen_sn (x) (y):
+ x < y → ∃m. x = yinj_nat m.
+#x #y * -x -y
+/2 width=2 by ex_intro/
+qed-.
+
+lemma ylt_des_lt_inf_dx (x) (y): x < y → x < ∞.
+#x #y #H
+elim (ylt_des_gen_sn … H) -y #m #H destruct //
+qed-.
+
+(*** ylt_fwd_lt_O1 *)
+lemma ylt_des_lt_zero_sn (x) (y): x < y → 𝟎 < y.
+#x #y * -x -y
+/3 width=2 by ylt_inf, ylt_inj, nlt_des_lt_zero_sn/
+qed-.
+
+(* Basic inversions *********************************************************)
+
+(*** ylt_inv_inj2 *)
+lemma ylt_inv_inj_dx (x) (n):
+ x < yinj_nat n →
+ ∃∃m. m < n & x = yinj_nat m.
+#x #n0 @(insert_eq_1 … (yinj_nat n0))
+#y * -x -y
+[ #m #n #Hmn #H >(eq_inv_yinj_nat_bi … H) -n0
+ /2 width=3 by ex2_intro/
+| #m0 #H elim (eq_inv_yinj_nat_inf … H)
+]
+qed-.
+
+(*** ylt_inv_inj *)
+lemma ylt_inv_inj_bi (m) (n):
+ yinj_nat m < yinj_nat n → m < n.
+#m #n #H elim (ylt_inv_inj_dx … H) -H
+#x #Hx #H >(eq_inv_yinj_nat_bi … H) -m //
+qed-.
+
+(*** ylt_inv_Y1 *)
+lemma ylt_inv_inf_sn (y): ∞ < y → ⊥.
+#y #H elim (ylt_des_gen_sn … H) -H
+#n #H elim (eq_inv_inf_yinj_nat … H)
+qed-.
+
+lemma ylt_inv_refl (x): x < x → ⊥.
+#x @(ynat_split_nat_inf … x) -x
+/3 width=2 by ylt_inv_inf_sn, ylt_inv_inj_bi, nlt_inv_refl/
+qed-.
+
+(* Main constructions *******************************************************)
+
+(*** ylt_trans *)
+theorem ylt_trans: Transitive … ylt.
+#x #y * -x -y
+[ #m #n #Hxy #z @(ynat_split_nat_inf … z) -z
+ /4 width=3 by ylt_inv_inj_bi, ylt_inj, nlt_trans/
+| #m #z #H elim (ylt_inv_inf_sn … H)
+]
+qed-.
+
+(*** lt_ylt_trans *)
+lemma lt_ylt_trans (m) (n) (z):
+ m < n → yinj_nat n < z → yinj_nat m < z.
+/3 width=3 by ylt_trans, ylt_inj/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/ynat_le.ma".
+include "ground/arith/ynat_lt.ma".
+
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
+
+(* Constructions with yle ***************************************************)
+
+(*** yle_split_eq *)
+lemma yle_split_lt_eq (x) (y):
+ x ≤ y → ∨∨ x < y | x = y.
+#x #y * -x -y
+[ #m #n #Hmn elim (nle_split_lt_eq … Hmn) -Hmn
+ /3 width=1 by or_introl, ylt_inj/
+| #x @(ynat_split_nat_inf … x) -x
+ /2 width=1 by or_introl, ylt_inf/
+]
+qed-.
+
+(*** ylt_split *)
+lemma ynat_split_lt_ge (x) (y): ∨∨ x < y | y ≤ x.
+#x #y elim (ynat_split_le_ge x y) /2 width=1 by or_intror/
+#H elim (yle_split_lt_eq … H) -H /2 width=1 by or_introl, or_intror/
+qed-.
+
+(*** ylt_split_eq *)
+lemma ynat_split_lt_eq_gt (x) (y): ∨∨ x < y | y = x | y < x.
+#x #y elim (ynat_split_lt_ge x y) /2 width=1 by or3_intro0/
+#H elim (yle_split_lt_eq … H) -H /2 width=1 by or3_intro1, or3_intro2/
+qed-.
+
+(*** ylt_yle_trans *)
+lemma ylt_yle_trans (x) (y) (z): y ≤ z → x < y → x < z.
+#x #y #z * -y -z
+[ #n #o #Hno #H elim (ylt_inv_inj_dx … H) -H
+ #m #Hmn #H destruct /3 width=3 by ylt_inj, nlt_nle_trans/
+| #y /2 width=2 by ylt_des_lt_inf_dx/
+]
+qed-.
+
+(*** yle_ylt_trans *)
+lemma yle_ylt_trans (x) (y) (z): y < z → x ≤ y → x < z.
+#x #y #z * -y -z
+[ #n #o #Hno #H elim (yle_inv_inj_dx … H) -H
+ #m #Hmn #H destruct /3 width=3 by ylt_inj, nle_nlt_trans/
+| #n #H elim (yle_inv_inj_dx … H) -H #m #_ #H destruct //
+]
+qed-.
+
+(*** le_ylt_trans *)
+lemma nle_ylt_trans (m) (n) (z):
+ m ≤ n → yinj_nat n < z → yinj_nat m < z.
+/3 width=3 by yle_ylt_trans, yle_inj/ qed-.
+
+(* Inversions with yle ******************************************************)
+
+(* ylt_yle_false *)
+lemma ylt_ge_false (x) (y): x < y → y ≤ x → ⊥.
+/3 width=4 by yle_ylt_trans, ylt_inv_refl/ qed-.
+
+(* Destructions with yle ****************************************************)
+
+(*** ylt_fwd_le *)
+lemma ylt_des_le (x) (y): x < y → x ≤ y.
+#x #y * -x -y
+/3 width=1 by nlt_des_le, yle_inj/
+qed-.
+
+(* Eliminations *************************************************************)
+
+(*** ynat_ind_lt_le_aux *)
+lemma ynat_ind_lt_le_inj_dx (Q:predicate …):
+ (∀y. (∀x. x < y → Q x) → Q y) →
+ ∀n,x. x ≤ yinj_nat n → Q x.
+#Q #IH #n #x #H
+elim (yle_inv_inj_dx … H) -H #m #Hmn #H destruct
+@(nat_ind_lt_le … Hmn) -Hmn #n0 #IH0
+@IH -IH #x #H
+elim (ylt_inv_inj_dx … H) -H #m0 #Hmn0 #H destruct
+/2 width=1 by/
+qed-.
+
+(*** ynat_ind_lt_aux *)
+lemma ynat_ind_lt_inj (Q:predicate …):
+ (∀y. (∀x. x < y → Q x) → Q y) →
+ ∀n. Q (yinj_nat n).
+/4 width=2 by ynat_ind_lt_le_inj_dx/ qed-.
+
+(*** ynat_ind_lt *)
+lemma ynat_ind_lt (Q:predicate …):
+ (∀y. (∀x. x < y → Q x) → Q y) →
+ ∀y. Q y.
+#Q #IH #y @(ynat_split_nat_inf … y) -y
+[ /4 width=1 by ynat_ind_lt_inj/
+| @IH #x #H
+ elim (ylt_des_gen_sn … H) -H #m #H destruct
+ /4 width=1 by ynat_ind_lt_inj/
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_lt_minus.ma".
+include "ground/arith/ynat_minus1.ma".
+include "ground/arith/ynat_le.ma".
+include "ground/arith/ynat_lt.ma".
+
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
+
+(* Cobstructions with yle and yminus1 **************************************)
+
+(*** monotonic_ylt_minus_dx *)
+lemma ylt_minus1_bi_dx (o) (x) (y):
+ x < y → yinj_nat o ≤ x → x - o < y - o.
+#o #x #y * -x -y
+/4 width=1 by ylt_inj, yle_inv_inj_bi, nlt_minus_bi_dx/
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/ynat_minus1_plus.ma".
+include "ground/arith/ynat_lt_le_minus1.ma".
+
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
+
+(* Constructions with yle and yminus1 and yplus ****************************)
+
+(*** ylt_plus2_to_minus_inj2 *)
+lemma ylt_plus_dx_dx_minus1_sn (o) (x) (y):
+ yinj_nat o ≤ x → x < y + yinj_nat o → x - o < y.
+/2 width=1 by ylt_minus1_bi_dx/ qed.
+
+(*** ylt_plus2_to_minus_inj1 *)
+lemma ylt_plus_dx_sn_minus1_sn (o) (x) (y):
+ yinj_nat o ≤ x → x < yinj_nat o + y → x - o < y.
+/2 width=1 by ylt_plus_dx_dx_minus1_sn/ qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/ynat_le_plus.ma".
+include "ground/arith/ynat_lt_plus.ma".
+include "ground/arith/ynat_lt_le.ma".
+
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
+
+(* Constructions with yle and yplus *****************************************)
+
+(*** monotonic_ylt_plus_inj *)
+lemma ylt_yle_plus_bi_inj (x1) (x2) (n1) (y2):
+ x1 < x2 → yinj_nat n1 ≤ y2 → x1 + yinj_nat n1 < x2 + y2.
+/3 width=3 by ylt_plus_bi_dx_inj, yle_plus_bi_sn, ylt_yle_trans/
+qed.
+
+(*** monotonic_ylt_plus *)
+lemma ylt_yle_plus_bi (x1) (x2) (y1) (y2):
+ x1 < x2 → y1 < ∞ → y1 ≤ y2 → x1 + y1 < x2 + y2.
+#x1 #x2 #y1 #y2 #Hx12 #Hy1 #Hy12
+elim (ylt_des_gen_sn … Hy1) -Hy1 #n1 #H destruct
+/2 width=1 by ylt_yle_plus_bi_inj/
+qed.
+
+(* Inversions with yle and yplus ********************************************)
+
+(*** yle_inv_monotonic_plus_dx *)
+lemma yle_inv_plus_bi_dx (z) (x) (y):
+ z < ∞ → x + z ≤ y + z → x ≤ y.
+#z #x #y #Hz #Hxy
+elim (ylt_des_gen_sn … Hz) -Hz #o #H destruct
+/2 width=2 by yle_inv_plus_bi_sn_inj/
+qed-.
+
+(*** yle_inv_monotonic_plus_sn *)
+lemma yle_inv_plus_bi_sn (z) (x) (y):
+ z < ∞ → z + x ≤ z + y → x ≤ y.
+/2 width=3 by yle_inv_plus_bi_dx/ qed-.
+
+(* Destructions with yle and yplus ******************************************)
+
+(*** ylt_fwd_plus_ge *)
+lemma ylt_des_plus_bi_sn_ge (x1) (x2) (y1) (y2):
+ x2 ≤ x1 → x1 + y1 < x2 + y2 → y1 < y2.
+#x1 #x2 #y1 #y2 #Hx21 #Hxy
+elim (ylt_des_gen_sn … Hxy) #o #H
+elim (eq_inv_yplus_inj … H) -H #m1 #n1 #_ #H2 #H3 destruct -o
+elim (yle_inv_inj_dx … Hx21) #m2 #_ #H destruct
+lapply (ylt_yle_plus_bi_inj … Hxy … Hx21) -Hxy -Hx21
+<yplus_plus_comm_13 #H
+/3 width=3 by ylt_des_plus_bi_sn, ylt_des_plus_bi_dx/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/ynat_le.ma".
+include "ground/arith/ynat_lt_pred.ma".
+
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
+
+(* Destructions with yle and ypred ******************************************)
+
+(*** ylt_fwd_le_pred2 *)
+lemma ylt_des_le_pred_dx (x) (y): x < y → x ≤ ↓y.
+#x #y * -x -y //
+#m #n #H
+elim (nlt_inv_gen … H) -H #Hm #_
+/2 width=1 by yle_inj/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/ynat_le_pred_succ.ma".
+include "ground/arith/ynat_lt_pred_succ.ma".
+
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
+
+(* Constructions with yle and ypred and ysucc *******************************)
+
+(*** yle_inv_succ_sn_lt yle_inv_succ1_lt *)
+lemma le_succ_sn_ylt (x) (y):
+ ↑x ≤ y → ∧∧ x ≤ ↓y & 𝟎 < y.
+#x #y #H elim (yle_inv_succ_sn … H) -H
+/4 width=2 by ylt_zero_sn, conj/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/ynat_lt_succ.ma".
+include "ground/arith/ynat_lt_le.ma".
+
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
+
+(* Constructions with ysucc *************************************************)
+
+(*** yle_lt yle_succ1_inj *)
+lemma ylt_le_succ_sn (x) (y):
+ x < ∞ → ↑x ≤ y → x < y.
+/3 width=3 by ylt_yle_trans, ylt_succ_dx_refl/ qed.
+
+(* Inversions and destructions on yle ***************************************)
+
+(*** ylt_inv_le *)
+lemma ylt_inv_le_succ_sn (x) (y):
+ x < y → ∧∧ x < ∞ & ↑x ≤ y.
+#x #y * -x -y
+/3 width=1 by yle_inj, conj/
+qed-.
+
+(* Destructions with yle and ysucc ******************************************)
+
+(*** ylt_fwd_le_succ1 *)
+lemma ylt_des_le_succ_sn (x) (y): x < y → ↑x ≤ y.
+#x #y #H
+elim (ylt_inv_le_succ_sn … H) -H #_ //
+qed-.
+
+(*** ylt_fwd_succ2 *)
+lemma ylt_des_succ_dx (x) (y): x < ↑y → x ≤ y.
+#x #y @(ynat_split_nat_inf … y) -y //
+#n <ysucc_inj #H
+elim (ylt_inv_inj_dx … H) -H #m #Hm #H destruct
+/3 width=1 by yle_inj, nlt_inv_succ_dx/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_lt_minus.ma".
+include "ground/arith/ynat_minus1.ma".
+include "ground/arith/ynat_lt.ma".
+
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
+
+(* Constructions with yminus1 ***********************************************)
+
+(*** ylt_to_minus *)
+lemma ylt_zero_minus1 (m) (y):
+ yinj_nat m < y → 𝟎 < y - m.
+#m #y @(ynat_split_nat_inf … y) -y //
+#n #Hmn <yminus1_inj_sn >yinj_nat_zero >(nminus_refl m)
+/4 width=1 by ylt_inj, ylt_inv_inj_bi, nlt_minus_bi_dx/
+qed.
+
+(* Inversions with yminus1 **************************************************)
+
+(*** yminus_to_lt *)
+lemma ylt_inv_zero_minus1 (m) (y):
+ (𝟎) < y - m → yinj_nat m < y.
+#m #y @(ynat_split_nat_inf … y) -y //
+#n <yminus1_inj_sn >yinj_nat_zero >(nminus_refl m) #Hmm
+/4 width=2 by ylt_inv_inj_bi, ylt_inj, nlt_inv_minus_bi_dx/
+qed-.
+
+(* Destructions with yminus1 ************************************************)
+
+(*** yminus_pred *)
+lemma yminus1_pred_bi (x:ynat) (n):
+ (𝟎) < x → 𝟎 < n → x - n = ↓x - ↓n.
+#x @(ynat_split_nat_inf … x) -x //
+#m #n >yinj_nat_zero
+#Hm #Hn <yminus1_inj_sn <ypred_inj <yminus1_inj_sn
+<nminus_pred_bi /2 width=1 by ylt_inv_inj_bi/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/ynat_plus.ma".
+include "ground/arith/ynat_minus1.ma".
+include "ground/arith/ynat_lt_pred_succ.ma".
+
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
+
+(* Constructions with yminus1 and yplus *************************************)
+
+(*** ylt_plus1_to_minus_inj2 *)
+lemma ylt_plus_sn_dx_minus1_dx (n) (x) (z):
+ x + yinj_nat n < z → x < z - n.
+#n @(nat_ind_succ … n) -n //
+#n #IH #x #z >ysucc_inj <yplus_succ_shift
+/3 width=1 by ylt_des_succ_sn/
+qed.
+
+(*** ylt_plus1_to_minus_inj1 *)
+lemma ylt_plus_sn_sn_minus1_dx (n) (x) (z):
+ yinj_nat n + x < z → x < z - n.
+/2 width=1 by ylt_plus_sn_dx_minus1_dx/ qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_lt_plus.ma".
+include "ground/arith/ynat_plus.ma".
+include "ground/arith/ynat_lt_succ.ma".
+
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
+
+(* Constructions with yplus *************************************************)
+
+(*** ylt_plus_Y *)
+lemma ylt_plus_inf (x) (y):
+ x < ∞ → y < ∞ → x + y < ∞.
+#x #y #Hx #Hy
+elim (ylt_des_gen_sn … Hx) -Hx #m #H destruct
+elim (ylt_des_gen_sn … Hy) -Hy #n #H destruct
+//
+qed.
+
+(*** ylt_plus_dx1_trans *)
+lemma ylt_plus_dx_sn (z) (x) (y):
+ z < x → z < x + y.
+#z #x #y * -z -x //
+#o #m #Hom @(ynat_split_nat_inf … y) - y //
+/3 width=1 by ylt_inj, nle_plus_bi/
+qed.
+
+(*** ylt_plus_dx2_trans *)
+lemma ylt_plus_dx_dx (z) (x) (y):
+ z < y → z < x + y.
+#z #x #y <yplus_comm
+/2 width=1 by ylt_plus_dx_sn/
+qed.
+
+(*** monotonic_ylt_plus_dx_inj *)
+lemma ylt_plus_bi_dx_inj (o) (x) (y):
+ x < y → x + yinj_nat o < y + yinj_nat o.
+#o #x #y #Hxy
+@(nat_ind_succ … o) -o //
+#n #IH >ysucc_inj <yplus_succ_dx <yplus_succ_dx
+/2 width=1 by ylt_succ_bi/
+qed.
+
+(*** monotonic_ylt_plus_sn_inj *)
+lemma ylt_plus_bi_sn_inj (o) (x) (y):
+ x < y → yinj_nat o + x < yinj_nat o + y.
+/2 width=1 by ylt_plus_bi_dx_inj/ qed.
+
+(*** monotonic_ylt_plus_dx *)
+lemma ylt_plus_bi_dx (z) (x) (y):
+ x < y → z < ∞ → x + z < y + z.
+#z #x #y #Hxy #Hz
+elim (ylt_des_gen_sn … Hz) -Hz #o #H destruct
+/2 width=1 by ylt_plus_bi_dx_inj/
+qed.
+
+(*** monotonic_ylt_plus_sn *)
+lemma ylt_plus_bi_sn (z) (x) (y):
+ x < y → z < ∞ → z + x < z + y.
+#z #x #y #Hxy #Hz <yplus_comm <yplus_comm in ⊢ (??%);
+/2 width=1 by ylt_plus_bi_dx/
+qed.
+
+(* Inversions with yplus ****************************************************)
+
+(*** yplus_inv_monotonic_dx *)
+lemma eq_inv_yplus_bi_dx (z) (x) (y):
+ z < ∞ → x + z = y + z → x = y.
+#z #x #y #H
+elim (ylt_des_gen_sn … H) -H #o #H destruct
+/2 width=2 by eq_inv_yplus_bi_dx_inj/
+qed-.
+
+(*** yplus_inv_monotonic_23 *)
+lemma yplus_inv_plus_bi_23 (z) (x1) (x2) (y1) (y2):
+ z < ∞ → x1 + z + y1 = x2 + z + y2 → x1 + y1 = x2 + y2.
+#z #x1 #x2 #y1 #y2 #Hz
+<yplus_plus_comm_23 <yplus_plus_comm_23 in ⊢ (???%→?); #H
+@(eq_inv_yplus_bi_dx … H) // (**) (* auto does not work *)
+qed-.
+
+(*** ylt_inv_plus_Y *)
+lemma ylt_inv_plus_inf (x) (y):
+ x + y < ∞ → ∧∧ x < ∞ & y < ∞.
+#x #y #H
+elim (ylt_des_gen_sn … H) -H #o #H
+elim (eq_inv_yplus_inj … H) -H
+/2 width=1 by conj/
+qed-.
+
+(* Destructions with yplus **************************************************)
+
+(*** ylt_inv_monotonic_plus_dx *)
+lemma ylt_des_plus_bi_dx (z) (x) (y):
+ x + z < y + z → x < y.
+#z @(ynat_split_nat_inf … z) -z
+[ #o #x @(ynat_split_nat_inf … x) -x
+ [ #m #y @(ynat_split_nat_inf … y) -y //
+ #n <yplus_inj_bi <yplus_inj_bi #H
+ /4 width=2 by ylt_inv_inj_bi, ylt_inj, nlt_inv_plus_bi_dx/
+ | #y <yplus_inf_sn #H
+ elim (ylt_inv_inf_sn … H)
+ ]
+| #x #y <yplus_inf_dx #H
+ elim (ylt_inv_inf_sn … H)
+]
+qed-.
+
+lemma ylt_des_plus_bi_sn (z) (x) (y):
+ z + x < z + y → x < y.
+/2 width=2 by ylt_des_plus_bi_dx/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/ynat_pred_succ.ma".
+include "ground/arith/ynat_plus.ma".
+include "ground/arith/ynat_lt_pred_succ.ma".
+
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
+
+(* Inversions with yplus and ypred ******************************************)
+
+(*** yplus_inv_succ_lt_dx *)
+lemma eq_inv_succ_yplus_lt_dx (z) (x) (y): 𝟎 < y → ↑z = x + y → z = x + ↓y.
+#z #x #y #Hy >(ylt_des_gen_dx … Hy) -Hy
+<yplus_succ_dx <ypred_succ
+/2 width=1 by eq_inv_ysucc_bi/
+qed-.
+
+(*** yplus_inv_succ_lt_sn *)
+lemma eq_inv_succ_yplus_lt_sn (z) (x) (y): 𝟎 < x → ↑z = x + y → z = ↓x + y.
+/2 width=1 by eq_inv_succ_yplus_lt_dx/ qed-.
+
+(* Destructions with yplus and ypred ****************************************)
+
+(*** yplus_pred1 *)
+lemma yplus_pred_sn (x) (y): 𝟎 < x → ↓(x+y) = ↓x + y.
+#x #y #Hx >(ylt_des_gen_dx … Hx) -Hx
+<yplus_succ_sn <ypred_succ <ypred_succ //
+qed-.
+
+(*** yplus_pred2 *)
+lemma yplus_pred_dx (x) (y): 𝟎 < y → x + ↓y = ↓(x+y).
+/2 width=1 by yplus_pred_sn/ qed-.
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_lt_pred.ma".
+include "ground/arith/ynat_pred.ma".
+include "ground/arith/ynat_lt.ma".
+
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
+
+(* Constructions with ypred *************************************************)
+
+(*** ylt_pred *)
+lemma ylt_pred_bi (x) (y):
+ x < y → 𝟎 < x → ↓x < ↓y.
+#x #y * -x -y
+/4 width=1 by ylt_inv_inj_bi, ylt_inj, nlt_pred_bi/
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/ynat_succ.ma".
+include "ground/arith/ynat_lt_pred.ma".
+
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
+
+(* Constructions with ypred and ysucc ***************************************)
+
+(*** ylt_O1 *)
+lemma ylt_zero_sn (y): y = ↑↓y → 𝟎 < y.
+#y @(ynat_split_nat_inf … y) -y
+/4 width=1 by ylt_inj, eq_inv_yinj_nat_bi, nlt_zero_sn/
+qed.
+
+(* Destructions with ypred and ysucc ****************************************)
+
+(*** ylt_inv_O1 *)
+lemma ylt_des_gen_dx (x) (y): x < y → y = ↑↓y.
+#x #y * //
+#m #n #H
+lapply (nlt_des_gen … H) -H //
+qed-.
+
+lemma ylt_des_succ_sn (x) (y):
+ ↑x < y → x < ↓y.
+#x #y @(insert_eq_1 … (↑x))
+#x0 * -x0 -y
+[ #m0 #n #Hn #H
+ elim (eq_inv_ysucc_inj … H) -H #m #H1 #H2 destruct
+ elim (nlt_inv_succ_sn … Hn) -Hn #Hm #_
+ /2 width=1 by ylt_inj/
+| #m0 #H
+ elim (eq_inv_ysucc_inj … H) -H #m #H1 #H2 destruct //
+]
+qed-.
+
+(* Inversions with ypred and ysucc ******************************************)
+
+(*** ylt_inv_succ1 *)
+lemma ylt_inv_succ_sn (x) (y):
+ ↑x < y → ∧∧ x < ↓y & y = ↑↓y.
+/3 width=2 by ylt_des_succ_sn, ylt_des_gen_dx, conj/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/ynat_succ.ma".
+include "ground/arith/ynat_lt.ma".
+
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
+
+(* Constructions with ysucc *************************************************)
+
+(*** ylt_O_succ *)
+lemma ylt_zero_succ (y): 𝟎 < ↑y.
+#y @(ynat_split_nat_inf … y) -y
+/2 width=1 by ylt_inj/
+qed.
+
+(*** ylt_succ *)
+lemma ylt_succ_bi (x) (y): x < y → ↑x < ↑y.
+#x #y * -x -y
+/3 width=1 by ylt_inj, ylt_inf, nlt_succ_bi/
+qed.
+
+(*** ylt_succ_Y *)
+lemma ylt_succ_inf (x): x < ∞ → ↑x < ∞.
+#x @(ynat_split_nat_inf … x) -x //
+qed.
+
+(*** ylt_succ2_refl *)
+lemma ylt_succ_dx_refl (x) (y): x < y → x < ↑x.
+#x #y #H
+elim (ylt_des_gen_sn … H) -y #n #H destruct
+/2 width=1 by ylt_inj/
+qed.
+
+(* Inversions with ysucc ****************************************************)
+
+lemma ylt_inv_succ_inf (x): ↑x < ∞ → x < ∞.
+#x #H
+elim (ylt_des_gen_sn … H) -H #m0 #H
+elim (eq_inv_ysucc_inj … H) -H #m #H1 #H2 destruct //
+qed-.
+
+(*** ylt_inv_succ *)
+lemma ylt_inv_succ_bi (x) (y): ↑x < ↑y → x < y.
+#x #y @(ynat_split_nat_inf … y) -y
+[ #n <ysucc_inj #H
+ elim (ylt_inv_inj_dx … H) -H #m0 #Hmn #H
+ elim (eq_inv_ysucc_inj … H) -H #m #H1 #H2 destruct
+ /3 width=1 by ylt_inj, nlt_inv_succ_bi/
+| /2 width=1 by ylt_inv_succ_inf/
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_minus.ma".
+include "ground/arith/ynat_pred.ma".
+
+(* LEFT SUBTRACTION FOR NON-NEGATIVE INTEGERS WITH INFINITY *****************)
+
+(*** yminus1_sn *)
+definition yminus1 (x) (n): ynat ≝
+ ypred^n x.
+
+interpretation
+ "left minus (non-negative integers with infinity)"
+ 'minus x n = (yminus1 x n).
+
+(* Basic constructions ******************************************************)
+
+(*** yminus_O2 *)
+lemma yminus1_zero_dx (x:ynat): x = x - 𝟎 .
+// qed.
+
+(*** yminus_pred1 *)
+lemma yminus_pred_sn (x) (n): ↓(x-n) = ↓x - n.
+#x #n @(niter_appl … ypred)
+qed.
+
+(*** yminus_succ2 yminus_S2 *)
+lemma yminus1_succ_dx (x:ynat) (n): ↓(x-n) = x - ↑n.
+#x #n @(niter_succ … ypred)
+qed.
+
+(*** yminus_SO2 *)
+lemma yminus1_one_dx (x): ↓x = x - (𝟏).
+// qed.
+
+(*** yminus_Y_inj *)
+lemma yminus1_inf_sn (n): ∞ = ∞ - n.
+#n @(nat_ind_succ … n) -n //
+qed.
+
+(* Constructions with nminus ************************************************)
+
+(*** yminus_inj *)
+lemma yminus1_inj_sn (m) (n): yinj_nat (m - n) = yinj_nat m - n.
+#m #n
+@(niter_compose ???? yinj_nat)
+@ypred_inj
+qed.
+
+(* Advanced constructions ***************************************************)
+
+(* yminus_O1 *)
+lemma yminus1_zero_sn (n): 𝟎 = 𝟎 - n.
+// qed.
+
+(*** yminus_refl *)
+lemma yminus1_refl (n): 𝟎 = yinj_nat n - n.
+// qed.
+
+(*** yminus_minus_comm *)
+lemma yminus1_minus_comm (x) (n) (o):
+ x - n - o = x - o - n.
+#x @(ynat_split_nat_inf … x) -x //
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_minus_plus.ma".
+include "ground/arith/ynat_plus.ma".
+include "ground/arith/ynat_minus1_succ.ma".
+
+(* LEFT SUBTRACTION FOR NON-NEGATIVE INTEGERS WITH INFINITY *****************)
+
+(* Constructions with yplus *************************************************)
+
+(*** yplus_minus *)
+lemma yminus1_plus_sn_refl_sn (x) (n):
+ x = x + yinj_nat n - n.
+#x @(ynat_split_nat_inf … x) -x //
+#n <yplus_inf_sn //
+qed.
+
+(*** yminus_plus2 *)
+lemma yminus_plus_dx (x:ynat) (n) (o):
+ x - n - o = x - (n + o).
+#x @(ynat_split_nat_inf … x) -x //
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/ynat_pred_succ.ma".
+include "ground/arith/ynat_minus1.ma".
+
+(* LEFT SUBTRACTION FOR NON-NEGATIVE INTEGERS WITH INFINITY *****************)
+
+(* Constructions with ysucc *************************************************)
+
+(*** yminus_succ *)
+lemma yminus1_succ_bi (x:ynat) (n): x - n = ↑x - ↑n.
+// qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat.ma".
+include "ground/arith/ynat.ma".
+
+(* NON-NEGATIVE INTEGERS TO NON-NEGATIVE INTEGERS WITH INFINITY *************)
+
+(*** yinj *)
+definition yinj_nat (n) ≝ match n with
+[ nzero ⇒ 𝟎
+| ninj p ⇒ yinj p
+].
+
+definition ynat_bind_nat: (nat → ynat) → ynat → (ynat → ynat).
+#f #y *
+[ @f @(𝟎)
+| #p @f @p
+| @y
+]
+qed-.
+
+(* Basic constructions ******************************************************)
+
+lemma yinj_nat_zero: 𝟎 = yinj_nat (𝟎).
+// qed.
+
+lemma yinj_nat_inj (p): yinj p = yinj_nat (ninj p).
+// qed.
+
+lemma ynat_bind_nat_inj (f) (y) (n):
+ f n = ynat_bind_nat f y (yinj_nat n).
+#f #y * // qed.
+
+lemma ynat_bind_nat_inf (f) (y):
+ y = ynat_bind_nat f y (∞).
+// qed.
+
+(* Basic inversions *********************************************************)
+
+lemma eq_inv_yinj_nat_inf (n1): yinj_nat n1 = ∞ → ⊥.
+* [| #p1 ]
+[ <yinj_nat_zero #H destruct
+| <yinj_nat_inj #H destruct
+]
+qed.
+
+lemma eq_inv_inf_yinj_nat (n2): ∞ = yinj_nat n2 → ⊥.
+/2 width=2 by eq_inv_yinj_nat_inf/ qed-.
+
+(*** yinj_inj *)
+lemma eq_inv_yinj_nat_bi (n1) (n2): yinj_nat n1 = yinj_nat n2 → n1 = n2.
+* [| #p1 ] * [2,4: #p2 ]
+[ <yinj_nat_zero <yinj_nat_inj #H destruct
+| <yinj_nat_inj <yinj_nat_inj #H destruct //
+| //
+| <yinj_nat_inj <yinj_nat_zero #H destruct
+]
+qed-.
+
+(* Basic eliminations *******************************************************)
+
+lemma ynat_split_nat_inf (Q:predicate …):
+ (∀n. Q (yinj_nat n)) → Q (∞) → ∀y. Q y.
+#Q #H1 #H2 * //
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/xoa/ex_3_2.ma".
+include "ground/arith/nat_plus.ma".
+include "ground/arith/ynat_succ.ma".
+
+(* ADDITION FOR NON-NEGATIVE INTEGERS WITH INFINITY *************************)
+
+definition yplus_aux (x) (n): ynat ≝
+ ysucc^n x.
+
+(*** yplus *)
+definition yplus (x): ynat → ynat ≝
+ ynat_bind_nat (yplus_aux x) (∞).
+
+interpretation
+ "plus (non-negative integers with infinity)"
+ 'plus x y = (yplus x y).
+
+(* Basic constructions ******************************************************)
+
+lemma yplus_inj_dx (x) (n):
+ ysucc^n x = x + yinj_nat n.
+#x @(ynat_bind_nat_inj (yplus_aux x))
+qed.
+
+(*** yplus_Y2 *)
+lemma yplus_inf_dx (x): ∞ = x + ∞.
+// qed.
+
+(*** yplus_O2 *)
+lemma yplus_zero_dx (x): x = x + 𝟎.
+// qed.
+
+(* Constructions with ysucc *************************************************)
+
+(*** yplus_SO2 *)
+lemma yplus_one_dx (x): ↑x = x + 𝟏.
+// qed.
+
+(*** yplus_S2 yplus_succ2 *)
+lemma yplus_succ_dx (x1) (x2): ↑(x1 + x2) = x1 + ↑x2.
+#x1 #x2 @(ynat_split_nat_inf … x2) -x2 //
+#n2 <ysucc_inj <yplus_inj_dx <yplus_inj_dx
+@niter_succ
+qed.
+
+(*** yplus_succ1 *)
+lemma yplus_succ_sn (x1) (x2): ↑(x1 + x2) = ↑x1 + x2.
+#x1 #x2 @(ynat_split_nat_inf … x2) -x2 //
+#n2 <yplus_inj_dx <yplus_inj_dx
+@niter_appl
+qed.
+
+(*** yplus_succ_swap *)
+lemma yplus_succ_shift (x1) (x2): ↑x1 + x2 = x1 + ↑x2.
+// qed-.
+
+(* Constructions with nplus *************************************************)
+
+(*** yplus_inj *)
+lemma yplus_inj_bi (n) (m):
+ yinj_nat (m + n) = yinj_nat m + yinj_nat n.
+#n @(nat_ind_succ … n) -n //
+#n #IH #m
+<nplus_succ_dx >ysucc_inj >ysucc_inj <yplus_succ_dx //
+qed.
+
+(* Advaced constructions ****************************************************)
+
+(*** ysucc_iter_Y yplus_Y1 *)
+lemma yplus_inf_sn (x): ∞ = ∞ + x.
+#x @(ynat_ind_succ … x) -x //
+#n #IH <yplus_succ_dx //
+qed.
+
+(*** yplus_O1 *)
+lemma yplus_zero_sn (x): x = 𝟎 + x.
+#x @(ynat_split_nat_inf … x) -x //
+qed.
+
+(*** yplus_comm *)
+lemma yplus_comm: commutative … yplus.
+#x1 @(ynat_split_nat_inf … x1) -x1 //
+#n1 #x2 @(ynat_split_nat_inf … x2) -x2 //
+#n2 <yplus_inj_bi <yplus_inj_bi //
+qed.
+
+(*** yplus_assoc *)
+lemma yplus_assoc: associative … yplus.
+#x1 #x2 @(ynat_split_nat_inf … x2) -x2 //
+#n2 #x3 @(ynat_split_nat_inf … x3) -x3 //
+#n3 @(ynat_split_nat_inf … x1) -x1 //
+<yplus_inf_sn //
+qed.
+
+(*** yplus_comm_23 *)
+lemma yplus_plus_comm_23 (z) (x) (y):
+ z + x + y = z + y + x.
+#z #x #y >yplus_assoc //
+qed.
+
+lemma yplus_plus_comm_13 (x) (y) (z):
+ x + z + y = y + z + x.
+// qed.
+
+(*** yplus_comm_24 *)
+lemma yplus_plus_comm_24 (x1) (x4) (x2) (x3):
+ x1 + x4 + x3 + x2 = x1 + x2 + x3 + x4.
+#x1 #x4 #x2 #x3
+>yplus_assoc >yplus_assoc >yplus_assoc >yplus_assoc //
+qed.
+
+(*** yplus_assoc_23 *)
+lemma yplus_plus_assoc_23 (x1) (x4) (x2) (x3):
+ x1 + (x2 + x3) + x4 = x1 + x2 + (x3 + x4).
+#x1 #x4 #x2 #x3
+>yplus_assoc >yplus_assoc //
+qed.
+
+(* Basic inversions *********************************************************)
+
+(*** yplus_inv_Y1 *)
+lemma eq_inv_inf_plus (x) (y):
+ ∞ = x + y → ∨∨ ∞ = x | ∞ = y.
+#x @(ynat_split_nat_inf … x) -x /2 width=1 by or_introl/
+#m #y @(ynat_split_nat_inf … y) -y /2 width=1 by or_introl/
+#n <yplus_inj_bi #H
+elim (eq_inv_inf_yinj_nat … H)
+qed-.
+
+(*** yplus_inv_Y2 *)
+lemma eq_inv_plus_inf (x) (y):
+ x + y = ∞ → ∨∨ ∞ = x | ∞ = y.
+/2 width=1 by eq_inv_inf_plus/ qed-.
+
+(*** discr_yplus_x_xy discr_yplus_xy_x *)
+lemma yplus_refl_sn (x) (y):
+ x = x + y → ∨∨ ∞ = x | 𝟎 = y.
+#x @(ynat_split_nat_inf … x) -x /2 width=1 by or_introl/
+#m #y @(ynat_split_nat_inf … y) -y /2 width=1 by or_introl/
+#n <yplus_inj_bi #H
+lapply (eq_inv_yinj_nat_bi … H) -H #H
+<(nplus_refl_sn … H) -n //
+qed-.
+
+(*** yplus_inv_monotonic_dx_inj *)
+lemma eq_inv_yplus_bi_dx_inj (o) (x) (y):
+ x + yinj_nat o = y + yinj_nat o → x = y.
+#o @(nat_ind_succ … o) -o //
+#o #IH #x #y >ysucc_inj <yplus_succ_dx <yplus_succ_dx #H
+/3 width=1 by eq_inv_ysucc_bi/
+qed-.
+
+lemma eq_inv_yplus_bi_sn_inj (o) (x) (y):
+ yinj_nat o + x = yinj_nat o + y → x = y.
+/2 width=2 by eq_inv_yplus_bi_dx_inj/ qed-.
+
+(* Inversions with nplus ****************************************************)
+
+(*** yplus_inv_inj *)
+lemma eq_inv_inj_yplus (o) (x) (y):
+ yinj_nat o = x + y →
+ ∃∃m,n. o = m + n & x = yinj_nat m & y = yinj_nat n.
+#o #x @(ynat_split_nat_inf … x) -x
+[| #y <yplus_inf_sn #H elim (eq_inv_yinj_nat_inf … H) ]
+#m #y @(ynat_split_nat_inf … y) -y
+[| #H elim (eq_inv_yinj_nat_inf … H) ]
+#n <yplus_inj_bi #H
+/3 width=5 by eq_inv_yinj_nat_bi, ex3_2_intro/
+qed-.
+
+lemma eq_inv_yplus_inj (o) (x) (y):
+ x + y = yinj_nat o →
+ ∃∃m,n. o = m + n & x = yinj_nat m & y = yinj_nat n.
+#o #x #y <yplus_comm
+/2 width=1 by eq_inv_inj_yplus/
+qed-.
+
+(* Advanced inversions ******************************************************)
+
+(*** yplus_inv_O *)
+lemma eq_inv_zero_yplus (x) (y):
+ (𝟎) = x + y → ∧∧ 𝟎 = x & 𝟎 = y.
+#x #y #H
+elim (eq_inv_inj_yplus (𝟎) ?? H) -H #m #n #H #H1 #H2 destruct
+elim (eq_inv_zero_nplus … H) -H #H1 #H2 destruct
+/2 width=1 by conj/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_pred.ma".
+include "ground/arith/ynat_nat.ma".
+
+(* PREDECESSOR FOR NON-NEGATIVE INTEGERS WITH INFINITY **********************)
+
+definition ypred_aux (n): ynat ≝
+ yinj_nat (↓n).
+
+(*** ypred *)
+definition ypred: ynat → ynat ≝
+ ynat_bind_nat ypred_aux (∞).
+
+interpretation
+ "successor (non-negative integers with infinity)"
+ 'DownArrow x = (ypred x).
+
+(* Constructions ************************************************************)
+
+(*** ypred_O *)
+lemma ypred_inj (n): yinj_nat (↓n) = ↓(yinj_nat n).
+@(ynat_bind_nat_inj ypred_aux)
+qed.
+
+(*** ypred_Y *)
+lemma ypred_inf: ∞ = ↓∞.
+// qed.
+
+(* Inversions ***************************************************************)
+
+lemma eq_inv_ypred_inj (x) (n):
+ ↓x = yinj_nat n →
+ ∃∃m. x = yinj_nat m & n = ↓m.
+#x #n @(ynat_split_nat_inf … x) -x
+[ #m <ypred_inj #H <(eq_inv_yinj_nat_bi … H) -n
+ /2 width=3 by ex2_intro/
+| #H elim (eq_inv_inf_yinj_nat … H)
+]
+qed-.
+
+(*** ypred_inv_refl *)
+lemma ypred_inv_refl (x): x = ↓x → ∨∨ 𝟎 = x | ∞ = x.
+#x @(ynat_split_nat_inf … x) -x //
+#n <ypred_inj #H
+lapply (eq_inv_yinj_nat_bi … H) -H #H
+lapply (npred_inv_refl … H) -H #H
+/2 width=1 by or_introl/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_pred_succ.ma".
+include "ground/arith/ynat_succ.ma".
+include "ground/arith/ynat_pred.ma".
+
+(* PREDECESSOR FOR NON-NEGATIVE INTEGERS WITH INFINITY **********************)
+
+(* Constructions with ysucc *************************************************)
+
+(*** ypred_succ ypred_S *)
+lemma ypred_succ (x): x = ↓↑x.
+#x @(ynat_split_nat_inf … x) -x //
+qed.
+
+(* Inversion with ysucc *****************************************************)
+
+(*** ynat_cases *)
+lemma ynat_split_zero_pos (x): ∨∨ 𝟎 = x | x = ↑↓x.
+#x @(ynat_split_nat_inf … x) -x //
+#n elim (nat_split_zero_pos n)
+/2 width=1 by or_introl, or_intror/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_succ.ma".
+include "ground/arith/ynat_nat.ma".
+
+(* SUCCESSOR FOR NON-NEGATIVE INTEGERS WITH INFINITY ************************)
+
+definition ysucc_aux (n): ynat ≝
+ yinj_nat (↑n).
+
+(*** ysucc *)
+definition ysucc: ynat → ynat ≝
+ ynat_bind_nat ysucc_aux (∞).
+
+interpretation
+ "successor (non-negative integers with infinity)"
+ 'UpArrow x = (ysucc x).
+
+(* Constructions ************************************************************)
+
+(*** ysucc_inj *)
+lemma ysucc_inj (n): yinj_nat (↑n) = ↑(yinj_nat n).
+@(ynat_bind_nat_inj ysucc_aux)
+qed.
+
+(*** ysucc_Y *)
+lemma ysucc_inf: ∞ = ↑(∞).
+// qed.
+
+(* Inversion lemmas *********************************************************)
+
+(*** ysucc_inv_inj_sn *)
+lemma eq_inv_inj_ysucc (n1) (x2):
+ yinj_nat n1 = ↑x2 →
+ ∃∃n2. yinj_nat n2 = x2 & ↑n2 = n1.
+#n1 #x2 @(ynat_split_nat_inf … x2) -x2
+[ /3 width=3 by eq_inv_yinj_nat_bi, ex2_intro/
+| #H elim (eq_inv_yinj_nat_inf … H)
+]
+qed-.
+
+(*** ysucc_inv_inj_dx *)
+lemma eq_inv_ysucc_inj (x1) (n2):
+ ↑x1 = yinj_nat n2 →
+ ∃∃n1. yinj_nat n1 = x1 & ↑n1 = n2.
+/2 width=1 by eq_inv_inj_ysucc/ qed-.
+
+(*** ysucc_inv_Y_sn *)
+lemma eq_inv_inf_ysucc (x2): ∞ = ↑x2 → ∞ = x2.
+#x2 @(ynat_split_nat_inf … x2) -x2 //
+#n1 <ysucc_inj #H elim (eq_inv_inf_yinj_nat … H)
+qed-.
+
+(*** ysucc_inv_Y_dx *)
+lemma eq_inv_ysucc_inf (x1): ↑x1 = ∞ → ∞ = x1.
+/2 width=1 by eq_inv_inf_ysucc/ qed-.
+
+(*** ysucc_inv_inj *)
+lemma eq_inv_ysucc_bi: injective … ysucc.
+#x1 @(ynat_split_nat_inf … x1) -x1
+[ #n1 #x2 <ysucc_inj #H
+ elim (eq_inv_inj_ysucc … H) -H #n2 #H1 #H2 destruct
+ /3 width=1 by eq_inv_nsucc_bi, eq_f/
+| #x2 #H <(eq_inv_inf_ysucc … H) -H //
+]
+qed-.
+
+(*** ysucc_inv_refl *)
+lemma ysucc_inv_refl (x): x = ↑x → ∞ = x.
+#x @(ynat_split_nat_inf … x) -x //
+#n <ysucc_inj #H
+lapply (eq_inv_yinj_nat_bi … H) -H #H
+elim (nsucc_inv_refl … H)
+qed-.
+
+(*** ysucc_inv_O_sn *)
+lemma eq_inv_zero_ysucc (x): 𝟎 = ↑x → ⊥.
+#x #H
+elim (eq_inv_inj_ysucc (𝟎) ? H) -H #n #_ #H
+/2 width=2 by eq_inv_zero_nsucc/
+qed-.
+
+(*** ysucc_inv_O_dx *)
+lemma eq_inv_ysucc_zero (x): ↑x = 𝟎 → ⊥.
+/2 width=2 by eq_inv_zero_ysucc/ qed-.
+
+(* Eliminators **************************************************************)
+
+(*** ynat_ind *)
+lemma ynat_ind_succ (Q:predicate …):
+ Q (𝟎) → (∀n:nat. Q (yinj_nat n) → Q (↑(yinj_nat n))) → Q (∞) → ∀x. Q x.
+#Q #IH1 #IH2 #IH3 #x @(ynat_split_nat_inf … x) -x //
+#n @(nat_ind_succ … n) -n /2 width=1 by/
+qed-.
#m #n #H1 #H2 #H3 destruct
elim (yle_inv_plus_inj2 … Hz) -Hz /2 width=2 by ex4_2_intro/
qed-.
+
+(* Inversions with yplus ****************************************************)
+
+(*** yle_inv_plus_dx *)
+lemma yle_inv_plus_dx (x) (y):
+ x ≤ y → ∃z. x + z = y.
+#x #y * -x -y
+[ #m #n #H
+
+ @(ex_intro … (yinj (n-m))) (**) (* explicit constructor *)
+ /3 width=1 by plus_minus, eq_f/
+| /2 width=2 by ex_intro/
+]
+qed-.
+
+lemma yle_inv_plus_sn: ∀x,y. x ≤ y → ∃z. z + x = y.
+#x #y #H elim (yle_inv_plus_dx … H) -H
+/2 width=2 by ex_intro/
+qed-.
+
+lemma ylt_inv_plus_sn: ∀x,y. x < y → ∃∃z. ↑z + x = y & x < ∞.
+#x #y #H elim (ylt_inv_le … H) -H
+#Hx #H elim (yle_inv_plus_sn … H) -H
+/2 width=2 by ex2_intro/
+qed-.
+
+lemma ylt_inv_plus_dx: ∀x,y. x < y → ∃∃z. x + ↑z = y & x < ∞.
+#x #y #H elim (ylt_inv_plus_sn … H) -H
+#z >yplus_comm /2 width=2 by ex2_intro/
+qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basics/relations.ma".
-
-(* GENERATED LIBRARY ********************************************************)
-
-lemma insert_eq_0: ∀A,a. ∀Q1,Q2:predicate A. (∀a0. Q1 a0 → a = a0 → Q2 a0) → Q1 a → Q2 a.
-/2 width=1 by/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basics/relations.ma".
+
+(* GENERATED LIBRARY ********************************************************)
+
+lemma insert_eq_1 (T1) (a1) (Q1,Q2:predicate T1):
+ (∀b1. Q1 b1 → a1 = b1 → Q2 b1) → Q1 a1 → Q2 a1.
+/2 width=1 by/ qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basics/core_notation/exp_2.ma".
-include "arithmetics/nat.ma".
-include "ground/xoa/ex_3_1.ma".
-include "ground/xoa/or_3.ma".
-include "ground/notation/functions/uparrow_1.ma".
-include "ground/notation/functions/downarrow_1.ma".
-include "ground/pull/pull_2.ma".
-include "ground/lib/relations.ma".
-
-(* ARITHMETICAL PROPERTIES **************************************************)
-
-interpretation "nat successor" 'UpArrow m = (S m).
-
-interpretation "nat predecessor" 'DownArrow m = (pred m).
-
-interpretation "nat min" 'and x y = (min x y).
-
-interpretation "nat max" 'or x y = (max x y).
-
-(* Iota equations ***********************************************************)
-
-lemma pred_O: pred 0 = 0.
-normalize // qed.
-
-lemma pred_S: ∀m. pred (S m) = m.
-// qed.
-
-lemma plus_S1: ∀x,y. ↑(x+y) = (↑x) + y.
-// qed.
-
-lemma max_O1: ∀n. n = (0 ∨ n).
-// qed.
-
-lemma max_O2: ∀n. n = (n ∨ 0).
-// qed.
-
-lemma max_SS: ∀n1,n2. ↑(n1∨n2) = (↑n1 ∨ ↑n2).
-#n1 #n2 elim (decidable_le n1 n2) #H normalize
-[ >(le_to_leb_true … H) | >(not_le_to_leb_false … H) ] -H //
-qed.
-
-(* Equalities ***************************************************************)
-
-lemma plus_SO_sn (n): 1 + n = ↑n.
-// qed-.
-
-lemma plus_SO_dx (n): n + 1 = ↑n.
-// qed.
-
-lemma minus_SO_dx (n): n-1 = ↓n.
-// qed.
-
-lemma minus_plus_m_m_commutative: ∀n,m:nat. n = m + n - m.
-// qed-.
-
-lemma plus_minus_m_m_commutative (n) (m): m ≤ n → n = m+(n-m).
-/2 width=1 by plus_minus_associative/ qed-.
-
-lemma plus_to_minus_2: ∀m1,m2,n1,n2. n1 ≤ m1 → n2 ≤ m2 →
- m1+n2 = m2+n1 → m1-n1 = m2-n2.
-#m1 #m2 #n1 #n2 #H1 #H2 #H
-@plus_to_minus >plus_minus_associative //
-qed-.
-
-(* Note: uses minus_minus_comm, minus_plus_m_m, commutative_plus, plus_minus *)
-lemma plus_minus_minus_be: ∀x,y,z. y ≤ z → z ≤ x → (x - z) + (z - y) = x - y.
-#x #z #y #Hzy #Hyx >plus_minus // >commutative_plus >plus_minus //
-qed-.
-
-lemma lt_succ_pred: ∀m,n. n < m → m = ↑↓m.
-#m #n #Hm >S_pred /2 width=2 by ltn_to_ltO/
-qed-.
-
-fact plus_minus_minus_be_aux: ∀i,x,y,z. y ≤ z → z ≤ x → i = z - y → x - z + i = x - y.
-/2 width=1 by plus_minus_minus_be/ qed-.
-
-lemma le_plus_minus: ∀m,n,p. p ≤ n → m + n - p = m + (n - p).
-/2 by plus_minus/ qed-.
-
-lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → m + n - p = m - p + n.
-/2 by plus_minus/ qed-.
-
-lemma minus_minus_comm3: ∀n,x,y,z. n-x-y-z = n-y-z-x.
-// qed.
-
-lemma idempotent_max: ∀n:nat. n = (n ∨ n).
-#n normalize >le_to_leb_true //
-qed.
-
-lemma associative_max: associative … max.
-#x #y #z normalize
-@(leb_elim x y) normalize #Hxy
-@(leb_elim y z) normalize #Hyz //
-[1,2: >le_to_leb_true /2 width=3 by transitive_le/
-| >not_le_to_leb_false /4 width=3 by lt_to_not_le, not_le_to_lt, transitive_lt/
- >not_le_to_leb_false //
-]
-qed.
-
-(* Properties ***************************************************************)
-
-lemma eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2).
-#n1 elim n1 -n1 [| #n1 #IHn1 ] * [2,4: #n2 ]
-[1,4: @or_intror #H destruct
-| elim (IHn1 n2) -IHn1 /3 width=1 by or_intror, or_introl/
-| /2 width=1 by or_introl/
-]
-qed-.
-
-lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m.
-#m #n elim (lt_or_ge m n) /2 width=1 by or3_intro0/
-#H elim H -m /2 width=1 by or3_intro1/
-#m #Hm * /3 width=1 by not_le_to_lt, le_S_S, or3_intro2/
-qed-.
-
-lemma monotonic_le_minus_l2: ∀x1,x2,y,z. x1 ≤ x2 → x1 - y - z ≤ x2 - y - z.
-/3 width=1 by monotonic_le_minus_l/ qed.
-
-lemma minus_le_trans_sn: ∀x1,x2. x1 ≤ x2 → ∀x. x1-x ≤ x2.
-/2 width=3 by transitive_le/ qed.
-
-lemma le_plus_to_minus_l: ∀a,b,c. a + b ≤ c → b ≤ c-a.
-/2 width=1 by le_plus_to_minus_r/
-qed-.
-
-lemma le_plus_to_minus_comm: ∀n,m,p. n ≤ p+m → n-p ≤ m.
-/2 width=1 by le_plus_to_minus/ qed-.
-
-lemma le_inv_S1: ∀m,n. ↑m ≤ n → ∃∃p. m ≤ p & ↑p = n.
-#m *
-[ #H lapply (le_n_O_to_eq … H) -H
- #H destruct
-| /3 width=3 by monotonic_pred, ex2_intro/
-]
-qed-.
-
-(* Note: this might interfere with nat.ma *)
-lemma monotonic_lt_pred: ∀m,n. m < n → 0 < m → pred m < pred n.
-#m #n #Hmn #Hm whd >(S_pred … Hm)
-@le_S_S_to_le >S_pred /2 width=3 by transitive_lt/
-qed.
-
-lemma lt_S_S: ∀x,y. x < y → ↑x < ↑y.
-/2 width=1 by le_S_S/ qed.
-
-lemma lt_S: ∀n,m. n < m → n < ↑m.
-/2 width=1 by le_S/ qed.
-
-lemma monotonic_lt_minus_r:
-∀p,q,n. q < n -> q < p → n-p < n-q.
-#p #q #n #Hn #H
-lapply (monotonic_le_minus_r … n H) -H #H
-@(le_to_lt_to_lt … H) -H
-/2 width=1 by lt_plus_to_minus/
-qed.
-
-lemma max_S1_le_S: ∀n1,n2,n. (n1 ∨ n2) ≤ n → (↑n1 ∨ n2) ≤ ↑n.
-/4 width=2 by to_max, le_maxr, le_S_S, le_S/ qed-.
-
-lemma max_S2_le_S: ∀n1,n2,n. (n1 ∨ n2) ≤ n → (n1 ∨ ↑n2) ≤ ↑n.
-/2 width=1 by max_S1_le_S/ qed-.
-
-(* Inversion & forward lemmas ***********************************************)
-
-lemma lt_refl_false: ∀n. n < n → ⊥.
-#n #H elim (lt_to_not_eq … H) -H /2 width=1 by/
-qed-.
-
-lemma lt_zero_false: ∀n. n < 0 → ⊥.
-#n #H elim (lt_to_not_le … H) -H /2 width=1 by/
-qed-.
-
-lemma lt_le_false: ∀x,y. x < y → y ≤ x → ⊥.
-/3 width=4 by lt_refl_false, lt_to_le_to_lt/ qed-.
-
-lemma le_dec (n) (m): Decidable (n≤m).
-#n elim n -n [ /2 width=1 by or_introl/ ]
-#n #IH * [ /3 width=2 by lt_zero_false, or_intror/ ]
-#m elim (IH m) -IH
-[ /3 width=1 by or_introl, le_S_S/
-| /4 width=1 by or_intror, le_S_S_to_le/
-]
-qed-.
-
-lemma succ_inv_refl_sn: ∀x. ↑x = x → ⊥.
-#x #H @(lt_le_false x (↑x)) //
-qed-.
-
-lemma le_plus_xSy_O_false: ∀x,y. x + S y ≤ 0 → ⊥.
-#x #y #H lapply (le_n_O_to_eq … H) -H <plus_n_Sm #H destruct
-qed-.
-
-lemma le_plus_xySz_x_false: ∀y,z,x. x + y + S z ≤ x → ⊥.
-#y #z #x elim x -x /3 width=1 by le_S_S_to_le/
-#H elim (le_plus_xSy_O_false … H)
-qed-.
-
-lemma plus_xySz_x_false: ∀z,x,y. x + y + S z = x → ⊥.
-/2 width=4 by le_plus_xySz_x_false/ qed-.
-
-lemma plus_xSy_x_false: ∀y,x. x + S y = x → ⊥.
-/2 width=4 by plus_xySz_x_false/ qed-.
-
-lemma pred_inv_fix_sn: ∀x. ↓x = x → 0 = x.
-* // #x <pred_Sn #H
-elim (succ_inv_refl_sn x) //
-qed-.
-
-lemma discr_plus_xy_y: ∀x,y. x + y = y → x = 0.
-// qed-.
-
-lemma discr_plus_x_xy: ∀x,y. x = x + y → y = 0.
-/2 width=2 by le_plus_minus_comm/ qed-.
-
-lemma plus2_le_sn_sn: ∀m1,m2,n1,n2. m1 + n1 = m2 + n2 → m1 ≤ m2 → n2 ≤ n1.
-#m1 #m2 #n1 #n2 #H #Hm
-lapply (monotonic_le_plus_l n1 … Hm) -Hm >H -H
-/2 width=2 by le_plus_to_le/
-qed-.
-
-lemma plus2_le_sn_dx: ∀m1,m2,n1,n2. m1 + n1 = n2 + m2 → m1 ≤ m2 → n2 ≤ n1.
-/2 width=4 by plus2_le_sn_sn/ qed-.
-
-lemma plus2_le_dx_sn: ∀m1,m2,n1,n2. n1 + m1 = m2 + n2 → m1 ≤ m2 → n2 ≤ n1.
-/2 width=4 by plus2_le_sn_sn/ qed-.
-
-lemma plus2_le_dx_dx: ∀m1,m2,n1,n2. n1 + m1 = n2 + m2 → m1 ≤ m2 → n2 ≤ n1.
-/2 width=4 by plus2_le_sn_sn/ qed-.
-
-lemma lt_S_S_to_lt: ∀x,y. ↑x < ↑y → x < y.
-/2 width=1 by le_S_S_to_le/ qed-.
-
-(* Note this should go in nat.ma *)
-lemma discr_x_minus_xy: ∀x,y. x = x - y → x = 0 ∨ y = 0.
-#x @(nat_ind_plus … x) -x /2 width=1 by or_introl/
-#x #_ #y @(nat_ind_plus … y) -y /2 width=1 by or_intror/
-#y #_ >minus_plus_plus_l
-#H lapply (discr_plus_xy_minus_xz … H) -H
-#H destruct
-qed-.
-
-lemma lt_inv_O1: ∀n. 0 < n → ∃m. ↑m = n.
-* /2 width=2 by ex_intro/
-#H cases (lt_le_false … H) -H //
-qed-.
-
-lemma lt_inv_S1: ∀m,n. ↑m < n → ∃∃p. m < p & ↑p = n.
-#m * /3 width=3 by lt_S_S_to_lt, ex2_intro/
-#H cases (lt_le_false … H) -H //
-qed-.
-
-lemma lt_inv_gen: ∀y,x. x < y → ∃∃z. x ≤ z & ↑z = y.
-* /3 width=3 by le_S_S_to_le, ex2_intro/
-#x #H elim (lt_le_false … H) -H //
-qed-.
-
-lemma plus_inv_O3: ∀x,y. x + y = 0 → x = 0 ∧ y = 0.
-/2 width=1 by plus_le_0/ qed-.
-
-lemma plus_inv_S3_sn: ∀x1,x2,x3. x1+x2 = ↑x3 →
- ∨∨ ∧∧ x1 = 0 & x2 = ↑x3
- | ∃∃y1. x1 = ↑y1 & y1 + x2 = x3.
-* /3 width=1 by or_introl, conj/
-#x1 #x2 #x3 <plus_S1 #H destruct
-/3 width=3 by ex2_intro, or_intror/
-qed-.
-
-lemma plus_inv_S3_dx: ∀x2,x1,x3. x1+x2 = ↑x3 →
- ∨∨ ∧∧ x2 = 0 & x1 = ↑x3
- | ∃∃y2. x2 = ↑y2 & x1 + y2 = x3.
-* /3 width=1 by or_introl, conj/
-#x2 #x1 #x3 <plus_n_Sm #H destruct
-/3 width=3 by ex2_intro, or_intror/
-qed-.
-
-lemma max_inv_O3: ∀x,y. (x ∨ y) = 0 → 0 = x ∧ 0 = y.
-/4 width=2 by le_maxr, le_maxl, le_n_O_to_eq, conj/
-qed-.
-
-lemma zero_eq_plus: ∀x,y. 0 = x + y → 0 = x ∧ 0 = y.
-* /2 width=1 by conj/ #x #y normalize #H destruct
-qed-.
-
-lemma nat_split: ∀x. x = 0 ∨ ∃y. ↑y = x.
-* /3 width=2 by ex_intro, or_introl, or_intror/
-qed-.
-
-lemma lt_elim: ∀R:relation nat.
- (∀n2. R O (↑n2)) →
- (∀n1,n2. R n1 n2 → R (↑n1) (↑n2)) →
- ∀n2,n1. n1 < n2 → R n1 n2.
-#R #IH1 #IH2 #n2 elim n2 -n2
-[ #n1 #H elim (lt_le_false … H) -H //
-| #n2 #IH * /4 width=1 by lt_S_S_to_lt/
-]
-qed-.
-
-lemma le_elim: ∀R:relation nat.
- (∀n2. R O (n2)) →
- (∀n1,n2. R n1 n2 → R (↑n1) (↑n2)) →
- ∀n1,n2. n1 ≤ n2 → R n1 n2.
-#R #IH1 #IH2 #n1 #n2 @(nat_elim2 … n1 n2) -n1 -n2
-/4 width=1 by monotonic_pred/ -IH1 -IH2
-#n1 #H elim (lt_le_false … H) -H //
-qed-.
-
-lemma nat_elim_le_sn (Q:relation …):
- (∀m1,m2. (∀m. m < m2-m1 → Q (m2-m) m2) → m1 ≤ m2 → Q m1 m2) →
- ∀n1,n2. n1 ≤ n2 → Q n1 n2.
-#Q #IH #n1 #n2 #Hn
-<(minus_minus_m_m … Hn) -Hn
-lapply (minus_le n2 n1)
-let d ≝ (n2-n1)
-@(nat_elim1 … d) -d -n1 #d
-@pull_2 #Hd
-<(minus_minus_m_m … Hd) in ⊢ (%→?); -Hd
-let n1 ≝ (n2-d) #IHd
-@IH -IH [| // ] #m #Hn
-/4 width=3 by lt_to_le, lt_to_le_to_lt/
-qed-.
-
-(* Iterators ****************************************************************)
-
-(* Note: see also: lib/arithemetics/bigops.ma *)
-rec definition iter (n:nat) (B:Type[0]) (op: B → B) (nil: B) ≝
- match n with
- [ O ⇒ nil
- | S k ⇒ op (iter k B op nil)
- ].
-
-interpretation "iterated function" 'exp op n = (iter n ? op).
-
-lemma iter_O: ∀B:Type[0]. ∀f:B→B.∀b. f^0 b = b.
-// qed.
-
-lemma iter_S: ∀B:Type[0]. ∀f:B→B.∀b,l. f^(S l) b = f (f^l b).
-// qed.
-
-lemma iter_n_Sm: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^l (f b) = f (f^l b).
-#B #f #b #l elim l -l normalize //
-qed.
-
-lemma iter_plus: ∀B:Type[0]. ∀f:B→B. ∀b,l1,l2. f^(l1+l2) b = f^l1 (f^l2 b).
-#B #f #b #l1 elim l1 -l1 normalize //
-qed.
-
-(* Trichotomy operator ******************************************************)
-
-(* Note: this is "if eqb n1 n2 then a2 else if leb n1 n2 then a1 else a3" *)
-rec definition tri (A:Type[0]) n1 n2 a1 a2 a3 on n1 : A ≝
- match n1 with
- [ O ⇒ match n2 with [ O ⇒ a2 | S n2 ⇒ a1 ]
- | S n1 ⇒ match n2 with [ O ⇒ a3 | S n2 ⇒ tri A n1 n2 a1 a2 a3 ]
- ].
-
-lemma tri_lt: ∀A,a1,a2,a3,n2,n1. n1 < n2 → tri A n1 n2 a1 a2 a3 = a1.
-#A #a1 #a2 #a3 #n2 elim n2 -n2
-[ #n1 #H elim (lt_zero_false … H)
-| #n2 #IH #n1 elim n1 -n1 /3 width=1 by monotonic_lt_pred/
-]
-qed.
-
-lemma tri_eq: ∀A,a1,a2,a3,n. tri A n n a1 a2 a3 = a2.
-#A #a1 #a2 #a3 #n elim n -n normalize //
-qed.
-
-lemma tri_gt: ∀A,a1,a2,a3,n1,n2. n2 < n1 → tri A n1 n2 a1 a2 a3 = a3.
-#A #a1 #a2 #a3 #n1 elim n1 -n1
-[ #n2 #H elim (lt_zero_false … H)
-| #n1 #IH #n2 elim n2 -n2 /3 width=1 by monotonic_lt_pred/
-]
-qed.
-
-(* Decidability of predicates ***********************************************)
-
-lemma dec_lt (R:predicate nat):
- (∀n. Decidable … (R n)) →
- ∀n. Decidable … (∃∃m. m < n & R m).
-#R #HR #n elim n -n [| #n * ]
-[ @or_intror * /2 width=2 by lt_zero_false/
-| * /4 width=3 by lt_S, or_introl, ex2_intro/
-| #H0 elim (HR n) -HR
- [ /3 width=3 by or_introl, ex2_intro/
- | #Hn @or_intror * #m #Hmn #Hm
- elim (le_to_or_lt_eq … Hmn) -Hmn #H destruct [ -Hn | -H0 ]
- /4 width=3 by lt_S_S_to_lt, ex2_intro/
- ]
-]
-qed-.
-
-lemma dec_min (R:predicate nat):
- (∀n. Decidable … (R n)) → ∀n. R n →
- ∃∃m. m ≤ n & R m & (∀p. p < m → R p → ⊥).
-#R #HR #n
-@(nat_elim1 n) -n #n #IH #Hn
-elim (dec_lt … HR n) -HR [ -Hn | -IH ]
-[ * #p #Hpn #Hp
- elim (IH … Hpn Hp) -IH -Hp #m #Hmp #Hm #HNm
- @(ex3_intro … Hm HNm) -HNm
- /3 width=3 by lt_to_le, le_to_lt_to_lt/
-| /4 width=4 by ex3_intro, ex2_intro/
-]
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground/lib/arith.ma".
-
-(* ARITHMETICAL PROPERTIES FOR λδ-2B ****************************************)
-
-(* Equalities ***************************************************************)
-
-lemma plus_n_2: ∀n. n + 2 = n + 1 + 1.
-// qed.
-
-lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b.
-#a #b #c1 #H >minus_minus_comm >minus_le_minus_minus_comm //
-qed-.
-
-lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b.
-#a #b #c1 #c2 #H >minus_plus >minus_plus >minus_plus /2 width=1 by arith_b1/
-qed-.
-
-lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b.
-/3 by monotonic_le_minus_l, le_to_le_to_eq, le_n/ qed.
-
-lemma arith_h1: ∀a1,a2,b,c1. c1 ≤ a1 → c1 ≤ b →
- a1 - c1 + a2 - (b - c1) = a1 + a2 - b.
-#a1 #a2 #b #c1 #H1 #H2 >plus_minus /2 width=1 by arith_b2/
-qed-.
-
-lemma arith_i: ∀x,y,z. y < x → x+z-y-1 = x-y-1+z.
-/2 width=1 by plus_minus/ qed-.
-
-(* Properties ***************************************************************)
-
-fact le_repl_sn_conf_aux: ∀x,y,z:nat. x ≤ z → x = y → y ≤ z.
-// qed-.
-
-fact le_repl_sn_trans_aux: ∀x,y,z:nat. x ≤ z → y = x → y ≤ z.
-// qed-.
-
-lemma arith_j: ∀x,y,z. x-y-1 ≤ x-(y-z)-1.
-/3 width=1 by monotonic_le_minus_l, monotonic_le_minus_r/ qed.
-
-lemma arith_k_sn: ∀z,x,y,n. z < x → x+n ≤ y → x-z-1+n ≤ y-z-1.
-#z #x #y #n #Hzx #Hxny
->plus_minus [2: /2 width=1 by monotonic_le_minus_r/ ]
->plus_minus [2: /2 width=1 by lt_to_le/ ]
-/2 width=1 by monotonic_le_minus_l2/
-qed.
-
-lemma arith_k_dx: ∀z,x,y,n. z < x → y ≤ x+n → y-z-1 ≤ x-z-1+n.
-#z #x #y #n #Hzx #Hyxn
->plus_minus [2: /2 width=1 by monotonic_le_minus_r/ ]
->plus_minus [2: /2 width=1 by lt_to_le/ ]
-/2 width=1 by monotonic_le_minus_l2/
-qed.
-
-(* Inversion & forward lemmas ***********************************************)
-
-lemma lt_plus_SO_to_le: ∀x,y. x < y + 1 → x ≤ y.
-/2 width=1 by monotonic_pred/ qed-.
-
-(* Iterators ****************************************************************)
-
-lemma iter_SO: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^(l+1) b = f (f^l b).
-#B #f #b #l >commutative_plus //
-qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground/lib/arith.ma".
-
-(* ARITHMETICAL PROPERTIES FOR λδ-2B ****************************************)
-
-lemma arith_l4 (m11) (m12) (m21) (m22):
- m21+m22-(m11+m12) = m21-m11-m12+(m22-(m11-m21)-(m12-(m21-m11))).
-#m11 #m12 #m21 #m22 >minus_plus
-elim (le_or_ge (m11+m12) m21) #Hm1121
-[ lapply (transitive_le m11 ??? Hm1121) // #Hm121
- lapply (le_plus_to_minus_l … Hm1121) #Hm12211
- <plus_minus // @eq_f2 // >(eq_minus_O m11 ?) // >(eq_minus_O m12 ?) //
-| >(eq_minus_O m21 ?) // <plus_O_n <minus_plus <commutative_plus
- elim (le_or_ge m11 m21) #Hm121
- [ lapply (le_plus_to_minus_comm … Hm1121) #Hm2112
- >(eq_minus_O m11 ?) // <plus_minus_associative // <minus_le_minus_minus_comm //
- | >(eq_minus_O m21 ?) // <minus_le_minus_minus_comm //
- ]
-]
-qed.
-
-lemma arith_l3 (m) (n1) (n2): n1+n2-m = n1-m+(n2-(m-n1)).
-// qed.
-
-lemma arith_l2 (n1) (n2): ↑n2-n1 = 1-n1+(n2-(n1-1)).
-#n1 #n2 <arith_l3 //
-qed.
-
-lemma arith_l1: ∀x. 1 = 1-x+(x-(x-1)).
-#x <arith_l2 //
-qed.
(* EXTENSIONAL EQUIVALENCE **************************************************)
definition exteq (A,B:Type[0]): relation (A → B) ≝
- λf1,f2. ∀a. f1 a = f2 a.
+ λf1,f2. ∀a. f1 a = f2 a.
-interpretation "extensional equivalence"
- 'DotEq A B f1 f2 = (exteq A B f1 f2).
+interpretation
+ "extensional equivalence"
+ 'DotEq A B f1 f2 = (exteq A B f1 f2).
-(* Basic_properties *********************************************************)
+(* Basic Constructions ******************************************************)
lemma exteq_refl (A) (B): reflexive … (exteq A B).
// qed.
lemma exteq_trans (A) (B): Transitive … (exteq A B).
/2 width=1 by exteq_repl/ qed-.
+
+lemma exteq_canc_sn (A) (B): left_cancellable … (exteq A B).
+/2 width=1 by exteq_repl/ qed-.
+
+lemma exteq_canc_dx (A) (B): right_cancellable … (exteq A B).
+/2 width=1 by exteq_repl/ qed-.
+
+(* Constructions with function composition **********************************)
+
+lemma compose_repl_fwd_dx (A) (B) (C) (g) (f1) (f2):
+ f1 ≐{A,B} f2 → g ∘ f1 ≐{A,C} g ∘ f2.
+#A #B #C #g #f1 #f2 #Hf12 #a
+whd in ⊢ (??%%); //
+qed.
+
+lemma compose_repl_bak_dx (A) (B) (C) (g) (f1) (f2):
+ f1 ≐{A,B} f2 → g ∘ f2 ≐{A,C} g ∘ f1.
+/3 width=1 by compose_repl_fwd_dx, exteq_sym/
+qed.
+
+lemma compose_repl_fwd_sn (A) (B) (C) (g1) (g2) (f):
+ g1 ≐{B,C} g2 → g1 ∘ f ≐{A,C} g2 ∘ f.
+#A #B #C #g1 #g2 #f #Hg12 #a
+whd in ⊢ (??%%); //
+qed.
+
+lemma compose_repl_bak_sn (A) (B) (C) (g1) (g2) (f):
+ g1 ≐{B,C} g2 → g2 ∘ f ≐{A,C} g1 ∘ f.
+/3 width=1 by compose_repl_fwd_sn, exteq_sym/
+qed.
+
+lemma compose_assoc (A1) (A2) (A3) (A4) (f3:A3→A4) (f2:A2→A3) (f1:A1→A2):
+ f3 ∘ (f2 ∘ f1) ≐ f3 ∘ f2 ∘ f1.
+// qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "𝟐"
+ non associative with precedence 55
+ for @{ 'Two }.
</body>
<table name="ground_sum"/>
+ <news class="gamma" date="2021-02-15.">
+ Primitive arithmetics library.
+ </news>
<news class="gamma" date="2020-12-08.">
Specification is repackaged for publication.
</news>
}
]
class "grass"
- [ { "natural numbers with infinity" * } {
- [ { "" * } {
- [ "ynat ( ∞ )" "ynat_pred ( ↓? )" "ynat_succ ( ↑? )"
- "ynat_le ( ? ≤ ? )" "ynat_lt ( ? < ? )"
- "ynat_plus ( ? + ? )" "ynat_minus_sn ( ? - ? )" *
- ]
+ [ { "arithmetics" * } {
+ [ { "extensions" * } {
+ [ "arith_2a ( 𝟐 )" "arith_2b" * ]
+ }
+ ]
+ [ { "well-founded induction" * } {
+ [ "wf1_ind_ylt" * ]
+ [ "wf1_ind_nlt" "wf2_ind_nlt" "wf3_ind_nlt.ma" * ]
+ }
+ ]
+ [ { "non-negative integers with infinity" * } {
+ [ "ynat_lt ( ?<? )" "ynat_lt_succ" "ynat_lt_pred" "ynat_lt_pred_succ" "ynat_lt_plus" "ynat_lt_plus_pred" "ynat_lt_minus1" "ynat_lt_minus1_plus" "ynat_lt_le" "ynat_lt_le_succ" "ynat_lt_le_pred" "ynat_lt_le_pred_succ" "ynat_lt_le_plus" "ynat_lt_le_minus1" "ynat_lt_le_minus1_plus" * ]
+ [ "ynat_le ( ?≤? )" "ynat_le_succ" "ynat_le_pred" "ynat_le_pred_succ" "ynat_le_plus" "ynat_le_minus1" "ynat_le_minus1_succ" "ynat_le_minus1_plus" * ]
+ [ "ynat_minus1 ( ?-? )" "ynat_minus1_succ" "ynat_minus1_plus" * ]
+ [ "ynat_plus ( ?+? )" * ]
+ [ "ynat_pred ( ↓? )" "ynat_pred_succ" * ]
+ [ "ynat_succ ( ↑? )" * ]
+ [ "ynat ( 𝟎 ) ( ∞ )" "ynat_nat" * ]
}
]
- }
- ]
- class "grass"
- [ { "arithmetics" * } {
[ { "non-negative integers" * } {
[ "nat_lt ( ?<? )" "nat_lt_tri" "nat_lt_pred" "nat_lt_plus" "nat_lt_minus" "nat_lt_minus_plus" * ]
[ "nat_le ( ?≤? )" "nat_le_pred" "nat_le_plus" "nat_le_minus" "nat_le_minus_plus" "nat_le_max" * ]
]
[ { "positive integers" * } {
[ "pnat_plus ( ?+? )" * ]
- [ "pnat ( 𝟏 ) ( ↑? )" "pnat_dis" "pnat_iter ( ?^{?}? )" *"pnat_tri" ]
+ [ "pnat ( 𝟏 ) ( ↑? )" "pnat_dis" "pnat_iter ( ?^{?}? )" "pnat_tri" * ]
}
]
}
[ { "" * } {
[ "stream ( ? ⨮{?} ? )" "stream_eq ( ? ≗{?} ? )" "stream_hdtl ( ⫰{?}? )" "stream_tls ( ⫰*{?}[?]? )" * ]
[ "list ( Ⓔ{?} ) ( ? ⨮{?} ? )" "list_length ( |?| )" * ]
- [ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ↑? ) ( ↓? ) ( ? ∨ ? ) ( ? ∧ ? )" "arith_2a" "arith_2b" * ]
+ [ "bool ( Ⓕ ) ( Ⓣ )" * ]
[ "ltc" "ltc_ctc" * ]
[ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "exteq ( ? ≐{?,?} ? )" "star" "lstar_2a" * ]
}
]
class "orange"
[ { "generated library" * } {
- [ { "well-founded induction" * } {
- [ "wf1_ind_nlt" "wf2_ind_nlt" "wf3_ind_nlt.ma" * ]
- }
- ]
[ { "generalization with equality" * } {
[ "insert_eq" * ]
}
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground/arith/nat_lt.ma".
-
-(* WELL-FOUNDED INDUCTION ***************************************************)
-
-fact wf1_ind_nlt_aux (A1) (f:A1→nat) (Q:predicate …):
- (∀n. (∀a1. f a1 < n → Q a1) → ∀a1. f a1 = n → Q a1) →
- ∀n,a1. f a1 = n → Q a1.
-#A1 #f #Q #H #n @(nat_ind_lt … n) -n /3 width=3 by/
-qed-.
-
-(*** f_ind *)
-lemma wf1_ind_nlt (A1) (f:A1→nat) (Q:predicate …):
- (∀n. (∀a1. f a1 < n → Q a1) → ∀a1. f a1 = n → Q a1) →
- ∀a1. Q a1.
-#A #f #Q #H #a1 @(wf1_ind_nlt_aux … H) -H //
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground/arith/nat_lt.ma".
-
-(* WELL-FOUNDED INDUCTION ***************************************************)
-
-fact wf2_ind_nlt_aux (A1) (A2) (f:A1→A2→nat) (Q:relation2 …):
- (∀n. (∀a1,a2. f a1 a2 < n → Q a1 a2) → ∀a1,a2. f a1 a2 = n → Q a1 a2) →
- ∀n,a1,a2. f a1 a2 = n → Q a1 a2.
-#A1 #A2 #f #Q #H #n @(nat_ind_lt … n) -n /3 width=3 by/
-qed-.
-
-(*** f2_ind *)
-lemma wf2_ind_nlt (A1) (A2) (f:A1→A2→nat) (Q:relation2 …):
- (∀n. (∀a1,a2. f a1 a2 < n → Q a1 a2) → ∀a1,a2. f a1 a2 = n → Q a1 a2) →
- ∀a1,a2. Q a1 a2.
-#A1 #A2 #f #Q #H #a1 #a2 @(wf2_ind_nlt_aux … H) -H //
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground/arith/nat_lt.ma".
-
-(* WELL-FOUNDED INDUCTION ***************************************************)
-
-fact wf3_ind_nlt_aux (A1) (A2) (A3) (f:A1→A2→A3→nat) (Q:relation3 …):
- (∀n. (∀a1,a2,a3. f a1 a2 a3 < n → Q a1 a2 a3) → ∀a1,a2,a3. f a1 a2 a3 = n → Q a1 a2 a3) →
- ∀n,a1,a2,a3. f a1 a2 a3 = n → Q a1 a2 a3.
-#A1 #A2 #A3 #f #Q #H #n @(nat_ind_lt … n) -n /3 width=3 by/
-qed-.
-
-(*** f3_ind *)
-lemma wf3_ind_nlt (A1) (A2) (A3) (f:A1→A2→A3→nat) (Q:relation3 …):
- (∀n. (∀a1,a2,a3. f a1 a2 a3 < n → Q a1 a2 a3) → ∀a1,a2,a3. f a1 a2 a3 = n → Q a1 a2 a3) →
- ∀a1,a2,a3. Q a1 a2 a3.
-#A1 #A2 #A3 #f #Q #H #a1 #a2 #a3 @(wf3_ind_nlt_aux … H) -H //
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground/lib/arith.ma".
-include "ground/notation/functions/infinity_0.ma".
-
-(* NATURAL NUMBERS WITH INFINITY ********************************************)
-
-(* the type of natural numbers with infinity *)
-inductive ynat: Type[0] ≝
-| yinj: nat → ynat
-| Y : ynat
-.
-
-coercion yinj.
-
-interpretation "ynat infinity" 'Infinity = Y.
-
-(* Inversion lemmas *********************************************************)
-
-lemma yinj_inj: ∀m,n. yinj m = yinj n → m = n.
-#m #n #H destruct //
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma eq_ynat_dec: ∀n1,n2:ynat. Decidable (n1 = n2).
-* [ #n1 ] * [1,3: #n2 ] /2 width=1 by or_introl/
-[2,3: @or_intror #H destruct ]
-elim (eq_nat_dec n1 n2) /4 width=1 by yinj_inj, or_intror, or_introl/
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground/ynat/ynat_succ.ma".
-
-(* NATURAL NUMBERS WITH INFINITY ********************************************)
-
-(* order relation *)
-inductive yle: relation ynat ≝
-| yle_inj: ∀m,n. m ≤ n → yle m n
-| yle_Y : ∀m. yle m (∞)
-.
-
-interpretation "ynat 'less or equal to'" 'leq x y = (yle x y).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact yle_inv_inj2_aux: ∀x,y. x ≤ y → ∀n. y = yinj n →
- ∃∃m. m ≤ n & x = yinj m.
-#x #y * -x -y
-[ #x #y #Hxy #n #Hy destruct /2 width=3 by ex2_intro/
-| #x #n #Hy destruct
-]
-qed-.
-
-lemma yle_inv_inj2: ∀x,n. x ≤ yinj n → ∃∃m. m ≤ n & x = yinj m.
-/2 width=3 by yle_inv_inj2_aux/ qed-.
-
-lemma yle_inv_inj: ∀m,n. yinj m ≤ yinj n → m ≤ n.
-#m #n #H elim (yle_inv_inj2 … H) -H
-#x #Hxn #H destruct //
-qed-.
-
-fact yle_inv_O2_aux: ∀m:ynat. ∀x:ynat. m ≤ x → x = 0 → m = 0.
-#m #x * -m -x
-[ #m #n #Hmn #H destruct /3 width=1 by le_n_O_to_eq, eq_f/
-| #m #H destruct
-]
-qed-.
-
-lemma yle_inv_O2: ∀m:ynat. m ≤ 0 → m = 0.
-/2 width =3 by yle_inv_O2_aux/ qed-.
-
-fact yle_inv_Y1_aux: ∀x,n. x ≤ n → x = ∞ → n = ∞.
-#x #n * -x -n //
-#x #n #_ #H destruct
-qed-.
-
-lemma yle_inv_Y1: ∀n. ∞ ≤ n → n = ∞.
-/2 width=3 by yle_inv_Y1_aux/ qed-.
-
-lemma yle_antisym: ∀y,x. x ≤ y → y ≤ x → x = y.
-#x #y #H elim H -x -y
-/4 width=1 by yle_inv_Y1, yle_inv_inj, le_to_le_to_eq, eq_f/
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma le_O1: ∀n:ynat. 0 ≤ n.
-* /2 width=1 by yle_inj/
-qed.
-
-lemma yle_refl: reflexive … yle.
-* /2 width=1 by le_n, yle_inj/
-qed.
-
-lemma yle_split: ∀x,y:ynat. x ≤ y ∨ y ≤ x.
-* /2 width=1 by or_intror/
-#x * /2 width=1 by or_introl/
-#y elim (le_or_ge x y) /3 width=1 by yle_inj, or_introl, or_intror/
-qed-.
-
-(* Inversion lemmas on successor ********************************************)
-
-fact yle_inv_succ1_aux: ∀x,y:ynat. x ≤ y → ∀m. x = ↑m → m ≤ ↓y ∧ ↑↓y = y.
-#x #y * -x -y
-[ #x #y #Hxy #m #H elim (ysucc_inv_inj_sn … H) -H
- #n #H1 #H2 destruct elim (le_inv_S1 … Hxy) -Hxy
- #m #Hnm #H destruct /3 width=1 by yle_inj, conj/
-| #x #y #H destruct /2 width=1 by yle_Y, conj/
-]
-qed-.
-
-lemma yle_inv_succ1: ∀m,y:ynat. ↑m ≤ y → m ≤ ↓y ∧ ↑↓y = y.
-/2 width=3 by yle_inv_succ1_aux/ qed-.
-
-lemma yle_inv_succ: ∀m,n. ↑m ≤ ↑n → m ≤ n.
-#m #n #H elim (yle_inv_succ1 … H) -H //
-qed-.
-
-lemma yle_inv_succ2: ∀x,y. x ≤ ↑y → ↓x ≤ y.
-#x #y #Hxy elim (ynat_cases x)
-[ #H destruct //
-| * #m #H destruct /2 width=1 by yle_inv_succ/
-]
-qed-.
-
-(* Properties on predecessor ************************************************)
-
-lemma yle_pred_sn: ∀m,n. m ≤ n → ↓m ≤ n.
-#m #n * -m -n /3 width=3 by transitive_le, yle_inj/
-qed.
-
-lemma yle_refl_pred_sn: ∀x. ↓x ≤ x.
-/2 width=1 by yle_refl, yle_pred_sn/ qed.
-
-lemma yle_pred: ∀m,n. m ≤ n → ↓m ≤ ↓n.
-#m #n * -m -n /3 width=1 by yle_inj, monotonic_pred/
-qed.
-
-(* Properties on successor **************************************************)
-
-lemma yle_succ: ∀m,n. m ≤ n → ↑m ≤ ↑n.
-#m #n * -m -n /3 width=1 by yle_inj, le_S_S/
-qed.
-
-lemma yle_succ_dx: ∀m,n. m ≤ n → m ≤ ↑n.
-#m #n * -m -n /3 width=1 by le_S, yle_inj/
-qed.
-
-lemma yle_refl_S_dx: ∀x. x ≤ ↑x.
-/2 width=1 by yle_succ_dx/ qed.
-
-lemma yle_refl_SP_dx: ∀x. x ≤ ↑↓x.
-* // * //
-qed.
-
-lemma yle_succ2: ∀x,y. ↓x ≤ y → x ≤ ↑y.
-#x #y #Hxy elim (ynat_cases x)
-[ #H destruct //
-| * #m #H destruct /2 width=1 by yle_succ/
-]
-qed-.
-
-(* Main properties **********************************************************)
-
-theorem yle_trans: Transitive … yle.
-#x #y * -x -y
-[ #x #y #Hxy * //
- #z #H lapply (yle_inv_inj … H) -H
- /3 width=3 by transitive_le, yle_inj/ (**) (* full auto too slow *)
-| #x #z #H lapply (yle_inv_Y1 … H) //
-]
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground/ynat/ynat_le.ma".
-
-(* NATURAL NUMBERS WITH INFINITY ********************************************)
-
-(* strict order relation *)
-inductive ylt: relation ynat ≝
-| ylt_inj: ∀m,n. m < n → ylt m n
-| ylt_Y : ∀m:nat. ylt m (∞)
-.
-
-interpretation "ynat 'less than'" 'lt x y = (ylt x y).
-
-(* Basic forward lemmas *****************************************************)
-
-lemma ylt_fwd_gen: ∀x,y. x < y → ∃m. x = yinj m.
-#x #y * -x -y /2 width=2 by ex_intro/
-qed-.
-
-lemma ylt_fwd_lt_O1: ∀x,y:ynat. x < y → 0 < y.
-#x #y #H elim H -x -y /3 width=2 by ylt_inj, ltn_to_ltO/
-qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact ylt_inv_inj2_aux: ∀x,y. x < y → ∀n. y = yinj n →
- ∃∃m. m < n & x = yinj m.
-#x #y * -x -y
-[ #x #y #Hxy #n #Hy elim (le_inv_S1 … Hxy) -Hxy
- #m #Hm #H destruct /3 width=3 by le_S_S, ex2_intro/
-| #x #n #Hy destruct
-]
-qed-.
-
-lemma ylt_inv_inj2: ∀x,n. x < yinj n →
- ∃∃m. m < n & x = yinj m.
-/2 width=3 by ylt_inv_inj2_aux/ qed-.
-
-lemma ylt_inv_inj: ∀m,n. yinj m < yinj n → m < n.
-#m #n #H elim (ylt_inv_inj2 … H) -H
-#x #Hx #H destruct //
-qed-.
-
-lemma ylt_inv_Y1: ∀n. ∞ < n → ⊥.
-#n #H elim (ylt_fwd_gen … H) -H
-#y #H destruct
-qed-.
-
-lemma ylt_inv_Y2: ∀x:ynat. x < ∞ → ∃n. x = yinj n.
-* /2 width=2 by ex_intro/
-#H elim (ylt_inv_Y1 … H)
-qed-.
-
-lemma ylt_inv_O1: ∀n:ynat. 0 < n → ↑↓n = n.
-* // #n #H lapply (ylt_inv_inj … H) -H normalize
-/3 width=1 by S_pred, eq_f/
-qed-.
-
-(* Inversion lemmas on successor ********************************************)
-
-fact ylt_inv_succ1_aux: ∀x,y:ynat. x < y → ∀m. x = ↑m → m < ↓y ∧ ↑↓y = y.
-#x #y * -x -y
-[ #x #y #Hxy #m #H elim (ysucc_inv_inj_sn … H) -H
- #n #H1 #H2 destruct elim (le_inv_S1 … Hxy) -Hxy
- #m #Hnm #H destruct /3 width=1 by ylt_inj, conj/
-| #x #y #H elim (ysucc_inv_inj_sn … H) -H
- #m #H #_ destruct /2 width=1 by ylt_Y, conj/
-]
-qed-.
-
-lemma ylt_inv_succ1: ∀m,y:ynat. ↑m < y → m < ↓y ∧ ↑↓y = y.
-/2 width=3 by ylt_inv_succ1_aux/ qed-.
-
-lemma ylt_inv_succ: ∀m,n. ↑m < ↑n → m < n.
-#m #n #H elim (ylt_inv_succ1 … H) -H //
-qed-.
-
-(* Forward lemmas on successor **********************************************)
-
-fact ylt_fwd_succ2_aux: ∀x,y. x < y → ∀n. y = ↑n → x ≤ n.
-#x #y * -x -y
-[ #x #y #Hxy #m #H elim (ysucc_inv_inj_sn … H) -H
- #n #H1 #H2 destruct /3 width=1 by yle_inj, le_S_S_to_le/
-| #x #n #H lapply (ysucc_inv_Y_sn … H) -H //
-]
-qed-.
-
-lemma ylt_fwd_succ2: ∀m,n. m < ↑n → m ≤ n.
-/2 width=3 by ylt_fwd_succ2_aux/ qed-.
-
-(* inversion and forward lemmas on order ************************************)
-
-lemma ylt_fwd_le_succ1: ∀m,n. m < n → ↑m ≤ n.
-#m #n * -m -n /2 width=1 by yle_inj/
-qed-.
-
-lemma ylt_fwd_le_pred2: ∀x,y:ynat. x < y → x ≤ ↓y.
-#x #y #H elim H -x -y /3 width=1 by yle_inj, monotonic_pred/
-qed-.
-
-lemma ylt_fwd_le: ∀m:ynat. ∀n:ynat. m < n → m ≤ n.
-#m #n * -m -n /3 width=1 by lt_to_le, yle_inj/
-qed-.
-
-lemma ylt_yle_false: ∀m:ynat. ∀n:ynat. m < n → n ≤ m → ⊥.
-#m #n * -m -n
-[ #m #n #Hmn #H lapply (yle_inv_inj … H) -H
- #H elim (lt_refl_false n) /2 width=3 by le_to_lt_to_lt/
-| #m #H lapply (yle_inv_Y1 … H) -H
- #H destruct
-]
-qed-.
-
-lemma ylt_inv_le: ∀x,y. x < y → x < ∞ ∧ ↑x ≤ y.
-#x #y #H elim H -x -y /3 width=1 by yle_inj, conj/
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma ylt_O1: ∀x:ynat. ↑↓x = x → 0 < x.
-* // * /2 width=1 by ylt_inj/ normalize
-#H destruct
-qed.
-
-lemma yle_inv_succ_sn_lt (x:ynat) (y:ynat):
- ↑x ≤ y → ∧∧ x ≤ ↓y & 0 < y.
-#x #y #H elim (yle_inv_succ1 … H) -H /3 width=2 by ylt_O1, conj/
-qed-.
-
-(* Properties on predecessor ************************************************)
-
-lemma ylt_pred: ∀m,n:ynat. m < n → 0 < m → ↓m < ↓n.
-#m #n * -m -n
-/4 width=1 by ylt_inv_inj, ylt_inj, monotonic_lt_pred/
-qed.
-
-(* Properties on successor **************************************************)
-
-lemma ylt_O_succ: ∀x:ynat. 0 < ↑x.
-* /2 width=1 by ylt_inj/
-qed.
-
-lemma ylt_succ: ∀m,n. m < n → ↑m < ↑n.
-#m #n #H elim H -m -n /3 width=1 by ylt_inj, le_S_S/
-qed.
-
-lemma ylt_succ_Y: ∀x. x < ∞ → ↑x < ∞.
-* /2 width=1 by/ qed.
-
-lemma yle_succ1_inj: ∀x. ∀y:ynat. ↑yinj x ≤ y → x < y.
-#x * /3 width=1 by yle_inv_inj, ylt_inj/
-qed.
-
-lemma ylt_succ2_refl: ∀x,y:ynat. x < y → x < ↑x.
-#x #y #H elim (ylt_fwd_gen … H) -y /2 width=1 by ylt_inj/
-qed.
-
-(* Properties on order ******************************************************)
-
-lemma yle_split_eq: ∀m,n:ynat. m ≤ n → m < n ∨ m = n.
-#m #n * -m -n
-[ #m #n #Hmn elim (le_to_or_lt_eq … Hmn) -Hmn
- /3 width=1 by or_introl, ylt_inj/
-| * /2 width=1 by or_introl, ylt_Y/
-]
-qed-.
-
-lemma ylt_split: ∀m,n:ynat. m < n ∨ n ≤ m.
-#m #n elim (yle_split m n) /2 width=1 by or_intror/
-#H elim (yle_split_eq … H) -H /2 width=1 by or_introl, or_intror/
-qed-.
-
-lemma ylt_split_eq: ∀m,n:ynat. ∨∨ m < n | n = m | n < m.
-#m #n elim (ylt_split m n) /2 width=1 by or3_intro0/
-#H elim (yle_split_eq … H) -H /2 width=1 by or3_intro1, or3_intro2/
-qed-.
-
-lemma ylt_yle_trans: ∀x:ynat. ∀y:ynat. ∀z:ynat. y ≤ z → x < y → x < z.
-#x #y #z * -y -z
-[ #y #z #Hyz #H elim (ylt_inv_inj2 … H) -H
- #m #Hm #H destruct /3 width=3 by ylt_inj, lt_to_le_to_lt/
-| #y * //
-]
-qed-.
-
-lemma yle_ylt_trans: ∀x:ynat. ∀y:ynat. ∀z:ynat. y < z → x ≤ y → x < z.
-#x #y #z * -y -z
-[ #y #z #Hyz #H elim (yle_inv_inj2 … H) -H
- #m #Hm #H destruct /3 width=3 by ylt_inj, le_to_lt_to_lt/
-| #y #H elim (yle_inv_inj2 … H) -H //
-]
-qed-.
-
-lemma le_ylt_trans (x) (y) (z): x ≤ y → yinj y < z → yinj x < z.
-/3 width=3 by yle_ylt_trans, yle_inj/
-qed-.
-
-lemma yle_inv_succ1_lt: ∀x,y:ynat. ↑x ≤ y → 0 < y ∧ x ≤ ↓y.
-#x #y #H elim (yle_inv_succ1 … H) -H /3 width=1 by ylt_O1, conj/
-qed-.
-
-lemma yle_lt: ∀x,y. x < ∞ → ↑x ≤ y → x < y.
-#x * // #y #H elim (ylt_inv_Y2 … H) -H #n #H destruct
-/3 width=1 by ylt_inj, yle_inv_inj/
-qed-.
-
-(* Main properties **********************************************************)
-
-theorem ylt_trans: Transitive … ylt.
-#x #y * -x -y
-[ #x #y #Hxy * //
- #z #H lapply (ylt_inv_inj … H) -H
- /3 width=3 by transitive_lt, ylt_inj/ (**) (* full auto too slow *)
-| #x #z #H elim (ylt_yle_false … H) //
-]
-qed-.
-
-lemma lt_ylt_trans (x) (y) (z): x < y → yinj y < z → yinj x < z.
-/3 width=3 by ylt_trans, ylt_inj/
-qed-.
-
-(* Elimination principles ***************************************************)
-
-fact ynat_ind_lt_le_aux: ∀R:predicate ynat.
- (∀y. (∀x. x < y → R x) → R y) →
- ∀y:nat. ∀x. x ≤ y → R x.
-#R #IH #y elim y -y
-[ #x #H >(yle_inv_O2 … H) -x
- @IH -IH #x #H elim (ylt_yle_false … H) -H //
-| /5 width=3 by ylt_yle_trans, ylt_fwd_succ2/
-]
-qed-.
-
-fact ynat_ind_lt_aux: ∀R:predicate ynat.
- (∀y. (∀x. x < y → R x) → R y) →
- ∀y:nat. R y.
-/4 width=2 by ynat_ind_lt_le_aux/ qed-.
-
-lemma ynat_ind_lt: ∀R:predicate ynat.
- (∀y. (∀x. x < y → R x) → R y) →
- ∀y. R y.
-#R #IH * /4 width=1 by ynat_ind_lt_aux/
-@IH #x #H elim (ylt_inv_Y2 … H) -H
-#n #H destruct /4 width=1 by ynat_ind_lt_aux/
-qed-.
-
-fact ynat_f_ind_aux: ∀A. ∀f:A→ynat. ∀R:predicate A.
- (∀x. (∀a. f a < x → R a) → ∀a. f a = x → R a) →
- ∀x,a. f a = x → R a.
-#A #f #R #IH #x @(ynat_ind_lt … x) -x
-/3 width=3 by/
-qed-.
-
-lemma ynat_f_ind: ∀A. ∀f:A→ynat. ∀R:predicate A.
- (∀x. (∀a. f a < x → R a) → ∀a. f a = x → R a) → ∀a. R a.
-#A #f #R #IH #a
-@(ynat_f_ind_aux … IH) -IH [2: // | skip ]
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground/ynat/ynat_plus.ma".
-
-(* NATURAL NUMBERS WITH INFINITY ********************************************)
-
-(* left subtraction *)
-definition yminus_sn (x) (y): ynat ≝ ypred^y x.
-
-interpretation "ynat left minus" 'minus x y = (yminus_sn x y).
-
-lemma yminus_O2: ∀m:ynat. m - 0 = m.
-// qed.
-
-lemma yminus_S2: ∀m:ynat. ∀n:nat. m - S n = ↓(m - n).
-// qed.
-
-(* Basic properties *********************************************************)
-
-lemma yminus_inj: ∀m,n. yinj m - n = yinj (m - n).
-#m #n elim n -n //
-#n #IH >yminus_S2 >IH -IH >eq_minus_S_pred //
-qed.
-
-lemma yminus_Y_inj: ∀n. ∞ - n = ∞.
-#n elim n -n //
-qed.
-
-lemma yminus_O1: ∀x:nat. yinj 0 - x = 0.
-// qed.
-
-lemma yminus_refl: ∀x:nat. yinj x - x = 0.
-// qed.
-
-lemma yminus_minus_comm: ∀x:ynat. ∀y,z. x - y - z = x - z - y.
-* // qed.
-
-(* Properties on predecessor ************************************************)
-
-lemma yminus_SO2: ∀m:ynat. m - 1 = ↓m.
-// qed.
-
-lemma yminus_pred1: ∀x,y. ↓x - y = ↓(x-y).
-#x * // #y elim y -y //
-qed.
-
-lemma yminus_pred: ∀m:ynat. ∀n. 0 < m → 0 < n → ↓m - ↓n = m - n.
-* // #m #n >yminus_inj >yminus_inj
-/4 width=1 by ylt_inv_inj, minus_pred_pred, eq_f/
-qed-.
-
-(* Properties on successor **************************************************)
-
-lemma yminus_succ: ∀m:ynat. ∀n. ↑m - ↑n = m - n.
-* // qed.
-
-lemma yminus_succ1_inj: ∀n:nat. ∀m:ynat. n ≤ m → ↑m - n = ↑(m - n).
-#n *
-[ #m #Hmn >yminus_inj >yminus_inj
- /4 width=1 by yle_inv_inj, plus_minus, eq_f/
-| >yminus_Y_inj //
-]
-qed-.
-
-lemma yminus_succ2: ∀x:ynat. ∀y. x - ↑y = ↓(x-y).
-* //
-qed.
-
-(* Properties on order ******************************************************)
-
-lemma yle_minus_sn: ∀m:ynat. ∀n. m - n ≤ m.
-* // #n /2 width=1 by yle_inj/
-qed.
-
-lemma yle_to_minus: ∀m:ynat. ∀n:nat. m ≤ n → m - n = 0.
-*
-[ #m #n #H >yminus_inj /4 width=1 by yle_inv_inj, eq_minus_O, eq_f/
-| #n #H lapply (yle_inv_Y1 … H) -H #H destruct
-]
-qed-.
-
-lemma yminus_to_le: ∀m:ynat. ∀n. m - n = 0 → m ≤ n.
-* [2: #n >yminus_Y_inj #H destruct ]
-#m #n >yminus_inj #H
-lapply (yinj_inj … H) -H (**) (* destruct lemma needed *)
-/2 width=1 by yle_inj/
-qed.
-
-lemma monotonic_yle_minus_dx: ∀x,y. x ≤ y → ∀z. x - z ≤ y - z.
-#x #y * /3 width=1 by yle_inj, monotonic_le_minus_l2/
-qed.
-
-(* Properties on strict order ***********************************************)
-
-lemma ylt_to_minus: ∀y:ynat. ∀x. yinj x < y → 0 < y - x.
-* // #y #x #H >yminus_inj
-/4 width=1 by ylt_inj, ylt_inv_inj, lt_plus_to_minus_r/
-qed.
-
-lemma yminus_to_lt: ∀y:ynat. ∀x. 0 < y - x → x < y.
-* // #y #x >yminus_inj #H
-/4 width=1 by ylt_inv_inj, ylt_inj, lt_minus_to_plus_r/
-qed-.
-
-lemma monotonic_ylt_minus_dx: ∀x,y:ynat. x < y → ∀z:nat. z ≤ x → x - z < y - z.
-#x #y * -x -y
-/4 width=1 by ylt_inj, yle_inv_inj, monotonic_lt_minus_l/
-qed.
-
-(* Properties on minus ******************************************************)
-
-lemma yplus_minus: ∀m:ynat. ∀n:nat. m + n - n = m.
-#m #n elim n -n //
-#n #IHn >(yplus_succ2 m n) >(yminus_succ … n) //
-qed.
-
-lemma yminus_plus2: ∀x:ynat. ∀y,z. x - (y + z) = x - y - z.
-* // qed.
-
-(* Forward lemmas on minus **************************************************)
-
-lemma yle_plus1_to_minus_inj2: ∀x,z:ynat. ∀y:nat. x + y ≤ z → x ≤ z - y.
-#x #z #y #H lapply (monotonic_yle_minus_dx … H y) -H //
-qed-.
-
-lemma yle_plus1_to_minus_inj1: ∀x,z:ynat. ∀y:nat. y + x ≤ z → x ≤ z - y.
-/2 width=1 by yle_plus1_to_minus_inj2/ qed-.
-
-lemma yle_plus2_to_minus_inj2: ∀x,y:ynat. ∀z:nat. x ≤ y + z → x - z ≤ y.
-/2 width=1 by monotonic_yle_minus_dx/ qed-.
-
-lemma yle_plus2_to_minus_inj1: ∀x,y:ynat. ∀z:nat. x ≤ z + y → x - z ≤ y.
-/2 width=1 by yle_plus2_to_minus_inj2/ qed-.
-
-lemma yminus_plus (x:ynat) (y:nat): y ≤ x → x = (x-y)+y.
-* // #x #y #H >yminus_inj >yplus_inj
-/4 width=1 by yle_inv_inj, plus_minus, eq_f/
-qed-.
-
-lemma yplus_minus_assoc_inj: ∀x:nat. ∀y,z:ynat. x ≤ y → z + (y - x) = z + y - x.
-#x *
-[ #y * // #z >yminus_inj >yplus_inj >yplus_inj
- /4 width=1 by yle_inv_inj, plus_minus, eq_f/
-| >yminus_Y_inj //
-]
-qed-.
-
-alias symbol "plus" (instance 5) = "ynat plus".
-alias symbol "minus" (instance 4) = "ynat left minus".
-alias symbol "minus" (instance 3) = "natural minus".
-alias symbol "minus" (instance 2) = "ynat left minus".
-alias symbol "leq" (instance 6) = "natural 'less or equal to'".
-lemma yplus_minus_assoc_comm_inj: ∀z:ynat. ∀x,y:nat. x ≤ y → z - (y - x) = z + x - y.
-* // #z #x #y >yminus_inj >yplus_inj >yminus_inj
-/4 width=1 by yle_inv_inj, minus_le_minus_minus_comm, eq_f/
-qed-.
-
-lemma yplus_minus_comm_inj: ∀y:nat. ∀x,z:ynat. y ≤ x → x + z - y = x - y + z.
-#y * // #x * //
-#z #Hxy >yplus_inj >yminus_inj <plus_minus
-/2 width=1 by yle_inv_inj/
-qed-.
-
-lemma ylt_plus1_to_minus_inj2: ∀x,z:ynat. ∀y:nat. x + y < z → x < z - y.
-#x #z #y #H lapply (monotonic_ylt_minus_dx … H y ?) -H //
-qed-.
-
-lemma ylt_plus1_to_minus_inj1: ∀x,z:ynat. ∀y:nat. y + x < z → x < z - y.
-/2 width=1 by ylt_plus1_to_minus_inj2/ qed-.
-
-lemma ylt_plus2_to_minus_inj2: ∀x,y:ynat. ∀z:nat. z ≤ x → x < y + z → x - z < y.
-/2 width=1 by monotonic_ylt_minus_dx/ qed-.
-
-lemma ylt_plus2_to_minus_inj1: ∀x,y:ynat. ∀z:nat. z ≤ x → x < z + y → x - z < y.
-/2 width=1 by ylt_plus2_to_minus_inj2/ qed-.
-
-lemma yplus_inv_Y1: ∀x,y. ∞ = x + y → ∨∨ ∞ = x | ∞ = y.
-* /2 width=1 by or_introl/ #x * // #y >yplus_inj #H destruct
-qed-.
-
-lemma yplus_inv_minus:
- ∀x1,y2:ynat.∀y1,x2:nat.
- y1 ≤ x1 → x1 + x2 = y2 + y1 → ∧∧ x1 - y1 = y2 - x2 & x2 ≤ y2.
-*
-[ #x1 * [| #y1 #x2 #_ >yplus_inj >yplus_Y1 #H destruct ]
- #y2 #y1 #x2 #H1 >yplus_inj >yplus_inj #H2 >yminus_inj >yminus_inj
- lapply (yle_inv_inj … H1) -H1 #Hyx1
- lapply (yinj_inj … H2) -H2 #Hxy (**) (* destruct lemma needed *)
- /5 width=4 by yle_inj, plus2_le_sn_sn, plus_to_minus_2, conj, eq_f2/
-| #y2 #y1 #x2 #_ >yplus_Y1 #H
- elim (yplus_inv_Y1 … H) -H #H destruct /2 width=1 by conj/
-]
-qed-.
-
-(* Inversion lemmas on minus ************************************************)
-
-lemma yle_inv_plus_inj2: ∀x,z:ynat. ∀y:nat. x + y ≤ z → x ≤ z - y ∧ y ≤ z.
-/3 width=3 by yle_plus1_to_minus_inj2, yle_trans, conj/ qed-.
-
-lemma yle_inv_plus_inj1: ∀x,z:ynat. ∀y:nat. y + x ≤ z → x ≤ z - y ∧ y ≤ z.
-/2 width=1 by yle_inv_plus_inj2/ qed-.
-
-lemma yle_inv_plus_inj_dx: ∀z,x:ynat. ∀y:nat. x + y ≤ z →
- ∧∧ x ≤ z - y & y ≤ z.
-* [| /2 width=1 by conj/ ]
-#z * [| #y >yplus_Y1 #H >(yle_inv_Y1 … H) -z /2 width=1 by conj/ ]
-#x #y >yplus_inj #H >yminus_inj
-/5 width=2 by yle_inv_inj, yle_inj, le_plus_to_minus_r, le_plus_b, conj/
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground/xoa/ex_3_2.ma".
-include "ground/ynat/ynat_lt.ma".
-
-(* NATURAL NUMBERS WITH INFINITY ********************************************)
-
-(* addition *)
-definition yplus: ynat → ynat → ynat ≝ λx,y. match y with
-[ yinj n ⇒ ysucc^n x
-| Y ⇒ Y
-].
-
-interpretation "ynat plus" 'plus x y = (yplus x y).
-
-lemma yplus_O2: ∀m:ynat. m + 0 = m.
-// qed.
-
-lemma yplus_S2: ∀m:ynat. ∀n. m + S n = ↑(m + n).
-// qed.
-
-lemma yplus_Y2: ∀m:ynat. m + (∞) = ∞.
-// qed.
-
-(* Properties on successor **************************************************)
-
-lemma yplus_succ2: ∀m,n. m + ↑n = ↑(m + n).
-#m * //
-qed.
-
-lemma yplus_succ1: ∀m,n. ↑m + n = ↑(m + n).
-#m * // #n elim n -n //
-qed.
-
-lemma yplus_succ_swap: ∀m,n. m + ↑n = ↑m + n.
-// qed.
-
-lemma yplus_SO2: ∀m:ynat. m + 1 = ↑m.
-* //
-qed.
-
-(* Basic properties *********************************************************)
-
-lemma yplus_inj: ∀n,m. yinj m + yinj n = yinj (m + n).
-#n elim n -n //
-#n #IHn #m >(yplus_succ2 ? n) >IHn -IHn
-<plus_n_Sm //
-qed.
-
-lemma yplus_Y1: ∀m. ∞ + m = ∞.
-* // #m elim m -m //
-qed.
-
-lemma yplus_comm: commutative … yplus.
-* [ #m ] * [1,3: #n ] //
-qed.
-
-lemma yplus_assoc: associative … yplus.
-#x #y * // #z cases y -y
-[ #y >yplus_inj whd in ⊢ (??%%); <iter_plus //
-| >yplus_Y1 //
-]
-qed.
-
-lemma yplus_O1: ∀n:ynat. 0 + n = n.
-#n >yplus_comm // qed.
-
-lemma yplus_comm_23: ∀x,y,z. x + z + y = x + y + z.
-#x #y #z >yplus_assoc //
-qed.
-
-lemma yplus_comm_24: ∀x1,x2,x3,x4. x1 + x4 + x3 + x2 = x1 + x2 + x3 + x4.
-#x1 #x2 #x3 #x4
->yplus_assoc >yplus_assoc >yplus_assoc >yplus_assoc
-/2 width=1 by eq_f2/
-qed.
-
-lemma yplus_assoc_23: ∀x1,x2,x3,x4. x1 + x2 + (x3 + x4) = x1 + (x2 + x3) + x4.
-#x1 #x2 #x3 #x4 >yplus_assoc >yplus_assoc
-/2 width=1 by eq_f2/
-qed.
-
-(* Inversion lemmas on successor *********************************************)
-
-lemma yplus_inv_succ_lt_dx: ∀x,y,z:ynat. 0 < y → x + y = ↑z → x + ↓y = z.
-#x #y #z #H <(ylt_inv_O1 y) // >yplus_succ2
-/2 width=1 by ysucc_inv_inj/
-qed-.
-
-lemma yplus_inv_succ_lt_sn: ∀x,y,z:ynat. 0 < x → x + y = ↑z → ↓x + y = z.
-#x #y #z #H <(ylt_inv_O1 x) // >yplus_succ1
-/2 width=1 by ysucc_inv_inj/
-
-qed-.
-
-(* Inversion lemmas on order ************************************************)
-
-lemma yle_inv_plus_dx: ∀x,y. x ≤ y → ∃z. x + z = y.
-#x #y #H elim H -x -y /2 width=2 by ex_intro/
-#m #n #H @(ex_intro … (yinj (n-m))) (**) (* explicit constructor *)
-/3 width=1 by plus_minus, eq_f/
-qed-.
-
-lemma yle_inv_plus_sn: ∀x,y. x ≤ y → ∃z. z + x = y.
-#x #y #H elim (yle_inv_plus_dx … H) -H
-/2 width=2 by ex_intro/
-qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma yplus_inv_inj: ∀z,y,x. x + y = yinj z →
- ∃∃m,n. m + n = z & x = yinj m & y = yinj n.
-#z * [2: normalize #x #H destruct ]
-#y * [2: >yplus_Y1 #H destruct ]
-/3 width=5 by yinj_inj, ex3_2_intro/
-qed-.
-
-lemma yplus_inv_O: ∀x,y:ynat. x + y = 0 → x = 0 ∧ y = 0.
-#x #y #H elim (yplus_inv_inj … H) -H
-#m * /2 width=1 by conj/ #n <plus_n_Sm #H destruct
-qed-.
-
-lemma discr_yplus_xy_x: ∀x,y. x + y = x → x = ∞ ∨ y = 0.
-* /2 width=1 by or_introl/
-#x elim x -x /2 width=1 by or_intror/
-#x #IHx * [2: >yplus_Y2 #H destruct ]
-#y <ysucc_inj >yplus_succ1 #H
-lapply (ysucc_inv_inj … H) -H #H
-elim (IHx … H) -IHx -H /2 width=1 by or_introl, or_intror/
-qed-.
-
-lemma discr_yplus_x_xy: ∀x,y. x = x + y → x = ∞ ∨ y = 0.
-/2 width=1 by discr_yplus_xy_x/ qed-.
-
-lemma yplus_inv_monotonic_dx_inj: ∀z,x,y. x + yinj z = y + yinj z → x = y.
-#z @(nat_ind_plus … z) -z /3 width=2 by ysucc_inv_inj/
-qed-.
-
-lemma yplus_inv_monotonic_dx: ∀z,x,y. z < ∞ → x + z = y + z → x = y.
-#z #x #y #H elim (ylt_inv_Y2 … H) -H /2 width=2 by yplus_inv_monotonic_dx_inj/
-qed-.
-
-lemma yplus_inv_Y2: ∀x,y. x + y = ∞ → x = ∞ ∨ y = ∞.
-* /2 width=1 by or_introl/ #x * // #y >yplus_inj #H destruct
-qed-.
-
-lemma yplus_inv_monotonic_23: ∀z,x1,x2,y1,y2. z < ∞ →
- x1 + z + y1 = x2 + z + y2 → x1 + y1 = x2 + y2.
-#z #x1 #x2 #y1 #y2 #Hz #H @(yplus_inv_monotonic_dx z) //
->yplus_comm_23 >H -H //
-qed-.
-
-(* Inversion lemmas on strict_order *****************************************)
-
-lemma ylt_inv_plus_Y: ∀x,y. x + y < ∞ → x < ∞ ∧ y < ∞.
-#x #y #H elim (ylt_inv_Y2 … H) -H
-#z #H elim (yplus_inv_inj … H) -H /2 width=1 by conj/
-qed-.
-
-lemma ylt_inv_plus_sn: ∀x,y. x < y → ∃∃z. ↑z + x = y & x < ∞.
-#x #y #H elim (ylt_inv_le … H) -H
-#Hx #H elim (yle_inv_plus_sn … H) -H
-/2 width=2 by ex2_intro/
-qed-.
-
-lemma ylt_inv_plus_dx: ∀x,y. x < y → ∃∃z. x + ↑z = y & x < ∞.
-#x #y #H elim (ylt_inv_plus_sn … H) -H
-#z >yplus_comm /2 width=2 by ex2_intro/
-qed-.
-
-(* Properties on order ******************************************************)
-
-lemma yle_plus_dx2: ∀n,m. n ≤ m + n.
-* //
-#n elim n -n //
-#n #IHn #m >(yplus_succ2 ? n) @(yle_succ n) // (**) (* full auto fails *)
-qed.
-
-lemma yle_plus_dx1: ∀n,m. m ≤ m + n.
-// qed.
-
-lemma yle_plus_dx1_trans: ∀x,z. z ≤ x → ∀y. z ≤ x + y.
-/2 width=3 by yle_trans/ qed.
-
-lemma yle_plus_dx2_trans: ∀y,z. z ≤ y → ∀x. z ≤ x + y.
-/2 width=3 by yle_trans/ qed.
-
-lemma monotonic_yle_plus_dx: ∀x,y. x ≤ y → ∀z. x + z ≤ y + z.
-#x #y #Hxy * //
-#z elim z -z /3 width=1 by yle_succ/
-qed.
-
-lemma monotonic_yle_plus_sn: ∀x,y. x ≤ y → ∀z. z + x ≤ z + y.
-/2 width=1 by monotonic_yle_plus_dx/ qed.
-
-lemma monotonic_yle_plus: ∀x1,y1. x1 ≤ y1 → ∀x2,y2. x2 ≤ y2 →
- x1 + x2 ≤ y1 + y2.
-/3 width=3 by monotonic_yle_plus_dx, monotonic_yle_plus_sn, yle_trans/ qed.
-
-lemma ylt_plus_Y: ∀x,y. x < ∞ → y < ∞ → x + y < ∞.
-#x #y #Hx elim (ylt_inv_Y2 … Hx) -Hx
-#m #Hm #Hy elim (ylt_inv_Y2 … Hy) -Hy //
-qed.
-
-(* Forward lemmas on order **************************************************)
-
-lemma yle_fwd_plus_sn2: ∀x,y,z. x + y ≤ z → y ≤ z.
-/2 width=3 by yle_trans/ qed-.
-
-lemma yle_fwd_plus_sn1: ∀x,y,z. x + y ≤ z → x ≤ z.
-/2 width=3 by yle_trans/ qed-.
-
-lemma yle_inv_monotonic_plus_dx_inj: ∀x,y:ynat.∀z:nat. x + z ≤ y + z → x ≤ y.
-#x #y #z elim z -z /3 width=1 by yle_inv_succ/
-qed-.
-
-lemma yle_inv_monotonic_plus_sn_inj: ∀x,y:ynat.∀z:nat. z + x ≤ z + y → x ≤ y.
-/2 width=2 by yle_inv_monotonic_plus_dx_inj/ qed-.
-
-lemma yle_inv_monotonic_plus_dx: ∀x,y,z. z < ∞ → x + z ≤ y + z → x ≤ y.
-#x #y #z #Hz elim (ylt_inv_Y2 … Hz) -Hz #m #H destruct
-/2 width=2 by yle_inv_monotonic_plus_sn_inj/
-qed-.
-
-lemma yle_inv_monotonic_plus_sn: ∀x,y,z. z < ∞ → z + x ≤ z + y → x ≤ y.
-/2 width=3 by yle_inv_monotonic_plus_dx/ qed-.
-
-lemma yle_fwd_plus_ge: ∀m1,m2:nat. m2 ≤ m1 → ∀n1,n2:ynat. m1 + n1 ≤ m2 + n2 → n1 ≤ n2.
-#m1 #m2 #Hm12 #n1 #n2 #H
-lapply (monotonic_yle_plus … Hm12 … H) -Hm12 -H
-/2 width=2 by yle_inv_monotonic_plus_sn_inj/
-qed-.
-
-lemma yle_fwd_plus_ge_inj: ∀m1:nat. ∀m2,n1,n2:ynat. m2 ≤ m1 → m1 + n1 ≤ m2 + n2 → n1 ≤ n2.
-#m2 #m1 #n1 #n2 #H elim (yle_inv_inj2 … H) -H
-#x #H0 #H destruct /3 width=4 by yle_fwd_plus_ge, yle_inj/
-qed-.
-
-lemma yle_fwd_plus_yge: ∀n2,m1:ynat. ∀n1,m2:nat. m2 ≤ m1 → m1 + n1 ≤ m2 + n2 → n1 ≤ n2.
-* // #n2 * /2 width=4 by yle_fwd_plus_ge_inj/
-qed-.
-
-(* Properties on strict order ***********************************************)
-
-lemma ylt_plus_dx1_trans: ∀x,z. z < x → ∀y. z < x + y.
-/2 width=3 by ylt_yle_trans/ qed.
-
-lemma ylt_plus_dx2_trans: ∀y,z. z < y → ∀x. z < x + y.
-/2 width=3 by ylt_yle_trans/ qed.
-
-lemma monotonic_ylt_plus_dx_inj: ∀x,y. x < y → ∀z:nat. x + yinj z < y + yinj z.
-#x #y #Hxy #z elim z -z /3 width=1 by ylt_succ/
-qed.
-
-lemma monotonic_ylt_plus_sn_inj: ∀x,y. x < y → ∀z:nat. yinj z + x < yinj z + y.
-/2 width=1 by monotonic_ylt_plus_dx_inj/ qed.
-
-lemma monotonic_ylt_plus_dx: ∀x,y. x < y → ∀z. z < ∞ → x + z < y + z.
-#x #y #Hxy #z #Hz elim (ylt_inv_Y2 … Hz) -Hz
-#m #H destruct /2 width=1 by monotonic_ylt_plus_dx_inj/
-qed.
-
-lemma monotonic_ylt_plus_sn: ∀x,y. x < y → ∀z. z < ∞ → z + x < z + y.
-/2 width=1 by monotonic_ylt_plus_dx/ qed.
-
-lemma monotonic_ylt_plus_inj: ∀m1,m2. m1 < m2 → ∀n1,n2. yinj n1 ≤ n2 → m1 + n1 < m2 + n2.
-/3 width=3 by monotonic_ylt_plus_sn_inj, monotonic_yle_plus_sn, ylt_yle_trans/
-qed.
-
-lemma monotonic_ylt_plus: ∀m1,m2. m1 < m2 → ∀n1. n1 < ∞ → ∀n2. n1 ≤ n2 → m1 + n1 < m2 + n2.
-#m1 #m2 #Hm12 #n1 #H elim (ylt_inv_Y2 … H) -H #m #H destruct /2 width=1 by monotonic_ylt_plus_inj/
-qed.
-
-(* Forward lemmas on strict order *******************************************)
-
-lemma ylt_inv_monotonic_plus_dx: ∀x,y,z. x + z < y + z → x < y.
-* [2: #y #z >yplus_comm #H elim (ylt_inv_Y1 … H) ]
-#x * // #y * [2: #H elim (ylt_inv_Y1 … H) ]
-/4 width=3 by ylt_inv_inj, ylt_inj, lt_plus_to_lt_l/
-qed-.
-
-lemma ylt_fwd_plus_ge: ∀m1,m2. m2 ≤ m1 → ∀n1,n2. m1 + n1 < m2 + n2 → n1 < n2.
-#m1 #m2 #Hm12 #n1 #n2 #H elim (ylt_fwd_gen … H)
-#x #H0 elim (yplus_inv_inj … H0) -H0
-#y #z #_ #H2 #H3 destruct -x
-elim (yle_inv_inj2 … Hm12)
-#x #_ #H0 destruct
-lapply (monotonic_ylt_plus … H … Hm12) -H -Hm12
-/2 width=2 by ylt_inv_monotonic_plus_dx/
-qed-.
-
-(* Properties on predeccessor ***********************************************)
-
-lemma yplus_pred1: ∀x,y:ynat. 0 < x → ↓x + y = ↓(x+y).
-#x * // #y elim y -y // #y #IH #Hx
->yplus_S2 >yplus_S2 >IH -IH // >ylt_inv_O1
-/2 width=1 by ylt_plus_dx1_trans/
-qed-.
-
-lemma yplus_pred2: ∀x,y:ynat. 0 < y → x + ↓y = ↓(x+y).
-/2 width=1 by yplus_pred1/ qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground/ynat/ynat.ma".
-
-(* NATURAL NUMBERS WITH INFINITY ********************************************)
-
-(* the predecessor function *)
-definition ypred: ynat → ynat ≝ λm. match m with
-[ yinj m ⇒ ↓m
-| Y ⇒ Y
-].
-
-interpretation "ynat predecessor" 'DownArrow m = (ypred m).
-
-lemma ypred_O: ↓(yinj 0) = yinj 0.
-// qed.
-
-lemma ypred_S: ∀m:nat. ↓(↑m) = yinj m.
-// qed.
-
-lemma ypred_Y: (↓∞) = ∞.
-// qed.
-
-(* Inversion lemmas *********************************************************)
-
-lemma ypred_inv_refl: ∀m:ynat. ↓m = m → m = 0 ∨ m = ∞.
-* // #m #H lapply (yinj_inj … H) -H (**) (* destruct lemma needed *)
-/4 width=1 by pred_inv_fix_sn, or_introl, eq_f/
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground/ynat/ynat_pred.ma".
-
-(* NATURAL NUMBERS WITH INFINITY ********************************************)
-
-(* the successor function *)
-definition ysucc: ynat → ynat ≝ λm. match m with
-[ yinj m ⇒ ↑m
-| Y ⇒ Y
-].
-
-interpretation "ynat successor" 'UpArrow m = (ysucc m).
-
-lemma ysucc_inj: ∀m:nat. ↑(yinj m) = yinj (↑m).
-// qed.
-
-lemma ysucc_Y: ↑(∞) = ∞.
-// qed.
-
-(* Properties ***************************************************************)
-
-lemma ypred_succ: ∀m. ↓↑m = m.
-* // qed.
-
-lemma ynat_cases: ∀n:ynat. n = 0 ∨ ∃m:ynat. n = ↑m.
-*
-[ * /2 width=1 by or_introl/
- #n @or_intror @(ex_intro … n) // (**) (* explicit constructor *)
-| @or_intror @(ex_intro … (∞)) // (**) (* explicit constructor *)
-]
-qed-.
-
-lemma ysucc_iter_Y: ∀m. ysucc^m (∞) = ∞.
-#m elim m -m //
-#m #IHm whd in ⊢ (??%?); >IHm //
-qed.
-
-(* Inversion lemmas *********************************************************)
-
-lemma ysucc_inv_inj: ∀m,n. ↑m = ↑n → m = n.
-#m #n #H <(ypred_succ m) <(ypred_succ n) //
-qed-.
-
-lemma ysucc_inv_refl: ∀m. ↑m = m → m = ∞.
-* //
-#m #H lapply (yinj_inj … H) -H (**) (* destruct lemma needed *)
-#H elim (lt_refl_false m) //
-qed-.
-
-lemma ysucc_inv_inj_sn: ∀m2,n1. yinj m2 = ↑n1 →
- ∃∃m1. n1 = yinj m1 & m2 = S m1.
-#m2 * normalize
-[ #n1 #H destruct /2 width=3 by ex2_intro/
-| #H destruct
-]
-qed-.
-
-lemma ysucc_inv_inj_dx: ∀m2,n1. ↑n1 = yinj m2 →
- ∃∃m1. n1 = yinj m1 & m2 = S m1.
-/2 width=1 by ysucc_inv_inj_sn/ qed-.
-
-lemma ysucc_inv_Y_sn: ∀m. ∞ = ↑m → m = ∞.
-* // normalize
-#m #H destruct
-qed-.
-
-lemma ysucc_inv_Y_dx: ∀m. ↑m = ∞ → m = ∞.
-/2 width=1 by ysucc_inv_Y_sn/ qed-.
-
-lemma ysucc_inv_O_sn: ∀m. yinj 0 = ↑m → ⊥. (**) (* explicit coercion *)
-#m #H elim (ysucc_inv_inj_sn … H) -H
-#n #_ #H destruct
-qed-.
-
-lemma ysucc_inv_O_dx: ∀m:ynat. ↑m = 0 → ⊥.
-/2 width=2 by ysucc_inv_O_sn/ qed-.
-
-(* Eliminators **************************************************************)
-
-lemma ynat_ind: ∀R:predicate ynat.
- R 0 → (∀n:nat. R n → R (↑n)) → R (∞) →
- ∀x. R x.
-#R #H1 #H2 #H3 * // #n elim n -n /2 width=1 by/
-qed-.
projects / helm.git / commitdiff