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?

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

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

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…

re easier proofs, the latter saves you from typing `forall`

and `intros`

.

you _might_ need `revert`

before induction, but that is probably clearer.

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: Jun 24 2024 at 14:01 UTC