X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fbackground%2Fpreamble.ma;h=769ffa5a366838ff9dd5660e3440d72f1a540cdd;hb=225887a9f23aac79d4cca907da026917b7df04dc;hp=dc5c144674ce67595764be5899978e7f9cd3d4d9;hpb=5c792a695677f2857e1984ababc9998d42fc8033;p=helm.git

diff --git a/matita/matita/contribs/lambda/background/preamble.ma b/matita/matita/contribs/lambda/background/preamble.ma
index dc5c14467..769ffa5a3 100644
--- a/matita/matita/contribs/lambda/background/preamble.ma
+++ b/matita/matita/contribs/lambda/background/preamble.ma
@@ -18,15 +18,20 @@ include "arithmetics/exp.ma".
 
 include "background/xoa_notation.ma".
 include "background/xoa.ma".
+include "background/notation.ma".
 
 (* logic *)
 
 (* Note: For some reason this cannot be in the standard library *) 
 interpretation "logical false" 'false = False.
 
-notation "⊥"
-  non associative with precedence 90
-  for @{'false}.
+(* booleans *)
+
+(* Note: For some reason this cannot be in the standard library *) 
+interpretation "boolean false" 'false = false.
+
+(* Note: For some reason this cannot be in the standard library *) 
+interpretation "boolean true" 'true = true.
 
 (* arithmetics *)
 
@@ -82,6 +87,10 @@ notation > "◊"
   non associative with precedence 90
   for @{'nil}.
 
+lemma list_inv: ∀A. ∀l:list A. ◊ = l ∨ ∃∃a0,l0. a0 :: l0 = l.
+#A * /2 width=1/ /3 width=3/
+qed-.
+
 definition map_cons: ∀A. A → list (list A) → list (list A) ≝ λA,a.
                      map … (cons … a).
 
@@ -91,13 +100,30 @@ notation "hvbox(a ::: break l)"
   right associative with precedence 47
   for @{'ho_cons $a $l}.
 
+lemma map_cons_inv_nil: ∀A,a,l1. map_cons A a l1 = ◊ → ◊ = l1.
+#A #a * // normalize #a1 #l1 #H destruct
+qed-.
+
+lemma map_cons_inv_cons: ∀A,a,a2,l2,l1. map_cons A a l1 = a2::l2 →
+                         ∃∃a1,l. a::a1 = a2 & a:::l = l2 & a1::l = l1.
+#A #a #a2 #l2 * normalize
+[ #H destruct
+| #a1 #l1 #H destruct /2 width=5/
+]
+qed-.
+
+lemma map_cons_append: ∀A,a,l1,l2. map_cons A a (l1@l2) =
+                       map_cons A a l1 @ map_cons A a l2.
+#A #a #l1 elim l1 -l1 // normalize /2 width=1/
+qed.
+
 (* lstar *)
 
 (* Note: this cannot be in lib because of the missing xoa quantifier *)
 lemma lstar_inv_pos: ∀A,B,R,l,b1,b2. lstar A B R l b1 b2 → 0 < |l| →
                      ∃∃a,ll,b. a::ll = l & R a b1 b & lstar A B R ll b b2.
 #A #B #R #l #b1 #b2 #H @(lstar_ind_l ????????? H) -b1
-[ #H elim (lt_refl_false … H) 
+[ #H elim (lt_refl_false … H)
 | #a #ll #b1 #b #Hb1 #Hb2 #_ #_ /2 width=6/ (**) (* auto fail if we do not remove the inductive premise *)
 ]
 qed-.