X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fpreamble.ma;h=c7c736f2ce1d3cad45775d2568fa537914ca2691;hb=f14ac9cceaaa7f1905f0dbc4548d24c4abe940e3;hp=eb0f409a5d1f2f59090750bf179e05051053977f;hpb=984f552a6b54e8b870d6e32df8325345d0f1ea5b;p=helm.git

diff --git a/matita/matita/contribs/lambda/preamble.ma b/matita/matita/contribs/lambda/preamble.ma
index eb0f409a5..c7c736f2c 100644
--- a/matita/matita/contribs/lambda/preamble.ma
+++ b/matita/matita/contribs/lambda/preamble.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basics/star.ma".
-include "basics/lists/list.ma".
+include "basics/lists/lstar.ma".
 include "arithmetics/exp.ma".
 
 include "xoa_notation.ma".
@@ -28,25 +28,6 @@ notation "⊥"
   non associative with precedence 90
   for @{'false}.
 
-lemma ex2_1_commute: ∀A0. ∀P0,P1:A0→Prop. (∃∃x0. P0 x0 & P1 x0) → ∃∃x0. P1 x0 & P0 x0.
-#A0 #P0 #P1 * /2 width=3/
-qed.
-
-(* relations *)
-
-definition confluent1: ∀A. relation A → predicate A ≝ λA,R,a0.
-                       ∀a1. R a0 a1 → ∀a2. R a0 a2 →
-                       ∃∃a. R a1 a & R a2 a. 
-
-(* Note: confluent1 would be redundant if \Pi-reduction where enabled *)                       
-definition confluent: ∀A. predicate (relation A) ≝ λA,R.
-                      ∀a0. confluent1 … R a0.
-
-(* booleans *)
-
-definition is_false: predicate bool ≝ λb.
-                     false = b.
-
 (* arithmetics *)
 
 lemma lt_refl_false: ∀n. n < n → ⊥.
@@ -101,8 +82,22 @@ notation > "◊"
   non associative with precedence 90
   for @{'nil}.
 
-let rec Allr (A:Type[0]) (R:relation A) (l:list A) on l : Prop ≝
-match l with
-[ nil       ⇒ True
-| cons a1 l ⇒ match l with [ nil ⇒ True | cons a2 _ ⇒ R a1 a2 ∧ Allr A R l ]
-].
+definition map_cons: ∀A. A → list (list A) → list (list A) ≝ λA,a.
+                     map … (cons … a).
+
+interpretation "map_cons" 'ho_cons a l = (map_cons ? a l).
+
+notation "hvbox(a ::: break l)"
+  right associative with precedence 47
+  for @{'ho_cons $a $l}.
+
+(* 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) 
+| #a #ll #b1 #b #Hb1 #Hb2 #_ #_ /2 width=6/ (**) (* auto fail if we do not remove the inductive premise *)
+]
+qed-.