- we enabled a notation for ex2

[helm.git] / matita / matita / lib / basics / lists / list.ma

diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma
index 5d000e5c19a81a7e6869da8214d4d65a3d31fc67..a8a01a904bfd98672ea46cce6f5c51cd63fbb122 100644 (file)
--- a/matita/matita/lib/basics/lists/list.ma
+++ b/matita/matita/lib/basics/lists/list.ma
@@ -419,6 +419,12 @@ lemma All_nth : ∀A,P,n,l.
   ]
 ] qed.
 
+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 ]
+].
+
 (**************************** Exists *******************************)
 
 let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
@@ -593,3 +599,50 @@ match n with
 [ O ⇒ [ ]
 | S m ⇒ a::(make_list A a m)
 ].
+
+(* ******** labelled reflexive and transitive closure ************)
+
+inductive lstar (A:Type[0]) (B:Type[0]) (R: A→relation B): list A → relation B ≝
+| lstar_nil : ∀b. lstar A B R ([]) b b
+| lstar_cons: ∀a,b1,b. R a b1 b →
+              ∀l,b2. lstar A B R l b b2 → lstar A B R (a::l) b1 b2
+.
+
+lemma lstar_step: ∀A,B,R,a,b1,b2. R a b1 b2 → lstar A B R ([a]) b1 b2.
+/2 width=3/
+qed.
+
+lemma lstar_inv_nil: ∀A,B,R,l,b1,b2. lstar A B R l b1 b2 → [] = l → b1 = b2.
+#A #B #R #l #b1 #b2 * -l -b1 -b2 //
+#a #b1 #b #_ #l #b2 #_ #H destruct
+qed-.
+
+lemma lstar_inv_cons: ∀A,B,R,l,b1,b2. lstar A B R l b1 b2 →
+                      ∀a0,l0. a0::l0 = l →
+                      ∃∃b. R a0 b1 b & lstar A B R l0 b b2.
+#A #B #R #l #b1 #b2 * -l -b1 -b2
+[ #b #a0 #l0 #H destruct
+| #a #b1 #b #Hb1 #l #b2 #Hb2 #a0 #l0 #H destruct /2 width=3/
+]
+qed-.
+
+lemma lstar_inv_step: ∀A,B,R,a,b1,b2. lstar A B R ([a]) b1 b2 → R a b1 b2.
+#A #B #R #a #b1 #b2 #H
+elim (lstar_inv_cons ?????? H ???) -H [4: // |2,3: skip ] #b #Hb1 #H (**) (* simplify line *)
+<(lstar_inv_nil ?????? H ?) -H // (**) (* simplify line *)
+qed-.
+
+theorem lstar_singlevalued: ∀A,B,R. (∀a. singlevalued ?? (R a)) →
+                            ∀l. singlevalued … (lstar A B R l).
+#A #B #R #HR #l #b #c1 #H elim H -l -b -c1
+[ /2 width=5 by lstar_inv_nil/
+| #a #b #b1 #Hb1 #l #c1 #_ #IHbc1 #c2 #H
+  elim (lstar_inv_cons ?????? H ???) -H [4: // |2,3: skip ] #b2 #Hb2 #Hbc2 (**) (* simplify line *)
+  lapply (HR … Hb1 … Hb2) -b #H destruct /2 width=1/
+]
+qed-.
+
+theorem lstar_trans: ∀A,B,R,l1,b1,b. lstar A B R l1 b1 b →
+                     ∀l2,b2. lstar A B R l2 b b2 → lstar A B R (l1@l2) b1 b2.
+#A #B #R #l1 #b1 #b #H elim H -l1 -b1 -b normalize // /3 width=3/
+qed-.