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
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
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