propagating the arithmetics library, partial commit

+ lib ported
+ minor corrections and renaming
+ old parked version of ynat removed

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/arith_2b.ma b/matita/matita/contribs/lambdadelta/ground/arith/arith_2b.ma
index f284a3c6cadc551ea4b29f44991426f1cd4becec..842fcc72a21f77e2fd3135f92e4047da878daa20 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/arith_2b.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/arith_2b.ma
@@ -22,7 +22,8 @@ lemma arith_l4 (m11) (m12) (m21) (m22):
 elim (nat_split_le_ge (m11+m12) m21) #Hm1121
 [ lapply (nle_trans m11 ??? Hm1121) // #Hm121
   lapply (nle_minus_dx_dx … Hm1121) #Hm12211
 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
 | <(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

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_le.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_le.ma
index 66a47dd4a0b4f6bd30a7dc0d40c18ed8dd29e859..1e1dad37f7f2bbe6f12c60f10ad40bbb0ca1e8ae 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_le.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_le.ma
@@ -71,7 +71,8 @@ qed-.
 lemma yle_antisym (x) (y):
       x ≤ y → y ≤ x → x = y.
 #x #y #H elim H -x -y
 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-.
 | /2 width=1 by yle_inv_inf_sn/
 ] 
 qed-.

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_lminus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_lminus.ma
new file mode 100644 (file)
index 0000000..bcad28e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_lminus.ma
@@ -0,0 +1,57 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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-.

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_lminus_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_lminus_plus.ma
new file mode 100644 (file)
index 0000000..b45afa8
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_lminus_plus.ma
@@ -0,0 +1,117 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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-.

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_lminus_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_lminus_succ.ma
new file mode 100644 (file)
index 0000000..93e73cf
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_lminus_succ.ma
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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-.

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_minus1.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_minus1.ma
deleted file mode 100644 (file)
index bd54804..0000000
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_minus1.ma
+++ /dev/null
@@ -1,57 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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-.

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_minus1_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_minus1_plus.ma
deleted file mode 100644 (file)
index 29057bd..0000000
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_minus1_plus.ma
+++ /dev/null
@@ -1,117 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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-.

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_minus1_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_minus1_succ.ma
deleted file mode 100644 (file)
index 76cfcaf..0000000
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_minus1_succ.ma
+++ /dev/null
@@ -1,29 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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-.

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma
new file mode 100644 (file)
index 0000000..15e58fd
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma
@@ -0,0 +1,76 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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.

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus_plus.ma
new file mode 100644 (file)
index 0000000..3169003
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus_plus.ma
@@ -0,0 +1,34 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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.

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus_succ.ma
new file mode 100644 (file)
index 0000000..6f04c9d
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus_succ.ma
@@ -0,0 +1,24 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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.

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus.ma
new file mode 100644 (file)
index 0000000..04e0c4c
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus.ma
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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.

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus_plus.ma
new file mode 100644 (file)
index 0000000..6a66bde
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus_plus.ma
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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.

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_minus1.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_minus1.ma
deleted file mode 100644 (file)
index 73b5817..0000000
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_minus1.ma
+++ /dev/null
@@ -1,29 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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.

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_minus1_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_minus1_plus.ma
deleted file mode 100644 (file)
index bd5ce71..0000000
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_minus1_plus.ma
+++ /dev/null
@@ -1,30 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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.

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_lminus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_lminus.ma
new file mode 100644 (file)
index 0000000..acee04e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_lminus.ma
@@ -0,0 +1,50 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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-.

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_lminus_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_lminus_plus.ma
new file mode 100644 (file)
index 0000000..c78a384
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_lminus_plus.ma
@@ -0,0 +1,34 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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.

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_minus1.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_minus1.ma
deleted file mode 100644 (file)
index 9ab5aa7..0000000
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_minus1.ma
+++ /dev/null
@@ -1,50 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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-.

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_minus1_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_minus1_plus.ma
deleted file mode 100644 (file)
index f0f1627..0000000
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_minus1_plus.ma
+++ /dev/null
@@ -1,34 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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.

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_minus1.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_minus1.ma
deleted file mode 100644 (file)
index 4e68e69..0000000
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_minus1.ma
+++ /dev/null
@@ -1,76 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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.

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_minus1_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_minus1_plus.ma
deleted file mode 100644 (file)
index 4c260d7..0000000
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_minus1_plus.ma
+++ /dev/null
@@ -1,34 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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.

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_minus1_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_minus1_succ.ma
deleted file mode 100644 (file)
index 9e4df6c..0000000
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_minus1_succ.ma
+++ /dev/null
@@ -1,24 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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.

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_succ.ma
index 8f8fe4047d04d994e09b49e8b60f1bbfeb32ca1b..9e4fb430cf71182640720323b20ffb472c656b25 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_succ.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_succ.ma
@@ -72,7 +72,7 @@ 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
 #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-.
 | #x2 #H <(eq_inv_inf_ysucc … H) -H //
 ]
 qed-.

diff --git a/matita/matita/contribs/lambdadelta/ground/etc/ynat_old/ynat.etc b/matita/matita/contribs/lambdadelta/ground/etc/ynat_old/ynat.etc
deleted file mode 100644 (file)
index 09df4db..0000000
--- a/matita/matita/contribs/lambdadelta/ground/etc/ynat_old/ynat.etc
+++ /dev/null
@@ -1,53 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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.

diff --git a/matita/matita/contribs/lambdadelta/ground/etc/ynat_old/ynat_iszero.etc b/matita/matita/contribs/lambdadelta/ground/etc/ynat_old/ynat_iszero.etc
deleted file mode 100644 (file)
index 3cb47bc..0000000
--- a/matita/matita/contribs/lambdadelta/ground/etc/ynat_old/ynat_iszero.etc
+++ /dev/null
@@ -1,35 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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-.

diff --git a/matita/matita/contribs/lambdadelta/ground/etc/ynat_old/ynat_le.etc b/matita/matita/contribs/lambdadelta/ground/etc/ynat_old/ynat_le.etc
deleted file mode 100644 (file)
index bde84cf..0000000
--- a/matita/matita/contribs/lambdadelta/ground/etc/ynat_old/ynat_le.etc
+++ /dev/null
@@ -1,84 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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-. 

