]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/turing/multi_universal/moves.ma
unistep_aux
[helm.git] / matita / matita / lib / turing / multi_universal / moves.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 "turing/turing.ma".
13 include "turing/inject.ma".
14 include "turing/while_multi.ma".
15
16 definition parmove_states ≝ initN 3.
17
18 definition parmove0 : parmove_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
19 definition parmove1 : parmove_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
20 definition parmove2 : parmove_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
21
22 (*
23
24 src: a b c ... z # ---→ a b c ... z #
25      ^                              ^
26
27 dst: _ _ _ ... _ d ---→ a b c ... z d
28      ^                              ^
29
30 0) (x ≠ sep,_) → (x,x)(R,R) → 1
31    (sep,d) → None 2
32 1) (_,_) → None 1
33 2) (_,_) → None 2
34
35 *)
36
37 definition trans_parmove_step ≝ 
38  λsrc,dst,sig,n,D,is_sep.
39  λp:parmove_states × (Vector (option sig) (S n)).
40  let 〈q,a〉 ≝ p in
41  match pi1 … q with
42  [ O ⇒ match nth src ? a (None ?) with
43    [ None ⇒ 〈parmove2,null_action ? n〉
44    | Some a0 ⇒ 
45      if is_sep a0 then 〈parmove2,null_action ? n〉
46      else match nth dst ? a (None ?) with
47      [ None ⇒ 〈parmove2,null_action ? n〉
48      | Some a1 ⇒ 〈parmove1,change_vec ? (S n)
49                           (change_vec ?(S n)
50                            (null_action ? n) (〈None sig,D〉) src)
51                           (〈None ?,D〉) dst〉 ] ]
52  | S q ⇒ match q with 
53    [ O ⇒ (* 1 *) 〈parmove1,null_action ? n〉
54    | S _ ⇒ (* 2 *) 〈parmove2,null_action ? n〉 ] ].
55
56 definition parmove_step ≝ 
57   λsrc,dst,sig,n,D,is_sep.
58   mk_mTM sig n parmove_states (trans_parmove_step src dst sig n D is_sep) 
59     parmove0 (λq.q == parmove1 ∨ q == parmove2).
60
61 definition R_parmove_step_true ≝ 
62   λsrc,dst,sig,n,D,is_sep.λint,outt: Vector (tape sig) (S n).
63   ∃x1,x2.
64    current ? (nth src ? int (niltape ?)) = Some ? x1 ∧
65    current ? (nth dst ? int (niltape ?)) = Some ? x2 ∧
66    is_sep x1 = false ∧
67    outt = change_vec ?? 
68             (change_vec ?? int
69               (tape_move_mono ? (nth src ? int (niltape ?)) (〈None ?,D〉)) src)
70             (tape_move_mono ? (nth dst ? int (niltape ?)) (〈None ?,D〉)) dst.
71
72 definition R_parmove_step_false ≝ 
73   λsrc,dst:nat.λsig,n,is_sep.λint,outt: Vector (tape sig) (S n).
74   ((∃x1.
75    current ? (nth src ? int (niltape ?)) = Some ? x1 ∧
76    is_sep x1 = true) ∨
77    current ? (nth src ? int (niltape ?)) = None ?  ∨
78    current ? (nth dst ? int (niltape ?)) = None ?) ∧
79    outt = int.
80
81 lemma parmove_q0_q2_null_src :
82   ∀src,dst,sig,n,D,is_sep,v.src < S n → dst < S n → 
83   nth src ? (current_chars ?? v) (None ?) = None ? → 
84   step sig n (parmove_step src dst sig n D is_sep)
85     (mk_mconfig ??? parmove0 v) =
86     mk_mconfig ??? parmove2 v.
87 #src #dst #sig #n #D #is_sep #v #Hsrc #Hdst #Hcurrent
88 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?);
89 @eq_f2
90 [ whd in ⊢ (??(???%)?); >Hcurrent %
91 | whd in ⊢ (??(????(???%))?); >Hcurrent @tape_move_null_action ]
92 qed.
93
94 lemma parmove_q0_q2_sep :
95   ∀src,dst,sig,n,D,is_sep,v,s.src < S n → dst < S n → 
96   nth src ? (current_chars ?? v) (None ?) = Some ? s → is_sep s = true → 
97   step sig n (parmove_step src dst sig n D is_sep)
98     (mk_mconfig ??? parmove0 v) =
99     mk_mconfig ??? parmove2 v.
100 #src #dst #sig #n #D #is_sep #v #s #Hsrc #Hdst #Hcurrent #Hsep
101 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?);
102 @eq_f2
103 [ whd in ⊢ (??(???%)?); >Hcurrent whd in ⊢ (??(???%)?); >Hsep %
104 | whd in ⊢ (??(????(???%))?); >Hcurrent
105   whd in ⊢ (??(????(???%))?); >Hsep @tape_move_null_action ]
106 qed.
107
108 lemma parmove_q0_q2_null_dst :
109   ∀src,dst,sig,n,D,is_sep,v,s.src < S n → dst < S n → 
110   nth src ? (current_chars ?? v) (None ?) = Some ? s → is_sep s = false → 
111   nth dst ? (current_chars ?? v) (None ?) = None ? → 
112   step sig n (parmove_step src dst sig n D is_sep)
113     (mk_mconfig ??? parmove0 v) =
114     mk_mconfig ??? parmove2 v.
115 #src #dst #sig #n #D #is_sep #v #s #Hsrc #Hdst #Hcursrc #Hsep #Hcurdst
116 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?);
117 @eq_f2
118 [ whd in ⊢ (??(???%)?); >Hcursrc whd in ⊢ (??(???%)?); >Hsep >Hcurdst %
119 | whd in ⊢ (??(????(???%))?); >Hcursrc
120   whd in ⊢ (??(????(???%))?); >Hsep >Hcurdst @tape_move_null_action ]
121 qed.
122
123 lemma parmove_q0_q1 :
124   ∀src,dst,sig,n,D,is_sep,v.src ≠ dst → src < S n → dst < S n → 
125   ∀a1,a2.
126   nth src ? (current_chars ?? v) (None ?) = Some ? a1 →
127   nth dst ? (current_chars ?? v) (None ?) = Some ? a2 → 
128   is_sep a1 = false → 
129   step sig n (parmove_step src dst sig n D is_sep)
130     (mk_mconfig ??? parmove0 v) =
131     mk_mconfig ??? parmove1 
132      (change_vec ? (S n) 
133        (change_vec ?? v
134          (tape_move_mono ? (nth src ? v (niltape ?)) (〈None ?, D〉)) src)
135        (tape_move_mono ? (nth dst ? v (niltape ?)) (〈None ?, D〉)) dst).
136 #src #dst #sig #n #D #is_sep #v #Hneq #Hsrc #Hdst
137 #a1 #a2 #Hcursrc #Hcurdst #Hsep
138 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2
139 [ whd in match (trans ????);
140   >Hcursrc >Hcurdst whd in ⊢ (??(???%)?); >Hsep //
141 | whd in match (trans ????);
142   >Hcursrc >Hcurdst whd in ⊢ (??(????(???%))?); >Hsep whd in ⊢ (??(????(???%))?);
143   <(change_vec_same ?? v dst (niltape ?)) in ⊢ (??%?);
144   >tape_move_multi_def >pmap_change
145   <(change_vec_same ?? v src (niltape ?)) in ⊢ (??%?);
146   >pmap_change <tape_move_multi_def >tape_move_null_action
147   @eq_f2 // @eq_f2 // >nth_change_vec_neq //
148 ]
149 qed.
150
151 lemma sem_parmove_step :
152   ∀src,dst,sig,n,D,is_sep.src ≠ dst → src < S n → dst < S n → 
153   parmove_step src dst sig n D is_sep ⊨ 
154     [ parmove1: R_parmove_step_true src dst sig n D is_sep, 
155              R_parmove_step_false src dst sig n is_sep ].
156 #src #dst #sig #n #D #is_sep #Hneq #Hsrc #Hdst #int
157 lapply (refl ? (current ? (nth src ? int (niltape ?))))
158 cases (current ? (nth src ? int (niltape ?))) in ⊢ (???%→?);
159 [ #Hcursrc %{2} %
160   [| % [ %
161     [ whd in ⊢ (??%?); >parmove_q0_q2_null_src /2/
162     | normalize in ⊢ (%→?); #H destruct (H) ]
163     | #_ % // % %2 // ] ]
164 | #a #Ha cases (true_or_false (is_sep a)) #Hsep
165   [ %{2} %
166     [| % [ %
167       [ whd in ⊢ (??%?); >(parmove_q0_q2_sep … Hsep) /2/
168       | normalize in ⊢ (%→?); #H destruct (H) ]
169       | #_ % // % % %{a} % // ] ]
170   | lapply (refl ? (current ? (nth dst ? int (niltape ?))))
171     cases (current ? (nth dst ? int (niltape ?))) in ⊢ (???%→?);
172     [ #Hcurdst %{2} %
173       [| % [ %
174         [ whd in ⊢ (??%?); >(parmove_q0_q2_null_dst … Hsep) /2/ 
175         | normalize in ⊢ (%→?); #H destruct (H) ]
176         | #_ % // %2 // ] ]
177     | #b #Hb %{2} %
178       [| % [ % 
179         [whd in ⊢  (??%?);  >(parmove_q0_q1 … Hneq Hsrc Hdst ? b ?? Hsep) //
180         | #_ %{a} %{b} % // % // % // ]
181         | * #H @False_ind @H % ]
182 ]]]]
183 qed.
184
185 definition parmove ≝ λsrc,dst,sig,n,D,is_sep.
186   whileTM … (parmove_step src dst sig n D is_sep) parmove1.
187
188 definition R_parmoveL ≝ 
189   λsrc,dst,sig,n,is_sep.λint,outt: Vector (tape sig) (S n).
190   (∀ls,x,xs,rs,sep.
191     nth src ? int (niltape ?) = midtape sig (xs@sep::ls) x rs →
192     (∀c.memb ? c (x::xs) = true → is_sep c = false) → is_sep sep = true → 
193     ∀ls0,x0,target,c,rs0.|xs| = |target| → 
194     nth dst ? int (niltape ?) = midtape sig (target@c::ls0) x0 rs0 → 
195     outt = change_vec ?? 
196            (change_vec ?? int (midtape sig ls sep (reverse ? xs@x::rs)) src)
197            (midtape sig ls0 c (reverse ? target@x0::rs0)) dst) ∧
198   (((∃s.current ? (nth src ? int (niltape ?)) = Some ? s ∧ is_sep s = true) ∨  
199      current ? (nth src ? int (niltape ?)) = None ? ∨
200      current ? (nth dst ? int (niltape ?)) = None ?) →
201      outt = int).
202   
203 lemma wsem_parmoveL : ∀src,dst,sig,n,is_sep.src ≠ dst → src < S n → dst < S n → 
204   parmove src dst sig n L is_sep ⊫ R_parmoveL src dst sig n is_sep.
205 #src #dst #sig #n #is_sep #Hneq #Hsrc #Hdst #ta #k #outc #Hloop
206 lapply (sem_while … (sem_parmove_step src dst sig n L is_sep Hneq Hsrc Hdst) … Hloop) //
207 -Hloop * #tb * #Hstar @(star_ind_l ??????? Hstar) -Hstar
208 [ whd in ⊢ (%→?); * #H #Houtc % [2: #_ @Houtc ] cases H
209   [ * [ * #x * #Hx #Hsep #ls #x0 #xs #rs #sep #Hsrctc #Hnosep >Hsrctc in Hx; normalize in ⊢ (%→?);
210     #Hx0 destruct (Hx0) lapply (Hnosep ? (memb_hd …)) >Hsep
211     #Hfalse destruct (Hfalse)
212   | #Hcur_src #ls #x0 #xs #rs #sep #Hsrctc >Hsrctc in Hcur_src;
213     normalize in ⊢ (%→?); #H destruct (H)]
214   |#Hcur_dst  #ls #x0 #xs #rs #sep #Hsrctc #Hnosep #Hsep #ls0 #x1 #target 
215    #c #rs0 #Hlen #Hdsttc >Hdsttc in Hcur_dst; normalize in ⊢ (%→?); #H destruct (H)
216   ]  
217 | #td #te * #c0 * #c1 * * * #Hc0 #Hc1 #Hc0nosep #Hd #Hstar #IH #He 
218   lapply (IH He) -IH * #IH1 #IH2 %
219   [ #ls #x #xs #rs #sep #Hsrc_tc #Hnosep #Hsep #ls0 #x0 #target
220     #c #rs0 #Hlen #Hdst_tc
221    >Hsrc_tc in Hc0; normalize in ⊢ (%→?); #Hc0 destruct (Hc0)
222    >Hdst_tc in Hd; >Hsrc_tc @(list_cases2 … Hlen)
223     [ #Hxsnil #Htargetnil >Hxsnil >Htargetnil #Hd >IH2 
224       [2: %1 %1 %{sep} % // >Hd >nth_change_vec_neq [|@(sym_not_eq … Hneq)]
225       >nth_change_vec //]  
226       >Hd -Hd @(eq_vec … (niltape ?))
227       #i #Hi cases (decidable_eq_nat i src) #Hisrc
228       [ >Hisrc >(nth_change_vec_neq … src dst) [|@(sym_not_eq … Hneq)]
229         >nth_change_vec //
230       | cases (decidable_eq_nat i dst) #Hidst
231         [ >Hidst >nth_change_vec // 
232         | >nth_change_vec_neq [|@(sym_not_eq … Hidst)]
233           >nth_change_vec_neq [|@(sym_not_eq … Hisrc)] % 
234         ]
235       ]
236     | #hd1 #hd2 #tl1 #tl2 #Hxs #Htarget >Hxs >Htarget #Hd
237       >(IH1 ls hd1 tl1 (c0::rs) sep ?? Hsep ls0 hd2 tl2 c (x0::rs0))
238       [ >Hd >(change_vec_commute … ?? td ?? src dst) //
239        >change_vec_change_vec
240        >(change_vec_commute … ?? td ?? dst src) [|@sym_not_eq //]
241        >change_vec_change_vec
242        >reverse_cons >associative_append
243        >reverse_cons >associative_append % 
244      | >Hd >nth_change_vec //
245      | >Hxs in Hlen; >Htarget normalize #Hlen destruct (Hlen) //
246      | <Hxs #c1 #Hc1 @Hnosep @memb_cons //
247      | >Hd >nth_change_vec_neq [|@sym_not_eq //]
248        >nth_change_vec // ]
249    ]
250  | >Hc0 >Hc1 * [* [ * #c * #Hc destruct (Hc) >Hc0nosep]] #Habs destruct (Habs)
251  ] ]
252 qed.
253  
254 lemma terminate_parmoveL :  ∀src,dst,sig,n,is_sep,t.
255   src ≠ dst → src < S n → dst < S n → 
256   parmove src dst sig n L is_sep ↓ t.
257 #src #dst #sig #n #is_sep #t #Hneq #Hsrc #Hdst
258 @(terminate_while … (sem_parmove_step …)) //
259 <(change_vec_same … t src (niltape ?))
260 cases (nth src (tape sig) t (niltape ?))
261 [ % #t1 * #x1 * #x2 * * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct 
262 |2,3: #a0 #al0 % #t1 * #x1 * #x2 * * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
263 | #ls lapply t -t elim ls
264   [#t #c #rs % #t1 * #x1 * #x2 * * * >nth_change_vec // normalize in ⊢ (%→?);
265    #H1 destruct (H1) #Hcurdst #Hxsep >change_vec_change_vec #Ht1 % 
266    #t2 * #y1 * #y2 * * * >Ht1 >nth_change_vec_neq [|@sym_not_eq //]
267    >nth_change_vec // normalize in ⊢ (%→?); #H destruct (H)
268   |#l0 #ls0 #IH #t #c #rs % #t1 * #x1 * #x2 * * * >nth_change_vec //
269    normalize in ⊢ (%→?); #H destruct (H) #Hcurdst #Hxsep
270    >change_vec_change_vec >change_vec_commute // #Ht1 >Ht1 @IH
271   ]
272 ]
273 qed.
274
275 lemma sem_parmoveL : ∀src,dst,sig,n,is_sep.
276   src ≠ dst → src < S n → dst < S n → 
277   parmove src dst sig n L is_sep ⊨ R_parmoveL src dst sig n is_sep.
278 #src #dst #sig #n #is_sep #Hneq #Hsrc #Hdst @WRealize_to_Realize 
279 [/2/ | @wsem_parmoveL //]
280 qed.