From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 20 Jan 2022 19:42:34 +0000 (+0100)
Subject: update in ground
X-Git-Tag: make_still_working~107
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=513a56a5990201abcf038e7242779e2d73621c86;p=helm.git

update in ground

+ advanced eliminators on lists
---

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma
index 05fefceb3..316449566 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma
@@ -67,3 +67,14 @@ lemma eq_inv_list_empty_append (A):
 | #a1 #l1 #l2 <list_append_lcons_sn #H destruct
 ]
 qed-.
+
+(* Advanced eliminations ****************************************************)
+
+lemma list_ind_append_dx (A) (Q:predicate …):
+      Q (ⓔ{A}) →
+      (∀l1,l2. Q l1 -> Q (l1⨁l2)) →
+      ∀l. Q l.
+#A #Q #IH1 #IH2 * //
+#a #l >(list_append_empty_sn … (a⨮l))
+/2 width=1 by/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
index 66910e1a9..9d2fcfaac 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
@@ -14,6 +14,7 @@
 
 include "ground/notation/functions/oplusleft_3.ma".
 include "ground/lib/list_append.ma".
+include "ground/generated/pull_2.ma". 
 
 (* RIGHT CONS FOR LISTS *****************************************************)
 
@@ -49,3 +50,15 @@ lemma eq_inv_list_empty_rcons (A):
 #A #l #a #H
 elim (eq_inv_list_empty_append … H) -H #_ #H destruct
 qed-.
+
+(* Advanced eliminations ****************************************************)
+
+lemma list_ind_rcons (A) (Q:predicate …):
+      Q (ⓔ{A}) →
+      (∀l,a. Q l -> Q (l⨭a)) →
+      ∀l. Q l.
+#A #Q #IH1 #IH2 #l
+@(list_ind_append_dx … l) -l //
+@pull_2 #l2 elim l2 -l2 //
+#a2 #l2 #IH0 #l1 #IH /3 width=1 by/
+qed-.