coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [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.