coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jonathan, 07/22/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jason Gross, 07/22/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jonathan, 07/22/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jason Gross, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jonathan, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Arnaud Spiwack, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Xavier Leroy, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Arnaud Spiwack, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jonathan, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jason Gross, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jonathan, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jason Gross, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jonathan, 07/23/2014
- [Coq-Club] nice evar tactics (was: Re: Prop smuggling (was: Re: Smart case analysis in Coq.)), Jonathan, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Arnaud Spiwack, 07/24/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jonathan, 07/24/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Xavier Leroy, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Arnaud Spiwack, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jonathan, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jason Gross, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jonathan, 07/22/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jason Gross, 07/22/2014
Archive powered by MHonArc 2.6.18.