coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: "gallais @ ensl.org" <guillaume.allais AT ens-lyon.org>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Variant of [etransitivity] that accepts arguments?
- Date: Wed, 4 Jul 2012 16:32:22 -0400
Sorry if my question wasn't clear. I'm looking for a way to pass a partially filled out _expression_ to (e)transitivity, where blanks are turned into existential variables, a la (e)apply or [refine].
So, for example, I want to be able to do something like
Goal forall a b b' c : nat, a + b + c = a + b' + c.
intros; etransitivity (a + _ + c).
But I get
Syntax error: '.' or '...' expected after [tactic:tactic] (in [proof_mode:subgoal_command]).
on the [etransitivity] there.
-Jason
On Wed, Jul 4, 2012 at 4:10 PM, gallais @ ensl.org <guillaume.allais AT ens-lyon.org> wrote:
Hi Jason,
I'm not sure I understood your question but isn't [transitivity]
what you are looking for? The [e] in [etransitivity] stands for
"existential" which means that it is a variant of the normal
tactic that introduces existential variables when it's not able
to figure out what a needed term ought to be.
Just like you have (e)transitivity, there's also (e)rewrite,
(e)apply, etc.
Cheers,
--
gallais
On 4 July 2012 21:01, Jason Gross <jasongross9 AT gmail.com> wrote:
> Is there a variant of [etransitivity] that accepts an argument, so that I
> can help Coq along in figuring out how to do transitivity? That is, is
> there a tactic that I can pass along an _expression_ [expr], which has some
> underscores in it, and which will do something like
> match goal with
> | [ |- @eq ?A ?a ?b ] => eapply (@eq_trans A a foo b)
> end.
> except that it will work with any parametric relation declared to be
> transitive?
>
> If I try [etransitivity foo], I get
> Toplevel input, characters 35-36:
> Syntax error: '.' or '...' expected after [tactic:tactic] (in
> [proof_mode:subgoal_command]).
>
> Thanks!
>
> -Jason
- [Coq-Club] Variant of [etransitivity] that accepts arguments?, Jason Gross, 07/04/2012
- Message not available
- Re: [Coq-Club] Variant of [etransitivity] that accepts arguments?, Jason Gross, 07/04/2012
- Message not available
Archive powered by MHonArc 2.6.18.