I'm in a situation where I have a goal of the following form:
exists x : T1, f x = y.
where y : T2
and f : T1 -> T2
. The trick is that I've defined T1
and T2
in such a way that their constructors correspond, so for a human, it's easy to see what value of x
will make the equality hold.
But, I have a large number of cases, and want my script to be robust, so I'd like to automate finding such an x
.
How can I use proof search to find such a value for x
?
Right now I've got something like this (borrowing CPDT's crush tactic):
Ltac postpone :=
match goal with
| [ |- ?X] => let H := fresh "Arg" in evar (H : X); apply H
end
(unshelve eexists; [(constructor; postpone) | (crush ; fail) ]).
i.e. I create an evar for x
, unshelve it, solve it using constructor, filling in all the sub-goals generated by constructor with evars, then use proof search to determine the equality.
However, this gives: Error: Tactic failure.
My intention was that, if constructor
picked the wrong constructor, crush
would not solve the goal, so fail
would trigger backtracking. But this doesn't seem to be happening, it's failing the first time it hits fail
.
My Question
What strategies can I use to have proof-search find the value for an existential variable? How can I use constructor
's backtracking to find the value that makes an existential hold?
I think all you need is unshelve eexists; [ econstructor | solve [ crush ] ]
- solve [ ]
triggers backtracking in the first goal. Here's a working example of where that works. It includes some deferred goals created from arguments to T1's constructors.
Inductive T1 := T1A | T1B (x:unit) (H: x = x) | T1C (A:Type) (x:A) (H: x = x).
Inductive T2 := T2A | T2B | T2C.
Definition f (x:T1) : T2 :=
match x with
| T1A => T2A
| T1B _ _ => T2B
| T1C _ _ _ => T2C
end.
Ltac crush := auto.
Goal exists x, f x = T2C.
Proof.
unshelve eexists;
[ econstructor | solve [ crush ] ].