The Coq mailing list

[Tom Payne <thp AT cs.ucr.edu>]

Adam Chlipala wrote:

Tom Payne wrote:

How do I use instances of multivariable propositional lemmas in a
subsequent proof?

Suppose I've proved a lemma, call it mylemma.  If it involves only one
propositional variable, I can subsequently use instances of it in
tactics, e.g., "case(mylemma(Q->R\/~R))."  But what if mylemma
involves two propositional varaiables, say P and Q ?  How can I
substitute say R\/~R for P and ~R for Q in mylemma and have a tactic
use that instance?  So far, my reading the manual and use of the
empirical method have failed to find an answer.

Coq has no special concept of "propositional variables."  These are just variables of type [Prop].  Some introductions to Coq treat propositional logic specially, to provide a gentler introduction for folks who aren't familiar with type theory, but I think your particular case is just complicated by that "simplification."

Lemmas whose statements begin with [forall] quantifiers are just functions.  In the example you gave above of a [case] invocation, you are just calling the function [mylemma] with the argument [Q->R\/~R].  You could just as well call such a function with two arguments, in the same way as you would call a two-argument function like [plus].  Try doing that with your two-argument lemma.

If that doesn't work, then the problem probably has to do with implicit arguments, where some arguments to functions aren't supposed to be specified, by default.  If you avoid running [Set Implicit Arguments] in your source file, this shouldn't be an issue for your own lemmas.

Hi Adam,

Thanks.  To summarize:

• I had tried "case(mylemma(R\/~R ~R))" and "case(mylemma(R\/~R, ~R))", and neither worked.
• From your advice, I first tried "case(mylemma R\/~R ~R))" and that didn't work either.
• I then tried "case( mylemma (R\/~R) (~R) )", and it worked perfectly!
  

Thanks again,
Tom Payne