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/star.ma".
13 include "turing/turing.ma".
15 (* The following machine implements a while-loop over a body machine $M$.
16 We just need to extend $M$ adding a single transition leading back from a
17 distinguished final state $q$ to the initial state. *)
19 definition while_trans ≝ λsig,n. λM: mTM sig n. λq:states sig n M. λp.
21 if s == q then 〈start ?? M, null_action ??〉
24 definition whileTM ≝ λsig,n. λM: mTM sig n. λqacc: states ?? M.
27 (while_trans sig n M qacc)
29 (λs.halt sig n M s ∧ ¬ s==qacc).
31 lemma while_trans_false : ∀sig,n,M,q,p.
32 \fst p ≠ q → trans sig n (whileTM sig n M q) p = trans sig n M p.
33 #sig #n #M #q * #q1 #a #Hq normalize >(\bf Hq) normalize //
36 lemma loop_lift_acc : ∀A,B,k,lift,f,g,h,hlift,c1,c2,subh.
37 (∀x.subh x = true → h x = true) →
38 (∀x.subh x = false → hlift (lift x) = h x) →
39 (∀x.h x = false → lift (f x) = g (lift x)) →
41 loop A k f h c1 = Some ? c2 →
42 loop B k g hlift (lift c1) = Some ? (lift … c2).
43 #A #B #k #lift #f #g #h #hlift #c1 #c2 #subh #Hsubh #Hlift #Hfg #Hc2
44 generalize in match c1; elim k
45 [#c0 normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
46 |#k0 #IH #c0 whd in ⊢ (??%? → ??%?);
47 cases (true_or_false (h c0)) #Hc0 >Hc0
48 [ normalize #Heq destruct (Heq) >(Hlift … Hc2) >Hc0 //
49 | normalize >(Hlift c0)
50 [>Hc0 normalize <(Hfg … Hc0) @IH
51 |cases (true_or_false (subh c0)) //
52 #H <Hc0 @sym_eq >H @Hsubh //
57 lemma tech1: ∀A.∀R1,R2:relation A.
58 ∀a,b. (R1 ∘ ((star ? R1) ∘ R2)) a b → ((star ? R1) ∘ R2) a b.
59 #A #R1 #R2 #a #b #H lapply (sub_assoc_l ?????? H) @sub_comp_l -a -b
63 lemma halt_while_acc :
64 ∀sig,n,M,acc.halt sig n (whileTM sig n M acc) acc = false.
65 #sig #n #M #acc normalize >(\b ?) // cases (halt sig n M acc) %
68 lemma halt_while_not_acc :
69 ∀sig,n,M,acc,s.s == acc = false →
70 halt sig n (whileTM sig n M acc) s = halt sig n M s.
71 #sig #n #M #acc #s #neqs normalize >neqs cases (halt sig n M s) %
74 lemma step_while_acc :
75 ∀sig,n,M,acc,c.cstate ??? c = acc →
76 step sig n (whileTM sig n M acc) c = initc … (ctapes ??? c).
77 #sig #n #M #acc * #s #t #Hs whd in match (step ????);
78 whd in match (trans ????); >(\b Hs)
79 <(tape_move_null_action ?? t) in ⊢ (???%); //
82 theorem sem_while: ∀sig,n,M,acc,Rtrue,Rfalse.
83 halt sig n M acc = true →
84 M ⊨ [acc: Rtrue,Rfalse] →
85 whileTM sig n M acc ⊫ (star ? Rtrue) ∘ Rfalse.
86 #sig #n #M #acc #Rtrue #Rfalse #Hacctrue #HaccR #t #i
87 generalize in match t;
88 @(nat_elim1 … i) #m #Hind #intape #outc #Hloop
89 cases (loop_split ?? (λc. halt sig n M (cstate ??? c)) ????? Hloop)
90 [#k1 * #outc1 * #Hloop1 #Hloop2
91 cases (HaccR intape) #k * #outcM * * #HloopM #HMtrue #HMfalse
93 [ @(loop_eq … k … Hloop1)
94 @(loop_lift ?? k (λc.c) ?
95 (step ?? (whileTM ?? M acc)) ?
96 (λc.halt sig n M (cstate ??? c)) ??
99 | * #s #t #Hx whd in ⊢ (??%%); >while_trans_false
101 |% #Hfalse <Hfalse in Hacctrue; >Hx #H0 destruct ]
103 | #HoutcM1 cases (true_or_false (cstate ??? outc1 == acc)) #Hacc
104 [@tech1 @(ex_intro … (ctapes ??? outc1)) %
105 [ <HoutcM1 @HMtrue >HoutcM1 @(\P Hacc)
108 [normalize #H destruct (H) ]
109 #m' #_ cases k1 in Hloop1;
110 [normalize #H destruct (H) ]
111 #k1' #_ normalize /2/
112 | <Hloop2 whd in ⊢ (???%);
113 >(\P Hacc) >halt_while_acc whd in ⊢ (???%);
114 normalize in match (halt ??? acc);
115 >step_while_acc // @(\P Hacc)
118 |@(ex_intro … intape) % //
119 cut (Some ? outc1 = Some ? outc)
120 [ <Hloop1 <Hloop2 >loop_p_true in ⊢ (???%); //
121 normalize >(loop_Some ?????? Hloop1) >Hacc %
122 | #Houtc1c destruct @HMfalse @(\Pf Hacc)
126 | * #s0 #t0 normalize cases (s0 == acc) normalize
127 [ cases (halt sig n M s0) normalize #Hfalse destruct
128 | cases (halt sig n M s0) normalize //
133 theorem terminate_while: ∀sig,n,M,acc,Rtrue,Rfalse,t.
134 halt sig n M acc = true →
135 M ⊨ [acc: Rtrue,Rfalse] →
136 WF ? (inv … Rtrue) t → whileTM sig n M acc ↓ t.
137 #sig #n #M #acc #Rtrue #Rfalse #t #Hacctrue #HM #HWF elim HWF
138 #t1 #H #Hind cases (HM … t1) #i * #outc * * #Hloop
139 #Htrue #Hfalse cases (true_or_false (cstate … outc == acc)) #Hcase
140 [cases (Hind ? (Htrue … (\P Hcase))) #iwhile * #outcfinal
141 #Hloopwhile @(ex_intro … (i+iwhile))
142 @(ex_intro … outcfinal) @(loop_merge … outc … Hloopwhile)
143 [@(λc.halt sig n M (cstate … c))
144 |* #s0 #t0 normalize cases (s0 == acc) normalize
145 [ cases (halt sig n M s0) //
146 | cases (halt sig n M s0) normalize //
148 |@(loop_lift ?? i (λc.c) ?
149 (step ?? (whileTM ?? M acc)) ?
150 (λc.halt sig n M (cstate ??? c)) ??
153 | * #s #t #Hx whd in ⊢ (??%%); >while_trans_false
155 |% #Hfalse <Hfalse in Hacctrue; >Hx #H0 destruct ]
157 |@step_while_acc @(\P Hcase)
158 |>(\P Hcase) @halt_while_acc
160 |@(ex_intro … i) @(ex_intro … outc)
161 @(loop_lift_acc ?? i (λc.c) ?????? (λc.cstate ??? c == acc) ???? Hloop)
163 |#x @halt_while_not_acc
164 |#x #H whd in ⊢ (??%%); >while_trans_false [%]
165 % #eqx >eqx in H; >Hacctrue #H destruct
171 theorem terminate_while_guarded: ∀sig,n,M,acc,Pre,Rtrue,Rfalse.
172 halt sig n M acc = true →
173 accGRealize sig n M acc Pre Rtrue Rfalse →
174 (∀t1,t2. Pre t1 → Rtrue t1 t2 → Pre t2) → ∀t.
175 WF ? (inv … Rtrue) t → Pre t → whileTM sig n M acc ↓ t.
176 #sig #n #M #acc #Pre #Rtrue #Rfalse #Hacctrue #HM #Hinv #t #HWF elim HWF
177 #t1 #H #Hind #HPre cases (HM … t1 HPre) #i * #outc * * #Hloop
178 #Htrue #Hfalse cases (true_or_false (cstate … outc == acc)) #Hcase
179 [cases (Hind ? (Htrue … (\P Hcase)) ?)
180 [2: @(Hinv … HPre) @Htrue @(\P Hcase)]
182 #Hloopwhile @(ex_intro … (i+iwhile))
183 @(ex_intro … outcfinal) @(loop_merge … outc … Hloopwhile)
184 [@(λc.halt sig n M (cstate … c))
185 |* #s0 #t0 normalize cases (s0 == acc) normalize
186 [ cases (halt sig n M s0) //
187 | cases (halt sig n M s0) normalize //
189 |@(loop_lift ?? i (λc.c) ?
190 (step ?? (whileTM ?? M acc)) ?
191 (λc.halt sig n M (cstate ??? c)) ??
194 | * #s #t #Hx whd in ⊢ (??%%); >while_trans_false
196 |% #Hfalse <Hfalse in Hacctrue; >Hx #H0 destruct ]
198 |@step_while_acc @(\P Hcase)
199 |>(\P Hcase) @halt_while_acc
201 |@(ex_intro … i) @(ex_intro … outc)
202 @(loop_lift_acc ?? i (λc.c) ?????? (λc.cstate ??? c == acc) ???? Hloop)
204 |#x @halt_while_not_acc
205 |#x #H whd in ⊢ (??%%); >while_trans_false [%]
206 % #eqx >eqx in H; >Hacctrue #H destruct