]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/turing/universal/universal.ma
match termination completed, still a small case ignored in wsem_match
[helm.git] / matita / matita / lib / turing / universal / universal.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
13 include "turing/universal/uni_step.ma".
14
15 (* definition zero : ∀n.initN n ≝ λn.mk_Sig ?? 0 (le_O_n n). *)
16
17 definition low_config: ∀M:normalTM.nconfig (no_states M) → tape STape ≝ 
18 λM:normalTM.λc.
19   let n ≝ no_states M in
20   let h ≝ nhalt M in
21   let t ≝ntrans M in 
22   let q ≝ cstate … c in
23   let q_low ≝  m_bits_of_state n h q in 
24   let current_low ≝ match current … (ctape … c) with [ None ⇒ null | Some b ⇒ bit b] in
25   let low_left ≝ map … (λb.〈bit b,false〉) (left … (ctape …c)) in
26   let low_right ≝ map … (λb.〈bit b,false〉) (right … (ctape …c)) in
27   let table ≝ flatten ? (tuples_list n h (graph_enum ?? t)) in
28   let right ≝ q_low@〈current_low,false〉::〈grid,false〉::table@〈grid,false〉::low_right in
29   mk_tape STape (〈grid,false〉::low_left) (option_hd … right) (tail … right).
30   
31 lemma low_config_eq: ∀t,M,c. t = low_config M c → 
32   ∃low_left,low_right,table,q_low_hd,q_low_tl,c_low.
33   low_left = map … (λb.〈bit b,false〉) (left … (ctape …c)) ∧
34   low_right = map … (λb.〈bit b,false〉) (right … (ctape …c)) ∧
35   table = flatten ? (tuples_list (no_states M) (nhalt M) (graph_enum ?? (ntrans M))) ∧
36   〈q_low_hd,false〉::q_low_tl = m_bits_of_state (no_states M) (nhalt M) (cstate … c) ∧
37   c_low =  match current … (ctape … c) with [ None ⇒ null| Some b ⇒ bit b] ∧
38   t = midtape STape (〈grid,false〉::low_left) 〈q_low_hd,false〉 (q_low_tl@〈c_low,false〉::〈grid,false〉::table@〈grid,false〉::low_right).
39 #t #M #c #eqt
40   @(ex_intro … (map … (λb.〈bit b,false〉) (left … (ctape …c))))
41   @(ex_intro … (map … (λb.〈bit b,false〉) (right … (ctape …c))))
42   @(ex_intro … (flatten ? (tuples_list (no_states M) (nhalt M) (graph_enum ?? (ntrans M)))))
43   @(ex_intro … (\fst (hd ? (m_bits_of_state (no_states M) (nhalt M) (cstate … c)) 〈bit true,false〉)))
44   @(ex_intro … (tail ? (m_bits_of_state (no_states M) (nhalt M) (cstate … c))))
45   @(ex_intro … (match current … (ctape … c) with [ None ⇒ null| Some b ⇒ bit b]))
46 % [% [% [% [% // | // ] | // ] | // ] | >eqt //]
47 qed.
48
49 let rec to_bool_list (l: list (unialpha×bool)) ≝ 
50   match l with
51   [ nil ⇒ nil ?
52   | cons a tl ⇒ 
53     match \fst a with 
54     [bit b ⇒ b::to_bool_list tl
55     |_ ⇒ nil ?
56     ]
57   ].
58
59 definition high_c ≝ λc:unialpha×bool.
60   match \fst c with
61   [ null ⇒ None ?
62   | bit b ⇒ Some ? b 
63   | _ ⇒ None ?].
64
65 definition high_tape ≝ λls,c,rs.
66   mk_tape FinBool (to_bool_list ls) (high_c c) (to_bool_list rs).
67
68 lemma high_tape_eq : ∀ls,c,rs. high_tape ls c rs =
69   mk_tape FinBool (to_bool_list ls) (high_c c) (to_bool_list rs).
70 // qed.
71
72 definition high_tape_from_tape ≝ λt:tape STape.
73   match t with
74   [niltape ⇒ niltape ?
75   |leftof a l ⇒ match \fst a with 
76      [bit b ⇒ leftof ? b (to_bool_list l)
77      |_ ⇒ niltape ?
78      ]
79   |rightof a r ⇒ match \fst a with 
80      [bit b ⇒ rightof ? b (to_bool_list r)
81      |_ ⇒ niltape ?
82      ]
83   |midtape l c r ⇒ high_tape l c r
84   ].
85
86 lemma high_tape_of_lift : ∀ls,c,rs. legal_tape ls c rs →
87   high_tape ls c rs =
88     high_tape_from_tape (lift_tape ls c rs).
89 #ls * #c #b #rs * #H cases c // 
90 >high_tape_eq  
91 * [ * [#H @False_ind /2/
92       | #Heq >Heq cases rs // * #a #b1 #tl 
93         whd in match (lift_tape ???); cases a // 
94       ]
95   |#Heq >Heq cases ls // * #a #b1 #tl 
96         whd in match (lift_tape ???); cases a //
97   ]
98 qed.
99
100 lemma bool_embedding: ∀l.
101   to_bool_list (map ?? (λb.〈bit b,false〉) l) = l.
102 #l elim l // #a #tl #Hind normalize @eq_f @Hind
103 qed.
104
105 lemma current_embedding: ∀c.
106   high_c (〈match c with [None ⇒ null | Some b ⇒ bit b],false〉) = c.
107   * normalize // qed.
108
109 lemma tape_embedding: ∀ls,c,rs.
110  high_tape 
111    (map ?? (λb.〈bit b,false〉) ls) 
112    (〈match c with [None ⇒ null | Some b ⇒ bit b],false〉)
113    (map ?? (λb.〈bit b,false〉) rs) = mk_tape ? ls c rs.
114 #ls #c #rs >high_tape_eq >bool_embedding >bool_embedding
115 >current_embedding %
116 qed.
117
118 definition high_move ≝ λc,mv.
119   match c with 
120   [ bit b ⇒ Some ? 〈b,move_of_unialpha mv〉
121   | _ ⇒ None ?
122   ].
123
124 definition map_move ≝ 
125   λc,mv.match c with [ null ⇒ None ? | _ ⇒ Some ? 〈c,false,move_of_unialpha mv〉 ].
126
127 definition low_step_R_true ≝ λt1,t2.
128   ∀M:normalTM.
129   ∀c: nconfig (no_states M). 
130     t1 = low_config M c →
131     halt ? M (cstate … c) = false ∧
132       t2 = low_config M (step ? M c).
133
134 definition low_tape_aux : ∀M:normalTM.tape FinBool → tape STape ≝ 
135 λM:normalTM.λt.
136   let current_low ≝ match current … t with 
137     [ None ⇒ None ? | Some b ⇒ Some ? 〈bit b,false〉] in
138   let low_left ≝ map … (λb.〈bit b,false〉) (left … t) in
139   let low_right ≝ map … (λb.〈bit b,false〉) (right … t) in
140   mk_tape STape low_left current_low low_right. 
141
142 lemma left_of_low_tape: ∀M,t. 
143   left ? (low_tape_aux M t) = map … (λb.〈bit b,false〉) (left … t).
144 #M * //
145 qed. 
146
147 lemma right_of_low_tape: ∀M,t. 
148   right ? (low_tape_aux M t) = map … (λb.〈bit b,false〉) (right … t).
149 #M * //
150 qed. 
151
152 definition low_move ≝ λaction:option (bool × move).
153   match action with
154   [None ⇒ None ?
155   |Some act ⇒ Some ? (〈〈bit (\fst act),false〉,\snd act〉)].
156
157 (* simulation lemma *)
158 lemma low_tape_move : ∀M,action,t.
159   tape_move STape (low_tape_aux M t) (low_move action) =
160   low_tape_aux M (tape_move FinBool t action). 
161 #M * // (* None *)
162 * #b #mv #t cases mv cases t //
163   [#ls #c #rs cases ls //|#ls #c #rs cases rs //]
164 qed.
165
166 lemma left_of_lift: ∀ls,c,rs. left ? (lift_tape ls c rs) = ls.
167 #ls * #c #b #rs cases c // cases ls // cases rs //
168 qed.
169
170 lemma right_of_lift: ∀ls,c,rs. legal_tape ls c rs →
171   right ? (lift_tape ls c rs) = rs.
172 #ls * #c #b #rs * #_ cases c // cases ls cases rs // #a #tll #b #tlr
173 #H @False_ind cases H [* [#H1 /2/ |#H1 destruct] |#H1 destruct]
174 qed.
175
176
177 lemma current_of_lift: ∀ls,c,b,rs. legal_tape ls 〈c,b〉 rs →
178   current STape (lift_tape ls 〈c,b〉 rs) =
179     match c with [null ⇒ None ? | _ ⇒ Some ? 〈c,b〉].
180 #ls #c #b #rs cases c // whd in ⊢ (%→?); * #_ 
181 * [* [#Hnull @False_ind /2/ | #Hls >Hls whd in ⊢ (??%%); cases rs //]
182   |#Hrs >Hrs whd in ⊢ (??%%); cases ls //]
183 qed.
184
185 lemma current_of_lift_None: ∀ls,c,b,rs. legal_tape ls 〈c,b〉 rs →
186   current STape (lift_tape ls 〈c,b〉 rs) = None ? →
187     c = null.
188 #ls #c #b #rs #Hlegal >(current_of_lift … Hlegal) cases c normalize  
189   [#b #H destruct |// |3,4,5:#H destruct ]
190 qed.
191
192 lemma current_of_lift_Some: ∀ls,c,c1,rs. legal_tape ls c rs →
193   current STape (lift_tape ls c rs) = Some ? c1 →
194     c = c1.
195 #ls * #c #cb #b #rs #Hlegal >(current_of_lift … Hlegal) cases c normalize 
196  [#b1 #H destruct // |#H destruct |3,4,5:#H destruct //]
197 qed.
198
199 lemma current_of_low_None: ∀M,t. current FinBool t = None ? → 
200   current STape (low_tape_aux M t) = None ?.
201 #M #t cases t // #l #b #r whd in ⊢ ((??%?)→?); #H destruct
202 qed.
203   
204 lemma current_of_low_Some: ∀M,t,b. current FinBool t = Some ? b → 
205   current STape (low_tape_aux M t) = Some ? 〈bit b,false〉.
206 #M #t cases t 
207   [#b whd in ⊢ ((??%?)→?); #H destruct
208   |#b #l #b1 whd in ⊢ ((??%?)→?); #H destruct
209   |#b #l #b1 whd in ⊢ ((??%?)→?); #H destruct
210   |#c #c1 #l #r whd in ⊢ ((??%?)→?); #H destruct %
211   ]
212 qed.
213
214 lemma current_of_low:∀M,tape,ls,c,rs. legal_tape ls c rs → 
215   lift_tape ls c rs = low_tape_aux M tape →
216   c = 〈match current … tape  with 
217        [ None ⇒ null | Some b ⇒ bit b], false〉.
218 #M #tape #ls * #c #cb #rs #Hlegal #Hlift  
219 cut (current ? (lift_tape ls 〈c,cb〉 rs) = current ? (low_tape_aux M tape))
220   [@eq_f @Hlift] -Hlift #Hlift
221 cut (current … tape = None ? ∨ ∃b.current … tape = Some ? b)
222   [cases (current … tape) [%1 // | #b1 %2 /2/ ]] *  
223   [#Hcurrent >Hcurrent normalize
224    >(current_of_low_None …Hcurrent) in Hlift; #Hlift 
225    >(current_of_lift_None … Hlegal Hlift) 
226    @eq_f cases Hlegal * * #Hmarks #_ #_ #_ @(Hmarks 〈c,cb〉) @memb_hd
227   |* #b #Hcurrent >Hcurrent normalize
228    >(current_of_low_Some …Hcurrent) in Hlift; #Hlift 
229    @(current_of_lift_Some … Hlegal Hlift) 
230   ]
231 qed.
232
233 (*
234 lemma current_of_low:∀M,tape,ls,c,rs. legal_tape ls c rs → 
235   lift_tape ls c rs = low_tape_aux M tape →
236   c = 〈match current … tape  with 
237        [ None ⇒ null | Some b ⇒ bit b], false〉.
238 #M #tape #ls * #c #cb #rs * * #_ #H cases (orb_true_l … H)
239   [cases c [2,3,4,5: whd in ⊢ ((??%?)→?); #Hfalse destruct]
240    #b #_ #_ cases tape 
241     [whd in ⊢ ((??%%)→?); #H destruct
242     |#a #l whd in ⊢ ((??%%)→?); #H destruct 
243     |#a #l whd in ⊢ ((??%%)→?); #H destruct 
244     |#a #l #r whd in ⊢ ((??%%)→?); #H destruct //
245     ]
246   |cases c 
247     [#b whd in ⊢ ((??%?)→?); #Hfalse destruct
248     |3,4,5:whd in ⊢ ((??%?)→?); #Hfalse destruct]
249    #_ * [* [#Habs @False_ind /2/
250            |#Hls >Hls whd in ⊢ ((??%%)→?); *)
251           
252     
253 (* sufficent conditions to have a low_level_config *)
254 lemma is_low_config: ∀ls,c,rs,M,s,tape,qhd,q_tl,table.
255 legal_tape ls c rs →
256 table = flatten ? (tuples_list (no_states M) (nhalt M) (graph_enum ?? (ntrans M))) →
257 lift_tape ls c rs = low_tape_aux M tape →
258 〈qhd,false〉::q_tl = m_bits_of_state (no_states M) (nhalt M) s →
259 midtape STape (〈grid,false〉::ls) 
260   〈qhd,false〉 
261   (q_tl@c::〈grid,false〉::table@〈grid,false〉::rs) = 
262   low_config M (mk_config ?? s tape).
263 #ls #c #rs #M #s #tape #qhd #q_tl #table #Hlegal #Htable
264 #Hlift #Hstate whd in match (low_config ??); <Hstate 
265 @eq_f3 
266   [@eq_f <(left_of_lift ls c rs) >Hlift //
267   | cut (∀A.∀a,b:A.∀l1,l2. a::l1 = b::l2 → a=b)
268     [#A #a #b #l1 #l2 #H destruct (H) %] #Hcut
269    @(Hcut …Hstate)
270   |@eq_f <(current_of_low … Hlegal Hlift) @eq_f @eq_f <Htable @eq_f @eq_f
271    <(right_of_lift ls c rs Hlegal) >Hlift @right_of_low_tape
272   ]
273 qed.
274
275 lemma unistep_true_to_low_step: ∀t1,t2.
276   R_uni_step_true t1 t2 → low_step_R_true t1 t2.
277 #t1 #t2 (* whd in ⊢ (%→%); *) #Huni_step * #n #posn #t #h * #qin #tape #eqt1
278 cases (low_config_eq … eqt1) 
279 #low_left * #low_right * #table * #q_low_hd * #q_low_tl * #current_low
280 ***** #Hlow_left #Hlow_right #Htable #Hq_low #Hcurrent_low #Ht1
281 letin trg ≝ (t 〈qin,current ? tape〉)
282 letin qout_low ≝ (m_bits_of_state n h (\fst trg))
283 letin qout_low_hd ≝ (hd ? qout_low 〈bit true,false〉)
284 letin qout_low_tl ≝ (tail ? qout_low)
285 letin low_act ≝ (low_action (\snd (t 〈qin,current ? tape〉)))
286 letin low_cout ≝ (\fst low_act)
287 letin low_m ≝ (\snd low_act)
288 lapply (Huni_step n table q_low_hd (\fst qout_low_hd) 
289        current_low low_cout low_left low_right q_low_tl qout_low_tl low_m … Ht1) 
290   [@daemon
291   |>Htable
292    @(trans_to_match n h t 〈qin,current ? tape〉 … (refl …))
293    >Hq_low  >Hcurrent_low whd in match (mk_tuple ?????);
294    >(eq_pair_fst_snd … (t …)) whd in ⊢ (??%?);
295    >(eq_pair_fst_snd … (low_action …)) %
296   |//
297   |@daemon
298   ]
299 -Ht1 #Huni_step lapply (Huni_step ? (refl …)) -Huni_step *
300 #q_low_head_false * #ls1 * #rs1 * #c2 * * 
301 #Ht2 #Hlift #Hlegal %
302   [whd in ⊢ (??%?); >q_low_head_false in Hq_low; 
303    whd in ⊢ ((???%)→?); generalize in match (h qin);
304    #x #H destruct (H) %
305   |>Ht2 whd in match (step FinBool ??); 
306    whd in match (trans ???); 
307    >(eq_pair_fst_snd … (t ?))
308    @is_low_config // >Hlift
309    <low_tape_move @eq_f2
310     [>Hlow_left >Hlow_right >Hcurrent_low whd in ⊢ (??%%); 
311      cases (current …tape) [%] #b whd in ⊢ (??%%); %
312     |whd in match low_cout; whd in match low_m; whd in match low_act; 
313      generalize in match (\snd (t ?)); * [%] * #b #mv
314      whd in  ⊢ (??(?(???%)?)%); cases mv % 
315     ]
316   ]
317 qed.
318
319 definition low_step_R_false ≝ λt1,t2.
320   ∀M:normalTM.
321   ∀c: nconfig (no_states M).  
322     t1 = low_config M c → halt ? M (cstate … c) = true  ∧ t1 = t2.
323
324 lemma unistep_false_to_low_step: ∀t1,t2.
325   R_uni_step_false t1 t2 → low_step_R_false t1 t2.
326 #t1 #t2 (* whd in ⊢ (%→%); *) #Huni_step * #n #posn #t #h * #qin #tape #eqt1
327 cases (low_config_eq … eqt1) #low_left * #low_right * #table * #q_low_hd * #q_low_tl * #current_low
328 ***** #_ #_ #_ #Hqin #_ #Ht1 whd in match (halt ???);
329 cases (Huni_step (h qin) ?) [/2/] >Ht1 whd in ⊢ (??%?); @eq_f
330 normalize in Hqin; destruct (Hqin) %
331 qed.
332
333 definition low_R ≝ λM,qstart,R,t1,t2.
334     ∀tape1. t1 = low_config M (mk_config ?? qstart tape1) → 
335     ∃q,tape2.R tape1 tape2 ∧
336     halt ? M q = true ∧ t2 = low_config M (mk_config ?? q tape2).
337
338 lemma sem_uni_step1: 
339   uni_step ⊨ [us_acc: low_step_R_true, low_step_R_false].
340 @daemon (* this no longer works: TODO *) (*
341 @(acc_Realize_to_acc_Realize … sem_uni_step) 
342   [@unistep_true_to_low_step | @unistep_false_to_low_step ]
343 *)
344 qed. 
345
346 definition universalTM ≝ whileTM ? uni_step us_acc.
347
348 theorem sem_universal: ∀M:normalTM. ∀qstart.
349   universalTM ⊫ (low_R M qstart (R_TM FinBool M qstart)).
350 @daemon (* this no longer works: TODO *) (*
351 #M #q #intape #i #outc #Hloop
352 lapply (sem_while … sem_uni_step1 intape i outc Hloop)
353   [@daemon] -Hloop 
354 * #ta * #Hstar generalize in match q; -q 
355 @(star_ind_l ??????? Hstar)
356   [#tb #q0 whd in ⊢ (%→?); #Htb #tape1 #Htb1
357    cases (Htb … Htb1) -Htb #Hhalt #Htb
358    <Htb >Htb1 @ex_intro 
359    [|%{tape1} %
360      [ % 
361        [ whd @(ex_intro … 1) @(ex_intro … (mk_config … q0 tape1))
362         % [|%] whd in ⊢ (??%?); >Hhalt % 
363        | @Hhalt ]
364      | % ]
365    ]
366   |#tb #tc #td whd in ⊢ (%→?); #Htc #Hstar1 #IH 
367    #q #Htd #tape1 #Htb 
368    lapply (IH (\fst (trans ? M 〈q,current ? tape1〉)) Htd) -IH 
369    #IH cases (Htc … Htb); -Htc #Hhaltq 
370    whd in match (step FinBool ??); >(eq_pair_fst_snd ?? (trans ???)) 
371    #Htc change with (mk_config ????) in Htc:(???(??%)); 
372    cases (IH ? Htc) #q1 * #tape2 * * #HRTM #Hhaltq1 #Houtc
373    @(ex_intro … q1) @(ex_intro … tape2) % 
374     [%
375       [cases HRTM #k * #outc1 * #Hloop #Houtc1
376        @(ex_intro … (S k)) @(ex_intro … outc1) % 
377         [>loopM_unfold >loop_S_false [2://] whd in match (step FinBool ??); 
378          >(eq_pair_fst_snd ?? (trans ???)) @Hloop
379         |@Houtc1
380         ]
381       |@Hhaltq1]
382     |@Houtc
383     ]
384   ]
385 *)  
386 qed.
387
388 theorem sem_universal2: ∀M:normalTM. ∀R.
389   M ⊫ R → universalTM ⊫ (low_R M (start ? M) R).
390 #M #R #HMR lapply (sem_universal … M (start ? M)) @WRealize_to_WRealize
391 #t1 #t2 whd in ⊢ (%→%); #H #tape1 #Htape1 cases (H ? Htape1)
392 #q * #tape2 * * #HRTM #Hhalt #Ht2 @(ex_intro … q) @(ex_intro … tape2)
393 % [% [@(R_TM_to_R … HRTM) @HMR | //] | //]
394 qed.
395  
396 axiom terminate_UTM: ∀M:normalTM.∀t. 
397   M ↓ t → universalTM ↓ (low_config M (mk_config ?? (start ? M) t)).
398