From Undecidability Require Import TM.Util.Prelim TM.Util.Relations TM.Util.TM_facts.

Set Default Proof Using "Type".


Section SujectTape.
  Variable sig : Type.
  Variable g : option sig.
  Variable def : sig.

  Definition surject : sig := t match (g t) with Some s s | None def end.

  Definition surjectTape := mapTape surject.

End SujectTape.

#[export] Hint Unfold surjectTape : tape.

Section lift_sigma_tau.
  Variable n : .
  Variable sig : Type.
  Variable g : option sig.
  Variable def : sig.
  Variable F : Type.

  Definition surjectTapes : tapes 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 n) (F * tapes n) :=
     tin '(yout,tout) R (surjectTapes tin) (yout, surjectTapes tout).

  Definition lift_sigma_tau_T (T : Rel (Vector.t (tape sig) n) ) :
    Rel (Vector.t (tape ) n) :=
     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 } (g) def !t.
Global Hint Rewrite surjectTapes_nth : tape.

Arguments lift_sigma_tau_Rel {n sig } (g def) {F} (R) x y /.
Arguments lift_sigma_tau_T {n sig } (g def T) x y /.

Section InjectTape.

  Variable sig : Type.
  Variable f : sig .

  Definition injectTape := mapTape f.
  Definition injectTapes {n: } := mapTapes (n := n) f.
End InjectTape.

Section InjectSurject.
  Variable sig : Type.
  Variable inj : Retract sig .
  Variable def : sig.

  Lemma surject_inject' (l : list sig) :
    List.map ( t : 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 := f map_fst (map_opt f).
End TranslateAct.

Section LiftAlphabet.
  Variable sig : finType.
  Variable n : .
  Variable F : finType.
  Variable pMSig : pTM sig F n.

  Variable Inj : Retract sig .

  Variable def : sig.

  Definition surjectReadSymbols : Vector.t (option ) n Vector.t (option sig) n :=
    Vector.map (map_opt (surject Retr_g def)).

  Definition lift_trans :=
     '(q, sym)
      let (q', act) := trans (m := pMSig) (q, surjectReadSymbols sym) in
      (q', Vector.map (map_act Retr_f) act).

  Definition LiftAlphabet_TM : TM n :=
    {| trans := lift_trans;
       start := start ( pMSig);
       halt := halt (m := pMSig) |}.

  Definition LiftAlphabet :pTM F n :=
    (LiftAlphabet_TM; pMSig).


  Definition surjectConf : (mconfig (state LiftAlphabet_TM) n) (mconfig sig (state ( pMSig)) n) :=
     c mk_mconfig (cstate c) (surjectTapes Retr_g def (ctapes c)).


  Lemma doAct_surject :
     (tape : tape ) (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 ; cbn; f_equal; now retract_adjoint.
    - destruct ; cbn; f_equal; now retract_adjoint.
  Qed.


  Lemma current_chars_surjectTapes (t : tapes 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 (state ( pMSig)) n) :
    step (M := 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 (state LiftAlphabet_TM) n) (k : ) :
    loopM (M := LiftAlphabet_TM) k = Some
    loopM (M := pMSig) (surjectConf ) k = Some (surjectConf ).
  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 : ) iconf (oconf : mconfig sig (state ( pMSig)) n) :
    loopM (surjectConf iconf) k = Some oconf
     oconf' : mconfig (state 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) ) :
     pMSig T
     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 : ) :
    pMSig c(k) R
    LiftAlphabet c(k) lift_sigma_tau_Rel Retr_g def R.
  Proof.
    intros [ ] % Realise_total. eapply Realise_total. split; cbn in *.
    - now eapply LiftAlphabet_Realise.
    - eapply LiftAlphabet_TerminatesIn in . auto.
  Qed.


End LiftAlphabet.

Arguments LiftAlphabet : simpl never.

Ltac smpl_TM_LiftAlphabetSigma :=
  once lazymatch goal with
  | [ |- LiftAlphabet _ _ _ _] eapply LiftAlphabet_Realise; swap 1 2
  | [ |- LiftAlphabet _ _ _ c(_) _] eapply LiftAlphabet_RealiseIn; swap 1 2
  | [ |- (LiftAlphabet _ _ _) _] eapply LiftAlphabet_TerminatesIn; swap 1 2
  end.
Smpl Add smpl_TM_LiftAlphabetSigma : TM_Correct.