10.3.2 First Example

10.3.2 First Example#

For the first example, the goal will be to implement addition via a function called “add”. The general form should be:

fun add :: "nat ⇒ nat ⇒ nat" where
    "base case"
    "recursive case"

where two natural numbers are added, and the result is a natural number that is the sum of the two input numbers. For example, sum m n should return the sum of m and n.

We first want to start off by defining the base case. Basically, if we add some arbitrary number n by 0, then it should return n.

"add 0 n = n"

General Proof Structure for a Proof by Induction#

Isabelle provides a general structure for how to approach and construct your proof. For this exercise, we will be using a proof by induction; first by proving a base case, and then by proving the sucessor case by using the induction hypothesis.

We start the proof by adding the command proof(induction m) after the lemma command. When we examine the output of this, we find that Isabele actually provides us with the overall goal, subgoals (such as the base case and successor cases), and the general proof outline

For example, for the associative property lemma, we get this:

goal (2 subgoals):
 1. add (add 0 n) p = add 0 (add n p)
 2. ⋀m. add (add m n) p = add m (add n p) ⟹ add (add (Suc m) n) p = add (Suc m) (add n p) 
Proof outline with cases:
  case 0
  then show ?case sorry
next
  case (Suc m)
  then show ?case sorry
qed

10.3.3 First Exercise#

For the first exercise, we will be proving the associative and commutative properties of a custom add function in Isabelle. This exercise comes from Exercise 2.2 of Concrete Semantics Exercises

The custom add function is defined here:

fun add :: "nat ⇒ nat ⇒ nat" where
    "add 0 n = n" |
    "add (Suc m) n = Suc(add m n)"

We use 2 lemmas to prove each part of the exercise, namely:

lemma add_assoc: "add (add m n) p = add m (add n p)"
lemma add_comm: "add m n = add n m"

Associative Property Proof#

We first start off by proving the associative property of addition, and we do this by declaring the lemma and its goal:

lemma add_assoc: "add (add m n) p = add m (add n p)"

We then add the type of proof, which in this case will be a simple induction proof via the proof command:

proof (induction m)

We then set the base case with:

  case 0

which will set m = 0 as the base case, and then will update the goal to: add (add 0 n) p = add 0 (add n p)

We then use:

  show ?case by simp

in order to simplify that new goal to: add n p = add n p

Next, we perform the inductive step in order to prove that if the associative property holds for m, it must also hold for it’s successor of Suc m

We introduce the inductive step:

next
  case (Suc m)

This creates 2 things:

  • A goal of: add (add (Suc m) n) p = add (Suc m) (add n p)

  • An induction hypothesis (Suc.IH) that assumes the property holds for m: add (add m n) p = add m (add n p)

  show ?case by (simp add: Suc.IH)

Here, simp first expands both sides of the equation using the recursive definition add (Suc m) n = Suc (add m n) This reduces the goal to Suc (add (add m n) p) = Suc (add m (add n p)) The induction hypothesis (Suc.IH) is then applied to replace add (add m n) p with add m (add n p), making both sides identical. The expression simplifies to Suc (…) = Suc (…) and completes the inductive step.

The full lemma proof for associativity is here:

lemma add_assoc: "add (add m n) p = add m (add n p)"
proof (induction m) 
  case 0
  show ?case by simp
next
  case (Suc m)
  show ?case by (simp add: Suc.IH)
qed

Communative Property Proof#

Next, to prove the communative property, we will first prove 2 helper lemmas:

lemma add_0_right: "add m 0 = m"
lemma add_Suc_right: "add m (Suc n) = Suc (add m n)"

These proofs follow the same general format for induction:

lemma add_0_right: "add m 0 = m"
proof (induction m)
  case 0
  show ?case by simp
next
  case (Suc m)
  show ?case by (simp add: Suc.IH)
qed

lemma add_Suc_right: "add m (Suc n) = Suc (add m n)"
proof (induction m)
  case 0
  show ?case by simp
next
  case (Suc m)
  show ?case by (simp add: Suc.IH)
qed

With the helper lemmas proven, we will use them to prove the commutative property

lemma add_comm: "add m n = add n m"
proof (induction m)
  case 0
  show ?case
    by (simp add: add_0_right)
next
  case (Suc m)
  show ?case
    by (simp add: Suc.IH add_Suc_right)
qed

where we use the add_0_right lemma in the base case and then the add_Suc_right lemma in the inductive step.

Contents