2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
8 \ / This file is distributed under the terms of the
9 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "basics/lists/list.ma".
14 (* labelled reflexive and transitive closure ********************************)
16 definition ltransitive: ∀A,B:Type[0]. predicate (list A → relation B) ≝ λA,B,R.
17 ∀l1,b1,b. R l1 b1 b → ∀l2,b2. R l2 b b2 → R (l1@l2) b1 b2.
19 inductive lstar (A:Type[0]) (B:Type[0]) (R: A→relation B): list A → relation B ≝
20 | lstar_nil : ∀b. lstar A B R ([]) b b
21 | lstar_cons: ∀a,b1,b. R a b1 b →
22 ∀l,b2. lstar A B R l b b2 → lstar A B R (a::l) b1 b2
25 fact lstar_ind_l_aux: ∀A,B,R,b2. ∀P:relation2 (list A) B.
27 (∀a,l,b1,b. R a b1 b → lstar … R l b b2 → P l b → P (a::l) b1) →
28 ∀l,b1,b. lstar … R l b1 b → b = b2 → P l b1.
29 #A #B #R #b2 #P #H1 #H2 #l #b1 #b #H elim H -b -b1
30 [ #b #H destruct /2 width=1/
31 | #a #b #b0 #Hb0 #l #b1 #Hb01 #IH #H destruct /3 width=4/
35 (* imporeved version of lstar_ind with "left_parameter" *)
36 lemma lstar_ind_l: ∀A,B,R,b2. ∀P:relation2 (list A) B.
38 (∀a,l,b1,b. R a b1 b → lstar … R l b b2 → P l b → P (a::l) b1) →
39 ∀l,b1. lstar … R l b1 b2 → P l b1.
40 #A #B #R #b2 #P #H1 #H2 #l #b1 #Hb12
41 @(lstar_ind_l_aux … H1 H2 … Hb12) //
44 lemma lstar_step: ∀A,B,R,a,b1,b2. R a b1 b2 → lstar A B R ([a]) b1 b2.
48 lemma lstar_inv_nil: ∀A,B,R,l,b1,b2. lstar A B R l b1 b2 → [] = l → b1 = b2.
49 #A #B #R #l #b1 #b2 * -l -b1 -b2 //
50 #a #b1 #b #_ #l #b2 #_ #H destruct
53 lemma lstar_inv_cons: ∀A,B,R,l,b1,b2. lstar A B R l b1 b2 →
55 ∃∃b. R a0 b1 b & lstar A B R l0 b b2.
56 #A #B #R #l #b1 #b2 * -l -b1 -b2
57 [ #b #a0 #l0 #H destruct
58 | #a #b1 #b #Hb1 #l #b2 #Hb2 #a0 #l0 #H destruct /2 width=3/
62 lemma lstar_inv_step: ∀A,B,R,a,b1,b2. lstar A B R ([a]) b1 b2 → R a b1 b2.
63 #A #B #R #a #b1 #b2 #H
64 elim (lstar_inv_cons ?????? H ???) -H [4: // |2,3: skip ] #b #Hb1 #H (**) (* simplify line *)
65 <(lstar_inv_nil ?????? H ?) -H // (**) (* simplify line *)
68 theorem lstar_singlevalued: ∀A,B,R. (∀a. singlevalued ?? (R a)) →
69 ∀l. singlevalued … (lstar A B R l).
70 #A #B #R #HR #l #b #c1 #H @(lstar_ind_l ????????? H) -l -b
71 [ /2 width=5 by lstar_inv_nil/
72 | #a #l #b #b1 #Hb1 #_ #IHbc1 #c2 #H
73 elim (lstar_inv_cons ?????? H ???) -H [4: // |2,3: skip ] #b2 #Hb2 #Hbc2 (**) (* simplify line *)
74 lapply (HR … Hb1 … Hb2) -b #H destruct /2 width=1/
78 theorem lstar_ltransitive: ∀A,B,R. ltransitive … (lstar A B R).
79 #A #B #R #l1 #b1 #b #H @(lstar_ind_l ????????? H) -l1 -b1 normalize // /3 width=3/
82 lemma lstar_app: ∀A,B,R,l,b1,b. lstar A B R l b1 b → ∀a,b2. R a b b2 →
83 lstar A B R (l@[a]) b1 b2.
84 #A #B #R #l #b1 #b #H @(lstar_ind_l ????????? H) -l -b1 /2 width=1/
88 inductive lstar_r (A:Type[0]) (B:Type[0]) (R: A→relation B): list A → relation B ≝
89 | lstar_r_nil: ∀b. lstar_r A B R ([]) b b
90 | lstar_r_app: ∀l,b1,b. lstar_r A B R l b1 b → ∀a,b2. R a b b2 →
91 lstar_r A B R (l@[a]) b1 b2
94 lemma lstar_r_cons: ∀A,B,R,l,b,b2. lstar_r A B R l b b2 → ∀a,b1. R a b1 b →
95 lstar_r A B R (a::l) b1 b2.
96 #A #B #R #l #b #b2 #H elim H -l -b2 /2 width=3/
97 #l #b1 #b #_ #a #b2 #Hb2 #IHb1 #a0 #b0 #Hb01
98 @(lstar_r_app … (a0::l) … Hb2) -b2 /2 width=1/
101 lemma lstar_lstar_r: ∀A,B,R,l,b1,b2. lstar A B R l b1 b2 → lstar_r A B R l b1 b2.
102 #A #B #R #l #b1 #b2 #H @(lstar_ind_l ????????? H) -l -b1 // /2 width=3/
105 lemma lstar_r_inv_lstar: ∀A,B,R,l,b1,b2. lstar_r A B R l b1 b2 → lstar A B R l b1 b2.
106 #A #B #R #l #b1 #b2 #H elim H -l -b1 -b2 // /2 width=3/
109 fact lstar_ind_r_aux: ∀A,B,R,b1. ∀P:relation2 (list A) B.
111 (∀a,l,b,b2. lstar … R l b1 b → R a b b2 → P l b → P (l@[a]) b2) →
112 ∀l,b,b2. lstar … R l b b2 → b = b1 → P l b2.
113 #A #B #R #b1 #P #H1 #H2 #l #b #b2 #H elim (lstar_lstar_r ?????? H) -l -b -b2
115 | #l #b #b0 #Hb0 #a #b2 #Hb02 #IH #H destruct /3 width=4 by lstar_r_inv_lstar/
119 lemma lstar_ind_r: ∀A,B,R,b1. ∀P:relation2 (list A) B.
121 (∀a,l,b,b2. lstar … R l b1 b → R a b b2 → P l b → P (l@[a]) b2) →
122 ∀l,b2. lstar … R l b1 b2 → P l b2.
123 #A #B #R #b1 #P #H1 #H2 #l #b2 #Hb12
124 @(lstar_ind_r_aux … H1 H2 … Hb12) //