The Coq mailing list

[t x <txrev319 AT gmail.com>]

(2) Very cool. Thanks for the trick.

(1) I apologize for this. This was a meant to be a comment, not a question, referring to my excitement that "refine (eq_rect .. )" was basically a "refine-rewrite"

On Sat, Aug 17, 2013 at 7:52 PM, Dmitry Grebeniuk <gdsfh1 AT gmail.com> wrote:

Hello.

> (1) This is really cool. I was hoping there was a way to extend refine's
> ability to "fill in the missing parts"

  What do you mean?  Give an example of building a term with "refine"
first, so people can help you.

> (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).

  You can do it.

Goal forall A (P : A -> Prop) (a : A) (H : P a) b (E : a = b), P b.
intros.
refine (let H0 := eq_ind _ _ H _ E in _).
exact H0.

(note that last two lines can be replaced with
refine (let H0 := eq_ind _ _ H _ E in H0).
)

  Generally, "refine (let H ...)" adds hypothesis H.
You can fill the body of H with "let H := thebody in ..." or leave it
empty just specifying the type with "let H : thetype := _ in ...",
then you will be prompted to build a value of thetype and the value
will be available as "H" later.