The Coq mailing list

[Siegfried <siegfried42 AT posteo.net>]

Hi,

On 15/01/2021 22:18, Abhishek Anand wrote:
> 
> 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.

I once needed something similar. I had a recursive Ltac that makes a
case analysis over a value and calls `shelve` when it can't destruct the
argument any more. Instead, you could `refine _` to create an unnamed evar.

The following code works, but produces warnings.

> Ltac destruct_shelve e :=
>   cbn in e;
>   let x1 := fresh "x" in
>   let x2 := fresh "x" in
>   first [ destruct e as [x1|x2]; [ try destruct_shelve x1 | try 
> destruct_shelve x2]; shelve
>         | destruct e as [x1]; [ try destruct_shelve x1 ]; shelve
>         | destruct e as []; shelve
>         ].
> 
> Lemma xx (b:bool): exists n, n = if b then 1 else 2.
>   eexists (ltac:(destruct_shelve b)).
>   destruct b.
>   - reflexivity.
>   - reflexivity.
> Qed.

Attachment: OpenPGP_signature
Description: OpenPGP digital signature