Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix steps tactic #190

Open
wants to merge 1 commit into
base: popl23ae
Choose a base branch
from
Open

Fix steps tactic #190

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions lib/Coqlib.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1459,6 +1459,15 @@ Ltac unseal x :=
end
.

Ltac seal_last_with key :=
refine (@eq_ind _ _ _ _ _ (@Seal.sealing_eq key _ _)).

Ltac seal_last :=
let key := fresh "key" in
assert (key:= "_deafult_");
seal_last_with key.


Notation "☃ y" := (Seal.sealing _ y) (at level 60, only printing).
Goal forall x, 5 + 5 = x. i. seal 5. seal x. Fail progress cbn. unseal key0. unseal 5. progress cbn. Abort.
Goal forall x y z, x + y = z. i. seal x. seal y. unseal y. unseal key. Abort.
Expand Down
10 changes: 6 additions & 4 deletions proofmode/HTactics.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -674,8 +674,9 @@ Ltac _force_l :=
let name := fresh "_GUARANTEE" in
destruct (classic P) as [name|name]; [ired_both; apply sim_itreeC_spec; eapply sim_itreeC_choose_src; [exists name]|contradict name]; cycle 1; clear name

| [ |- (gpaco8 (_sim_itree _ _) _ _ _ _ _ _ _ _ _ (_, ?i_src) (_, ?i_tgt)) ] =>
seal i_tgt; apply sim_itreeC_spec; econs; unseal i_tgt
| [ |- (gpaco8 (_sim_itree ?a0 ?a1) ?a2 ?a3 ?a4 ?a5 ?a6 ?a7 ?a8 ?a9 ?a10 (?a11, ?i_src) (?a12, ?i_tgt)) ] =>
change ((fun x => gpaco8 (_sim_itree a0 a1) a2 a3 a4 a5 a6 a7 a8 a9 a10 (a11, i_src) (a12, x)) i_tgt);
seal_last; apply sim_itreeC_spec; econs; unseal i_tgt
end
.

Expand All @@ -695,8 +696,9 @@ Ltac _force_r :=
let name := fresh "_ASSUME" in
destruct (classic P) as [name|name]; [ired_both; apply sim_itreeC_spec; eapply sim_itreeC_take_tgt; [exists name]|contradict name]; cycle 1

| [ |- (gpaco8 (_sim_itree _ _) _ _ _ _ _ _ _ _ _ (_, ?i_src) (_, ?i_tgt)) ] =>
seal i_src; apply sim_itreeC_spec; econs; unseal i_src
| [ |- (gpaco8 (_sim_itree ?a0 ?a1) ?a2 ?a3 ?a4 ?a5 ?a6 ?a7 ?a8 ?a9 ?a10 (?a11, ?i_src) (?a12, ?i_tgt)) ] =>
change ((fun x => gpaco8 (_sim_itree a0 a1) a2 a3 a4 a5 a6 a7 a8 a9 a10 (a11, x) (a12, i_tgt)) i_src);
seal_last; apply sim_itreeC_spec; econs; unseal i_src
end
.

Expand Down