Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Using tactics to build Existentials

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Using tactics to build Existentials


Chronological Thread 
  • 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:
(1) construct existentials using tactics or
(2) have some form of rewrite generate new goals rather than existentials?

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.

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





Archive powered by MHonArc 2.6.18.

Top of Page