The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

This is equivalent to assuming `Coq.Logic.ChoiceFacts.ConstructiveIndefiniteDescription_on _` of type `(exists x, P x) -> { x:A | P x }`.  If you have this, then I believe you can just do `refine (let H := _ in proj2_sig (ConstructiveIndefiniteDescription_axiom H))`

As for why this requires classical axioms, consider the case where you do `eexists ?[x]; pose ?x as y.`  And then you want to go back to the case where you just had `exists x, P x`, except whatever you use to fill in `x` will still be accessible as `y`.

On Thu, May 21, 2020 at 12:09 AM Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

Is there a way to undo eexists?

Suppose my goal is like:

....

---------

exists x, P x

Then I do eexists

....

---------

P ?x

Then I try to find a solution of ?x. This form with no quantifiers is easier to maniplulate the goal to find solutions. If I cannot find one, I would like to undo the eexists and make the goal as follows (perhaps this eexists should be done later when more info is available):

....

---------

exists x, P x

We would be grateful for ideas on how to achieve this.

Our actual problem is more complex and this "exists" is in an embedded logic (RHS of separation logic |--) that does not have Coq's nice constructivity properties that ensure (I think) that eexists always preserves provability of a goal.

Thanks

-- Abhishek

http://www.cs.cornell.edu/~aa755/