From 513a56a5990201abcf038e7242779e2d73621c86 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 20 Jan 2022 20:42:34 +0100 Subject: [PATCH] update in ground + advanced eliminators on lists --- .../contribs/lambdadelta/ground/lib/list_append.ma | 11 +++++++++++ .../contribs/lambdadelta/ground/lib/list_rcons.ma | 13 +++++++++++++ 2 files changed, 24 insertions(+) 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 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-. -- 2.39.2