Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] evar-aware destruct?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] evar-aware destruct?


Chronological Thread 
  • From: Guillaume Melquiond <guillaume.melquiond AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] evar-aware destruct?
  • Date: Fri, 21 Nov 2014 07:44:29 +0100

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



Archive powered by MHonArc 2.6.18.

Top of Page