PreTalent23.Arith

From PreTalent23 Require Import Overture.

Natural numbers

Coq features inductive types. These are types that are defined inductively, i.e., consisting of a few base cases, and inductive cases. One of the quintessential inductive types is the type nat of natural numbers.

The type of natural numbers in Coq's standard library is defined as follows:

Module Nat.

  Inductive nat : Set :=
    O : nat
  | S : nat → nat.

End Nat.

A note on modules

Here we define nat in a module simply to avoid shadowing the type nat (defined in exactly the same way) in the standard library of Coq — outside the module the type defined in the module can only be referred to as Nat.nat while nat refers to the definition in the standard library. This is the only use of the module system of Coq in this course. Otherwise, Coq modules can be ignored for all intents and purposes for the rest of this course.

Constructors

The inductive type nat has two constructors: O and S, respectively representing zero and the successor function. Coq has special parsing and pretty printing facilities for the type of natural numbers which allows users to write natural numbers in decimal format (Coq comments are delimited by "(*" and "*)"):

Check 20 : nat. (* This command checks that the type of "20" is indeed nat. *)

Check S (S (S (S (S O)))) : nat. (* Run this command in Coq and note that it
reports "5" (and not "S (S (S (S (S O))))") has type nat. *)

Universes

The type Set in the definition above, i.e., the type of the type nat, is a universe. Universes are types whose terms (programs) are types themselves. Recall that Coq is a dependent type theory where types are also terms and themselves have types, this includes universes themselves. In order to avoid self-referential paradoxes (similar to Russel's paradox) a universe cannot be its own type. Hence, Coq features a hierarchy of universes Type₀ : Type₁ : Type₂ : ⋯ The universe Type₀ is referred to as Set. Most simple types, e.g., nat, bool, etc. live in this universe. In this course we will mostly ignore universes — this is in fact what most Coq developers do as Coq can automatically figure out which universe types should belong to. The only universe that is distinguished from the other universes, Typeᵢ, is the universe Prop of propositions. Quintessential types in Prop are the types/propositions True and False. In fact these types are defined as inductive types too, True with a single constructor, and False with no constructor! Use the following commands to see the definitions of these two types:

Print True.

Print False.

Recursive functions on inductive types (Fixpoints)

We can use the Fixpoint command of Coq to define recursive functions by recursion on the structure of an inductively defined type, e.g., natural numbers. We can use the match ... with ... end construct to do case analysis on inductive types.

Exercise (in class)

Use Fixpoints and the matching mechanism of Coq to define addition and multiplication on natural numbers. (See the example below, sum.)

Module addition_multiplication.

(* Fixpoint add (n m : nat) : nat := *)

(* Fixpoint mul (n m : nat) : nat := *)

End addition_multiplication.

Using Fixpoints and the matching mechanism allow us to define the function sum which given a number n adds up all natural numbers less than or equal to n:

Fixpoint sum (n : nat) : nat :=
  match n with
  | 0 => 0
  | S m => n + (sum m)
  end.

Commutativity and associativity of addition

Exercise (in class)

Prove the following two theorems.

In Coq we use tactics to prove theorems. Tactis are commands that correspond to steps in the proof. Tactics can be used when Coq is in proof mode, i.e., after the Proof command that follows a command like Theorem, Lemma, etc.

A comprehensive list of tactics and their explanations can be found in Coq's reference manual: https://coq.inria.fr/refman/proof-engine/tactics.html

Theorem add_comm : ∀ n m , n + m = m + n.
Proof.
Abort.

Theorem add_assoc : ∀ n m k , n + (m + k ) = (n + m ) + k.
Abort.

Exercise (in class)

Prove the following theorem.

From Coq.Arith Require Import Arith. (* We import arithmetic lemmas of the library. *)

Pro tip

You can use the search command to search all the existing constructions, e.g., lemmas, theorems, definitions, etc., including all those from the loaded libraries. You can read about the search command on https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:cmd.Search. Here are a few of the query formats supported by the search command:

Command	Description
search "add".	finds constructions whose name contains the string "add".
search "+". search add.	finds constructions whose type features the addition operation. Note how the string "+" here is not considered a name as it is a notation (see +).
search _ + (S _).	finds constructions whose type involves an addition where the right hand side expression is the successor of some number.

Theorem expand_add_mul n m k l : (n + m ) * (k + 1) + (l + k ) = k * S (n + m) + n + m + l.
Proof.
Abort.

Gauss

Exercise

Prove the following theorem and helper lemma.

Lemma sum_S n : sum (S n) = sum n + S n.
Proof.
Abort.

Theorem Gauss : ∀ n , 2 * sum n = n * (S n ).
Proof.
Abort.