Software Foundations Reading Note 1: Functional Programming in Coq

Yuchong Pan edited this page Sep 2, 2018 · 9 revisions

Overview

This module introduces some basic syntax of the Coq programming language, such as type definitions, function definitions and theorems. Then three proof techniques in Coq are discussed -- proof by simplification, proof by rewriting and proof by case analysis.

Types

Unlike other programming languages, Coq offers a powerful mechanism to define types from scratch. In this module, the author introduces how to define an Inductive type. For instance, the booleans can be defined as follows.

Inductive bool : Type :=
  | true : bool
  | false : bool.

Constructors of types can take parameters. For instance, the unary representation of natural numbers can be defined as follows.

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

The natural numbers can also be defined from its binary representation, as shown in the exercises.

Please note that the type definitions do not have actual meanings. In the above example, the definition merely says "O is a nat, and if n is a nat then so is S n." The interpretation of type constructors comes from how we use these constructors (e.g. function definitions, theorems, proofs, etc.).

As Coq is a functional programming language, every expression in Coq has a type. Functions are also values in Coq, and thus have types. These types are called function types, and are written with arrows. The Check command prints the type of an expression; for instance, Check negb. prints negb: bool -> bool.

Coq supports type inference. However the author recommends readers to include types to make code more readable.

Functions

In Coq, functions are defined with the Definition and Fixpoint keywords. Definition is used for non-recursive functions, and Fixpoint is used for recursive ones. For instance, the logical AND can be defined as follows.

Definition andb (b1 : bool) (b2 : bool) : bool :=
  match b1 with
  | true => b2
  | false => false
  end.

Here, the match ... end is used for pattern matching in Coq. A famous example of the recursive definition is the addition operation of two natural numbers of the unary representation:

Fixpoint plus (n : nat) (m : nat) : nat :=
  match n with
  | O => m
  | S n' => S (plus n' m)
  end.

Coq requires some argument of every Fixpoint definition to be "decreasing." Coq uses this restriction to guarantee that Fixpoint functions will eventually terminate. However, there exist some recursive functions that terminate but violate this restriction (see exercises for details).

Notation

Notations can be defined in Coq to increase the readability of function applications. For instance, infix plus can be defined as follows:

Notation "x + y" := (plus x y)
                      (at level 50, left associativity)
                      : nat_scope

Here, the precedence level, associativity and notation scope are defined with the notation. In Coq, 0%nat means the natural number zero, while 0%Z means the integer zero.

Proofs

Proof by Simplification

Consider the following unit test:

Example test_orb1: (orb true false) = true.
Proof. simpl. reflexivity. Qed.

Here, simpl is used to simplify / expand the both sides of the equation (orb true false) = true using the function definitions, and reflexivity is used to check if the both sides of the equation contain identical values. In fact, reflexivity performs some simplification and "unfolding" automatically; hence, in the above unit test, simpl is not required, but can make results more readable.

Theorems in Coq can be defined as follows.

Theorem plus_O_n : forall n : nat, 0 + n = n.
Proof.
  intros n. simpl. reflexivity. Qed.

Here, forall has the same meaning as the quantifier in mathematics. intros n moves n from the quantifier in the goal to a context of current assumptions; it does the same thing as "suppose n is a natural number" in informal proofs.

Proof by Rewriting

Proof by rewriting is often used in theorems that contain implication. For instance, consider the following theorem:

Theorem plus_id_example : forall n m : nat,
  n = m ->
  n + n = m + m.

In the previous example, we mentioned that intros n moves n from the quantifier to the context. Similarly, we can use intros H to move the hypothesis n = m to the context. Then, rewrite -> H can be used to rewrite the remaining goal (i.e. n + n = m + m) using the hypothesis n = m.

Note that -> performs the rewrite from left to right and that <- performs the rewrite from right to left. For instance, rewrite -> H rewrites n + n = m + m to m + m = m + m, and rewrite <- H rewrites the same equation to n + n = n + n.

Following is a complete proof of the above theorem:

Proof.
  intros n m.
  intros H.
  rewrite -> H.
  reflexivity. Qed.

Proof by Case Analysis

When function definitions start with a pattern matching, proof by simplification does not work. Instead, we need to use proof by case analysis to split the argument(s) into multiple cases, and then prove each case separately. For instance, consider the following theorem:

Theorem plus_1_neq_0 : forall n : nat,
  beq_nat (n + 1) 0 = false.