diff --git a/matita/matita/contribs/lambdadelta/ground/etc/ynat_old/ynat_pred.etc b/matita/matita/contribs/lambdadelta/ground/etc/ynat_old/ynat_pred.etc
deleted file mode 100644 (file)
index 202649e..0000000
--- a/matita/matita/contribs/lambdadelta/ground/etc/ynat_old/ynat_pred.etc
+++ /dev/null
@@ -1,40 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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-.

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/bool.ma b/matita/matita/contribs/lambdadelta/ground/lib/bool.ma
index 69bc66c87f7f8e1a579948f56812fa860ce72905..7b827baf913f99f6b091556ce883e9213ee0aa41 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/bool.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/bool.ma
@@ -17,43 +17,20 @@ include "ground/lib/relations.ma".
 include "ground/notation/functions/no_0.ma".
 include "ground/notation/functions/yes_0.ma".
 
 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-.
 * * /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-.

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/bool_and.ma b/matita/matita/contribs/lambdadelta/ground/lib/bool_and.ma
new file mode 100644 (file)
index 0000000..b7a8bf9
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/lib/bool_and.ma
@@ -0,0 +1,38 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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-.

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/bool_or.ma b/matita/matita/contribs/lambdadelta/ground/lib/bool_or.ma
new file mode 100644 (file)
index 0000000..187b46e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/lib/bool_or.ma
@@ -0,0 +1,38 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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-.

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/exteq.ma b/matita/matita/contribs/lambdadelta/ground/lib/exteq.ma
index 6e39281188722a81545cf2b47572a1e0003f8f2f..5b655e686a5cec35230bedbe9bc819e9d717ed6e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/exteq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/exteq.ma
@@ -24,7 +24,7 @@ interpretation
   "extensional equivalence"
   'DotEq A B f1 f2 = (exteq A B f1 f2).
 
   "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.
 
 lemma exteq_refl (A) (B): reflexive … (exteq A B).
 // qed.

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list.ma b/matita/matita/contribs/lambdadelta/ground/lib/list.ma
index 7864ed0abfe41274f172e0b2be6b2e55f3d75d84..781fc27a55791dde08660777837f20b879e9892e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/list.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list.ma
@@ -19,15 +19,20 @@ include "ground/lib/relations.ma".
 (* LISTS ********************************************************************)
 
 inductive list (A:Type[0]) : Type[0] :=
 (* 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
+].

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_eq.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_eq.ma
index 6f89d187f16bc09ec3f438eac960a7b9bb885dba..ffa06ab6d9960c2a0e5758d666be328e0c5efd06 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/list_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list_eq.ma
@@ -17,37 +17,38 @@ include "ground/lib/list.ma".
 
 (* EXTENSIONAL EQUIVALENCE OF LISTS *****************************************)
 
 
 (* 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
 match l1 with

-[ nil        ⇒
+[ list_nil        ⇒

   match l2 with
   match l2 with

-  [ nil      ⇒ ⊤
-  | cons _ _ ⇒ ⊥
+  [ list_nil      ⇒ ⊤
+  | list_cons _ _ ⇒ ⊥

   ]
   ]

-| cons a1 l1 ⇒
+| list_cons a1 l1 ⇒

   match l2 with
   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.
 
 #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.
 
 // 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
 #A #l1 elim l1 -l1 [| #a1 #l1 #IH ] *
 [ //
 | #a2 #l2 #H elim H

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_length.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_length.ma
index ab736bdd4196e6733d764464d2357a0fbb926c17..0d67e73901dd2778ccf7c76ad6a31effd0638652 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/list_length.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list_length.ma
@@ -12,44 +12,53 @@
 (*                                                                        *)
 (**************************************************************************)
 
 (*                                                                        *)
 (**************************************************************************)
 

-include "ground/lib/arith.ma".

 include "ground/lib/list.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.
 
 // 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.
 
 // 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-.
 
 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 *
 #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-.
 
 ]
 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-.

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/logic.ma b/matita/matita/contribs/lambdadelta/ground/lib/logic.ma
index dc721648096a70f8dd38ae3c689328a03eccf47f..fc2e2ea85ca75abccc27963613769ea412dd60a5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/logic.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/logic.ma
@@ -18,11 +18,17 @@ include "ground/notation/xoa/true_0.ma".
 include "ground/notation/xoa/or_2.ma".
 include "ground/notation/xoa/and_2.ma".
 
 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/
 
 lemma commutative_and: ∀A,B. A ∧ B → B ∧ A.
 #A #B * /2 width=1 by conj/

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/lstar_2a.ma b/matita/matita/contribs/lambdadelta/ground/lib/lstar_2a.ma
index ae707f2b96038cb5aed1a5206b3a702778961e49..ba513ae859d49cc7e0147893ab01b72d9d5b2202 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/lstar_2a.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/lstar_2a.ma
@@ -12,9 +12,16 @@
 (*                                                                        *)
 (**************************************************************************)
 
 (*                                                                        *)
 (**************************************************************************)
 

-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.

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/ltc.ma b/matita/matita/contribs/lambdadelta/ground/lib/ltc.ma
index 4f3962671e212fb675d969686f101c41c5d24702..1d08fb15d98b9bd7af24e7d55f3ed133c8eea363 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/ltc.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/ltc.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
 (*                                                                        *)
 (**************************************************************************)
 

-include "ground/insert_eq/insert_eq_0.ma".
+include "ground/insert_eq/insert_eq_1.ma".

 include "ground/lib/functions.ma".
 
 (* LABELLED TRANSITIVE CLOSURE **********************************************)
 include "ground/lib/functions.ma".
 
 (* LABELLED TRANSITIVE CLOSURE **********************************************)


@@ -22,7 +22,7 @@ inductive ltc (A:Type[0]) (f) (B) (R:relation3 A B B): relation3 A B B ≝
 | ltc_trans: ∀a1,a2,b1,b,b2. ltc … a1 b1 b → ltc … a2 b b2 → ltc … (f a1 a2) b1 b2
 .
 
 | 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.
 
 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.


@@ -32,13 +32,13 @@ lemma ltc_dx (A) (f) (B) (R): ∀a1,b1,b. ltc A f B R a1 b1 b →
                               ∀a2,b2. R a2 b b2 → ltc … f … R (f a1 a2) b1 b2.
 /3 width=3 by ltc_rc, ltc_trans/ qed.
 
                               ∀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.
 
 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
 #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


@@ -49,14 +49,14 @@ lemma ltc_ind_dx (A) (f) (B) (R) (Q:A→predicate B) (b1): associative … f →
                  (∀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,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-.
 
 #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) →
 
 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) →


@@ -78,7 +78,7 @@ lemma ltc_ind_dx_refl (A) (i) (f) (B) (R) (Q:A→predicate B) (b1):
 >(H2f a) -H2f /3 width=4 by ltc_rc/
 qed-.
 
 >(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) →
 
 lemma ltc_lsub_trans: ∀A,f. associative … f →
                       ∀B,C,R,S. (∀n. lsub_trans B C (λL. R L n) S) →

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/ltc_ctc.ma b/matita/matita/contribs/lambdadelta/ground/lib/ltc_ctc.ma
index 0f8ddd10789ffefcf2aa2c40909a4e64cce0ff18..54b1117b6260d007a2258dae9f54eb19663683e8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/ltc_ctc.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/ltc_ctc.ma
@@ -17,9 +17,9 @@ include "ground/lib/ltc.ma".
 
 (* LABELLED TRANSITIVE CLOSURE **********************************************)
 
 
 (* 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 →
 
 lemma ltc_CTC (C) (A) (i) (f) (B) (R:relation4 C A B B):
               left_identity … f i →


@@ -28,13 +28,13 @@ lemma ltc_CTC (C) (A) (i) (f) (B) (R:relation4 C A B B):
 #b #b2 #_ #Hb2 #IH >(Hf i) -Hf /2 width=3 by ltc_dx/
 qed.
 
 #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
 
 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
 @(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

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/relations.ma b/matita/matita/contribs/lambdadelta/ground/lib/relations.ma
index b132d8682735f4c893e6f14dc44f103908fac508..56f6e21f79cf0d3bbad1159d5a257bdb33d98386 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/relations.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/relations.ma
@@ -135,13 +135,13 @@ lemma NF_to_SN_sn (A) (R) (S): ∀a. NF_sn A R S a → SN_sn A R S a.
 elim HSa12 -HSa12 /2 width=1 by/
 qed.
 
 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
 .
 
 
 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.
 
 definition tri_RC (A,B,C): tri_relation A B C → tri_relation A B C ≝
            λR,a1,b1,c1,a2,b2,c2.

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/star.ma b/matita/matita/contribs/lambdadelta/ground/lib/star.ma
index e1580c46eb241c25a832c74897ace7810c02445f..5e748c5ea74ca8a369f09c40251f8e272c1054fe 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/star.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/star.ma
@@ -149,7 +149,7 @@ lemma SN_to_NF: ∀A,R,S. NF_dec A R S →
 * #a0 #Ha10 #Ha01 elim (IHa1 … Ha10 Ha01) -IHa1 -Ha01 /3 width=3 by star_compl, ex2_intro/
 qed-.
 
 * #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 →
 
 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 →


@@ -190,7 +190,7 @@ lemma bi_TC_decomp_l: ∀A,B. ∀R:bi_relation A B.
 ]
 qed-.
 
 ]
 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).
 
 definition tri_star: ∀A,B,C,R. tri_relation A B C ≝
                      λA,B,C,R. tri_RC A B C (tri_TC … R).

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream.ma
index 490a0d0d99bd723ed7e97acd03946bebc1bf0be0..d0e05e17e067632d71937926eba6a6494969265c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/stream.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/stream.ma
@@ -18,13 +18,15 @@ include "ground/lib/relations.ma".
 (* STREAMS ******************************************************************)
 
 coinductive stream (A:Type[0]): Type[0] ≝
 (* 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.
 #A * //
 qed.

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream_eq.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream_eq.ma
index 425f91e825759d5b191a5470d851d295ff1530c9..311930686057e113b7d20faecfa5cdb1513220e0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/stream_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/stream_eq.ma
@@ -15,57 +15,58 @@
 include "ground/notation/relations/ringeq_3.ma".
 include "ground/lib/stream.ma".
 
 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-.
 
 #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.
 
 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
 #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-.
 
 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
 #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-.
 
 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-.

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl.ma
index b29772d320fca59ef849ff2a0ff4bf28c713ac31..4a3640baed498488974f0c6e34ec370343c8d807 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl.ma
@@ -14,26 +14,30 @@
 
 include "ground/notation/functions/downspoon_2.ma".
 include "ground/lib/stream_eq.ma".
 
 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.
 
 // qed.
 

-lemma tl_rew (A) (a) (t): t = tl A (a⨮t).
+lemma stream_tl_cons (A) (a) (t):
+      t = ⫰{A}(a⨮t).

 // qed.
 
 // 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.
 #A * //
 qed.

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma
index 051c58cca7db7011de8029d30c38b376ebb2e4c7..9f34ba81d06f5b1a723571a005b11f2be8f22654 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma
@@ -14,28 +14,41 @@
 
 include "ground/notation/functions/downspoonstar_3.ma".
 include "ground/lib/stream_hdtl.ma".
 
 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.
 
 // 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.
 
 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.
 qed.

diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
index e79511f7cf2eda76b9f7847f87e0042157150f04..ca692ea2f2b5fbb643e9501330816989fcce70d2 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
@@ -57,9 +57,9 @@ table {
         }
       ]
       [ { "non-negative integers with infinity" * } {
         }
       ]
       [ { "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 ( ↑? )" * ]
           [ "ynat_plus ( ?+? )" * ]
           [ "ynat_pred ( ↓? )" "ynat_pred_succ" * ]
           [ "ynat_succ ( ↑? )" * ]


@@ -88,8 +88,8 @@ table {
   [ { "extensions to the library" * } {
       [ { "" * } {
           [ "stream ( ? ⨮{?} ? )" "stream_eq ( ? ≗{?} ? )" "stream_hdtl ( ⫰{?}? )" "stream_tls ( ⫰*{?}[?]? )" * ]
   [ { "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" * ]
         }
           [ "ltc" "ltc_ctc" * ]
           [ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "exteq ( ? ≐{?,?} ? )" "star" "lstar_2a" * ]
         }