The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

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.