From Undecidability.TM Require Import TMTac.
From Undecidability.TM Require Export Basic.Basic Compound.MoveToSymbol.

From Undecidability.TM.Hoare Require Import HoareLogic HoareCombinators HoareRegister HoareTactics HoareTacticsView.


Lemma DoAct_SpecTReg (sig : finType) act (P : tape (boundary + sig) Prop):
TripleT (≃≃(([], [|Custom P|]))) 1 (DoAct act)
        ( _ ≃≃(([], [|Custom ( t t', t = doAct t' act P t')|]))).
Proof.
  eapply RealiseIn_TripleT.
  - apply DoAct_Sem.
  - intros tin [] tout H HEnc. cbn in *.
  specialize (HEnc ). simpl_vector in *; cbn in *. tspec_solve. eauto.
Qed.


Ltac hstep_DoAct :=
  lazymatch goal with
  | [ |- TripleT ?P ?k (DoAct _) ?Q ] eapply DoAct_SpecTReg
  | [ |- TripleT ?P ?k (Write _) ?Q ] eapply DoAct_SpecTReg
  | [ |- TripleT ?P ?k (WriteMove _ _) ?Q ] eapply DoAct_SpecTReg
  | [ |- TripleT ?P ?k (Move _) ?Q ] eapply DoAct_SpecTReg
  end.

Smpl Add hstep_DoAct : hstep_Spec.

Lemma CaseChar_SpecTReg (sig F : finType) (f : option (boundary + sig) F) P:
TripleT ≃≃([],[|Custom P|])
  1 (CaseChar f) ( y ≃≃([ t, y = f (current t) P t],[|Custom ( t y = f (current t) P t) |])).
Proof.
  eapply RealiseIn_TripleT. now apply CaseChar_Sem. cbn. intros ? ? ? [ ] [[] H']%tspecE.
  specialize (H' ). cbn in H'. eapply tspecI;cbn. now eauto. intros i; destruct_fin i. easy.
Qed.


Ltac hstep_CaseChar :=
lazymatch goal with
| [ |- TripleT ?P ?k (CaseChar _) ?Q ] eapply CaseChar_SpecTReg
| [ |- TripleT ?P ?k ReadChar ?Q ] refine (_ : TripleT _ _ (CaseChar ( x x)) _);eapply CaseChar_SpecTReg
end.
Smpl Add hstep_CaseChar : hstep_Spec.

Lemma MoveToSymbol_SpecTReg (sig : finType) (f : boundary + sig _) g tin:
TripleT ≃≃([], [|Custom (eq tin) |])
    (MoveToSymbol_steps f g tin) (MoveToSymbol f g)
    ( _ ≃≃([], [|Custom (eq (MoveToSymbol_Fun f g tin))|])).
Proof.
eapply Realise_TripleT.
- apply MoveToSymbol_Realise.
- apply MoveToSymbol_Terminates.
- intros ? [] tout H HEnc. cbn in *.
  specialize (HEnc ). cbn in HEnc. subst. now tspec_solve.
- intros ? k HEnc Hk.
  specialize (HEnc ) as . simpl_vector in *; cbn in *. now subst.
Qed.


Ltac hstep_MoveToSymbol :=
lazymatch goal with
| [ |- TripleT ?P ?k (MoveToSymbol _ _) ?Q ] eapply MoveToSymbol_SpecTReg
end.
Smpl Add hstep_MoveToSymbol : hstep_Spec.