The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Hello Judy,

Your questions look a beginner's questions.  Normally, I don't answer 
these questions,
because I believe that such question were actually given by an 
instructor as homework
assignment.  Still I am willing to help:

In you examples, there are lines that don't make sense:

x y m:nat.

Such a line can only be a fragment of a legitimate Coq command, what 
keyword do you
want to put in front?

The same holds for "P(x y m:nat):Prop:= ... x<>5).", but we may guess that
you assume the keyword "Definition" to be placed in front in this case.

Next, with your second definition of P, we can show that P x y m holds 
exactly when
(x<>4) and (x<>5).  This is probably not what you intend.

So, I believe you should try finding the right combination of \/ /\ -> 
and = that will
give a well-formed predicate definition and then check that this 
predicate definition
fits your needs.  Thus, you should be able to perform the following 
proofs where the "..."
represents work to be done by you.

Definition P(x y m:nat) := ...

Lemma verify_P1 : P 5 3 0.
...
Qed.

Lemma verify_P2 : P 4 10 10.
...
Qed.

Lemma verify_P3 : P 3 2 1.
...
Qed.

Obviously, the three verification lemmas don't capture all of your 
specification, but
it is often useful to prove restricted verification lemmas like these to 
make sure your
specification captures your initial intent.

Yves