X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Flib%2Flist_rcons.ma;h=7d67f5526371571af90a41756b2254bd005a6382;hb=61bc42e04598a9f5e489c3867af72e700c7fda04;hp=66910e1a90fd775370bb047504a0a521f0108422;hpb=160b7f7385763d872b5f2632696d02fd540c4eae;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
index 66910e1a9..7d67f5526 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 *****************************************************)
 
@@ -39,13 +40,59 @@ lemma list_append_rcons_sn (A):
 // qed.
 
 lemma list_append_rcons_dx (A):
-      ∀l1,l2,a. l1 ⨁ l2 ⨭ a = l1 ⨁{A} (l2 ⨭ a).
+      ∀l1,l2,a. (l1 ⨁ l2) ⨭ a = l1 ⨁{A} (l2 ⨭ a).
 // qed.
 
 (* Basic inversions *********************************************************)
 
 lemma eq_inv_list_empty_rcons (A):
       ∀l,a. ⓔ = l⨭{A}a → ⊥.
-#A #l #a #H
-elim (eq_inv_list_empty_append … H) -H #_ #H destruct
+#A #l #a #H0
+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):
+      ∀a1,a2,l1,l2. l1 ⨭{A} a1 = l2 ⨭ a2 →
+      ∧∧ l1 = l2 & a1 = a2.
+#A #a1 #a2 #l1 elim l1 -l1 [| #b1 #l1 #IH ] *
+[ <list_append_empty_sn <list_append_empty_sn #H destruct
+  /2 width=1 by conj/
+| #b2 #l2 <list_append_empty_sn <list_append_lcons_sn #H destruct -H
+  elim (eq_inv_list_empty_rcons ??? e0)
+| <list_append_lcons_sn <list_append_empty_sn #H destruct -H
+  elim (eq_inv_list_empty_rcons ??? (sym_eq … e0))
+| #b2 #l2 <list_append_lcons_sn <list_append_lcons_sn #H destruct -H
+  elim (IH … e0) -IH -e0 #H1 #H2 destruct
+  /2 width=1 by conj/
+]
+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-.
+
+(* Advanced inversions with list_append *************************************)
+
+lemma eq_inv_list_append_dx_dx_refl (A) (l1) (l2):
+      l1 = l2⨁{A}l1 → ⓔ = l2.
+#A #l1 @(list_ind_rcons … l1) -l1 [ // ]
+#l1 #a1 #IH #l2 <list_append_rcons_dx #H0
+elim (eq_inv_list_rcons_bi ????? H0) -H0 #H0 #_
+/2 width=1 by/
 qed-.