From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 20 May 2022 20:43:51 +0000 (+0200)
Subject: update in ground
X-Git-Tag: make_still_working~70
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ef07f57f5fb5bc34897fdef44987e6a154206807;hp=77479649510792efe4d9cbff508e118360862594;p=helm.git

update in ground

+ additions to lifts
---

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list.ma b/matita/matita/contribs/lambdadelta/ground/lib/list.ma
index 6dc752d65..a486fd39a 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/list.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list.ma
@@ -35,3 +35,12 @@ rec definition list_all A (R:predicate A) (l:list A) on l ≝ match l with
 [ list_empty       ⇒ ⊤
 | list_lcons hd tl ⇒ ∧∧ R hd & list_all A R tl
 ].
+
+(* Basic inversions *********************************************************)
+
+lemma eq_inv_list_lcons_bi (A) (a1) (a2) (l1) (l2):
+      a1⨮l1 = a2⨮{A}l2 →
+      ∧∧ a1 = a2 & l1 = l2.
+#A #a1 #a2 #l1 #l2 #H0 destruct
+/2 width=1 by conj/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma
index 042497aac..e4c3d743e 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma
@@ -68,6 +68,15 @@ lemma eq_inv_list_empty_append (A):
 ]
 qed-.
 
+lemma eq_inv_list_append_empty (A):
+      ∀l1,l2. l1⨁{A}l2 = ⓔ →
+      ∧∧ l1 = ⓔ & l2 = ⓔ.
+#A *
+[ #l2 /2 width=1 by conj/
+| #a1 #l1 #l2 <list_append_lcons_sn #H destruct
+]
+qed-.
+
 (* Advanced inversions ******************************************************)
 
 lemma eq_inv_list_append_dx_sn_refl (A) (l1) (l2):
diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
index 00faad83d..bfbc0e986 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
@@ -51,6 +51,12 @@ lemma eq_inv_list_empty_rcons (A):
 elim (eq_inv_list_empty_append … H0) -H0 #_ #H0 destruct
 qed-.
 
+lemma eq_inv_list_rcons_empty (A):
+      ∀l,a. l⨭{A}a = ⓔ → ⊥.
+#A #l #a #H0
+elim (eq_inv_list_append_empty … H0) -H0 #_ #H0 destruct
+qed-.
+
 (* Advanced inversions ******************************************************)
 
 lemma eq_inv_list_rcons_bi (A):
diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_tl.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_tl.ma
new file mode 100644
index 000000000..0e9b887e5
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list_tl.ma
@@ -0,0 +1,36 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "ground/notation/functions/downharpoonright_2.ma".
+include "ground/lib/list.ma".
+
+(* TAIL FOR LISTS ***********************************************************)
+
+definition list_tl (A:Type[0]): list A → list A.
+#A * [ @(ⓔ) | #_ #t @t ]
+defined.
+
+interpretation
+  "tail (streams)"
+  'DownHarpoonRight A t = (list_tl A t).
+
+(* Basic constructions ******************************************************)
+
+lemma list_tl_empty (A):
+      ⓔ = ⇂{A}ⓔ.
+// qed.
+
+lemma list_tl_lcons (A) (a) (t):
+      t = ⇂{A}(a⨮t).
+// qed.