]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/turing/while_machine.ma
- cprs and cnx on the way
[helm.git] / matita / matita / lib / turing / while_machine.ma
1 (*
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.           
5     ||I||                                                            
6     ||T||  
7     ||A||  
8     \   /  This file is distributed under the terms of the       
9      \ /   GNU General Public License Version 2   
10       V_____________________________________________________________*)
11
12 include "basics/star.ma".
13 include "turing/mono.ma".
14
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. *)
18
19 definition while_trans ≝ λsig. λM : TM sig. λq:states sig M. λp.
20   let 〈s,a〉 ≝ p in
21   if s == q then 〈start ? M, None ?,N〉
22   else trans ? M p.
23   
24 definition whileTM ≝ λsig. λM : TM sig. λqacc: states ? M.
25   mk_TM sig 
26     (states ? M)
27     (while_trans sig M qacc)
28     (start sig M)
29     (λs.halt sig M s ∧ ¬ s==qacc).
30
31 lemma while_trans_false : ∀sig,M,q,p.
32   \fst p ≠ q → trans sig (whileTM sig M q) p = trans sig M p.
33 #sig #M #q * #q1 #a #Hq normalize >(\bf Hq) normalize //
34 qed.
35
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)) →
40   subh c2 = false →
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 //
53    ]
54  ]
55 qed.
56
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 
60 #a #b * #c * /2/ 
61 qed.
62
63 lemma halt_while_acc : 
64   ∀sig,M,acc.halt sig (whileTM sig M acc) acc = false.
65 #sig #M #acc normalize >(\b ?) // cases (halt sig M acc) %
66 qed.
67
68 lemma halt_while_not_acc : 
69   ∀sig,M,acc,s.s == acc = false → halt sig (whileTM sig M acc) s = halt sig M s.
70 #sig #M #acc #s #neqs normalize >neqs cases (halt sig M s) %
71 qed.
72
73 lemma step_while_acc :
74  ∀sig,M,acc,c.cstate ?? c = acc → 
75    step sig (whileTM sig M acc) c = initc … (ctape ?? c).
76 #sig #M #acc * #s #t #Hs normalize >(\b Hs) %
77 qed.
78
79 theorem sem_while: ∀sig,M,acc,Rtrue,Rfalse.
80   halt sig M acc = true →
81   M ⊨ [acc: Rtrue,Rfalse] → 
82     whileTM sig M acc ⊫ (star ? Rtrue) ∘ Rfalse.
83 #sig #M #acc #Rtrue #Rfalse #Hacctrue #HaccR #t #i
84 generalize in match t;
85 @(nat_elim1 … i) #m #Hind #intape #outc #Hloop
86 cases (loop_split ?? (λc. halt sig M (cstate ?? c)) ????? Hloop)
87   [#k1 * #outc1 * #Hloop1 #Hloop2
88    cases (HaccR intape) #k * #outcM * * #HloopM #HMtrue #HMfalse
89    cut (outcM = outc1)
90    [ @(loop_eq … k … Hloop1) 
91      @(loop_lift ?? k (λc.c) ? 
92                 (step ? (whileTM ? M acc)) ? 
93                 (λc.halt sig M (cstate ?? c)) ?? 
94                 ?? HloopM)
95      [ #x %
96      | * #s #t #Hx whd in ⊢ (??%%); >while_trans_false
97        [%
98        |% #Hfalse <Hfalse in Hacctrue; >Hx #H0 destruct ]
99      ]
100   | #HoutcM1 cases (true_or_false (cstate ?? outc1 == acc)) #Hacc
101       [@tech1 @(ex_intro … (ctape ?? outc1)) %
102         [ <HoutcM1 @HMtrue >HoutcM1 @(\P Hacc)
103         |@(Hind (m-k1)) 
104           [ cases m in Hloop;
105             [normalize #H destruct (H) ]
106              #m' #_ cases k1 in Hloop1;
107              [normalize #H destruct (H) ]
108              #k1' #_ normalize /2/
109            | <Hloop2 whd in ⊢ (???%);
110              >(\P Hacc) >halt_while_acc whd in ⊢ (???%);
111              normalize in match (halt ?? acc);
112              >step_while_acc // @(\P Hacc)
113            ]
114          ]
115       |@(ex_intro … intape) % //
116        cut (Some ? outc1 = Some ? outc)
117        [ <Hloop1 <Hloop2 >loop_p_true in ⊢ (???%); //
118          normalize >(loop_Some ?????? Hloop1) >Hacc %
119        | #Houtc1c destruct @HMfalse @(\Pf Hacc)
120        ]
121      ]
122    ]
123  | * #s0 #t0 normalize cases (s0 == acc) normalize
124    [ cases (halt sig M s0) normalize #Hfalse destruct
125    | cases (halt sig M s0) normalize //
126    ]
127  ]
128 qed.
129
130 theorem terminate_while: ∀sig,M,acc,Rtrue,Rfalse,t.
131   halt sig M acc = true →
132   M ⊨ [acc: Rtrue,Rfalse] → 
133   WF ? (inv … Rtrue) t → whileTM sig M acc ↓ t.
134 #sig #M #acc #Rtrue #Rfalse #t #Hacctrue #HM #HWF elim HWF
135 #t1 #H #Hind cases (HM … t1) #i * #outc * * #Hloop
136 #Htrue #Hfalse cases (true_or_false (cstate … outc == acc)) #Hcase
137   [cases (Hind ? (Htrue … (\P Hcase))) #iwhile * #outcfinal
138    #Hloopwhile @(ex_intro … (i+iwhile)) 
139    @(ex_intro … outcfinal) @(loop_merge … outc … Hloopwhile)
140     [@(λc.halt sig M (cstate … c))
141     |* #s0 #t0 normalize cases (s0 == acc) normalize
142      [ cases (halt sig M s0) // 
143      | cases (halt sig M s0) normalize //
144      ]
145     |@(loop_lift ?? i (λc.c) ? 
146                 (step ? (whileTM ? M acc)) ? 
147                 (λc.halt sig M (cstate ?? c)) ?? 
148                 ?? Hloop)
149      [ #x %
150      | * #s #t #Hx whd in ⊢ (??%%); >while_trans_false
151        [%
152        |% #Hfalse <Hfalse in Hacctrue; >Hx #H0 destruct ]
153      ]
154    |@step_while_acc @(\P Hcase)
155    |>(\P Hcase) @halt_while_acc
156    ]
157  |@(ex_intro … i) @(ex_intro … outc)
158   @(loop_lift_acc ?? i (λc.c) ?????? (λc.cstate ?? c == acc) ???? Hloop)
159    [#x #Hx >(\P Hx) //
160    |#x @halt_while_not_acc
161    |#x #H whd in ⊢ (??%%); >while_trans_false [%]
162     % #eqx >eqx in H; >Hacctrue #H destruct
163    |@Hcase
164    ]
165  ]
166 qed.
167
168 theorem terminate_while_guarded: ∀sig,M,acc,Pre,Rtrue,Rfalse.
169   halt sig M acc = true →
170   accGRealize sig M acc Pre Rtrue Rfalse → 
171   (∀t1,t2. Pre t1 → Rtrue t1 t2 → Pre t2) → ∀t.
172   WF ? (inv … Rtrue) t → Pre t → whileTM sig M acc ↓ t.
173 #sig #M #acc #Pre #Rtrue #Rfalse #Hacctrue #HM #Hinv #t #HWF elim HWF
174 #t1 #H #Hind #HPre cases (HM … t1 HPre) #i * #outc * * #Hloop
175 #Htrue #Hfalse cases (true_or_false (cstate … outc == acc)) #Hcase
176   [cases (Hind ? (Htrue … (\P Hcase)) ?) 
177     [2: @(Hinv … HPre) @Htrue @(\P Hcase)]
178    #iwhile * #outcfinal
179    #Hloopwhile @(ex_intro … (i+iwhile)) 
180    @(ex_intro … outcfinal) @(loop_merge … outc … Hloopwhile)
181     [@(λc.halt sig M (cstate … c))
182     |* #s0 #t0 normalize cases (s0 == acc) normalize
183      [ cases (halt sig M s0) // 
184      | cases (halt sig M s0) normalize //
185      ]
186     |@(loop_lift ?? i (λc.c) ? 
187                 (step ? (whileTM ? M acc)) ? 
188                 (λc.halt sig M (cstate ?? c)) ?? 
189                 ?? Hloop)
190      [ #x %
191      | * #s #t #Hx whd in ⊢ (??%%); >while_trans_false
192        [%
193        |% #Hfalse <Hfalse in Hacctrue; >Hx #H0 destruct ]
194      ]
195    |@step_while_acc @(\P Hcase)
196    |>(\P Hcase) @halt_while_acc
197    ]
198  |@(ex_intro … i) @(ex_intro … outc)
199   @(loop_lift_acc ?? i (λc.c) ?????? (λc.cstate ?? c == acc) ???? Hloop)
200    [#x #Hx >(\P Hx) //
201    |#x @halt_while_not_acc
202    |#x #H whd in ⊢ (??%%); >while_trans_false [%]
203     % #eqx >eqx in H; >Hacctrue #H destruct
204    |@Hcase
205    ]
206  ]
207 qed.
208