The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 21/11/2014 04:35, Jason Gross wrote:
> Hi,
> Is there any way to destruct a variable in a way that results in the
> fresh hypotheses being accessible from an evar?  I would like something
> like the following to work:
>
>    Ltac evar1_aware_destruct_nat n :=
>      instantiate (1 := match n with 0 => _ | _ => _ end);
>      let n' := fresh "n'" in
>      destruct n as [|n'].
>
>    Goal forall n : nat, exists n0, match n with 0 => 0 | S n' => S n'
> end = n0.
>    Proof.
>      intros.
>      eexists.
>      evar1_aware_destruct_nat n; [ reflexivity | ].
>      instantiate (1 := n'). (* Error: Instance is not well-typed in the
> environment of ?589 *)

That is because n' is not in the environment of your evar, so it is 
fortunate that Coq complains. (Otherwise it would be trivial to prove 
False.) So you have to make sure it somehow is:

instantiate (1 := match n with 0 => _ | S m => _ m end).

Best regards,

Guillaume