From Undecidability Require Import TMTac.
From Undecidability Require Import TM.Hoare.HoareLogic TM.Hoare.HoareCombinators TM.Hoare.HoareRegister TM.Hoare.HoareTacticsView.
From smpl Require Import Smpl.
Ltac contains_evar e := has_evar e.
Ltac triple_with_space :=
lazymatch goal with
| [ |- context [withSpace] ] => idtac
end.
Smpl Create hstep_Spec.
Ltac hstep_Spec := smpl hstep_Spec.
Ltac hstep_Seq :=
match goal with
| [ |- Triple ?P (?M1;; ?M2) ?Q ] => eapply Seq_Spec
| [ |- TripleT ?P ?k (?M1;; ?M2) ?Q ] => eapply Seq_SpecT
end.
Ltac hstep_If :=
cbn beta;
lazymatch goal with
| [ |- Triple _ (If ?M1 ?M2 ?M3) _ ] => eapply If_Spec
| [ |- TripleT ≃≃( _,_) ?k (If ?M1 ?M2 ?M3) _ ] =>
eapply If_SpecTReg with (R:= fun y => (_,_)) (Q:= fun y => (_,_))
| [ |- TripleT ?P ?k (If ?M1 ?M2 ?M3) ?Q ] => eapply If_SpecT
end.
Ltac hstep_Switch :=
lazymatch goal with
| [ |- Triple ?P (Switch ?M1 ?M2) ?Q ] => eapply Switch_Spec
| [ |- TripleT ?P ?k (Switch ?M1 ?M2) ?Q ] => eapply Switch_SpecT
end.
Ltac hstep_Return :=
lazymatch goal with
| [ |- Triple ?P (Return ?M ?x) ?Q ] =>
(eapply Return_Spec_con)
| [ |- TripleT ?P ?k (Return ?M ?x) ?Q ] =>
(eapply Return_SpecT_con)
| [ |- Triple ?P (Relabel ?M ?f) ?Q ] =>
(eapply Relabel_Spec_con)
| [ |- TripleT ?P ?k (Relabel ?M ?f) ?Q ] =>
(eapply Relabel_SpecT_con)
end.
Ltac hstep_LiftTapes :=
lazymatch goal with
| [ |- Triple ?PRE (LiftTapes ?M ?I) ?POST ] =>
tryif contains_evar POST then
(tryif triple_with_space
then (eapply LiftTapes_Spec_space with (Q':= fun y => _) (Q:= fun y => _); [smpl_dupfree | ])
else (eapply LiftTapes_Spec with (Q':= fun y => _) (Q:= fun y => _); [smpl_dupfree | ]))
else
(tryif triple_with_space then (eapply LiftTapes_Spec_space_con with (R':= fun y => _) (R:= fun y => _); [smpl_dupfree | | ])
else (eapply LiftTapes_Spec_con with (R':= fun y => _) (R:= fun y => _); [smpl_dupfree | | ]))
| [ |- TripleT ?PRE ?k (LiftTapes ?M ?I) ?POST ] =>
tryif contains_evar POST then
(tryif triple_with_space then (refine (LiftTapes_SpecT_space (Q':= fun y => _) (Q:= fun y => _) _ _); [smpl_dupfree | ])
else (refine (LiftTapes_SpecT (Q':= fun y => _) (Q:= fun y => _) _ _); [smpl_dupfree | ]))
else
(tryif triple_with_space then (eapply LiftTapes_SpecT_space_con with (R':= fun y => _) (R:= fun y => _); [smpl_dupfree | | ])
else (eapply LiftTapes_SpecT_con with (R':= fun y => _) (R:= fun y => _); [smpl_dupfree | | ]))
end.
Ltac hstep_ChangeAlphabet :=
lazymatch goal with
| [ |- Triple ?PRE (ChangeAlphabet ?M ?I)?POST ] =>
tryif contains_evar POST then
(tryif triple_with_space then (eapply ChangeAlphabet_Spec_space_pre with (Q:= fun y => _) (Q0:= fun y => _); [ | ])
else (eapply ChangeAlphabet_Spec_pre with (Q:= fun y => _) (Q0:= fun y => _); [ | ]))
else
(tryif triple_with_space then (eapply ChangeAlphabet_Spec_space_pre_post with (Q':= fun y => _) (Q0:= fun y => _); [ | | ])
else (eapply ChangeAlphabet_Spec_pre_post with (Q':= fun y => _) (Q':= fun y => _) (Q0:= fun y => _); [ | | ]))
| [ |- TripleT ?PRE ?k (ChangeAlphabet ?M ?I)?POST ] =>
tryif contains_evar POST then
(tryif triple_with_space then (eapply ChangeAlphabet_SpecT_space_pre with (Q:= fun y => _) (Q0:= fun y => _); [ | ])
else (eapply ChangeAlphabet_SpecT_pre with (Q:= fun y => _) (Q0:= fun y => _); [ | ]))
else
(tryif triple_with_space then (eapply ChangeAlphabet_SpecT_space_pre_post with (Q':= fun y => _) (Q0:= fun y => _); [ | | ])
else (eapply ChangeAlphabet_SpecT_pre_post with (Q:= fun y => _) (Q':= fun y => _) (Q0:= fun y => _); [ | | ]))
end.
Local Tactic Notation "noSpace" tactic(t) :=
let test :=
tryif triple_with_space
then fail
else reflexivity
in
lazymatch goal with
| [ |- Triple ?P ?M ?Q ] =>
eapply Consequence_pre;[t| test ]
| [ |- TripleT ?P _ ?M ?Q ] =>
eapply ConsequenceT_pre;[t| test |reflexivity]
end || fail "could not find user-rule applicable here".
Ltac hstep_user :=
lazymatch goal with
| [ |- Triple ?P ?M ?Q ] =>
tryif contains_evar Q then
(tryif triple_with_space then
((eapply TripleT_Triple; hstep_Spec)
|| (hstep_Spec))
else ((eapply TripleT_Triple;refine (TripleT_RemoveSpace (Q:=fun y => _) (Q':=fun y => _) _); now (intros; hstep_Spec))
|| (refine (TripleT_RemoveSpace (Q:=fun y => _) (Q':=fun y => _) _); now (intros; hstep_Spec))
|| (eapply TripleT_Triple; hstep_Spec)
|| (noSpace hstep_Spec)))
else (eapply Consequence_post; [ hstep_user | ])
| [ |- TripleT ?P ?k ?M ?Q ] =>
tryif contains_evar Q then
(tryif triple_with_space then hstep_Spec
else (refine (TripleT_RemoveSpace (Q:=fun y => _) (Q':=fun y => _)_); now (intros; hstep_Spec))
|| (noSpace hstep_Spec))
else (eapply ConsequenceT_post; [ hstep_user | ])
end.
Ltac hstep_Nop :=
lazymatch goal with
| [ |- TripleT ?P ?k Nop ?Q ] => eapply Nop_SpecT
end.
Smpl Add hstep_Nop : hstep_Spec.
Ltac hstep_forall_unit :=
hnf;
lazymatch goal with
| [ |- unit -> ?H ] => intros _
| [ |- forall (y : finType_CS unit), ?H] => intros []
| [ |- forall (y : unit), ?H] => intros []
end.
Ltac hstep_pre := clear_abbrevs;cbn beta.
Ltac hstep_post := lazy beta.
Ltac hstep_Combinators := hstep_Seq || hstep_If || hstep_Switch || hstep_Return. Ltac hstep_Lifts := (hstep_LiftTapes || hstep_ChangeAlphabet).
Ltac hstep := hstep_pre; (hstep_forall_unit || hstep_Combinators || hstep_Lifts || hstep_user); hstep_post.
Ltac hsteps := repeat first [hstep | hstep_post] .
Ltac hsteps_cbn := repeat (cbn; hstep).
Ltac openFoldRight :=
try (hnf;
lazymatch goal with
| |- _ /\ _ => refine (conj _ _);[ | openFoldRight]
| |- True => exact I
end).
Ltac tspec_solve :=
lazymatch goal with
| [ |- tspec (_,withSpace _ ?ss) ?t ] =>
eapply tspec_space_solve;openFoldRight;[ .. | intros i; destruct_fin i;
cbn [tspec_single withSpace_single Vector.map Vector.nth Vector.case0 Vector.caseS]; try (simple apply I || contains_ext || isVoid_mono)]
| [ |- tspec (?P,?R) ?t ] =>
eapply tspec_solve;openFoldRight;[ .. | intros i; destruct_fin i;
cbn [tspec_single Vector.nth Vector.case0 Vector.caseS]; try (simple apply I || contains_ext || isVoid_mono)]
end.
Ltac trySolveTrivEq := lazymatch goal with |- ?s = ?s => reflexivity | |- _ => idtac end.
Ltac tspec_ext :=
unfold_abbrev;intros;
lazymatch goal with
| [ |- Entails (tspec _) (tspec _) ] => simple apply EntailsI;intros ? ?; tspec_ext
| [ |- forall t, t ≃≃ ?P -> t ≃≃ ?Q ] =>
let Ht := fresh "H"t in
intros t Ht; tspec_ext; eauto
| [ H : tspec (_,withSpace _ ?ss) ?t |- tspec (_,withSpace _ ?ss') ?t ] =>
apply tspec_space_ext with (1 := H);[ cbn [implList];intros; openFoldRight;trySolveTrivEq |
((now eauto)
|| (intros i; destruct_fin i;
cbn [tspec_single withSpace_single Vector.nth Vector.case0 Vector.caseS];
intros; try (simple apply I ||contains_ext || isVoid_mono)))]
| [ H : tspec (?P',?R') ?t |- tspec (?P,?R) ?t ] =>
apply tspec_ext with (1 := H);[ cbn [implList];intros; openFoldRight;trySolveTrivEq |
((now eauto)
|| (intros i; destruct_fin i;
cbn [tspec_single Vector.nth Vector.case0 Vector.caseS];
intros; try (simple apply I || contains_ext || isVoid_mono)))]
end.
Ltac underBinders t :=
lazymatch goal with
| |- forall x, _ => let x := fresh x in intros x;underBinders t;revert x
| |- _ => t
end.
Ltac introPure_prepare :=
lazymatch goal with
| |- Entails (tspec ((_,_))) _ => eapply tspec_introPure
| |- Triple (tspec (?P,_)) _ _ => eapply Triple_introPure
| |- TripleT (tspec (?P,_)) _ _ _ => eapply TripleT_introPure
end;simpl implList at 1.
Tactic Notation "hintros" simple_intropattern_list(pat) := underBinders introPure_prepare;intros pat.
Ltac hstep_seq :=
lazymatch goal with
| |- ?R (_;;_) _ => hstep;[(hstep;hsteps_cbn;cbn);let n := numgoals in (tryif ( guard n = 1) then try tspec_ext else idtac ) |cbn;try hstep_forall_unit | reflexivity..]
| |- ?R (LiftTapes _ _) _ => hsteps_cbn
| |- ?R (ChangeAlphabet _ _) _ => hsteps_cbn
end.