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 ?) //
+ <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
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/
+[ #m #n #Hmn #Hnm
+ <(nle_antisym … Hmn) -Hmn /2 width=1 by yle_inv_inj_bi/
| /2 width=1 by yle_inv_inf_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_minus.ma".
+include "ground/arith/ynat_lminus.ma".
+include "ground/arith/ynat_le.ma".
+
+(* ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY ****************************)
+
+(* Constructions with ylminus ***********************************************)
+
+(*** yle_minus_sn *)
+lemma yle_lminus_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_lminus_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_lminus (x) (n): 𝟎 = x - n → x ≤ yinj_nat n.
+#x @(ynat_split_nat_inf … x) -x
+[ #m #n <ylminus_inj_sn >yinj_nat_zero #H
+ /4 width=1 by nle_eq_zero_minus, yle_inj, eq_inv_yinj_nat_bi/
+| #n <ylminus_inf_sn #H destruct
+]
+qed.
+
+(* Inversions with ylminus **************************************************)
+
+(*** yle_to_minus *)
+lemma yle_inv_eq_zero_lminus (x) (n):
+ x ≤ yinj_nat n → 𝟎 = x - n.
+#x @(ynat_split_nat_inf … x) -x
+[ #m #n #H <ylminus_inj_sn
+ <nle_inv_eq_zero_minus /2 width=1 by yle_inv_inj_bi/
+| #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_lminus_plus.ma".
+include "ground/arith/ynat_le_plus.ma".
+include "ground/arith/ynat_le_lminus.ma".
+
+(* ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY ****************************)
+
+(* Constructions with yminus and yplus **************************************)
+
+(*** yle_plus1_to_minus_inj2 *)
+lemma yle_plus_sn_dx_lminus_dx (n) (x) (z):
+ x + yinj_nat n ≤ z → x ≤ z - n.
+#n #x #z #H
+lapply (yle_lminus_bi_dx n … H) -H //
+qed.
+
+(*** yle_plus1_to_minus_inj1 *)
+lemma yle_plus_sn_sn_lminus_dx (n) (x) (z):
+ yinj_nat n + x ≤ z → x ≤ z - n.
+/2 width=1 by yle_plus_sn_dx_lminus_dx/ qed.
+
+(*** yle_plus2_to_minus_inj2 *)
+lemma yle_plus_dx_dx_lminus_sn (o) (x) (y):
+ x ≤ y + yinj_nat o → x - o ≤ y.
+/2 width=1 by yle_lminus_bi_dx/ qed.
+
+(*** yle_plus2_to_minus_inj1 *)
+lemma yle_plus_dx_sn_lminus_sn (o) (x) (y):
+ x ≤ yinj_nat o + y → x - o ≤ y.
+/2 width=1 by yle_plus_dx_dx_lminus_sn/ qed.
+
+(* Destructions with yminus and yplus ***************************************)
+
+(*** yplus_minus_comm_inj *)
+lemma ylminus_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 <ylminus_inj_sn <yplus_inj_bi <yplus_inj_bi <ylminus_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_lminus_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 <ylminus_inj_sn <yplus_inj_bi <yplus_inj_bi
+ <nplus_minus_assoc /2 width=1 by yle_inv_inj_bi/
+| #_ <ylminus_inf_sn //
+]
+qed-.
+
+(*** yplus_minus_assoc_comm_inj *)
+lemma ylminus_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 <ylminus_inj_sn <yplus_inj_bi <ylminus_inj_sn
+ <nminus_assoc_comm_23 //
+| #_ <ylminus_inf_sn <yplus_inf_sn //
+]
+qed-.
+
+(* Inversions with yminus and yplus *****************************************)
+
+(*** yminus_plus *)
+lemma yplus_lminus_sn_refl_sn (n) (x):
+ yinj_nat n ≤ x → x = x - n + yinj_nat n.
+/2 width=1 by ylminus_plus_comm_23/ qed-.
+
+lemma yplus_lminus_dx_refl_sn (n) (x):
+ yinj_nat n ≤ x → x = yinj_nat n + (x - n).
+/2 width=1 by yplus_lminus_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_lminus_sn_refl_sn … Hmy2) in ⊢ (%→?); <yplus_assoc #H
+lapply (eq_inv_yplus_bi_dx_inj … H) -H
+>(yplus_lminus_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_lminus_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_lminus.ma".
+
+(* ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY ****************************)
+
+(* Constructions with ylminus and ysucc *************************************)
+
+(*** yminus_succ1_inj *)
+lemma ylminus_succ_sn (x) (n):
+ yinj_nat n ≤ x → ↑(x - n) = ↑x - n.
+#x @(ynat_split_nat_inf … x) -x //
+#m #n #Hnm
+<ylminus_inj_sn <ysucc_inj <ysucc_inj <ylminus_inj_sn
+<nminus_succ_sn /2 width=1 by yle_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/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_minus.ma".
+include "ground/arith/ynat_pred.ma".
+
+(* LEFT SUBTRACTION FOR NON-NEGATIVE INTEGERS WITH INFINITY *****************)
+
+(*** yminus_sn *)
+definition ylminus (x) (n): ynat ≝
+ ypred^n x.
+
+interpretation
+ "left minus (non-negative integers with infinity)"
+ 'minus x n = (ylminus x n).
+
+(* Basic constructions ******************************************************)
+
+(*** yminus_O2 *)
+lemma ylminus_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 ylminus_succ_dx (x:ynat) (n): ↓(x-n) = x - ↑n.
+#x #n @(niter_succ … ypred)
+qed.
+
+(*** yminus_SO2 *)
+lemma ylminus_one_dx (x): ↓x = x - (𝟏).
+// qed.
+
+(*** yminus_Y_inj *)
+lemma ylminus_inf_sn (n): ∞ = ∞ - n.
+#n @(nat_ind_succ … n) -n //
+qed.
+
+(* Constructions with nminus ************************************************)
+
+(*** yminus_inj *)
+lemma ylminus_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 ylminus_zero_sn (n): 𝟎 = 𝟎 - n.
+// qed.
+
+(*** yminus_refl *)
+lemma ylminus_refl (n): 𝟎 = yinj_nat n - n.
+// qed.
+
+(*** yminus_minus_comm *)
+lemma ylminus_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_lminus_succ.ma".
+
+(* LEFT SUBTRACTION FOR NON-NEGATIVE INTEGERS WITH INFINITY *****************)
+
+(* Constructions with yplus *************************************************)
+
+(*** yplus_minus *)
+lemma ylminus_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_lminus.ma".
+
+(* LEFT SUBTRACTION FOR NON-NEGATIVE INTEGERS WITH INFINITY *****************)
+
+(* Constructions with ysucc *************************************************)
+
+(*** yminus_succ *)
+lemma ylminus_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_lt_minus.ma".
+include "ground/arith/ynat_lminus.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 ylminus **************************************)
+
+(*** monotonic_ylt_minus_dx *)
+lemma ylt_lminus_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_lminus_plus.ma".
+include "ground/arith/ynat_lt_le_lminus.ma".
+
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
+
+(* Constructions with yle and ylminus and yplus ****************************)
+
+(*** ylt_plus2_to_minus_inj2 *)
+lemma ylt_plus_dx_dx_lminus_sn (o) (x) (y):
+ yinj_nat o ≤ x → x < y + yinj_nat o → x - o < y.
+/2 width=1 by ylt_lminus_bi_dx/ qed.
+
+(*** ylt_plus2_to_minus_inj1 *)
+lemma ylt_plus_dx_sn_lminus_sn (o) (x) (y):
+ yinj_nat o ≤ x → x < yinj_nat o + y → x - o < y.
+/2 width=1 by ylt_plus_dx_dx_lminus_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_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/nat_lt_minus.ma".
+include "ground/arith/ynat_lminus.ma".
+include "ground/arith/ynat_lt.ma".
+
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
+
+(* Constructions with ylminus ***********************************************)
+
+(*** ylt_to_minus *)
+lemma ylt_zero_lminus (m) (y):
+ yinj_nat m < y → 𝟎 < y - m.
+#m #y @(ynat_split_nat_inf … y) -y //
+#n #Hmn <ylminus_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 ylminus **************************************************)
+
+(*** yminus_to_lt *)
+lemma ylt_inv_zero_lminus (m) (y):
+ (𝟎) < y - m → yinj_nat m < y.
+#m #y @(ynat_split_nat_inf … y) -y //
+#n <ylminus_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 ylminus ************************************************)
+
+(*** yminus_pred *)
+lemma ylminus_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 <ylminus_inj_sn <ypred_inj <ylminus_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_lminus.ma".
+include "ground/arith/ynat_lt_pred_succ.ma".
+
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
+
+(* Constructions with ylminus and yplus *************************************)
+
+(*** ylt_plus1_to_minus_inj2 *)
+lemma ylt_plus_sn_dx_lminus_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_lminus_dx (n) (x) (z):
+ yinj_nat n + x < z → x < z - n.
+/2 width=1 by ylt_plus_sn_dx_lminus_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_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.
#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/
+ <(eq_inv_nsucc_bi … H2) -H2 //
| #x2 #H <(eq_inv_inf_ysucc … 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 "arithmetics/nat.ma".
-
-(* INFINITARY NATURAL NUMBERS ***********************************************)
-
-(* the type of infinitary natural numbers *)
-coinductive ynat: Type[0] ≝
-| YO: ynat
-| YS: ynat → ynat
-.
-
-interpretation "ynat successor" 'Successor m = (YS m).
-
-(* the coercion of nat to ynat *)
-let rec ynat_of_nat n ≝ match n with
-[ O ⇒ YO
-| S m ⇒ YS (ynat_of_nat m)
-].
-
-coercion ynat_of_nat.
-
-(* the infinity *)
-let corec Y : ynat ≝ ⫯Y.
-
-interpretation "ynat infinity" 'Infinity = Y.
-
-(* destructing identity on ynat *)
-definition yid: ynat → ynat ≝ λm. match m with
-[ YO ⇒ 0
-| YS n ⇒ ⫯n
-].
-
-(* Properties ***************************************************************)
-
-fact yid_rew: ∀n. yid n = n.
-* // qed-.
-
-lemma Y_rew: ⫯∞ = ∞.
-<(yid_rew ∞) in ⊢ (???%); //
-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_2/notation.ma".
-include "ground_2/xoa_props.ma".
-include "ground_2/ynat/ynat.ma".
-
-(* INFINITARY NATURAL NUMBERS ***********************************************)
-
-(* "is_zero" predicate *)
-definition yzero: predicate ynat ≝ λx. match x with
-[ YO ⇒ ⊤
-| YS _ ⇒ ⊥
-].
-
-(* Inversion lemmas *********************************************************)
-
-lemma discr_YS_YO: ∀n. ⫯n = 0 → ⊥.
-#n #H change with (yzero (⫯n))
->H -H //
-qed-.
-
-lemma discr_YO_YS: ∀n. ynat_of_nat 0 = ⫯n → ⊥. (**) (* explicit coercion *)
-/2 width=2 by discr_YS_YO/ 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_2/star.ma".
-include "ground_2/ynat/ynat_iszero.ma".
-include "ground_2/ynat/ynat_pred.ma".
-
-(* INFINITARY NATURAL NUMBERS ***********************************************)
-
-(* order relation *)
-coinductive yle: relation ynat ≝
-| yle_O: ∀n. yle 0 n
-| yle_S: ∀m,n. yle m n → yle (⫯m) (⫯n)
-.
-
-interpretation "natural 'less or equal to'" 'leq x y = (yle x y).
-
-(* Inversion lemmas *********************************************************)
-
-fact yle_inv_O2_aux: ∀m,x. m ≤ x → x = 0 → m = 0.
-#m #x * -m -x //
-#m #x #_ #H elim (discr_YS_YO … H) (**) (* destructing lemma needed *)
-qed-.
-
-lemma yle_inv_O2: ∀m. m ≤ 0 → m = 0.
-/2 width =3 by yle_inv_O2_aux/ qed-.
-
-fact yle_inv_S1_aux: ∀x,y. x ≤ y → ∀m. x = ⫯m → ∃∃n. m ≤ n & y = ⫯n.
-#x #y * -x -y
-[ #y #m #H elim (discr_YO_YS … H) (**) (* destructing lemma needed *)
-| #x #y #Hxy #m #H destruct /2 width=3 by ex2_intro/
-]
-qed-.
-
-lemma yle_inv_S1: ∀m,y. ⫯m ≤ y → ∃∃n. m ≤ n & y = ⫯n.
-/2 width=3 by yle_inv_S1_aux/ qed-.
-
-lemma yle_inv_S: ∀m,n. ⫯m ≤ ⫯n → m ≤ n.
-#m #n #H elim (yle_inv_S1 … H) -H
-#x #Hx #H destruct //
-qed-.
-
-(* Properties ***************************************************************)
-
-let corec yle_refl: reflexive … yle ≝ ?.
-* [ @yle_O | #x @yle_S // ]
-qed.
-
-let corec yle_Y: ∀m. m ≤ ∞ ≝ ?.
-* [ @yle_O | #m <Y_rew @yle_S // ]
-qed.
-
-let corec yle_S_dx: ∀m,n. m ≤ n → m ≤ ⫯n ≝ ?.
-#m #n * -m -n [ #n @yle_O | #m #n #H @yle_S /2 width=1 by/ ]
-qed.
-
-lemma yle_refl_S_dx: ∀x. x ≤ ⫯x.
-/2 width=1 by yle_refl, yle_S_dx/ qed.
-
-lemma yle_pred_sn: ∀m,n. m ≤ n → ⫰m ≤ n ≝ ?.
-* // #m #n #H elim (yle_inv_S1 … H) -H
-#x #Hm #H destruct /2 width=1 by yle_S_dx/
-qed.
-
-lemma yle_refl_pred_sn: ∀x. ⫰x ≤ x.
-/2 width=1 by yle_refl, yle_pred_sn/ qed.
-
-let corec yle_trans: Transitive … yle ≝ ?.
-#x #y * -x -y [ #x #z #_ @yle_O ]
-#x #y #Hxy #z #H elim (yle_inv_S1 … H) -H
-#n #Hyz #H destruct
-@yle_S @(yle_trans … Hxy … Hyz) (**) (* cofix not guarded by constructors *)
-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_2/ynat/ynat.ma".
-
-(* INFINITARY NATURAL NUMBERS ***********************************************)
-
-(* the predecessor on ynat *)
-definition ypred: ynat → ynat ≝ λm. match m with
-[ YO ⇒ 0
-| YS n ⇒ n
-].
-
-notation "hvbox( ⫰ term 55 T )"
- non associative with precedence 55
- for @{ 'Predecessor $T }.
-
-interpretation "ynat predecessor" 'Predecessor m = (ypred m).
-
-(* Properties ***************************************************************)
-
-lemma ypred_S: ∀m. ⫰⫯m = m.
-// qed.
-
-(* Inversion lemmas *********************************************************)
-
-lemma YS_inj: ∀m,n. ⫯m = ⫯n → m = n.
-#m #n #H <(ypred_S m) <(ypred_S n) //
-qed-.
include "ground/notation/functions/no_0.ma".
include "ground/notation/functions/yes_0.ma".
-(* BOOLEAN PROPERTIES *******************************************************)
+(* BOOLEANS *****************************************************************)
-interpretation "boolean false" 'no = false.
+interpretation
+ "false (booleans)"
+ 'no = false.
-interpretation "boolean true" 'yes = true.
+interpretation
+ "true (booleans)"
+ 'yes = true.
-(* Basic properties *********************************************************)
+(* Advanced constructions ***************************************************)
-lemma commutative_orb: commutative … orb.
-* * // qed.
-
-lemma orb_true_dx: ∀b. (b ∨ Ⓣ) = Ⓣ.
-* // qed.
-
-lemma orb_true_sn: ∀b. (Ⓣ ∨ b) = Ⓣ.
-// qed.
-
-lemma commutative_andb: commutative … andb.
-* * // qed.
-
-lemma andb_false_dx: ∀b. (b ∧ Ⓕ) = Ⓕ.
-* // qed.
-
-lemma andb_false_sn: ∀b. (Ⓕ ∧ b) = Ⓕ.
-// qed.
-
-lemma eq_bool_dec: ∀b1,b2:bool. Decidable (b1 = b2).
+lemma eq_bool_dec (b1:bool) (b2:bool):
+ Decidable (b1 = b2).
* * /2 width=1 by or_introl/
@or_intror #H destruct
qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma orb_inv_false_dx: ∀b1,b2:bool. (b1 ∨ b2) = Ⓕ → b1 = Ⓕ ∧ b2 = Ⓕ.
-* normalize /2 width=1 by conj/ #b2 #H destruct
-qed-.
-
-lemma andb_inv_true_dx: ∀b1,b2:bool. (b1 ∧ b2) = Ⓣ → b1 = Ⓣ ∧ b2 = Ⓣ.
-* normalize /2 width=1 by conj/ #b2 #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/lib/bool.ma".
+
+(* CONJUNCTION FOR BOOLEANS *************************************************)
+
+(* Advanced constructions ***************************************************)
+
+lemma commutative_andb:
+ commutative … andb.
+* * // qed.
+
+lemma andb_false_dx (b):
+ (b ∧ Ⓕ) = Ⓕ.
+* // qed.
+
+lemma andb_false_sn (b):
+ (Ⓕ ∧ b) = Ⓕ.
+// qed.
+
+(* Advanced inversions ******************************************************)
+
+lemma andb_inv_true_dx (b1) (b2):
+ (b1 ∧ b2) = Ⓣ → ∧∧ b1 = Ⓣ & b2 = Ⓣ.
+* normalize /2 width=1 by conj/ #b2 #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/lib/bool.ma".
+
+(* DISJUNCTION FOR BOOLEANS *************************************************)
+
+(* Advanced constructions ***************************************************)
+
+lemma commutative_orb:
+ commutative … orb.
+* * // qed.
+
+lemma orb_true_dx (b):
+ (b ∨ Ⓣ) = Ⓣ.
+* // qed.
+
+lemma orb_true_sn (b):
+ (Ⓣ ∨ b) = Ⓣ.
+// qed.
+
+(* Advanced inversions ******************************************************)
+
+lemma orb_inv_false_dx (b1) (b2):
+ (b1 ∨ b2) = Ⓕ → ∧∧ b1 = Ⓕ & b2 = Ⓕ.
+* normalize /2 width=1 by conj/ #b2 #H destruct
+qed-.
"extensional equivalence"
'DotEq A B f1 f2 = (exteq A B f1 f2).
-(* Basic Constructions ******************************************************)
+(* Basic constructions ******************************************************)
lemma exteq_refl (A) (B): reflexive … (exteq A B).
// qed.
(* LISTS ********************************************************************)
inductive list (A:Type[0]) : Type[0] :=
- | nil : list A
- | cons: A → list A → list A.
+| list_nil : list A
+| list_cons: A → list A → list A
+.
-interpretation "nil (list)" 'CircledE A = (nil A).
+interpretation
+ "nil (lists)"
+ 'CircledE A = (list_nil A).
-interpretation "cons (list)" 'OPlusRight A hd tl = (cons A hd tl).
+interpretation
+ "cons (lists)"
+ 'OPlusRight A hd tl = (list_cons A hd tl).
-rec definition all A (R:predicate A) (l:list A) on l ≝
- match l with
- [ nil ⇒ ⊤
- | cons hd tl ⇒ ∧∧ R hd & all A R tl
- ].
+rec definition list_all A (R:predicate A) (l:list A) on l ≝
+match l with
+[ list_nil ⇒ ⊤
+| list_cons hd tl ⇒ ∧∧ R hd & list_all A R tl
+].
(* EXTENSIONAL EQUIVALENCE OF LISTS *****************************************)
-rec definition eq_list A (l1,l2:list A) on l1 ≝
+rec definition list_eq A (l1,l2:list A) on l1 ≝
match l1 with
-[ nil ⇒
+[ list_nil ⇒
match l2 with
- [ nil ⇒ ⊤
- | cons _ _ ⇒ ⊥
+ [ list_nil ⇒ ⊤
+ | list_cons _ _ ⇒ ⊥
]
-| cons a1 l1 ⇒
+| list_cons a1 l1 ⇒
match l2 with
- [ nil ⇒ ⊥
- | cons a2 l2 ⇒ a1 = a2 ∧ eq_list A l1 l2
+ [ list_nil ⇒ ⊥
+ | list_cons a2 l2 ⇒ a1 = a2 ∧ list_eq A l1 l2
]
].
-interpretation "extensional equivalence (list)"
- 'RingEq A l1 l2 = (eq_list A l1 l2).
+interpretation
+ "extensional equivalence (lists)"
+ 'RingEq A l1 l2 = (list_eq A l1 l2).
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
-lemma eq_list_refl (A): reflexive … (eq_list A).
+lemma list_eq_refl (A): reflexive … (list_eq A).
#A #l elim l -l /2 width=1 by conj/
qed.
-(* Main properties **********************************************************)
+(* Main constructions *******************************************************)
-theorem eq_eq_list (A,l1,l2): l1 = l2 → l1 ≗{A} l2.
+theorem eq_list_eq (A,l1,l2): l1 = l2 → l1 ≗{A} l2.
// qed.
-(* Main inversion propertiess ***********************************************)
+(* Main inversions **********************************************************)
-theorem eq_list_inv_eq (A,l1,l2): l1 ≗{A} l2 → l1 = l2.
+theorem list_eq_inv_eq (A,l1,l2): l1 ≗{A} l2 → l1 = l2.
#A #l1 elim l1 -l1 [| #a1 #l1 #IH ] *
[ //
| #a2 #l2 #H elim H
(* *)
(**************************************************************************)
-include "ground/lib/arith.ma".
include "ground/lib/list.ma".
+include "ground/arith/nat_succ.ma".
-(* LENGTH OF A LIST *********************************************************)
+(* LENGTH FOR LISTS *********************************************************)
-rec definition length A (l:list A) on l ≝ match l with
-[ nil ⇒ 0
-| cons _ l ⇒ ↑(length A l)
+rec definition list_length A (l:list A) on l ≝
+match l with
+[ list_nil ⇒ 𝟎
+| list_cons _ l ⇒ ↑(list_length A l)
].
-interpretation "length (list)"
- 'card l = (length ? l).
+interpretation
+ "length (lists)"
+ 'card l = (list_length ? l).
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
-lemma length_nil (A:Type[0]): |nil A| = 0.
+lemma list_length_nil (A:Type[0]): |list_nil A| = 𝟎.
// qed.
-lemma length_cons (A:Type[0]) (l:list A) (a:A): |a⨮l| = ↑|l|.
+lemma list_length_cons (A:Type[0]) (l:list A) (a:A): |a⨮l| = ↑|l|.
// qed.
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
-lemma length_inv_zero_dx (A:Type[0]) (l:list A): |l| = 0 → l = Ⓔ.
-#A * // #a #l >length_cons #H destruct
+lemma list_length_inv_zero_dx (A:Type[0]) (l:list A):
+ |l| = 𝟎 → l = Ⓔ.
+#A * // #a #l >list_length_cons #H
+elim (eq_inv_nsucc_zero … H)
qed-.
-lemma length_inv_zero_sn (A:Type[0]) (l:list A): 0 = |l| → l = Ⓔ.
-/2 width=1 by length_inv_zero_dx/ qed-.
+lemma list_length_inv_zero_sn (A:Type[0]) (l:list A):
+ (𝟎) = |l| → l = Ⓔ.
+/2 width=1 by list_length_inv_zero_dx/ qed-.
-lemma length_inv_succ_dx (A:Type[0]) (l:list A) (x): |l| = ↑x →
- ∃∃tl,a. x = |tl| & l = a ⨮ tl.
+lemma list_length_inv_succ_dx (A:Type[0]) (l:list A) (x):
+ |l| = ↑x →
+ ∃∃tl,a. x = |tl| & l = a ⨮ tl.
#A *
-[ #x >length_nil #H destruct
-| #a #l #x >length_cons #H destruct /2 width=4 by ex2_2_intro/
+[ #x >list_length_nil #H
+ elim (eq_inv_zero_nsucc … H)
+| #a #l #x >list_length_cons #H
+ /3 width=4 by eq_inv_nsucc_bi, ex2_2_intro/
]
qed-.
-lemma length_inv_succ_sn (A:Type[0]) (l:list A) (x): ↑x = |l| →
- ∃∃tl,a. x = |tl| & l = a ⨮ tl.
-/2 width=1 by length_inv_succ_dx/ qed.
+lemma list_length_inv_succ_sn (A:Type[0]) (l:list A) (x):
+ ↑x = |l| →
+ ∃∃tl,a. x = |tl| & l = a ⨮ tl.
+/2 width=1 by list_length_inv_succ_dx/ qed-.
include "ground/notation/xoa/or_2.ma".
include "ground/notation/xoa/and_2.ma".
-interpretation "logical false" 'false = False.
+interpretation
+ "false (logic)"
+ 'false = False.
-interpretation "logical true" 'true = True.
+interpretation
+ "true (logic)"
+ 'true = True.
-(* Logical properties missing in the basic library **************************)
+(* LOGIC ********************************************************************)
+
+(* Constructions with And ***************************************************)
lemma commutative_and: ∀A,B. A ∧ B → B ∧ A.
#A #B * /2 width=1 by conj/
(* *)
(**************************************************************************)
-include "arithmetics/lstar.ma".
+include "ground/lib/ltc.ma".
+include "ground/arith/nat_plus.ma".
-(* PROPERTIES OF NAT-LABELED REFLEXIVE AND TRANSITIVE CLOSURE ***************)
+(* NAT-LABELED REFLEXIVE AND TRANSITIVE CLOSURE FOR FOR λδ-2A ***************)
-definition llstar: ∀A:Type[0]. ∀B. (A→relation B) → nat → (A→relation B) ≝
- λA,B,R,l,a. lstar … (R a) l.
+definition lstar_aux (B) (R:relation B) (l): relation B ≝
+ λb1,b2. ∨∨ (∧∧ l = 𝟎 & b1 = b2) | (∧∧ l = 𝟏 & R b1 b2).
+
+definition lstar (B) (R:relation B): nat → relation B ≝
+ ltc … nplus … (lstar_aux … R).
+
+definition llstar (A) (B) (R:relation3 A B B) (l:nat): relation3 A B B ≝
+ λa. lstar … (R a) l.
(* *)
(**************************************************************************)
-include "ground/insert_eq/insert_eq_0.ma".
+include "ground/insert_eq/insert_eq_1.ma".
include "ground/lib/functions.ma".
(* LABELLED TRANSITIVE CLOSURE **********************************************)
| ltc_trans: ∀a1,a2,b1,b,b2. ltc … a1 b1 b → ltc … a2 b b2 → ltc … (f a1 a2) b1 b2
.
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
lemma ltc_sn (A) (f) (B) (R): ∀a1,b1,b. R a1 b1 b →
∀a2,b2. ltc A f B R a2 b b2 → ltc … f … R (f a1 a2) b1 b2.
∀a2,b2. R a2 b b2 → ltc … f … R (f a1 a2) b1 b2.
/3 width=3 by ltc_rc, ltc_trans/ qed.
-(* Basic eliminators ********************************************************)
+(* Basic eliminations *******************************************************)
lemma ltc_ind_sn (A) (f) (B) (R) (Q:relation2 A B) (b2): associative … f →
(∀a,b1. R a b1 b2 → Q a b1) →
(∀a1,a2,b1,b. R a1 b1 b → ltc … f … R a2 b b2 → Q a2 b → Q (f a1 a2) b1) →
∀a,b1. ltc … f … R a b1 b2 → Q a b1.
-#A #f #B #R #Q #b2 #Hf #IH1 #IH2 #a #b1 @(insert_eq_0 … b2)
+#A #f #B #R #Q #b2 #Hf #IH1 #IH2 #a #b1 @(insert_eq_1 … b2)
#b0 #H elim H -a -b1 -b0 /2 width=2 by/
#a1 #a2 #b1 #b #b0 #H #Hb2 #_
generalize in match Hb2; generalize in match a2; -Hb2 -a2
(∀a,b2. R a b1 b2 → Q a b2) →
(∀a1,a2,b,b2. ltc … f … R a1 b1 b → Q a1 b → R a2 b b2 → Q (f a1 a2) b2) →
∀a,b2. ltc … f … R a b1 b2 → Q a b2.
-#A #f #B #R #Q #b1 #Hf #IH1 #IH2 #a #b2 @(insert_eq_0 … b1)
+#A #f #B #R #Q #b1 #Hf #IH1 #IH2 #a #b2 @(insert_eq_1 … b1)
#b0 #H elim H -a -b0 -b2 /2 width=2 by/
#a1 #a2 #b0 #b #b2 #Hb0 #H #IHb0 #_
generalize in match IHb0; generalize in match Hb0; generalize in match a1; -IHb0 -Hb0 -a1
elim H -a2 -b -b2 /4 width=4 by ltc_trans/
qed-.
-(* Advanced elimiators with reflexivity *************************************)
+(* Advanced elimiations with reflexivity ************************************)
lemma ltc_ind_sn_refl (A) (i) (f) (B) (R) (Q:relation2 A B) (b2):
associative … f → right_identity … f i → reflexive B (R i) →
>(H2f a) -H2f /3 width=4 by ltc_rc/
qed-.
-(* Properties with lsub *****************************************************)
+(* Constructions with lsub **************************************************)
lemma ltc_lsub_trans: ∀A,f. associative … f →
∀B,C,R,S. (∀n. lsub_trans B C (λL. R L n) S) →
(* LABELLED TRANSITIVE CLOSURE **********************************************)
-alias symbol "subseteq" = "relation inclusion".
+alias symbol "subseteq" = "relation inclusion". (**)
-(* Properties with contextual transitive closure ****************************)
+(* Constructions with contextual transitive closure *************************)
lemma ltc_CTC (C) (A) (i) (f) (B) (R:relation4 C A B B):
left_identity … f i →
#b #b2 #_ #Hb2 #IH >(Hf i) -Hf /2 width=3 by ltc_dx/
qed.
-(* Inversion lemmas with contextual transitive closure **********************)
+(* Inversions with contextual transitive closure ****************************)
lemma ltc_inv_CTC (C) (A) (i) (f) (B) (R:relation4 C A B B):
associative … f → annulment_2 … f i →
∀c. ltc … f … (R c) i ⊆ CTC … (λc. R c i) c.
#C #A #i #f #B #R #H1f #H2f #c #b1 #b2
-@(insert_eq_0 … i) #a #H
+@(insert_eq_1 … i) #a #H
@(ltc_ind_dx A f B … H) -a -b2 /2 width=1 by inj/ -H1f
#a1 #a2 #b #b2 #_ #IH #Hb2 #H <H
elim (H2f … H) -H2f -H #H1 #H2 destruct
elim HSa12 -HSa12 /2 width=1 by/
qed.
-(* Normal form and strong normalization on unboxed triples ******************)
+(* Normal form and strong normalization with unboxed triples ****************)
inductive SN3 (A) (B) (C) (R,S:relation6 A B C A B C): relation3 A B C ≝
| SN3_intro: ∀a1,b1,c1. (∀a2,b2,c2. R a1 b1 c1 a2 b2 c2 → (S a1 b1 c1 a2 b2 c2 → ⊥) → SN3 … R S a2 b2 c2) → SN3 … R S a1 b1 c1
.
-(* Relations on unboxed triples *********************************************)
+(* Relations with unboxed triples *******************************************)
definition tri_RC (A,B,C): tri_relation A B C → tri_relation A B C ≝
λR,a1,b1,c1,a2,b2,c2.
* #a0 #Ha10 #Ha01 elim (IHa1 … Ha10 Ha01) -IHa1 -Ha01 /3 width=3 by star_compl, ex2_intro/
qed-.
-(* Relations on unboxed pairs ***********************************************)
+(* Relations with unboxed pairs *********************************************)
lemma bi_TC_strip: ∀A,B,R. bi_confluent A B R →
∀a0,a1,b0,b1. R a0 b0 a1 b1 → ∀a2,b2. bi_TC … R a0 b0 a2 b2 →
]
qed-.
-(* Relations on unboxed triples *********************************************)
+(* Relations with unboxed triples *******************************************)
definition tri_star: ∀A,B,C,R. tri_relation A B C ≝
λA,B,C,R. tri_RC A B C (tri_TC … R).
(* STREAMS ******************************************************************)
coinductive stream (A:Type[0]): Type[0] ≝
-| seq: A → stream A → stream A
+| stream_cons: A → stream A → stream A
.
-interpretation "cons (stream)" 'OPlusRight A a u = (seq A a u).
+interpretation
+ "cons (streams)"
+ 'OPlusRight A a u = (stream_cons A a u).
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
-lemma stream_rew (A) (t:stream A): match t with [ seq a u ⇒ a ⨮ u ] = t.
+lemma stream_rew (A) (t:stream A): match t with [ stream_cons a u ⇒ a ⨮ u ] = t.
#A * //
qed.
include "ground/notation/relations/ringeq_3.ma".
include "ground/lib/stream.ma".
-(* STREAMS ******************************************************************)
+(* EXTENSIONAL EQUIVALENCE FOR STREAMS **************************************)
-coinductive eq_stream (A): relation (stream A) ≝
-| eq_seq: ∀t1,t2,b1,b2. b1 = b2 → eq_stream A t1 t2 → eq_stream A (b1⨮t1) (b2⨮t2)
+coinductive stream_eq (A): relation (stream A) ≝
+| stream_eq_cons: ∀t1,t2,b1,b2. b1 = b2 → stream_eq A t1 t2 → stream_eq A (b1⨮t1) (b2⨮t2)
.
-interpretation "extensional equivalence (stream)"
- 'RingEq A t1 t2 = (eq_stream A t1 t2).
+interpretation
+ "extensional equivalence (streams)"
+ 'RingEq A t1 t2 = (stream_eq A t1 t2).
-definition eq_stream_repl (A) (R:relation …) ≝
- ∀t1,t2. t1 ≗{A} t2 → R t1 t2.
+definition stream_eq_repl (A) (R:relation …) ≝
+ ∀t1,t2. t1 ≗{A} t2 → R t1 t2.
-definition eq_stream_repl_back (A) (R:predicate …) ≝
- ∀t1. R t1 → ∀t2. t1 ≗{A} t2 → R t2.
+definition stream_eq_repl_back (A) (R:predicate …) ≝
+ ∀t1. R t1 → ∀t2. t1 ≗{A} t2 → R t2.
-definition eq_stream_repl_fwd (A) (R:predicate …) ≝
- ∀t1. R t1 → ∀t2. t2 ≗{A} t1 → R t2.
+definition stream_eq_repl_fwd (A) (R:predicate …) ≝
+ ∀t1. R t1 → ∀t2. t2 ≗{A} t1 → R t2.
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
-lemma eq_stream_inv_seq: ∀A,t1,t2. t1 ≗{A} t2 →
- ∀u1,u2,a1,a2. a1⨮u1 = t1 → a2⨮u2 = t2 →
- u1 ≗ u2 ∧ a1 = a2.
+lemma stream_eq_inv_cons: ∀A,t1,t2. t1 ≗{A} t2 →
+ ∀u1,u2,a1,a2. a1⨮u1 = t1 → a2⨮u2 = t2 →
+ u1 ≗ u2 ∧ a1 = a2.
#A #t1 #t2 * -t1 -t2
#t1 #t2 #b1 #b2 #Hb #Ht #u1 #u2 #a1 #a2 #H1 #H2 destruct /2 width=1 by conj/
qed-.
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
-corec lemma eq_stream_refl: ∀A. reflexive … (eq_stream A).
-#A * #b #t @eq_seq //
+corec lemma stream_eq_refl: ∀A. reflexive … (stream_eq A).
+#A * #b #t @stream_eq_cons //
qed.
-corec lemma eq_stream_sym: ∀A. symmetric … (eq_stream A).
+corec lemma stream_eq_sym: ∀A. symmetric … (stream_eq A).
#A #t1 #t2 * -t1 -t2
-#t1 #t2 #b1 #b2 #Hb #Ht @eq_seq /2 width=1 by/
+#t1 #t2 #b1 #b2 #Hb #Ht @stream_eq_cons /2 width=1 by/
qed-.
-lemma eq_stream_repl_sym: ∀A,R. eq_stream_repl_back A R → eq_stream_repl_fwd A R.
-/3 width=3 by eq_stream_sym/ qed-.
+lemma stream_eq_repl_sym: ∀A,R. stream_eq_repl_back A R → stream_eq_repl_fwd A R.
+/3 width=3 by stream_eq_sym/ qed-.
-(* Main properties **********************************************************)
+(* Main constructions *******************************************************)
-corec theorem eq_stream_trans: ∀A. Transitive … (eq_stream A).
+corec theorem stream_eq_trans: ∀A. Transitive … (stream_eq A).
#A #t1 #t * -t1 -t
-#t1 #t #b1 #b * #Ht1 * #b2 #t2 #H cases (eq_stream_inv_seq A … H) -H -b
-/3 width=7 by eq_seq/
+#t1 #t #b1 #b * #Ht1 * #b2 #t2 #H cases (stream_eq_inv_cons A … H) -H -b
+/3 width=7 by stream_eq_cons/
qed-.
-theorem eq_stream_canc_sn: ∀A,t,t1,t2. t ≗ t1 → t ≗ t2 → t1 ≗{A} t2.
-/3 width=3 by eq_stream_trans, eq_stream_sym/ qed-.
+theorem stream_eq_canc_sn: ∀A,t,t1,t2. t ≗ t1 → t ≗ t2 → t1 ≗{A} t2.
+/3 width=3 by stream_eq_trans, stream_eq_sym/ qed-.
-theorem eq_stream_canc_dx: ∀A,t,t1,t2. t1 ≗ t → t2 ≗ t → t1 ≗{A} t2.
-/3 width=3 by eq_stream_trans, eq_stream_sym/ qed-.
+theorem stream_eq_canc_dx: ∀A,t,t1,t2. t1 ≗ t → t2 ≗ t → t1 ≗{A} t2.
+/3 width=3 by stream_eq_trans, stream_eq_sym/ qed-.
include "ground/notation/functions/downspoon_2.ma".
include "ground/lib/stream_eq.ma".
-include "ground/lib/arith.ma".
-(* STREAMS ******************************************************************)
+(* HEAD AND TAIL FOR STREAMS ************************************************)
-definition hd (A:Type[0]): stream A → A ≝
- λt. match t with [ seq a _ ⇒ a ].
+definition stream_hd (A:Type[0]): stream A → A ≝
+ λt. match t with [ stream_cons a _ ⇒ a ].
-definition tl (A:Type[0]): stream A → stream A ≝
- λt. match t with [ seq _ t ⇒ t ].
+definition stream_tl (A:Type[0]): stream A → stream A ≝
+ λt. match t with [ stream_cons _ t ⇒ t ].
-interpretation "tail (stream)" 'DownSpoon A t = (tl A t).
+interpretation
+ "tail (streams)"
+ 'DownSpoon A t = (stream_tl A t).
-(* basic properties *********************************************************)
+(* Basic constructions ******************************************************)
-lemma hd_rew (A) (a) (t): a = hd A (a⨮t).
+lemma stream_hd_cons (A) (a) (t):
+ a = stream_hd A (a⨮t).
// qed.
-lemma tl_rew (A) (a) (t): t = tl A (a⨮t).
+lemma stream_tl_cons (A) (a) (t):
+ t = ⫰{A}(a⨮t).
// qed.
-lemma eq_stream_split (A) (t): (hd … t) ⨮ ⫰t ≗{A} t.
+lemma eq_stream_split_hd_tl (A) (t):
+ stream_hd … t ⨮ ⫰t ≗{A} t.
#A * //
qed.
include "ground/notation/functions/downspoonstar_3.ma".
include "ground/lib/stream_hdtl.ma".
+include "ground/arith/nat_succ_iter.ma".
-(* STREAMS ******************************************************************)
+(* ITERATED TAIL FOR STREAMS ************************************************)
-rec definition tls (A:Type[0]) (n:nat) on n: stream A → stream A ≝ ?.
-cases n -n [ #t @t | #n #t @tl @(tls … n t) ]
-defined.
+definition stream_tls (A) (n): stream A → stream A ≝
+ (stream_tl A)^n.
-interpretation "iterated tail (stram)" 'DownSpoonStar A n f = (tls A n f).
+interpretation
+ "iterated tail (strams)"
+ 'DownSpoonStar A n f = (stream_tls A n f).
-(* basic properties *********************************************************)
+(* Basic constructions ******************************************************)
-lemma tls_rew_O (A) (t): t = tls A 0 t.
+lemma stream_tls_zero (A) (t):
+ t = ⫰*{A}[𝟎]t.
// qed.
-lemma tls_rew_S (A) (n) (t): ⫰⫰*[n]t = tls A (↑n) t.
-// qed.
+lemma stream_tls_tl (A) (n) (t):
+ (⫰⫰*[n]t) = ⫰*{A}[n]⫰t.
+#A #n #t
+@(niter_appl … (stream_tl …))
+qed.
-lemma tls_S1 (A) (n) (t): ⫰*[n]⫰t = tls A (↑n) t.
-#A #n elim n -n //
+lemma stream_tls_succ (A) (n) (t):
+ (⫰⫰*[n]t) = ⫰*{A}[↑n]t.
+#A #n #t
+@(niter_succ … (stream_tl …))
qed.
-lemma tls_eq_repl (A) (n): eq_stream_repl A (λt1,t2. ⫰*[n] t1 ≗ ⫰*[n] t2).
-#A #n elim n -n //
-#n #IH * #n1 #t1 * #n2 #t2 #H elim (eq_stream_inv_seq … H) /2 width=7 by/
+lemma stream_tls_swap (A) (n) (t):
+ (⫰*[n]⫰t) = ⫰*{A}[↑n]t.
+// qed.
+
+lemma stream_tls_eq_repl (A) (n):
+ stream_eq_repl A (λt1,t2. ⫰*[n] t1 ≗ ⫰*[n] t2).
+#A #n @(nat_ind_succ … n) -n //
+#n #IH * #n1 #t1 * #n2 #t2 #H elim (stream_eq_inv_cons … H) /2 width=7 by/
qed.
}
]
[ { "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_lt ( ?<? )" "ynat_lt_succ" "ynat_lt_pred" "ynat_lt_pred_succ" "ynat_lt_plus" "ynat_lt_plus_pred" "ynat_lt_lminus" "ynat_lt_lminus_plus" "ynat_lt_le" "ynat_lt_le_succ" "ynat_lt_le_pred" "ynat_lt_le_pred_succ" "ynat_lt_le_plus" "ynat_lt_le_lminus" "ynat_lt_le_lminus_plus" * ]
+ [ "ynat_le ( ?≤? )" "ynat_le_succ" "ynat_le_pred" "ynat_le_pred_succ" "ynat_le_plus" "ynat_le_lminus" "ynat_le_lminus_succ" "ynat_le_lminus_plus" * ]
+ [ "ynat_lminus ( ?-? )" "ynat_lminus_succ" "ynat_lminus_plus" * ]
[ "ynat_plus ( ?+? )" * ]
[ "ynat_pred ( ↓? )" "ynat_pred_succ" * ]
[ "ynat_succ ( ↑? )" * ]
[ { "extensions to the library" * } {
[ { "" * } {
[ "stream ( ? ⨮{?} ? )" "stream_eq ( ? ≗{?} ? )" "stream_hdtl ( ⫰{?}? )" "stream_tls ( ⫰*{?}[?]? )" * ]
- [ "list ( Ⓔ{?} ) ( ? ⨮{?} ? )" "list_length ( |?| )" * ]
- [ "bool ( Ⓕ ) ( Ⓣ )" * ]
+ [ "list ( Ⓔ{?} ) ( ? ⨮{?} ? )" "list_eq" "list_length ( |?| )" * ]
+ [ "bool ( Ⓕ ) ( Ⓣ )" "bool_or" "bool_and" * ]
[ "ltc" "ltc_ctc" * ]
[ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "exteq ( ? ≐{?,?} ? )" "star" "lstar_2a" * ]
}