Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Variant of [etransitivity] that accepts arguments?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Variant of [etransitivity] that accepts arguments?


Chronological Thread 
  • 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




Archive powered by MHonArc 2.6.18.

Top of Page