X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fmulti_to_mono%2Fshift_trace.ma;h=1e5e36e9122050e5588c7c91f744dc1c2776daf5;hb=0e3962b42f821bd7a2b30345a02488958d70fa2f;hp=9ff88de28f7607db10cb60f43547774e70252103;hpb=0a21dcbee5c00208edf949bf511d2d1768833a32;p=helm.git
diff --git a/matita/matita/lib/turing/multi_to_mono/shift_trace.ma b/matita/matita/lib/turing/multi_to_mono/shift_trace.ma
index 9ff88de28..1e5e36e91 100644
--- a/matita/matita/lib/turing/multi_to_mono/shift_trace.ma
+++ b/matita/matita/lib/turing/multi_to_mono/shift_trace.ma
@@ -24,7 +24,7 @@ axiom regular_tail: âsig,n,l,i.
regular_i sig n l i â regular_i sig n (tail ? l) i.
axiom regular_extend: âsig,n,l,i.
- regular_i sig n l i â regular_i sig n (l@[all_blank sig n]) i.
+ regular_i sig n l i â regular_i sig n (l@[all_blanks sig n]) i.
axiom all_blank_after_blank: âsig,n,l1,b,l2,i.
nth i ? (vec ⦠b) (blank ?) = blank ? â
@@ -32,7 +32,7 @@ axiom all_blank_after_blank: âsig,n,l1,b,l2,i.
lemma regular_trace_extl: âsig,n,a,ls,rs,i.
regular_trace sig n a ls rs i â
- regular_trace sig n a (ls@[all_blank sig n]) rs i.
+ regular_trace sig n a (ls@[all_blanks sig n]) rs i.
#sig #n #a #ls #rs #i *
[* #H1 #H2 % % // @(regular_extend ⦠H1)
|* #H1 #H2 %2 % // @(regular_extend ⦠H1)
@@ -41,7 +41,7 @@ qed.
lemma regular_cons_hd_rs: âsig,n.âa:multi_sig sig n.âls,rs1,rs2,i.
regular_trace sig n a ls (rs1@rs2) i â
- regular_trace sig n a ls (rs1@((hd ? rs2 (all_blank â¦))::(tail ? rs2))) i.
+ regular_trace sig n a ls (rs1@((hd ? rs2 (all_blanks â¦))::(tail ? rs2))) i.
#sig #n #a #ls #rs1 #rs2 #i cases rs2 [2: #b #tl #H @H]
*[* #H1 >append_nil #H2 %1 %
[@H1 | whd in match (hd ???); @(regular_extend ⦠rs1) //]
@@ -69,7 +69,7 @@ qed.
improve semantics *)
definition move_to_blank_L â λsig,n,i.
- (move_until ? L (no_blank sig n i)) · extend ? (all_blank sig n).
+ (move_until ? L (not_blank sig n i)) · extend ? (all_blanks sig n).
(*
definition R_move_to_blank_L â λsig,n,i,t1,t2.
@@ -85,7 +85,7 @@ definition R_move_to_blank_L â λsig,n,i,t1,t2.
definition R_move_to_blank_L â λsig,n,i,t1,t2.
(current ? t1 = None ? â
- t2 = midtape (multi_sig sig n) (left ? t1) (all_blank â¦) (right ? t1)) â§
+ t2 = midtape (multi_sig sig n) (left ? t1) (all_blanks â¦) (right ? t1)) â§
âls,a,rs.
t1 = midtape (multi_sig sig n) ls a rs â
regular_i sig n (a::ls) i â
@@ -93,17 +93,17 @@ definition R_move_to_blank_L â λsig,n,i,t1,t2.
(âb,ls1,ls2.
(regular_i sig n (ls1@b::ls2) i) â§
(âj. j â i â regular_trace â¦
- (hd ? (ls1@b::ls2) (all_blank â¦)) (tail ? (ls1@b::ls2)) rs j) â§
- (no_blank sig n i b = false) â§
- (hd (multi_sig sig n) (ls1@[b]) (all_blank â¦) = a) ⧠(* not implied by the next fact *)
- (âj.j â¤n â to_blank_i ?? j (ls1@b::ls2) = to_blank_i ?? j (a::ls)) â§
+ (hd ? (ls1@b::ls2) (all_blanks â¦)) (tail ? (ls1@b::ls2)) rs j) â§
+ (not_blank sig n i b = false) â§
+ (hd (multi_sig sig n) (ls1@[b]) (all_blanks â¦) = a) ⧠(* not implied by the next fact *)
+ (âj.j < n â to_blank_i ?? j (ls1@b::ls2) = to_blank_i ?? j (a::ls)) â§
t2 = midtape ? ls2 b ((reverse ? ls1)@rs)).
theorem sem_move_to_blank_L: âsig,n,i.
move_to_blank_L sig n i ⨠R_move_to_blank_L sig n i.
#sig #n #i
@(sem_seq_app ??????
- (ssem_move_until_L ? (no_blank sig n i)) (sem_extend ? (all_blank sig n)))
+ (ssem_move_until_L ? (not_blank sig n i)) (sem_extend ? (all_blanks sig n)))
#tin #tout * #t1 * * #Ht1a #Ht1b * #Ht2a #Ht2b %
[#Hcur >(Ht1a Hcur) in Ht2a; /2 by /
|#ls #a #rs #Htin #Hreg #Hreg2 -Ht1a cases (Ht1b ⦠Htin)
@@ -122,11 +122,11 @@ theorem sem_move_to_blank_L: âsig,n,i.
]
|* #b * #lss * * #H1 #H2 #Ht1 -Ht1b >Ht1 in Ht2a;
whd in match (left ??); whd in match (right ??); #Hout
- %{(all_blank â¦)} %{(lss@[b])} %{[]}
+ %{(all_blanks â¦)} %{(lss@[b])} %{[]}
%[%[%[%[%[
blank_all_blank //]
+ |whd in match (not_blank ????); >blank_all_blanks //]
|reverse_append >reverse_single @Hout normalize //
@@ -138,9 +138,9 @@ qed.
(******************************************************************************)
definition shift_i_L â λsig,n,i.
- ncombf_r (multi_sig â¦) (shift_i sig n i) (all_blank sig n) ·
+ ncombf_r (multi_sig â¦) (shift_i sig n i) (all_blanks sig n) ·
mti sig n i ·
- extend ? (all_blank sig n).
+ extend ? (all_blanks sig n).
definition R_shift_i_L â λsig,n,i,t1,t2.
(âa,ls,rs.
@@ -155,13 +155,13 @@ definition R_shift_i_L â λsig,n,i,t1,t2.
(âx. mem ? x rs â nth i ? (vec ⦠x) (blank ?) â (blank ?)) â§
shift_l sig n i (a::rs) (rss@[b]) â§
t2 = midtape (multi_sig sig n)
- ((reverse ? (rss@[b]))@ls) (all_blank sig n) [ ]))).
+ ((reverse ? (rss@[b]))@ls) (all_blanks sig n) [ ]))).
definition R_shift_i_L_new â λsig,n,i,t1,t2.
(âa,ls,rs.
t1 = midtape ? ls a rs â
ârs1,b,rs2,rss.
- b = hd ? rs2 (all_blank sig n) â§
+ b = hd ? rs2 (all_blanks sig n) â§
nth i ? (vec ⦠b) (blank ?) = (blank ?) â§
rs = rs1@rs2 â§
(âx. mem ? x rs1 â nth i ? (vec ⦠x) (blank ?) â (blank ?)) â§
@@ -171,12 +171,12 @@ definition R_shift_i_L_new â λsig,n,i,t1,t2.
theorem sem_shift_i_L: âsig,n,i. shift_i_L sig n i ⨠R_shift_i_L sig n i.
#sig #n #i
@(sem_seq_app ??????
- (sem_ncombf_r (multi_sig sig n) (shift_i sig n i)(all_blank sig n))
+ (sem_ncombf_r (multi_sig sig n) (shift_i sig n i)(all_blanks sig n))
(sem_seq ????? (ssem_mti sig n i)
- (sem_extend ? (all_blank sig n))))
+ (sem_extend ? (all_blanks sig n))))
#tin #tout * #t1 * * #Ht1a #Ht1b * #t2 * * #Ht2a #Ht2b * #Htout1 #Htout2
#a #ls #rs cases rs
- [#Htin %2 %{(shift_i sig n i a (all_blank sig n))} %{[ ]}
+ [#Htin %2 %{(shift_i sig n i a (all_blanks sig n))} %{[ ]}
%[%[#x @False_ind | @daemon]
|lapply (Ht1a ⦠Htin) -Ht1a -Ht1b #Ht1
lapply (Ht2a ⦠Ht1) -Ht2a -Ht2b #Ht2 >Ht2 in Htout1;
@@ -200,7 +200,7 @@ theorem sem_shift_i_L: âsig,n,i. shift_i_L sig n i ⨠R_shift_i_L sig n i.
]
|* #b * #rss * * #H1 #H2
#Ht2 %2
- %{(shift_i sig n i b (all_blank sig n))} %{(shift_i sig n i a a1::rss)}
+ %{(shift_i sig n i b (all_blanks sig n))} %{(shift_i sig n i a a1::rss)}
%[%[@H1 |@daemon ]
|>Ht2 in Htout1; #Htout >Htout //
whd in match (left ??); whd in match (right ??);
@@ -221,53 +221,88 @@ theorem sem_shift_i_L_new: âsig,n,i.
%{rs1} %{b} %{(b::rs2)} %{(a1::rss)}
%[%[%[%[%[//|@H2]|@H1]|@H3]|@H4] | whd in match (tail ??); @Ht2]
|* #b * #rss * * #H1 #H2 #Ht2
- %{rs} %{(all_blank sig n)} %{[]} %{(rss@[b])}
- %[%[%[%[%[//|@blank_all_blank]|//]|@H1]|@H2] | whd in match (tail ??); @Ht2]
+ %{rs} %{(all_blanks sig n)} %{[]} %{(rss@[b])}
+ %[%[%[%[%[//|@blank_all_blanks]|//]|@H1]|@H2] | whd in match (tail ??); @Ht2]
]
qed.
(*******************************************************************************
-The following machine implements a full move of for a trace: we reach the left
-border, shift the i-th trace and come back to the head position. *)
+The following machine implements a full move for a trace: we reach the left
+border, shift the i-th trace and come back to the head position.
+The head may hold additional information A, so we suppose that the tape alphabet
+is the disjoint sum between A and the alphabet sig of the multi tape machine. *)
+
+definition TA â λA,sig. FinSum A sig.
+definition MTA â λA,sig,n.multi_sig (TA A sig) n.
+
+definition is_head â λA,sig.λc:sig_ext (TA A sig).
+ match c with
+ [ None â false
+ | Some a â match a with
+ [ inl _ â true
+ | inr _ â false]].
+
+definition is_sig â λA,sig.λc:sig_ext (TA A sig).
+ match c with
+ [ None â false
+ | Some a â match a with
+ [ inl _ â false
+ | inr _ â true]].
+
+definition not_head â λA,sig,n.λc:multi_sig (TA A sig) (S n).
+ ¬(is_head A sig (nth n ? (vec ⦠c) (blank ?))).
+
+lemma not_head_all_blanks : âA,sig,n.
+ not_head A sig n (all_blanks ⦠(S n)) = true.
+#A #sig #n whd in ⢠(??%?); >blank_all_blanks //
+qed.
+
+definition no_head_in â λA,sig,n,l.
+ âx. mem ? x (trace (TA A sig) (S n) n l) â is_head ⦠x = false.
+
+(*
+lemma not_head_true: âA,sig,n,c. not_head A sig n c = true â
+ is_head ⦠(nth n ? (vec ⦠c) (blank ?)) = false.
+*)
-(* this exclude the possibility that traces do not overlap: the head must
-remain inside all traces *)
+lemma hd_nil : âA,d. hd A [ ] d = d.
+// qed.
-definition mtiL â λsig,n,i.
- move_to_blank_L sig n i ·
- shift_i_L sig n i ·
- move_until ? L (no_head sig n).
+definition mtiL â λA,sig,n,i.
+ move_to_blank_L (TA A sig) (S n) i ·
+ shift_i_L (TA A sig) (S n) i ·
+ move_until ? L (not_head A sig n).
-definition Rmtil â λsig,n,i,t1,t2.
+definition Rmtil â λA,sig,n,i,t1,t2.
âls,a,rs.
- t1 = midtape (multi_sig sig n) ls a rs â
- nth n ? (vec ⦠a) (blank ?) = head ? â
- (âi.regular_trace sig n a ls rs i) â
+ t1 = midtape (MTA A sig (S n)) ls a rs â
+ is_head A sig (nth n ? (vec ⦠a) (blank ?)) = true â
+ (âi.regular_trace (TA A sig) (S n) a ls rs i) â
(* next: we cannot be on rightof on trace i *)
(nth i ? (vec ⦠a) (blank ?) = (blank ?)
- â nth i ? (vec ⦠(hd ? rs (all_blank â¦))) (blank ?) â (blank ?)) â
+ â nth i ? (vec ⦠(hd ? rs (all_blanks â¦))) (blank ?) â (blank ?)) â
no_head_in ⦠ls â
no_head_in ⦠rs â
(âls1,a1,rs1.
- t2 = midtape (multi_sig â¦) ls1 a1 rs1 â§
+ t2 = midtape (MTA A sig (S n)) ls1 a1 rs1 â§
(âi.regular_trace ⦠a1 ls1 rs1 i) â§
- (âj. j ⤠n â j â i â to_blank_i ? n j (a1::ls1) = to_blank_i ? n j (a::ls)) â§
- (âj. j ⤠n â j â i â to_blank_i ? n j rs1 = to_blank_i ? n j rs) â§
- (to_blank_i ? n i ls1 = to_blank_i ? n i (a::ls)) â§
- (to_blank_i ? n i (a1::rs1)) = to_blank_i ? n i rs).
+ (âj. j ⤠n â j â i â to_blank_i ? (S n) j (a1::ls1) = to_blank_i ? (S n) j (a::ls)) â§
+ (âj. j ⤠n â j â i â to_blank_i ? (S n) j rs1 = to_blank_i ? (S n) j rs) â§
+ (to_blank_i ? (S n) i ls1 = to_blank_i ? (S n) i (a::ls)) â§
+ (to_blank_i ? (S n) i (a1::rs1)) = to_blank_i ? (S n) i rs).
-theorem sem_Rmtil: âsig,n,i. i < n â mtiL sig n i ⨠Rmtil sig n i.
-#sig #n #i #lt_in
+theorem sem_Rmtil: âA,sig,n,i. i < n â mtiL A sig n i ⨠Rmtil A sig n i.
+#A #sig #n #i #lt_in
@(sem_seq_app ??????
(sem_move_to_blank_L ⦠)
(sem_seq ????? (sem_shift_i_L_new â¦)
- (ssem_move_until_L ? (no_head sig n))))
+ (ssem_move_until_L ? (not_head A sig n))))
#tin #tout * #t1 * * #_ #Ht1 * #t2 * #Ht2 * #_ #Htout
(* we start looking into Rmitl *)
#ls #a #rs #Htin (* tin is a midtape *)
-#Hhead #Hreg #no_rightof #Hnohead_ls #Hnohead_rs
-cut (regular_i sig n (a::ls) i)
+#Hheada #Hreg #no_rightof #Hnohead_ls #Hnohead_rs
+cut (regular_i ? (S n) (a::ls) i)
[cases (Hreg i) * //
cases (true_or_false (nth i ? (vec ⦠a) (blank ?) == (blank ?))) #Htest
[#_ @daemon (* absurd, since hd rs non e' blank *)
@@ -299,12 +334,10 @@ lapply (Htout ⦠Ht2) -Htout -Ht2 *
[(* the current character on trace i holds the head-mark.
The case is absurd, since b0 is the head of rs2, that is a sublist of rs,
and the head-mark is not in rs *)
- * #H3 @False_ind @(absurd (nth n ? (vec ⦠b0) (blank sig) = head ?))
- [@(\P ?) @injective_notb @H3 ]
- @Hnohead_rs >H2 >trace_append @mem_append_l2
+ * #H3 @False_ind @(absurd (true=false)) [2://] H2 >trace_append @mem_append_l2
lapply Hb0 cases rs2
- [whd in match (hd ???); #H >H in H3; whd in match (no_head ???);
- >all_blank_n normalize -H #H destruct (H); @False_ind
+ [>hd_nil #H >H in H3; >not_head_all_blanks #Habs destruct (Habs)
|#c #r #H4 %1 >H4 //
]
|*
@@ -312,43 +345,43 @@ lapply (Htout ⦠Ht2) -Htout -Ht2 *
(* cut (trace sig n j (a1::ls20)=trace sig n j (ls1@b::ls2)) *)
* #ls10 * #a1 * #ls20 * * * #Hls20 #Ha1 #Hnh #Htout
cut (âj.j â i â
- trace sig n j (reverse (multi_sig sig n) rs1@b::ls2) =
- trace sig n j (ls10@a1::ls20))
+ trace ? (S n) j (reverse (multi_sig (TA A sig) (S n)) rs1@b::ls2) =
+ trace ? (S n) j (ls10@a1::ls20))
[#j #ineqj >append_cons trace_def reverse_map >map_append @eq_f @Hls20 ]
#Htracej
- cut (trace sig n i (reverse (multi_sig sig n) (rs1@[b0])@ls2) =
- trace sig n i (ls10@a1::ls20))
+ cut (trace ? (S n) i (reverse (multi_sig (TA A sig) (S n)) (rs1@[b0])@ls2) =
+ trace ? (S n) i (ls10@a1::ls20))
[>trace_def Hcut
- lapply (trace_shift ⦠lt_in ⦠Hrss) [//] whd in match (tail ??); #Htr Hcut
+ lapply (trace_shift ⦠(le_S ⦠lt_in) ⦠Hrss) [//] whd in match (tail ??); #Htr reverse_map >map_append trace_def in ⢠(%â?); trace_def in ⢠(%â?); H1 in Htracei; >reverse_append >reverse_single >reverse_append
>reverse_reverse >associative_append >associative_append
@daemon
] #H3
cut (âj. j â i â
- trace sig n j (reverse (multi_sig sig n) ls10@rs2) = trace sig n j rs)
- [#j #jneqi @(injective_append_l ⦠(trace sig n j (reverse ? ls1)))
+ trace ? (S n) j (reverse ? ls10@rs2) = trace ? (S n) j rs)
+ [#j #jneqi @(injective_append_l ⦠(trace ? (S n) j (reverse ? ls1)))
>map_append >map_append >Hrs1 >H1 >associative_append
eqji (* by cases wether a1 is blank *)
@@ -361,17 +394,17 @@ lapply (Htout ⦠Ht2) -Htout -Ht2 *
|@sym_eq @Hrs_j //
]
]]
- |#j #lejn #jneqi <(Hls1 ⦠lejn)
+ |#j #lejn #jneqi <(Hls1 ⦠(le_S_S ⦠lejn))
>to_blank_i_def >to_blank_i_def @eq_f @sym_eq @(proj2 ⦠(H2 j jneqi))]
|#j #lejn #jneqi >reverse_cons >associative_append >Hb0
to_blank_i_def >to_blank_i_def @eq_f @Hrs_j //]
- |<(Hls1 i) [2:@lt_to_le //]
+ |<(Hls1 i) [2:@le_S //]
lapply (all_blank_after_blank ⦠reg_ls1_i)
[@(\P ?) @daemon] #allb_ls2
whd in match (to_blank_i ????); <(proj2 ⦠H3)
@daemon ]
|>reverse_cons >associative_append
- cut (to_blank_i sig n i rs = to_blank_i sig n i (rs11@[b0])) [@daemon]
+ cut (to_blank_i ? (S n) i rs = to_blank_i ? (S n) i (rs11@[b0])) [@daemon]
#Hcut >Hcut >(to_blank_i_chop ⦠b0 (a1::reverse â¦ls10)) [2: @Hb0blank]
>to_blank_i_def >to_blank_i_def @eq_f
>trace_def >trace_def @injective_reverse >reverse_map >reverse_cons
@@ -380,14 +413,14 @@ lapply (Htout ⦠Ht2) -Htout -Ht2 *
]
|(*we do not find the head: this is absurd *)
* #b1 * #lss * * #H2 @False_ind
- cut (âx0. mem ? x0 (trace sig n n (b0::reverse ? rss@ls2)) â x0 â head ?)
+ cut (âx0. mem ? x0 (trace ? (S n) n (b0::reverse ? rss@ls2)) â is_head ⦠x0 = false)
[@daemon] -H2 #H2
- lapply (trace_shift_neq sig n i n ⦠lt_in ⦠Hrss)
+ lapply (trace_shift_neq ? (S n) i n ⦠(le_S ⦠lt_in) ⦠Hrss)
[@lt_to_not_eq @lt_in | // ]
#H3 @(absurd
- (nth n ? (vec ⦠(hd ? (ls1@[b]) (all_blank sig n))) (blank ?) = head ?))
+ (is_head ⦠(nth n ? (vec ⦠(hd ? (ls1@[b]) (all_blanks ⦠(S n)))) (blank ?)) = true))
[>Hhead //
- |@H2 >trace_def %2 trace_def %2 H3 >H1 >trace_def >reverse_map >reverse_cons >reverse_append
>reverse_reverse >associative_append