-
-(* ******** 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-.