Stream: Coq users

Topic: Why parameter outside in lemmas?

Julin S (Jun 12 2022 at 06:02):

Not sure if it's a correct observation but I think coq theorems and lemmas that take a parameter are usually defined like

Theorem thm1 : forall n:nat, n + 0 = n.

with the parameter 'outside' rather than

Theorem thm1'  (n:nat) : n + 0 = n.

with parameter 'inside'.

Is there any reason for that?

Paolo Giarrusso (Jun 12 2022 at 06:06):

It’s a matter of style, and there are projects that prefer the latter…

Julin S (Jun 12 2022 at 06:14):

Okay, I thought maybe it leads to easier proofs or something. Thanks!

Paolo Giarrusso (Jun 12 2022 at 06:15):

they are completely equivalent in Coq (and in type theory), but they might not be in other logics; so maybe the first style is more readable if you’re not familiar with type theory/Coq? But at least for most of my code, such readers are not in the target audience anyway…

Paolo Giarrusso (Jun 12 2022 at 06:16):

re easier proofs, the latter saves you from typing forall and intros.

Paolo Giarrusso (Jun 12 2022 at 06:16):

you _might_ need revert before induction, but that is probably clearer.

Paolo Giarrusso (Jun 12 2022 at 06:29):

For instance, in this proof I chose to have forall n : nat, m + n = n + m as induction hypothesis, and the first proof makes this explicit via revert:

Theorem add_comm m n : m + n = n + m.
Proof.
  revert n; induction m as [|m IHm]; intros n. easy.
  now rewrite <-plus_n_Sm, <-IHm.
Qed.

Theorem add_comm' : forall m n, m + n = n + m.
Proof.
  induction m as [|m IHm]; intros n. easy.
  (* induction m as [|m IHm]. easy.  *)
  now rewrite <-plus_n_Sm, <-IHm.
Qed.

(this lemma isn't the best example because the generalization is not needed here, but better examples exist).

Last updated: Apr 19 2024 at 11:02 UTC