## 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: Dec 05 2023 at 12:01 UTC