include "turing/basic_machines.ma".
include "turing/if_machine.ma".
-include "basics/vector_finset.ma".
include "turing/auxiliary_machines1.ma".
-
-(* a multi_sig characheter is composed by n+1 sub-characters: n for each tape
-of a multitape machine, and an additional one to mark the position of the head.
-We extend the tape alphabet with two new symbols true and false.
-false is used to pad shorter tapes, and true to mark the head of the tape *)
-
-definition sig_ext ≝ λsig. FinSum FinBool sig.
-definition blank : ∀sig.sig_ext sig ≝ λsig. inl … false.
-definition head : ∀sig.sig_ext sig ≝ λsig. inl … true.
-
-definition multi_sig ≝ λsig:FinSet.λn.FinVector (sig_ext sig) n.
-
-let rec all_blank sig n on n : multi_sig sig n ≝
- match n with
- [ O ⇒ Vector_of_list ? []
- | S m ⇒ vec_cons ? (blank ?) m (all_blank sig m)
- ].
-
-lemma blank_all_blank: ∀sig,n,i.
- nth i ? (vec … (all_blank sig n)) (blank sig) = blank ?.
-#sig #n elim n normalize
- [#i >nth_nil //
- |#m #Hind #i cases i // #j @Hind
- ]
-qed.
-
-lemma all_blank_n: ∀sig,n.
- nth n ? (vec … (all_blank sig n)) (blank sig) = blank ?.
-#sig #n @blank_all_blank
-qed.
-
-(* compute the i-th trace *)
-definition trace ≝ λsig,n,i,l.
- map ?? (λa. nth i ? (vec … n a) (blank sig)) l.
-
-lemma trace_def : ∀sig,n,i,l.
- trace sig n i l = map ?? (λa. nth i ? (vec … n a) (blank sig)) l.
-// qed.
-
-(*
-let rec trace sig n i l on l ≝
- match l with
- [ nil ⇒ nil ?
- | cons a tl ⇒ nth i ? (vec … n a) (blank sig)::(trace sig n i tl)]. *)
-
-lemma tail_trace: ∀sig,n,i,l.
- tail ? (trace sig n i l) = trace sig n i (tail ? l).
-#sig #n #i #l elim l //
-qed.
-
-lemma trace_append : ∀sig,n,i,l1,l2.
- trace sig n i (l1 @ l2) = trace sig n i l1 @ trace sig n i l2.
-#sig #n #i #l1 #l2 elim l1 // #a #tl #Hind normalize >Hind //
-qed.
-
-lemma trace_reverse : ∀sig,n,i,l.
- trace sig n i (reverse ? l) = reverse (sig_ext sig) (trace sig n i l).
-#sig #n #i #l elim l //
-#a #tl #Hind whd in match (trace ??? (a::tl)); >reverse_cons >reverse_cons
->trace_append >Hind //
-qed.
-
-lemma nth_trace : ∀sig,n,i,j,l.
- nth j ? (trace sig n i l) (blank ?) =
- nth i ? (nth j ? l (all_blank sig n)) (blank ?).
-#sig #n #i #j elim j
- [#l cases l normalize // >blank_all_blank //
- |-j #j #Hind #l whd in match (nth ????); whd in match (nth ????);
- cases l
- [normalize >nth_nil >nth_nil >blank_all_blank //
- |#a #tl normalize @Hind]
- ]
-qed.
-
-lemma length_trace: ∀sig,n,i,l.
- |trace sig n i l| = |l|.
-#sig #n #i #l elim l // #a #tl #Hind normalize @eq_f @Hind
-qed.
-
-(* some lemmas over lists *)
-lemma injective_append_l: ∀A,l. injective ?? (append A l).
-#A #l elim l
- [#l1 #l2 normalize //
- |#a #tl #Hind #l1 #l2 normalize #H @Hind @(cons_injective_r … H)
- ]
-qed.
-
-lemma injective_append_r: ∀A,l. injective ?? (λl1.append A l1 l).
-#A #l #l1 #l2 #H
-cut (reverse ? (l1@l) = reverse ? (l2@l)) [//]
->reverse_append >reverse_append #Hrev
-lapply (injective_append_l … Hrev) -Hrev #Hrev
-<(reverse_reverse … l1) <(reverse_reverse … l2) //
-qed.
-
-lemma injective_reverse: ∀A. injective ?? (reverse A).
-#A #l1 #l2 #H <(reverse_reverse … l1) <(reverse_reverse … l2) //
-qed.
-
-lemma first_P_to_eq : ∀A:Type[0].∀P:A→Prop.∀l1,l2,l3,l4,a1,a2.
- l1@a1::l2 = l3@a2::l4 → (∀x. mem A x l1 → P x) → (∀x. mem A x l2 → P x) →
- ¬ P a1 → ¬ P a2 → l1 = l3 ∧ a1::l2 = a2::l4.
-#A #P #l1 elim l1
- [#l2 *
- [#l4 #a1 #a2 normalize #H destruct /2/
- |#c #tl #l4 #a1 #a2 normalize #H destruct
- #_ #H #_ #H1 @False_ind @(absurd ?? H1) @H @mem_append_l2 %1 //
- ]
- |#b #tl1 #Hind #l2 *
- [#l4 #a1 #a2 normalize #H destruct
- #H1 #_ #_ #H2 @False_ind @(absurd ?? H2) @H1 %1 //
- |#c #tl2 #l4 #a1 #a2 normalize #H1 #H2 #H3 #H4 #H5
- lapply (Hind l2 tl2 l4 … H4 H5)
- [destruct @H3 |#x #H6 @H2 %2 // | destruct (H1) //
- |* #H6 #H7 % // >H7 in H1; #H1 @(injective_append_r … (a2::l4)) @H1
- ]
- ]
-qed.
-
-lemma nth_to_eq: ∀A,l1,l2,a. |l1| = |l2| →
- (∀i. nth i A l1 a = nth i A l2 a) → l1 = l2.
-#A #l1 elim l1
- [* // #a #tl #d normalize #H destruct (H)
- |#a #tl #Hind *
- [#d normalize #H destruct (H)
- |#b #tl1 #d #Hlen #Hnth @eq_f2
- [@(Hnth 0) | @(Hind tl1 d) [@injective_S @Hlen | #i @(Hnth (S i)) ]]
- ]
- ]
-qed.
-
-lemma nth_extended: ∀A,i,l,a.
- nth i A l a = nth i A (l@[a]) a.
-#A #i elim i [* // |#j #Hind * // #b #tl #a normalize @Hind]
-qed.
+include "turing/multi_to_mono/trace_alphabet.ma".
(* a machine that moves the i trace r: we reach the left margin of the i-trace
and make a (shifted) copy of the old tape up to the end of the right margin of
projects / helm.git / blobdiff