Created
June 12, 2019 19:17
goal inclusion matching from jason
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Definition tmp {T} (x : T) := x. | |
Ltac first_goal_occurs_in_other_goal := | |
unshelve ( | |
repeat (let y := multimatch goal with | |
| [ |- context[?y] ] => y | |
| [ H : context[?y] |- _ ] => y | |
| [ H := context[?y] |- _ ] => y | |
end in | |
is_evar y; | |
lazymatch goal with | |
| [ H : tmp (y = y) |- _ ] => fail | |
| _ => pose proof (eq_refl y : tmp (y = y)) | |
end); | |
[ > | shelve_unifiable.. ]; | |
let n1 := numgoals in | |
shelve_unifiable; | |
let n2 := numgoals in | |
guard n2 < n1; | |
(* cleanup now *) | |
repeat match goal with | |
| [ H : tmp (_ = _) |- _ ] => clear H | |
end | |
). | |
Goal True. | |
unshelve epose (_:nat) as n. | |
all: first_goal_occurs_in_other_goal. | |
2: clear. | |
all: first_goal_occurs_in_other_goal. (* Error: Condition not satisfied: 2<2 *) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment