From Undecidability.TM Require Import Util.Prelim Util.TM_facts.
Section Mono_Nop.
Variable sig : finType.
Definition NullTM : TM sig 0 :=
{|
trans := fun '(q, s) => (q, Vector.nil _);
start := tt;
halt _ := true;
|}.
Definition Null : pTM sig unit 0 := (NullTM; fun _ => tt).
Definition Null_Rel : pRel sig unit 0 :=
ignoreParam (fun t t' => True).
Lemma Null_Sem: Null ⊨c(0) Null_Rel.
Proof. intros t. cbn. unfold initc; cbn. eexists (mk_mconfig _ _); cbn; eauto. Qed.
End Mono_Nop.
Arguments Null : simpl never.
Arguments Null {sig}.
Arguments Null_Rel { sig } x y / : rename.
Ltac smpl_TM_Null :=
once lazymatch goal with
| [ |- Null ⊨ _] => eapply RealiseIn_Realise; eapply Null_Sem
| [ |- Null ⊨c(_) _] => eapply Null_Sem
| [ |- projT1 (Null) ↓ _] => eapply RealiseIn_TerminatesIn; eapply Null_Sem
end.
Smpl Add smpl_TM_Null : TM_Correct.
Section Mono_Nop.
Variable sig : finType.
Definition NullTM : TM sig 0 :=
{|
trans := fun '(q, s) => (q, Vector.nil _);
start := tt;
halt _ := true;
|}.
Definition Null : pTM sig unit 0 := (NullTM; fun _ => tt).
Definition Null_Rel : pRel sig unit 0 :=
ignoreParam (fun t t' => True).
Lemma Null_Sem: Null ⊨c(0) Null_Rel.
Proof. intros t. cbn. unfold initc; cbn. eexists (mk_mconfig _ _); cbn; eauto. Qed.
End Mono_Nop.
Arguments Null : simpl never.
Arguments Null {sig}.
Arguments Null_Rel { sig } x y / : rename.
Ltac smpl_TM_Null :=
once lazymatch goal with
| [ |- Null ⊨ _] => eapply RealiseIn_Realise; eapply Null_Sem
| [ |- Null ⊨c(_) _] => eapply Null_Sem
| [ |- projT1 (Null) ↓ _] => eapply RealiseIn_TerminatesIn; eapply Null_Sem
end.
Smpl Add smpl_TM_Null : TM_Correct.