Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.)


Chronological Thread 
  • From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.)
  • Date: Wed, 23 Jul 2014 10:44:33 +0200


Instantiate deprecated?  I thought that was the way to handle evars manually.  How else?

Kinda sorta… ish.

Coq has a lot of backstory and stuff. So the treatment of existential variables is not superbly uniform. In trunk, the [refine] tactic introduces existential variable as goals. It is the preferred way to manipulate existential variable explicitly.

For instance, instead of [evar (P:Prop)], you can use [refine (let P:Prop := _ in _)] and get two goals: one for your goal with a new binding [P := ?x : Prop], and one (the first one actually) of type [Prop], whose solution will instantiate [?x] (and vice-versa, if [?x] is partially instantiated, the goal will be considered solved).

Now, it may not fit your needs. Since the new refine is new, and the possibilities are largely unexplored and suffer from limited support, you may still need [instantiate]. But hopefully, we can get rid of [instantiate] eventually: it's not a very elegant solution.



Archive powered by MHonArc 2.6.18.

Top of Page