-(* 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.
-
-(* 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
-the i-trace. Then come back to the origin. *)
-
-definition shift_i ≝ λsig,n,i.λa,b:Vector (sig_ext sig) n.
- change_vec (sig_ext sig) n a (nth i ? b (blank ?)) i.
-
-(* vec is a coercion. Why should I insert it? *)
-definition mti_step ≝ λsig:FinSet.λn,i.
- ifTM (multi_sig sig n) (test_char ? (λc:multi_sig sig n.¬(nth i ? (vec … c) (blank ?))==blank ?))
- (single_finalTM … (ncombf_r (multi_sig sig n) (shift_i sig n i) (all_blank sig n)))
- (nop ?) tc_true.
-
-definition Rmti_step_true ≝
-λsig,n,i,t1,t2.
- ∃b:multi_sig sig n. (nth i ? (vec … b) (blank ?) ≠ blank ?) ∧
- ((∃ls,a,rs.
- t1 = midtape (multi_sig sig n) ls b (a::rs) ∧
- t2 = midtape (multi_sig sig n) ((shift_i sig n i b a)::ls) a rs) ∨
- (∃ls.
- t1 = midtape ? ls b [] ∧
- t2 = rightof ? (shift_i sig n i b (all_blank sig n)) ls)).
-
-(* 〈combf0,all_blank sig n〉 *)
-definition Rmti_step_false ≝
- λsig,n,i,t1,t2.
- (∀ls,b,rs. t1 = midtape (multi_sig sig n) ls b rs →
- (nth i ? (vec … b) (blank ?) = blank ?)) ∧ t2 = t1.
-
-lemma sem_mti_step :
- ∀sig,n,i.
- mti_step sig n i ⊨
- [inr … (inl … (inr … start_nop)): Rmti_step_true sig n i, Rmti_step_false sig n i].
-#sig #n #i
-@(acc_sem_if_app (multi_sig sig n) ??????????
- (sem_test_char …) (sem_ncombf_r (multi_sig sig n) (shift_i sig n i)(all_blank sig n))
- (sem_nop (multi_sig sig n)))
- [#intape #outtape #tapea whd in ⊢ (%→%→%); * * #c *
- #Hcur cases (current_to_midtape … Hcur) #ls * #rs #Hintape
- #ctest #Htapea * #Hout1 #Hout2 @(ex_intro … c) %
- [@(\Pf (injective_notb … )) @ctest]
- generalize in match Hintape; -Hintape cases rs
- [#Hintape %2 @(ex_intro …ls) % // @Hout1 >Htapea @Hintape
- |#a #rs1 #Hintape %1
- @(ex_intro … ls) @(ex_intro … a) @(ex_intro … rs1) % //
- @Hout2 >Htapea @Hintape
- ]
- |#intape #outtape #tapea whd in ⊢ (%→%→%);
- * #Htest #tapea #outtape
- % // #ls #b #rs
- #intape lapply (Htest b ?) [>intape //] -Htest #Htest
- lapply (injective_notb ? true Htest) -Htest #Htest @(\P Htest)
- ]
-qed.
-
-(* move tape i machine *)
-definition mti ≝
- λsig,n,i.whileTM (multi_sig sig n) (mti_step sig n i) (inr … (inl … (inr … start_nop))).
-
-(* v2 is obtained from v1 shifting left the i-th trace *)
-definition shift_l ≝ λsig,n,i,v1,v2. (* multi_sig sig n*)
- |v1| = |v2| ∧
- ∀j.nth j ? v2 (all_blank sig n) =
- change_vec ? n (nth j ? v1 (all_blank sig n))
- (nth i ? (vec … (nth (S j) ? v1 (all_blank sig n))) (blank ?)) i.
-
-lemma trace_shift: ∀sig,n,i,v1,v2. i < n → 0 < |v1| →
- shift_l sig n i v1 v2 → trace ? n i v2 = tail ? (trace ? n i v1)@[blank sig].
-#sig #n #i #v1 #v2 #lein #Hlen * #Hlen1 #Hnth @(nth_to_eq … (blank ?))
- [>length_trace <Hlen1 generalize in match Hlen; cases v1
- [normalize #H @(le_n_O_elim … H) //
- |#b #tl #_ normalize >length_append >length_trace normalize //
- ]
- |#j >nth_trace >Hnth >nth_change_vec // >tail_trace
- cut (trace ? n i [all_blank sig n] = [blank sig])
- [normalize >blank_all_blank //]
- #Hcut <Hcut <trace_append >nth_trace
- <nth_extended //
- ]
-qed.
-
-lemma trace_shift_neq: ∀sig,n,i,j,v1,v2. i < n → 0 < |v1| → i ≠ j →
- shift_l sig n i v1 v2 → trace ? n j v2 = trace ? n j v1.
-#sig #n #i #j #v1 #v2 #lein #Hlen #Hneq * #Hlen1 #Hnth @(nth_to_eq … (blank ?))
- [>length_trace >length_trace @sym_eq @Hlen1
- |#k >nth_trace >Hnth >nth_change_vec_neq // >nth_trace //
- ]
-qed.
-
-axiom daemon: ∀P:Prop.P.
-
-definition R_mti ≝
- λsig,n,i,t1,t2.
- (∀a,rs. t1 = rightof ? a rs → t2 = t1) ∧
- (∀a,ls,rs.
- t1 = midtape (multi_sig sig n) ls a rs →
- (nth i ? (vec … a) (blank ?) = blank ? ∧ t2 = t1) ∨
- ((∃rs1,b,rs2,rss.
- rs = rs1@b::rs2 ∧
- nth i ? (vec … b) (blank ?) = (blank ?) ∧
- (∀x. mem ? x (a::rs1) → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
- shift_l sig n i (a::rs1) rss ∧
- t2 = midtape (multi_sig sig n) ((reverse ? rss)@ls) b rs2) ∨
- (∃b,rss.
- (∀x. mem ? x (a::rs) → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
- shift_l sig n i (a::rs) (rss@[b]) ∧
- t2 = rightof (multi_sig sig n) (shift_i sig n i b (all_blank sig n))
- ((reverse ? rss)@ls)))).
-
-lemma sem_mti:
- ∀sig,n,i.
- WRealize (multi_sig sig n) (mti sig n i) (R_mti sig n i).
-#sig #n #i #inc #j #outc #Hloop
-lapply (sem_while … (sem_mti_step sig n i) inc j outc Hloop) [%]
--Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
-[ whd in ⊢ (% → ?); * #H1 #H2 %
- [#a #rs #Htape1 @H2
- |#a #ls #rs #Htapea % % [@(H1 … Htapea) |@H2]
- ]
-| #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
- lapply (IH HRfalse) -IH -HRfalse whd in ⊢ (%→%);
- * #IH1 #IH2 %
- [#b0 #ls #Htapeb cases Hstar1 #b * #_ *
- [* #ls0 * #a * #rs0 * >Htapeb #H destruct (H)
- |* #ls0 * >Htapeb #H destruct (H)
- ]
- |#b0 #ls #rs #Htapeb cases Hstar1 #b * #btest *
- [* #ls1 * #a * #rs1 * >Htapeb #H destruct (H) #Htapec
- %2 cases (IH2 … Htapec)
- [(* case a = None *)
- * #testa #Hout %1
- %{[ ]} %{a} %{rs1} %{[shift_i sig n i b a]} %
- [%[%[% // |#x #Hb >(mem_single ??? Hb) // ]
- |@daemon]
- |>Hout >reverse_single @Htapec
- ]
- |*
- [ (* case a \= None and exists b = None *) -IH1 -IH2 #IH
- %1 cases IH -IH #rs10 * #b0 * #rs2 * #rss * * * *
- #H1 #H2 #H3 #H4 #H5
- %{(a::rs10)} %{b0} %{rs2} %{(shift_i sig n i b a::rss)}
- %[%[%[%[>H1 //|@H2]
- |#x * [#eqxa >eqxa (*?? *) @daemon|@H3]]
- |@daemon]
- |>H5 >reverse_cons >associative_append //
- ]
- | (* case a \= None and we reach the end of the (full) tape *) -IH1 -IH2 #IH
- %2 cases IH -IH #b0 * #rss * * #H1 #H2 #H3
- %{b0} %{(shift_i sig n i b a::rss)}
- %[%[#x * [#eqxb >eqxb @btest|@H1]
- |@daemon]
- |>H3 >reverse_cons >associative_append //
- ]
- ]
- ]
- |(* b \= None but the left tape is empty *)
- * #ls0 * >Htapeb #H destruct (H) #Htapec
- %2 %2 %{b} %{[ ]}
- %[%[#x * [#eqxb >eqxb @btest|@False_ind]
- |@daemon (*shift of dingle char OK *)]
- |>(IH1 … Htapec) >Htapec //
- ]
- ]
-qed.
-
-lemma WF_mti_niltape:
- ∀sig,n,i. WF ? (inv ? (Rmti_step_true sig n i)) (niltape ?).
-#sig #n #i @wf #t1 whd in ⊢ (%→?); * #b * #_ *
- [* #ls * #a * #rs * #H destruct|* #ls * #H destruct ]
-qed.
-
-lemma WF_mti_rightof:
- ∀sig,n,i,a,ls. WF ? (inv ? (Rmti_step_true sig n i)) (rightof ? a ls).
-#sig #n #i #a #ls @wf #t1 whd in ⊢ (%→?); * #b * #_ *
- [* #ls * #a * #rs * #H destruct|* #ls * #H destruct ]
-qed.
-
-lemma WF_mti_leftof:
- ∀sig,n,i,a,ls. WF ? (inv ? (Rmti_step_true sig n i)) (leftof ? a ls).
-#sig #n #i #a #ls @wf #t1 whd in ⊢ (%→?); * #b * #_ *
- [* #ls * #a * #rs * #H destruct|* #ls * #H destruct ]
-qed.
-
-lemma terminate_mti:
- ∀sig,n,i.∀t. Terminate ? (mti sig n i) t.
-#sig #n #i #t @(terminate_while … (sem_mti_step sig n i)) [%]
-cases t // #ls #c #rs lapply c -c lapply ls -ls elim rs
- [#ls #c @wf #t1 whd in ⊢ (%→?); * #b * #_ *
- [* #ls1 * #a * #rs1 * #H destruct
- |* #ls1 * #H destruct #Ht1 >Ht1 //
- ]
- |#a #rs1 #Hind #ls #c @wf #t1 whd in ⊢ (%→?); * #b * #_ *
- [* #ls1 * #a2 * #rs2 * #H destruct (H) #Ht1 >Ht1 //
- |* #ls1 * #H destruct
- ]
- ]
-qed.
-
-lemma ssem_mti: ∀sig,n,i.
- Realize ? (mti sig n i) (R_mti sig n i).
-/2/ qed.
-