The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

Abhishek,

Your issue sounds similar to something I raised a few years ago:

https://github.com/jonleivent/ceps/blob/patch-1/text/011-coevolving-evars.md

Jonathan

On Fri, 15 Jan 2021 22:48:07 +0100
Hugo Herbelin <Hugo.Herbelin AT inria.fr> wrote:

> Hi Abhishek,
> 
> I don't know who would have the opportunity to implement it, a way or
> another, but that seems indeed to be a very good idea!
> 
> Best,
> 
> Hugo
> 
> On Fri, Jan 15, 2021 at 01:18:37PM -0800, 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/