The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

Hi Abishek,

In this particular example, I would do the step
destruct b.
before doing
eexists.

This seems to avoid the problem.  The way I would think of it is that 
the eexists step puts in one value (although you haven't yet worked out 
what it is) to satisfy the existential goal - and neither 1 nor 2 would 
be a satisfactory choice.  So you need to split the whole thing into two 
separate problems, each with its own existential goal.

Cheers,

Jeremy

On 16/1/21 8:18 am, Abhishek Anand wrote:
> eexists is very helpful in proofs because it lets us avoid 
> computing/simplifying complex things in our head and let Coq do all that 
> and almost figure out the right answer.
> However, the eexists implementation in Coq does not achieve the full 
> potential.
> For example, making cases is dangerous as it requires the value on both 
> sides to be equal:
>
> Require Import Nat.
>
> Lemma xx (b:bool): exists n, n = if b then 1 else 2.
>    eexists.
>    destruct b.
>    - reflexivity.
>    - (* cant prove 1=2 *)
> Abort.
>
> In the above simple/contrived, the right answer is immediately clear but 
> it is not the case in many proofs. Is there a way to ask destruct to 
> clone some chosen evars for each case as I did below manually:
>
> Lemma xxx (b:bool): exists n, n = if b then 1 else 2.
>    eexists.
>    Unshelve.
>    Focus 2.
>    evar (x:nat).
>    evar (y:nat).
>    exact (if b then ?x else ?y).
>    simpl.
>    destruct b.
>    - reflexivity.
>    - reflexivity.
> Qed.
>
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/