Search code examples
coq

Coq syntax for defining lemmas

I can see the different syntax of Coq for defining lemmas. For example, Lemma plus_n_O: forall n:nat, n = n + 0. and Lemma plus_n_O n: n = n + 0. both define that the sum of zero by any number is equal to the number. How these definitions differ? Or this is a new feature of Coq to remove forall quantifier from definitions.

Solution

  • These two definitions are essentially equivalent. Generally speaking, any statement of the form

    Lemma foo x y z : P.
Proof.
(* ... *)

    is equivalent to

    Lemma foo : forall x y z, P.
Proof.
intros x y z.
(* ... *)