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: Dmitry Grebeniuk <gdsfh1 AT gmail.com>
  • To: t x <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Using tactics to build Existentials
  • Date: Sat, 17 Aug 2013 22:52:41 +0300

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.



Archive powered by MHonArc 2.6.18.

Top of Page