PreTalent23.Arith_in_class
From PreTalent23 Require Import Overture.
(* This is the version that we developed together in the class. *)
(* This is the version that we developed together in the class. *)
Natural numbers
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
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
Recursive functions on inductive types (Fixpoints)
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 :=
match n with
| 0 => m
| S n' => S (add n' m)
end.
Fixpoint mul (n m : nat) : nat :=
match n with
| 0 => 0
| S n' => add m (mul n' m)
end.
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:
Commutativity and associativity of addition
Exercise (in class)
Prove the following two theorems.
Lemma add_zero : ∀ n, n + 0 = n.
Proof.
induction n as [|n IHn].
- simpl. reflexivity.
- simpl. rewrite IHn. trivial.
Qed.
Print add_zero.
Lemma add_S : ∀ n m, n + S m = S (n + m).
Proof.
induction n as [|n IHn]; intros m; simpl; trivial.
rewrite IHn; trivial.
Qed.
Theorem add_comm : ∀ n m, n + m = m + n.
Proof.
induction n as [|n IHn]; intros m; simpl.
- rewrite add_zero; trivial.
- rewrite IHn, add_S; trivial.
Qed.
Theorem add_assoc : ∀ n m k, n + (m + k) = (n + m) + k.
Abort.
Exercise (in class)
Prove the following theorem.
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. |
(* Don't use lia: From Coq.micromega Require Import Lia. *)
Theorem expand_add_mul n m k l : (n + m) * (k + 1) + (l + k) = k * S (n + m) + n + m + l.
Proof.
Abort.
Lemma sum_S n : sum (S n) = sum n + S n.
Proof.
Admitted.
From Coq.micromega Require Import Lia.
Theorem Gauss : ∀ n, 2 * sum n = n * (S n).
Proof.
induction n as [|n IHn]; [trivial; fail|].
rewrite sum_S.
rewrite Nat.mul_add_distr_l.
rewrite IHn.
rewrite <- (Nat.mul_add_distr_r n 2 (S n)).
rewrite (Nat.add_comm n 2).
change ((2 + n) * S n) with ((S (S n)) * S n).
rewrite Nat.mul_comm.
reflexivity.
Qed.