How do you import part of the standard library in Coq?

Question

How do you import part of the standard library in Coq?

• How do you import Nat specifically?
• Why is reporting Nat not required to use +?

I did the warmup exercise of proving commutativity of addition in Coq, as described here. I have a verbose solution in Appendix A of this question.

I added a slightly modified version of Lemma comm_plus in Nick Dattani's answer to the buffer.

This isn't the entire proof. coqtop (via Proof-General) refuses to advance past Nat.add_0_r.

Theorem comm_plus_truenat: forall a b, a + b = b + a.
Proof.
  intros. induction a.
  - simpl.
    symmetry.
    apply Nat.add_0_r.
Qed

Attempting to run this incomplete proof produces the error Error: The reference Nat.add_0_r was not found in the current environment..

This makes sense, I haven't imported the Nat library.

However, adding Require Nat., adding Import Nat., and adding both all produce the same error message.

How does one import Nat (or another part of the standard library)? I'm also curious why the theorem which uses +, wasn't rejected.

---

Appendix A:

verbose, extremely naive proof of commutativity of natural number addition in Coq.

---

Inductive nat : Set :=
| O : nat
| S : nat -> nat .

Fixpoint plus (a b : nat) {struct a} : nat :=
  match a with
  | O => b
  | S a'' => S (plus a'' b)
  end.

Theorem comm_plus: forall (a b : nat), plus a b = plus b a.
Proof.
  induction a.
  intros.
  simpl.
  unfold plus.
  induction b.
  tauto.
  simpl.
  simpl in IHb.
  f_equal.
  tauto.
  intros.
  simpl.
  rewrite IHa.
  induction b.
  simpl.
  tauto.
  simpl.
  f_equal.
  tauto.
Qed.
```

Answer 1

The recommended import to get the many lemmas associated with nat is Require Import Arith. This includes PeanoNat.

Similarly, for N import NArith and for Z import ZArith.

Answer 2

I would recommend using Require Import Arith. as suggested by Li-yao. To add to this answer, the reason why + is in scope when you start using Coq without importing anything is because Coq's library has a "prelude" which imports a few basic notions that are really useful to have everywhere. This includes not only operators such as + (notation for Nat.add BTW), but also the definition of natural numbers and even of = (none of this is a primitive notion in Coq's language). In fact, even the implication arrow (->) is a notation that is defined in Coq's prelude.

You can run Coq without the prelude, and some (like the HoTT library) actually rely on this. To do this, you can pass the -noinit option to coqtop or coqide. If you use this option, then your initial statement won't work anymore, and even the code from your appendix won't (because you rely on things like -> and =... and tactics, which are also not loaded by default with this option).

Answer 3

In order for Nat.add_0_r to be in scope, one must add Require Import Coq.Arith.PeanoNat..

The documentation for this library is here.

Here is the explanation of what the Nat module is, which is inside this library is and what signatures it implements.

Module Nat
 <: NAxiomsSig
 <: UsualDecidableTypeFull
 <: OrderedTypeFull
 <: TotalOrder.