Need explanation of how the stdlib creates Nat.add_comm (Include and modules)

[jfehrle]

I wanted to use Nat.add_comm in a proof. I expected to find it in Init/Nat.v. It's not there, nor did I find any Theorem add_comm anywhere in the standard library. It appears that this is defined in Arith/PeanoNat.v by the command

Include NBasicProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.

Looking at the definitions of NBasicProp and the modules, I don't see anything that seems related to defining add_comm.

If someone can explain how add_comm is created by this command and the meaning of <+ here, I'll add something covering that to the doc.

This doesn't seem very easily discoverable by users. Also, Search Nat.add_comm seems broken:

Require Import PeanoNat.
Search "add".   (* includes Nat.add_comm *)
Search "+".     (* includes Nat.add_comm *)
Search Nat.add_comm.   (* no output *)
Search add_comm.    (* The reference add_comm was not found in the current environment. *)

FWIW, the proof term for Nat.add_comm is 55 lines, probably machine generated. I expect a handwritten proof would be considerably shorter.

[olaure01]

I am not at all an expert in modules, but here is the path which I think generates Nat.add_comm in PeanoNat:

add_comm --[NZAdd.v]--> Module Type NZAddProp --[NZMul.v]--> Module Type NZMulProp [[Include NZAddProp]] --[NZAddOrder.v]--> Module Type NZAddOrderProp [[Include NZMulProp]] --[NZMulOrderProp.v]--> Module Type NZMulOrderProp [[Include NZAddOrderProp]] --[NZProperties.v]--> Module Type NZProp := NZMulOrderProp. --[NBase.v]--> Module NBaseProp [[Include NZProp]] --[NAdd.v]--> Module NAddProp [[Include NBaseProp] --[NOrder.v]--> Module NOrderProp [[Include NAddProp] --[NAddOrder.v]--> Module NAddOrderProp [[Include NOrderProp]] --[NMulOrder.v]--> Module NMulOrderProp [[Include NAddOrderProp]] --[NSub.v]--> Module NSubProp [[Include NMulOrderProp]] --[NMaxMin.v]--> Module Type NMaxMinProp [[Include NSubProp]] --[NProperties.v]--> Module Type NBasicProp (N:NAxiomsMiniSig) := NMaxMinProp N. --[PeanoNat.v]--> Include NBasicProp.

The definition is apparently handwritten in NZAdd.v:

Theorem add_comm : forall n m, n + m == m + n.
Proof.
  intros n m; nzinduct n.
  - now nzsimpl.
  - intro. nzsimpl. now rewrite succ_inj_wd.
Qed.

Here is a kind of shorten PeanoNat which more direclty accesses this definition:

Require Import NAxioms.
Include Coq.Init.Nat.

(** When including property functors, inline t eq zero one two lt le succ *)

Set Inline Level 50.

(** All operations are well-defined (trivial here since eq is Leibniz) *)

Definition eq_equiv : Equivalence (@eq nat) := eq_equivalence.
Local Obligation Tactic := simpl_relation.
Program Instance succ_wd : Proper (eq==>eq) S.
Program Instance pred_wd : Proper (eq==>eq) pred.
Program Instance add_wd : Proper (eq==>eq==>eq) plus.
Program Instance sub_wd : Proper (eq==>eq==>eq) minus.
Program Instance mul_wd : Proper (eq==>eq==>eq) mult.

(** Bi-directional induction. *)

Theorem bi_induction :
  forall A : nat -> Prop, Proper (eq==>iff) A ->
    A 0 -> (forall n : nat, A n <-> A (S n)) -> forall n : nat, A n.
Proof.
intros A A_wd A0 AS. apply nat_ind. assumption. intros; now apply -> AS.
Qed.

(** ** Remaining constants not defined in Coq.Init.Nat *)

(** NB: Aliasing [le] is mandatory, since only a Definition can implement
    an interface Parameter... *)
Definition eq := @Logic.eq nat.
Definition le := Peano.le.
Definition lt := Peano.lt.

(** ** Basic specifications : pred add sub mul *)

Lemma pred_succ n : pred (S n) = n.
Proof.
reflexivity.
Qed.

Lemma pred_0 : pred 0 = 0.
Proof.
reflexivity.
Qed.

Lemma one_succ : 1 = S 0.
Proof.
reflexivity.
Qed.

Lemma two_succ : 2 = S 1.
Proof.
reflexivity.
Qed.

Lemma add_0_l n : 0 + n = n.
Proof.
reflexivity.
Qed.

Lemma add_succ_l n m : (S n) + m = S (n + m).
Proof.
reflexivity.
Qed.

Lemma sub_0_r n : n - 0 = n.
Proof.
now destruct n.
Qed.

Lemma sub_succ_r n m : n - (S m) = pred (n - m).
Proof.
revert m. induction n; intro m; destruct m; simpl; auto. apply sub_0_r.
Qed.

Lemma mul_0_l n : 0 * n = 0.
Proof.
reflexivity.
Qed.

Lemma mul_succ_l n m : S n * m = n * m + m.
Proof.
assert (succ_r : forall x y, x+S y = S(x+y)) by now intro x; induction x.
assert (comm : forall x y, x+y = y+x).
{ intro x; induction x; simpl; auto. intros; rewrite succ_r; now f_equal. }
now rewrite comm.
Qed.

Include NZBase.NZBaseProp.
Include NZAdd.NZAddProp.

About add_comm.

To conclude, I have also been facing troubles going trough the Arith part of the standard library. This includes files marked as "mostly obsolete" (see #11356 and discourse ). I think there is clearly room here for documentation and cleaning, and would be happy to be involved if something is done into this direction.

[jfehrle]

Thanks. Somehow I missed seeing the theorem itself.

Is there much need for tooling that tells you the path for including a theorem? Print Module PeanoNat seems broken; all it says is Module PeanoNat := Struct Module Nat End. Shouldn't it do something like list all the members (perhaps recursively)? That might be helpful for untangling the theorems and modules.

Should there be a way for the user to give a theorem name and get the path through the modules?

I think there is clearly room here for documentation and cleaning, and would be happy to be involved if something is done into this direction.

Sounds worth improving, but not an area I focus on.

[olaure01]

Print Module PeanoNat seems broken; all it says is Module PeanoNat := Struct Module Nat End.

Is it really surprising? Print Module Nat then gives you its own content (however no detailed path inclusion information).

[jfehrle]

Ah, I didn't notice that everything in PeanoNat is the Nat module. Of course Print Module Nat is different from Print Module PeanoNat.Nat; the former doesn't contain add_comm. It's hard to know what to expect because the documentation doesn't cover many of the details. The differing behaviors seem unintuitive.

[olaure01]

As far as I can see, the following:

Require Import PeanoNat.
Print Module Nat.
Print Module PeanoNat.Nat.

gives twice the same output for me.

[jfehrle]

These give different output, that's a bit unexpected:

Print Module Nat.
Require Import PeanoNat.
Print Module Nat.

[olaure01]

The first one should give the content of the file Nat.v, loaded from Init. Nat is then overridden by PeanoNat.Nat:

About Nat.
Require Import PeanoNat.
About Nat.

[jfehrle]

@gares Related to the Print Module item you added to the Coq call for Jan 13.

[JasonGross]

Also, Search Nat.add_comm seems broken:

I think you're looking for Locate, not Search; the latter looks for definitions whose types mention Nat.add_comm