Using backtracking to find value for existential in Coq

Question

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?

Answer 1

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 ] ].