Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] evar-aware destruct?


Chronological Thread 
  • From: Jason Gross <jasongross9 AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] evar-aware destruct?
  • Date: Thu, 20 Nov 2014 22:35:35 -0500

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 *)

Thanks,
Jason



Archive powered by MHonArc 2.6.18.

Top of Page