coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: t x <txrev319 AT gmail.com>
- To: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
- Cc: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Using tactics to build Existentials
- Date: Sat, 17 Aug 2013 17:51:18 +0000
(1) This is really cool. I was hoping there was a way to extend refine's ability to "fill in the missing parts"
(2) This also only works on _goals_ right? Since "refine" is a generalized apply, I can't use this technique to rewrite an existing hypothesis (rather than a goal).Thanks!
On Sat, Aug 17, 2013 at 12:42 PM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:
On 17/08/2013 14:32, t x wrote:Have you tried the refine tactic? You give it a partial term corresponding to the part of the proof you're building, and it turns the holes into goals.
(1) construct existentials using tactics or
(2) have some form of rewrite generate new goals rather than existentials?
To simulate a rewrite, you have to refine a term on [eq_rect], like this for instance:
Goal forall m n, m + S n = S (m + n).
Proof.
intros m n.
refine (eq_rect _ _ _ _ (plus_Sn_m _ _)).
Abort.
PMP
- [Coq-Club] Using tactics to build Existentials, t x, 08/17/2013
- Re: [Coq-Club] Using tactics to build Existentials, Pierre-Marie Pédrot, 08/17/2013
- Re: [Coq-Club] Using tactics to build Existentials, t x, 08/17/2013
- Re: [Coq-Club] Using tactics to build Existentials, Dmitry Grebeniuk, 08/17/2013
- Re: [Coq-Club] Using tactics to build Existentials, t x, 08/18/2013
- Re: [Coq-Club] Using tactics to build Existentials, Dmitry Grebeniuk, 08/17/2013
- Re: [Coq-Club] Using tactics to build Existentials, t x, 08/17/2013
- Re: [Coq-Club] Using tactics to build Existentials, Jason Gross, 08/17/2013
- Re: [Coq-Club] Using tactics to build Existentials, Pierre-Marie Pédrot, 08/17/2013
Archive powered by MHonArc 2.6.18.