From Undecidability.TM Require Import ProgrammingTools.
From Undecidability Require Import CaseList WriteString Hoare.
Module Cons_constant.
Section Fix.
Context {Σ__X: finType} {X : Type} {cX : codable Σ__X X}.
Variable (c:X).
Definition M : pTM (sigList Σ__X)^+ unit 1 :=
WriteString Lmove (rev (inr sigList_cons::map (fun x => inr (sigList_X x)) ((encode c))));;
Move Lmove;;
Write (inl START).
Definition Rel : pRel (sigList Σ__X)^+ unit 1 :=
ignoreParam (
fun tin tout =>
forall l (s0 : nat),
tin[@Fin0] ≃(;s0) l ->
tout[@Fin0] ≃(;s0 - size c - 1) c :: l
).
Lemma Realise : M ⊨ Rel.
Proof.
eapply Realise_monotone.
{ unfold M. TM_Correct. eapply RealiseIn_Realise,WriteString_Sem. }
{
intros tin ((), tout) H. TMSimp.
destruct H2 as (?&->&?);cbn.
simpl_tape.
rewrite WriteString_L_left;cbn. autorewrite with list.
erewrite !tape_right_move_left.
2:{rewrite WriteString_L_current. autorewrite with list. cbn. reflexivity. }
rewrite WriteString_L_right. cbn.
eexists. repeat (cbn;autorewrite with list;try rewrite !map_map).
split. reflexivity.
rewrite tl_length,List.skipn_length. unfold size. nia.
}
Qed.
Definition time {sigX} {X : Type} {cX : codable sigX X} (c:X) := 5 + 2 * size c.
Lemma Terminates :
projT1 M ↓
(fun tin k =>
exists (l: list X) ,
tin[@Fin0] ≃ l /\
time c<= k).
Proof.
unfold Constr_cons_steps. eapply TerminatesIn_monotone.
{ unfold M. TM_Correct.
eapply RealiseIn_Realise. 2:eapply RealiseIn_TerminatesIn.
all:apply WriteString_Sem.
}
{
intros tin k (l&Hin&Hk). cbn. autorewrite with list.
infTer 4.
2:{
intros. infTer 4. intros. reflexivity.
}
cbn. unfold time,size in Hk. nia.
}
Qed.
Lemma SpecT (l:list X) ss:
TripleT ≃≃([],withSpace [|Contains _ l|] ss) (time c) M (fun _ => ≃≃([],withSpace [|Contains _ (c::l)|] (appSize [|fun s0 => s0 - size c - 1|] ss ))).
Proof.
unfold withSpace in *.
eapply Realise_TripleT. now apply Realise. now apply Terminates.
- intros tin yout tout H HEnc. cbn in *.
specialize (HEnc Fin0). simpl_vector in *; cbn in *. modpon H. tspec_solve.
- intros tin k HEnc Hk. cbn in *.
specialize (HEnc Fin0). simpl_vector in *; cbn in *. do 2 eexists. 2:assumption. contains_ext.
Qed.
End Fix.
End Cons_constant.
Ltac hstep_Cons_constant :=
match goal with
| [ |- TripleT ?P ?k (Cons_constant.M _) ?Q ] => eapply Cons_constant.SpecT
end.
Smpl Add hstep_Cons_constant : hstep_Spec.
From Undecidability Require Import CaseList WriteString Hoare.
Module Cons_constant.
Section Fix.
Context {Σ__X: finType} {X : Type} {cX : codable Σ__X X}.
Variable (c:X).
Definition M : pTM (sigList Σ__X)^+ unit 1 :=
WriteString Lmove (rev (inr sigList_cons::map (fun x => inr (sigList_X x)) ((encode c))));;
Move Lmove;;
Write (inl START).
Definition Rel : pRel (sigList Σ__X)^+ unit 1 :=
ignoreParam (
fun tin tout =>
forall l (s0 : nat),
tin[@Fin0] ≃(;s0) l ->
tout[@Fin0] ≃(;s0 - size c - 1) c :: l
).
Lemma Realise : M ⊨ Rel.
Proof.
eapply Realise_monotone.
{ unfold M. TM_Correct. eapply RealiseIn_Realise,WriteString_Sem. }
{
intros tin ((), tout) H. TMSimp.
destruct H2 as (?&->&?);cbn.
simpl_tape.
rewrite WriteString_L_left;cbn. autorewrite with list.
erewrite !tape_right_move_left.
2:{rewrite WriteString_L_current. autorewrite with list. cbn. reflexivity. }
rewrite WriteString_L_right. cbn.
eexists. repeat (cbn;autorewrite with list;try rewrite !map_map).
split. reflexivity.
rewrite tl_length,List.skipn_length. unfold size. nia.
}
Qed.
Definition time {sigX} {X : Type} {cX : codable sigX X} (c:X) := 5 + 2 * size c.
Lemma Terminates :
projT1 M ↓
(fun tin k =>
exists (l: list X) ,
tin[@Fin0] ≃ l /\
time c<= k).
Proof.
unfold Constr_cons_steps. eapply TerminatesIn_monotone.
{ unfold M. TM_Correct.
eapply RealiseIn_Realise. 2:eapply RealiseIn_TerminatesIn.
all:apply WriteString_Sem.
}
{
intros tin k (l&Hin&Hk). cbn. autorewrite with list.
infTer 4.
2:{
intros. infTer 4. intros. reflexivity.
}
cbn. unfold time,size in Hk. nia.
}
Qed.
Lemma SpecT (l:list X) ss:
TripleT ≃≃([],withSpace [|Contains _ l|] ss) (time c) M (fun _ => ≃≃([],withSpace [|Contains _ (c::l)|] (appSize [|fun s0 => s0 - size c - 1|] ss ))).
Proof.
unfold withSpace in *.
eapply Realise_TripleT. now apply Realise. now apply Terminates.
- intros tin yout tout H HEnc. cbn in *.
specialize (HEnc Fin0). simpl_vector in *; cbn in *. modpon H. tspec_solve.
- intros tin k HEnc Hk. cbn in *.
specialize (HEnc Fin0). simpl_vector in *; cbn in *. do 2 eexists. 2:assumption. contains_ext.
Qed.
End Fix.
End Cons_constant.
Ltac hstep_Cons_constant :=
match goal with
| [ |- TripleT ?P ?k (Cons_constant.M _) ?Q ] => eapply Cons_constant.SpecT
end.
Smpl Add hstep_Cons_constant : hstep_Spec.