coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] evar-aware destruct?, Jason Gross, 11/21/2014
- Re: [Coq-Club] evar-aware destruct?, Guillaume Melquiond, 11/21/2014
Archive powered by MHonArc 2.6.18.