The Coq mailing list

[t x <txrev319 AT gmail.com>]

(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