The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

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/