Proof.
  intros n. destruct n as [|n'].
  - reflexivity.
  - reflexivity. Qed.

In the above code, destruct is used to split the argument n into two cases / subgoals, because nat is defined by two cases -- O and S n'. as [|n'] is called an intro pattern. Intro patterns are lists separated by |s, and are used to tell Coq what variable name it should give to new variables introduced by destruct. We then need to prove the two subgoals separately.

The - signs are called bullets, and are used to mark the parts of the proof corresponding to each subgoal. In the above example, the first - corresponds to the subgoal beq_nat (O + 1) 0 = false, and the second - corresponds to the subgoal beq_nat (S n' + 1) 0 = false. For the second subgoal, we simplify it to beq_nat (S (n' + 1)) 0 = false by the definition of + 1, which can then be simplified by unfolding beq_nat to complete the proof.

Bullets can have multiple levels, as destruct may be used inside a subgoal. In Coq, the default three levels of bullets are marked by +, - and *. Sub-proofs can also be enclosed by curly braces, inside which +, - and * can be reused. Examples of multiple levels of bullets can be found in the book.

As an aside, we can perform case analysis when introducing variables by using intro patterns. For instance, the above proof can be rewritten as

Proof.
  intros [|n'].
  - reflexivity.
  - reflexivity. Qed.

Exercises

nandb (1 star)

This exercise asks readers to complete the definition of the nandb function and the unit tests. This can be done using the definition of the NAND logic gate: NAND is false if and only if both operands are true. Hence, if the first operand b1 is false, the return value is true. Otherwise the return value is the negation of the second operand.

As mentioned in the notes, the Examples in Coq can be proved using proof by simplification.

Definition nandb (b1:bool) (b2:bool) : bool :=
  match b1 with
  | false => true
  | true => (negb b2)
  end.

Example test_nandb1:               (nandb true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb2:               (nandb false false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb3:               (nandb false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb4:               (nandb true true) = false.
Proof. simpl. reflexivity. Qed.

andb3 (1 star)

This exercise asks readers to complete the definition of the andb3 function. As mentioned in the exercise, the function should return true when all of its inputs are true, and false otherwise. Then, we can perform case analysis on the first argument. If b1 is false, then the result must be false. Otherwise the result equals b2 && b3.

Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool :=
  match b1 with
  | false => false
  | true => (andb b2 b3)
  end.

Example test_andb31:                 (andb3 true true true) = true.
Proof. simpl. reflexivity. Qed.
Example test_andb32:                 (andb3 false true true) = false.
Proof. simpl. reflexivity. Qed.
Example test_andb33:                 (andb3 true false true) = false.
Proof. simpl. reflexivity. Qed.
Example test_andb34:                 (andb3 true true false) = false.
Proof. simpl. reflexivity. Qed.

factorial (1 star)

This exercise asks readers to implement the factorial function. This is the standard problem for recursion and examines the understanding of recursion and pattern matching in Coq.

Fixpoint factorial (n:nat) : nat :=
  match n with
  | O => 1
  | S n' => (mult n (factorial n'))
  end.

Example test_factorial1:          (factorial 3) = 6.
Proof. simpl. reflexivity. Qed.
Example test_factorial2:          (factorial 5) = (mult 10 12).
Proof. simpl. reflexivity. Qed.

blt_nat (1 star)

This exercises asks readers to implement the less-than function for natural numbers in terms of a previously defined function. In the text, we have defined beq_nat for equality check, and leb for less-than-or-equal-to. Hence, the less-than function is obvious; we check both equality and less-than-or-equal-to.

Definition blt_nat (n m : nat) : bool :=
  (leb n m) && (negb (beq_nat n m)).

Example test_blt_nat1:             (blt_nat 2 2) = false.
Proof. simpl. reflexivity. Qed.
Example test_blt_nat2:             (blt_nat 2 4) = true.
Proof. simpl. reflexivity. Qed.
Example test_blt_nat3:             (blt_nat 4 2) = false.
Proof. simpl. reflexivity. Qed.

plus_id_exercise (1 star)

This exercise asks readers to prove the stated theorem: forall n m o : nat, n = m -> m = o -> n + m = m + o. Here, we use proof by rewriting. First, we introduce the two hypotheses, n = m and m = o. Then, we rewrite the remaining goal n + m = m + o using the first hypothesis and get m + m = m + o. Similarly, we rewrite the current goal using the second hypothesis and get o + o = o + o. This can be proved using proof by simplification.

Theorem plus_id_exercise : forall n m o : nat,
  n = m -> m = o -> n + m = m + o.
Proof.
  intros n m o.
  intros H.
  intros H0.
  rewrite -> H.
  rewrite -> H0.
  reflexivity. Qed.

mult_S_1 (2 stars)

This exercises asks readers to prove the stated theorem forall n m : nat, m = S n -> m * (1 + n) = m * m. We again prove this by rewriting. Recall that we have a theorem named plus_1_l stating that 1 + n and S n are equivalent. Hence, we can first rewrite the goal m * (1 + n) = m * m with the theorem plus_1_l, getting m * (S n) = m * m. Then, we rewrite the hypothesis m = S n from right to left, and get m * m = m * m. This can be proved by simplification.

Theorem mult_S_1 : forall n m : nat,
  m = S n ->
  m * (1 + n) = m * m.
Proof.
  intros n m.
  intros H.
  rewrite -> plus_1_l.
  rewrite <- H.
  reflexivity. Qed.

andb_true_elim2 (2 stars)

This exercise asks readers to complete the proof by case analysis for the stated theorem forall b c : bool, andb b c = true -> c = true. First, we apply destruct on b. Since b is a bool, it can be either false or true. Thus, we get two cases: andb true c = true -> c = true and andb false c = true -> c = true.

For the first case, simplification by the andb definition gives c = true -> c = true. We then introduce the hypothesis c = true and rewrite the remaining goal c = true with the hypothesis. This gives true = true and can be proved by reflexivity.

For the second case, we further destruct c and get two subgoals: andb false true = true -> true = true and andb false false = true -> false = true. For the first subgoal, we can simply move the hypothesis, and the remaining goal true = true can be directly proved by reflexivity. For the second subgoal, we can first simplify the goal using the andb definition, getting false = true -> false = true. Then, we can take the hypothesis false = true and rewrite the remaining goal using this hypothesis, which gives true = true. The proof of this is trivial.

Theorem andb_true_elim2 : forall b c : bool,
  andb b c = true -> c = true.
Proof.
  intros b c. destruct b.
  - simpl. intros H. rewrite -> H. reflexivity.
  - destruct c.
    + intros H. reflexivity.
    + simpl. intros H. rewrite -> H. reflexivity.
Qed.

zero_nbeq_plus_1 (1 star)

This exercise asks readers to complete the proof for the stated theorem forall n : nat, beq_nat 0 (n + 1) = false. As the definition of the plus function performs pattern matching on n, we destruct n to two subgoals: beq_nat 0 (O + 1) = false and beq_nat 0 (S n' + 1) = false.

For the first subgoal, simplification by the definition of plus yields beq_nat 0 1 = false, which can then be proved by simplification using the definition of beq_nat.

For the second subgoal, simplification by the definition of plus yields beq_nat 0 S (n' + 1) = false. From the definition of beq_nat, this can be proved by simplification.

Theorem zero_nbeq_plus_1 : forall n : nat,
  beq_nat 0 (n + 1) = false.
Proof.
  intros n. destruct n.
  - reflexivity.
  - reflexivity.
Qed.

decreasing (2 stars)

This exercise asks readers to provide an example of a recursive function that terminates on all inputs but is rejected by Coq because of the violation of the "decreasing restriction". To construct such an example, we make one of the argument increasing till it reaches the other argument. Thus, although none of the arguments is decreasing, it still terminates on all inputs.

Fixpoint sum (cur : nat) (n : nat) : nat :=
  match (leb cur n) with
  | true => cur + (sum (cur + 1) n)
  | false => 0
  end.

boolean_functions (2 stars)

The first part of the exercise asks readers to prove the theorem where applying the identity function twice to a boolean values gives the original value. After introducing the three variables f, x and b, we first rewrite the remaining goal f (f b) = b using x : bool, f x = x, getting f b = b. Then, we apply x again and get b = b. The proof of this remaining goal is trivial.

Theorem identity_fn_applied_twice :
  forall (f : bool -> bool),
  (forall (x : bool), f x = x) ->
  forall (b : bool), f (f b) = b.
Proof.
  intros f.
  intros x.
  intros b.
  rewrite -> x.
  rewrite -> x.
  reflexivity.
Qed.

The second part of the exercise asks readers to state and prove a similar theorem where applying the negation function twice to a boolean value yields the original value. Similarly, after introducing f, x and b, we rewrite the remaining goal f (f b) = b twice using x : bool, f b = negb b, getting negb (negb b) = b. As the definition of negb pattern matches its argument, we perform case analysis on b. Then for both cases, we can simply simplify the goal using the definition of negb.

Theorem negation_fn_applied_twice :
  forall (f : bool -> bool),
  (forall (x : bool), f x = negb x) ->
  forall (b : bool), f (f b) = b.
Proof.
  intros f.
  intros x.
  intros b.
  rewrite -> x.
  rewrite -> x. destruct b.
  - reflexivity.
  - reflexivity.
Qed.

andb_eq_orb (3 stars)

This exercise asks readers to prove the theorem where the equality of b && c and b || c implies the equality of b and c. As both andb and orb pattern match their first argument, we destruct b to two subgoals: (andb true c = orb true c) -> true = c and (andb false c = orb false c) -> false = c.

For the first subgoal, we first simplify the remaining goal using the definitions of andb and orb and get c = true -> true = c. The proof then becomes trivial: we can just take the hypothesis and rewrite the remaining goal.

For the second subgoal, we again simplify the remaining goal using the defnitions of andb and orb and get false = c -> false = c. Trivially, we can prove this by rewriting.

Theorem andb_eq_orb :
  forall (b c : bool),
  (andb b c = orb b c) ->
  b = c.
Proof.
  intros b c. destruct b.
  - simpl. intros H. rewrite -> H. reflexivity.
  - simpl. intros H. rewrite -> H. reflexivity.
Qed.

binary (3 stars)

This exercise asks readers to define natural numbers using a binary representation rather than unary system. As given in the exercise, a binary number is either

  • zero,
  • twice a binary number, or
  • one more than twice a binary number.

That is, the second branch is adding a zero after a binary number, and the third branch is adding a one after a binary number.

Part (a)

The first part asks for an inductive definition of binary numbers. This is obvious by analogy with the definition of the nat type given in the text.

Inductive bin : Type :=
| Zero         : bin
| Twice        : bin -> bin
| TwicePlusOne : bin -> bin.

Part (b)

This part asks for an increment function incr for binary numbers, and a function bin_to_nat to convert binary numbers to unary numbers. Recall that the definition of the bin type has three branches, we perform pattern matching for both two functions.

For incr, we consider the three cases:

  • If n is zero, then we have . Hence, the result is one more than twice zero, i.e. TwicePlusOne Zero.
  • If n is twice a binary number, namely n', then we have . Hence, the result is one more than twice n', i.e. TwicePlusOne n'.
  • If n is one more than twice a binary number, namely n', then we have . Hence, the result can be evaluated recursively, i.e. Twice (incr n').

For bin_to_nat, we again consider the three cases:

  • If n is zero, then it corresponds to zero in the unary system; i.e. the result is O.
  • If n is twice a binary number, namely n', then we first convert n' to the unary representation recursively, and add up two converted n's. Hence, the result is (bin_to_nat n') + (bin_to_nat n').
  • If n is one more than twice a binary number, namely n', then we again convert n' to the unary representation recursively, and result is the sum of two converted n's plus one. Hence, the result is S ((bin_to_nat n') + (bin_to_nat n')).
Fixpoint incr (n : bin) : bin :=
  match n with
  | Zero            => TwicePlusOne Zero
  | Twice n'        => TwicePlusOne n'
  | TwicePlusOne n' => Twice (incr n')
  end.

Fixpoint bin_to_nat (n : bin) : nat :=
  match n with
  | Zero            => O
  | Twice n'        => (bin_to_nat n') + (bin_to_nat n')
  | TwicePlusOne n' => S ((bin_to_nat n') + (bin_to_nat n'))
  end.

Part (c)

The last part asks for five unit tests for the two functions defined in the previous part. For instance, following are five valid unit tests.

Example test_bin_incr1: (bin_to_nat (incr Zero)) = 1.
Proof. reflexivity. Qed.
Example test_bin_incr2: (bin_to_nat (incr (TwicePlusOne Zero))) = 2.
Proof. reflexivity. Qed.
Example test_bin_incr3: (bin_to_nat (incr (Twice (TwicePlusOne Zero)))) = 3.
Proof. reflexivity. Qed.
Example test_bin_incr4: (bin_to_nat (incr (TwicePlusOne (Twice (TwicePlusOne Zero))))) = 6.
Proof. reflexivity. Qed.
Example test_bin_incr5: (bin_to_nat (incr (Twice (Twice (Twice (Twice (TwicePlusOne Zero))))))) = 17.
Proof. reflexivity. Qed.
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.