From Undecidability.TM Require Import Util.TM_facts.

Set Default Proof Using "Type".

Section CaseChar2.
  Variable sig : finType.
  Variable (F : finType) (f : option sig -> option sig -> F).

  Definition CaseChar2_TM : TM sig 2 :=
    {|
      trans := fun '(_, sym) => (Some (f sym[@Fin0] sym[@Fin1]), [| (None, Nmove); (None, Nmove) |]);
      start := None;
      halt := fun s => match s with
                    | None => false
                    | Some _ => true
                    end;
    |}.

  Definition CaseChar2 : pTM sig F 2 := (CaseChar2_TM; fun s => match s with None => f None None | Some y => y end).

  Definition CaseChar2_Rel : pRel sig F 2 :=
    fun t '(y, t') =>
      y = f (current t[@Fin0]) (current t[@Fin1]) /\
      t' = t.

  Definition CaseChar2_Sem : CaseChar2 ⊨c(1) CaseChar2_Rel.
  Proof.
    intros t. destruct_tapes. cbn. unfold initc; cbn. cbv [step]; cbn. unfold current_chars; cbn.
    eexists (mk_mconfig _ _); cbv [step]; cbn. split. eauto. cbn. auto.
  Qed.

End CaseChar2.

Arguments CaseChar2 : simpl never.
Arguments CaseChar2 {sig F} f.
Arguments CaseChar2_Rel sig F f x y /.

Section ReadChar2.

  Variable sig : finType.

  Definition ReadChar2 : pTM sig (option sig * option sig) 2 := CaseChar2 pair.

  Definition ReadChar2_Rel : pRel sig (option sig * option sig) 2 :=
    fun t '(y, t') =>
      y = (current t[@Fin0], current t[@Fin1]) /\
      t' = t.

  Lemma ReadChar2_Sem : ReadChar2 ⊨c(1) ReadChar2_Rel.
  Proof.
    eapply RealiseIn_monotone.
    - apply CaseChar2_Sem.
    - reflexivity.
    - intros tin (yout, tout) (->&->). hnf. split; auto.
  Qed.

End ReadChar2.

Arguments ReadChar2 : simpl never.
Arguments ReadChar2 {sig}.
Arguments ReadChar2_Rel sig x y /.


Ltac smpl_TM_Duo :=
  once lazymatch goal with
  | [ |- CaseChar2 _ ⊨ _] => eapply RealiseIn_Realise; eapply CaseChar2_Sem
  | [ |- CaseChar2 _ ⊨c(_) _] => eapply CaseChar2_Sem
  | [ |- projT1 (CaseChar2 _) ↓ _] => eapply RealiseIn_TerminatesIn; eapply CaseChar2_Sem
  | [ |- ReadChar2 ⊨ _] => eapply RealiseIn_Realise; eapply ReadChar2_Sem
  | [ |- ReadChar2 ⊨c(_) _] => eapply ReadChar2_Sem
  | [ |- projT1 (ReadChar2) ↓ _] => eapply RealiseIn_TerminatesIn; eapply ReadChar2_Sem
  end.

Smpl Add smpl_TM_Duo : TM_Correct.