From Undecidability.TM.Hoare Require Import HoareLogic.
Definition abbreviate {A:Type} (x:A) := x.
Arguments abbreviate {A} {x}.
Tactic Notation "abbreviate" constr(y) "as" ident(x) :=
(first [ is_var y
| let x' := fresh x in pose (x':= @abbreviate _ y);
change y with x']).
Tactic Notation "abbreviate" constr(y) ":" constr(t) "as" ident(x) :=
(first [ is_var y
| let x' := fresh x in pose (x':= @abbreviate t y);
change y with x']).
Ltac unfold_abbrev :=
repeat match goal with H := @abbreviate _ _ |- _ =>
unfold H, abbreviate; clear H
end.
Ltac clear_abbrevs := repeat match goal with
| H := @abbreviate (_ -> Assert _ _) _ |- _ => clear H
| H := @abbreviate (Assert _) _ |- _ => clear H
end.
Ltac force_sequential :=
lazymatch goal with
| |- TripleT _ _ _ ?P => abbreviate P as POSTCONDITION
| |- Triple _ _ ?P => abbreviate P as POSTCONDITION
end.
Ltac abbreviate_TM := force_sequential.
Ltac start_TM := abbreviate_TM.
Definition abbreviate {A:Type} (x:A) := x.
Arguments abbreviate {A} {x}.
Tactic Notation "abbreviate" constr(y) "as" ident(x) :=
(first [ is_var y
| let x' := fresh x in pose (x':= @abbreviate _ y);
change y with x']).
Tactic Notation "abbreviate" constr(y) ":" constr(t) "as" ident(x) :=
(first [ is_var y
| let x' := fresh x in pose (x':= @abbreviate t y);
change y with x']).
Ltac unfold_abbrev :=
repeat match goal with H := @abbreviate _ _ |- _ =>
unfold H, abbreviate; clear H
end.
Ltac clear_abbrevs := repeat match goal with
| H := @abbreviate (_ -> Assert _ _) _ |- _ => clear H
| H := @abbreviate (Assert _) _ |- _ => clear H
end.
Ltac force_sequential :=
lazymatch goal with
| |- TripleT _ _ _ ?P => abbreviate P as POSTCONDITION
| |- Triple _ _ ?P => abbreviate P as POSTCONDITION
end.
Ltac abbreviate_TM := force_sequential.
Ltac start_TM := abbreviate_TM.