Section SujectTape.
Variable sig tau : Type.
Variable g : tau -> option sig.
Variable def : sig.
Definition surject : tau -> sig := fun t => match (g t) with Some s => s | None => def end.
Definition surjectTape := mapTape surject.
End SujectTape.
Hint Unfold surjectTape : tape.
Section lift_sigma_tau.
Variable n : nat.
Variable sig tau : Type.
Variable g : tau -> option sig.
Variable def : sig.
Variable F : Type.
Definition surjectTapes : tapes tau n -> tapes sig n :=
Vector.map (surjectTape g def).
Definition lift_sigma_tau_Rel (R : Rel (tapes sig n) (F * tapes sig n)) :
Rel (tapes tau n) (F * tapes tau n) :=
fun tin '(yout,tout) => R (surjectTapes tin) (yout, surjectTapes tout).
Definition lift_sigma_tau_T (T : Rel (Vector.t (tape sig) n) nat) :
Rel (Vector.t (tape tau) n) nat :=
fun tin k => T (surjectTapes tin) k.
Lemma surjectTapes_nth t i :
(surjectTapes t)[@i] = surjectTape g def t[@i].
Proof. unfold surjectTapes. now simpl_vector. Qed.
End lift_sigma_tau.
Arguments surjectTapes {n sig tau} (g) def !t.
Hint Rewrite surjectTapes_nth : tape.
Arguments lift_sigma_tau_Rel {n sig tau} (g def) {F} (R) x y /.
Arguments lift_sigma_tau_T {n sig tau} (g def T) x y /.
Section InjectTape.
Variable sig tau : Type.
Variable f : sig -> tau.
Definition injectTape := mapTape f.
Definition injectTapes {n: nat} := mapTapes (n := n) f.
End InjectTape.
Section InjectSurject.
Variable sig tau : Type.
Variable inj : Retract sig tau.
Variable def : sig.
Lemma surject_inject' (l : list sig) :
List.map (fun t : tau => match Retr_g t with
| Some s => s
| None => def
end) (List.map Retr_f l) = l.
Proof.
induction l; cbn.
- reflexivity.
- retract_adjoint. f_equal. assumption.
Qed.
Lemma surject_inject_tape (t : tape sig) :
surjectTape Retr_g def (injectTape Retr_f t) = t.
Proof.
unfold surjectTape, injectTape, surject.
destruct t; cbn; f_equal; try rewrite retract_g_adjoint; auto; apply surject_inject'.
Qed.
End InjectSurject.
Section TranslateAct.
Variable X Y : Type.
Definition map_act : (X -> Y) -> option X * move -> option Y * move := fun f => map_fst (map_opt f).
End TranslateAct.
Section LiftAlphabet.
Variable sig tau : finType.
Variable n : nat.
Variable F : finType.
Variable pMSig : pTM sig F n.
Variable Inj : Retract sig tau.
Variable def : sig.
Definition surjectReadSymbols : Vector.t (option tau) n -> Vector.t (option sig) n :=
Vector.map (map_opt (surject Retr_g def)).
Definition lift_trans :=
fun '(q, sym) =>
let (q', act) := trans (m := projT1 pMSig) (q, surjectReadSymbols sym) in
(q', Vector.map (map_act Retr_f) act).
Definition LiftAlphabet_TM : mTM tau n :=
{| trans := lift_trans;
start := start (projT1 pMSig);
halt := halt (m := projT1 pMSig) |}.
Definition LiftAlphabet :pTM tau F n :=
(LiftAlphabet_TM; projT2 pMSig).
Definition surjectConf : (mconfig tau (states LiftAlphabet_TM) n) -> (mconfig sig (states (projT1 pMSig)) n) :=
fun c => mk_mconfig (cstate c) (surjectTapes Retr_g def (ctapes c)).
Lemma doAct_surject :
forall (tape : tape tau) (act : option sig * move) (d : sig),
doAct (surjectTape Retr_g d tape) act =
surjectTape Retr_g d (doAct tape (map_act Retr_f act)).
Proof.
intros tape. intros (w,m) d; cbn.
unfold surjectTape, doAct, tape_move, tape_write, surject; cbn.
destruct tape, m, w; cbn; f_equal; try retract_adjoint; auto.
- destruct l; cbn; f_equal; now retract_adjoint.
- destruct l; cbn; f_equal; now retract_adjoint.
- destruct l0; cbn; f_equal; now retract_adjoint.
- destruct l0; cbn; f_equal; now retract_adjoint.
Qed.
Lemma current_chars_surjectTapes (t : tapes tau n) :
current_chars (surjectTapes Retr_g def t) = surjectReadSymbols (current_chars t).
Proof.
unfold current_chars, surjectTapes, surjectReadSymbols. apply Vector.eq_nth_iff; intros i ? <-. simpl_tape.
unfold surjectTape, surject. now simpl_tape.
Qed.
Lemma LiftAlphabet_comp_step (c : mconfig tau (states (projT1 pMSig)) n) :
step (M := projT1 pMSig) (surjectConf c) = surjectConf (step (M := LiftAlphabet_TM) c).
Proof.
unfold surjectConf. destruct c as [q t]. cbn in *.
unfold step. cbn -[doAct_multi].
rewrite current_chars_surjectTapes.
destruct (trans (q, surjectReadSymbols (current_chars t))) eqn:E. cbn.
f_equal. unfold doAct_multi, surjectTapes. apply Vector.eq_nth_iff; intros i ? <-. simpl_tape. apply doAct_surject.
Qed.
Lemma LiftAlphabet_lift (c1 c2 : mconfig tau (states LiftAlphabet_TM) n) (k : nat) :
loopM (M := LiftAlphabet_TM) c1 k = Some c2 ->
loopM (M := projT1 pMSig) (surjectConf c1) k = Some (surjectConf c2).
Proof.
unfold loopM. intros H. eapply loop_lift. 3: apply H. auto.
- intros ? _. apply LiftAlphabet_comp_step.
Qed.
Lemma LiftAlphabet_Realise (R : Rel (tapes sig n) (F * tapes sig n)) :
pMSig ⊨ R ->
LiftAlphabet ⊨ lift_sigma_tau_Rel Retr_g def R.
Proof.
intros H. intros t i outc Hloop. unfold lift_sigma_tau_Rel. hnf in H.
specialize (H (surjectTapes Retr_g def t) i (mk_mconfig (cstate outc) (surjectTapes Retr_g def (ctapes outc)))).
cbn in H. apply H.
now apply (@LiftAlphabet_lift (initc LiftAlphabet_TM t) outc i).
Qed.
Lemma LiftAlphabet_unlift (k : nat) iconf (oconf : mconfig sig (states (projT1 pMSig)) n) :
loopM (surjectConf iconf) k = Some oconf ->
exists oconf' : mconfig tau (states LiftAlphabet_TM) n,
loopM iconf k = Some oconf'.
Proof.
intros HLoop. unfold loopM in *.
apply loop_unlift with (f := step(M:=LiftAlphabet_TM)) (h:=haltConf(M:=LiftAlphabet_TM)) in HLoop as (c'&HLoop&->); eauto.
- intros ? _. now apply LiftAlphabet_comp_step.
Qed.
Lemma LiftAlphabet_TerminatesIn (T : Rel (tapes sig n) nat) :
projT1 pMSig ↓ T ->
projT1 LiftAlphabet ↓ lift_sigma_tau_T Retr_g def T.
Proof.
intros H. hnf. intros tin k HTerm. hnf in HTerm, H. specialize (H _ _ HTerm) as (oconf&HLoop).
eapply LiftAlphabet_unlift; eauto.
Qed.
Lemma LiftAlphabet_RealiseIn (R : Rel (tapes sig n) (F * tapes sig n)) (k : nat) :
pMSig ⊨c(k) R ->
LiftAlphabet ⊨c(k) lift_sigma_tau_Rel Retr_g def R.
Proof.
intros [H1 H2] % Realise_total. eapply Realise_total. split; cbn in *.
- now eapply LiftAlphabet_Realise.
- eapply LiftAlphabet_TerminatesIn in H2. auto.
Qed.
End LiftAlphabet.
Arguments LiftAlphabet : simpl never.
Ltac smpl_TM_LiftAlphabetSigma :=
lazymatch goal with
| [ |- LiftAlphabet _ _ _ ⊨ _] => eapply LiftAlphabet_Realise; swap 1 2
| [ |- LiftAlphabet _ _ _ ⊨c(_) _] => eapply LiftAlphabet_RealiseIn; swap 1 2
| [ |- projT1 (LiftAlphabet _ _ _) ↓ _] => eapply LiftAlphabet_TerminatesIn; swap 1 2
end.
Smpl Add smpl_TM_LiftAlphabetSigma : TM_Correct.