Welcome > Logics > Software Foundations > V1 Logical Foundations > Coq

Coq

References:

Basics: Functional Programming in Coq

Functional style of programming is founded on simple, everyday mathematical intuition: If a procedure or method has no side effects, then (ignoring efficiency) all we need to understand about it is how it maps input to outputs.

The direct connection between programs and simple mathematical objects supports both formal correctness proofs and sound informal reasoning about program behavior.

Features of functional programming in Coq:

Function as first-class values – can be passed as argument to other functions.
Algebraic data types
Pattern matching
Polymorphic type systems

Language Gallina in Coq

Gallina is Coq’s native functional programming language.

Data and Functions

Enumerated Types

Inductive and Definition

Days of the Week:

Type name is day, members are monday, tuesday, etc.

Inductive day: Type :=
    | monday
    | tuesday
    | wednesday
    | thursday
    | friday
    | saturday
    | sunday.

A function that operate on days:

Definition next_weekday (d:day) : day :=
  match d with
  | monday => tuesday
  | tuesday => wednesday
  | wednesday => thursday
  | thursday => friday
  | friday => monday
  | saturday => monday
  | sunday => monday
  end.

Compute, Example

To check the function works on examples, in three ways:

use command Compute to evaluate a compound expression:
```
Compute (next_weekday monday).
```

use Coq Example with expected values and proof or define it:

Example test_next_weekday:
(next_weekday (next_weekday monday)) = wednesday.
Proof. simpl. reflexivity. Qed.

use Coq to extract a program in another more conventional programming language with a high-performance compiler.

Notation

The Notation command defines a new symbolic notation for an existing definition.

Notation "x && y" := (andb x y).
Notation "x || y" := (orb x y).
Notation "x + y" := (plus x y) (at level 50, left associativity) : nat_scope.
Notation "x - y" := (minus x y) (at level 50, left associativity) : nat_scope.
Notation "x * y" := (mult x y) (at level 40, left associativity) : nat_scope.

Check ((0 + 1) + 1) : nat.

Example test_orb5: false || false || true = true.
Proof. simpl. reflexivity. Qed.

The level, associativity, and nat_scope annotations control how these notations are treated by Coq’s parser.

level is for precedence. Precedence level of n is specified by writing at level n; This helps Coq compound expressions.

The associativity setting helps to disambiguate expressions containing multiple occurrences of the same symbol.

Coq uses precedence levels from 0 to 100, and left, right, or no associativity.

Each notation symbol is also associated with a notation scope. Coq tries to guess what scope is meant from context, so when it sees S (O x O) it guesses nat_scope. Occasionally, it is necessary to help it out with percent-notation by writing (axb)%nat; sometimes in what Coq prints it will use %nat to indicate what scope a notation is in.

Admitted

The Admitted command can be used as a placeholder for an incomplete proof. It tells Coq that we want to skip to prove the theorem and just accept it as a given.

Fixpoint factorial (n:nat) : nat
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Example test_factorial1:          (factorial 3) = 6.
(* FILL IN HERE *) Admitted.
Example test_factorial2:          (factorial 5) = (mult 10 12).
(* FILL IN HERE *) Admitted.

Check

The Check command

prints the type of the expression; if the expression is followed by a colon and a type, Coq will verify the expression matches the type and halt with error if not.

It can be used to examine the statements of previously declared lemmas and theorems.

Check true. 
(* ==> true : bool *)
Check (negb true) : bool.

Check negb : bool -> bool.
(* Function types are written with arrows *)

Check andb : bool -> bool -> bool.

Check mult_n_0.
(* ==> forall n : nat, 0 = n * 0 *)

Types

Types

New Types from Old

Types can be inductively defined by constructor expressions.

Inductive rgb : Type :=
  | red
  | green
  | blue.

(* `red`, `green`, and `blue` are the only constructor expressions belonging to `rgb`, a set of constructor expressions. *)

Inductive color : Type :=
  | black
  | white
  | primary (p : rgb).

(* `black` and `white` belong the the set color; 
if `p` is a constructor expression belonging to the set `rgb`, 
then `primary p` is a constructor expression blonging to the set `color`.*)

Constructors, such as red, primary, true, false, etc.
Constructor expressions are formed by applying a constructor to zero or more other constructors, or constructor expressions. E.g.,
- red
- true
- primary
- primary red
- red primary
- red true
- …
Inductive definition carves out a subset of the whole space of constructor expressions and gives it a name, as Type, like bool, rgb, or color.

Functions

Define functions using pattern matching:

Definition monochrome (c : color) : bool :=
 match c with
 | black => true
 | white => true
 | primary p => false
 end.

Definition isred (c : color) : bool :=
 match c with
 | primary red => true
 | _ => false
 end.

Compute isred primary blue.

Computer isred primary red.

Modules

Coq’s module system to aid in organizing large developments.

One feature: if we enclose a collection of declarations between Module X and End X markers, then, in the remainder of the file after the End, these definitions are referred to by names like X.foo instead of just foo.

Module Playground.
 Definition b : rgb := blue.
End Playground.

Definition b : bool := true.

Check Playground.b : rgb.
Check b : bool.

Tuples

A single constructor with multiple parameters can be used to create a tuple type.

A tuple of four bits nybble:

Inductive bit : Type :=
 | B0
 | B1.

Inductive nybble : Type :=
 | bits (b0 b1 b2 b3 : bit).

Check (bits B0 B1 B0 B0) : nybble.

(* the `bits` constructor acts as a wrapper for its contents.
Unwrapping can be done by pattern matching.*)

Definition all_zero (nb : nybble) : bool :=
 match nb with
 | bits B0 B0 B0 B0 => true
 | bits _ _ _ _ => false
end.

Compute (all_zero (bits B0 B0 B0 B0)).
Compute (all_zero (bits B0 B1 B0 B0)).

Numbers

Example of natrual numbers definition, an infinite set.

A representation is simpler than binary.

It makes proofs simpler.

The unary, base 1.

In Coq datatype, we use two constructors:

Capital-letter O, represents zero;

Captial-letter S, stands for “successor”. When the S constructor is applied to the representation of the natural number n, the result is the representation of n+1.

Inductive nat : Type :=
| O
| S (n : nat).

(* zero is represented by `O` , 1 by `S O`, 2 by `S (S O)`, and so on.*)

(* the names `O` and `S` are arbitrary, just two different marks. It is the same meaning with definition below:*)

Inductive nat' : Type :=
| stop
| tick (foo : nat').

Coq provides a tiny bit of built-in magic for parsing and printing natrual numbers (for constructors S and O)

Check (S (S O)).
(* ==> 4 : nat *)

Definition minusTwo (n : nat) : nat :=
 match n with
 | O => O
 | S O => O
 | S (S n') => n'
end.

Compute (minusTwo (S (S (S (S O))))).
(* ==> 2 : nat *)
Compute (minusTwo 4).
(* ==> 2 : nat *)

Fixpoint

To define functions with recursion, use keyword Fixpoint instead of Definition.

To check a numer n is even or odd:

Fixpoint evenb (n:nat) : bool :=
 match n with
 | O => true
 | S O => false
 | S (S n') => evenb n'
 end.

Definition oddb (n:nat) : bool :=
 negb (evenb n).

Example test_oddb1: oddb 1 = true.
Proof. simpl. reflexivity. Qed.

Example test_oddb2: oddb 4 = false.
Proof. simpl. reflexivity. Qed.

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

Example test_mult1: (mult 3 9) = 27.
Proof. simpl. reflexivity. Qed.

Proof by Simplification.

Use simpl to simplify both sides of the equation;

Use reflexivity to check that both sides contain identical values. It can also:

do simplification as simpl; Adding simpl command allow us to see the intermediate state.

do more simplification than simpl. For example, it tries “unfolding” defined terms, replacing them with their right-hand sides.

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

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

Theorem plus_1_l: forall n:nat, 1+n = S n.
Proof. intros n. reflexivity. Qed.

Theorem mult_0_l: forall n:nat, 0 * n = 0.
Proof. intros n. reflexivity. Qed.

Use intros n or intros m to move n from the qualifier in the goal to a context of current assumptions.

Use Example, Theorem, or Lemma, Fact, Remark keywords to define a property.

Tactics

A tactic is a command that is used between Proof and Qed to guide the process of checking some claim we are making.

The keywords intros, simpl, and reflexivity are examples of tactics.

Proof by Rewriting.

To prove:

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

we need to assume we are given such numbers n and m. We also need to assume the hypothesis n = m. The intros tactic will serve to move all three of these from the goal into assumptions in the current context.

Since n and m are arbitrary numbers, we can’t just use simplification to prove this theorem. Instead, we prove it by observing that, if we are assuming n = m, then we can replace n with m in the goal statement and obtain an equality with the same expression on both sides. The tactic that tells Coq to perform this replacement is called rewrite.

Theorem plus_id_example : forall n m : nat, 
 n = m -> n + n = m + m.
Proof.
 (* move both quantifiers into the context: *)
 intros n m.

 (* move the hypothsis `n=m` into the context and give it the name H. *)
 intros H.

 (* rewrite the current goal `n+n=m+m` by replacing the left side of the equality hypothsis H with the right side. *)
 rewrite -> H.
 reflexivity. Qed.

The arrow symbol in the rewrite has nothing to do with implication: it tells Coq to apply the rewrite from left to right. To rewrite from right to left, you can use rewrite <-.

rewrite tactic can be used with a previously proved theorem instead of a hypothesis from the context.

If the statement of the previously proved theorem involves quantified variables, as in the example below, Coq tries to instantiate them by matching with the current goal.

Check mult_n_O.
(* mult_n_O
     : forall n : nat, 0 = n * 0
*)

Theorem mult_n_0_m_0 : forall p q : nat,
  (p * 0) + (q * 0) = 0.
Proof.
 intros p q.
 (* rewrite -> mult_n_O. 
   ==> Unable to find an instance for the variable n.
 *)
 rewrite <- mult_n_O.
 rewrite <- mult_n_O.

Proof by Case Analysis – destruct

destruct tactic tells Coq to consider, separately, different cases for the problem, such as cases for an unknown argument.

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

as [|n'] is called an intro pattern. It tells what variable names to introduce in each subgoal. Between the square brackets is a list of lists of names, separated by |.

In this case, first component is empty, since the O constructor is nullary. The second component gives a single name, n', since S is a unary constructor. (???)

eqn:E tells destruct to give the name E to the equation of n=0 and n=S n' which are assumptions about n that are relevant for subgoals. It can be elided but it is better practice to keep these for the sake of documentation.

- sign are called bullets, optional, each for one subgoal. Can also be other signs such as +, *, or -- ***, or using pairs of (nested) curly braces {}

destruct can be used with any inductively defined datatype.

Theorem negb_involutive : forall b : bool,
negb (negb b) = b.
Proof.
intros b.
destruct b eqn:E. (* no as clause because no need of variable names)
- reflexivity. (* b = true *)
- reflexivity. (* b = false *)
Qed.

destruct can be invoked inside a subgoal.

Theorem andb_commutative : forall b c,
andb b c = andb c b.
Proof.
intros b c. destruct b eqn:Eb.
- destruct c eqn:Ec.
+ reflexivity.
+ reflexivity.
- destruct c eqn:Ec.
+ reflexivity.
+ reflexivity.
Qed.

destruct [] shorthand with intros.

intros [|n], means intros n. destruct n as [|n].

intros [] [], means intros x y. destruct x. destruct y.

(* [] --> destruct *)

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

Theorem andb_commutative' : forall b c,
andb b c = andb c b.
Proof.
intros [] []
- reflexivity.
- reflexivity.
- reflexivity.
- reflexivity.
Qed.

true = false

Exercise: Prove

Theorem andb_true_elim2 : forall b c : bool,
  andb b c = true -> c = true.

Proof. Admitted.

(*https://gist.github.com/kencoba/933961#file-sf_1-v-L363*)
Theorem andb_true_elim2' : forall b c : bool,
 andb b c = true -> c = true.
Proof.
intros b c H.
destruct c eqn:Ec.
- reflexivity.
- rewrite <- H. 
  destruct b.
  * reflexivity.
  * reflexivity.
Qed.

(*https://www.reddit.com/r/Coq/comments/855k3n/beginner_question/*)

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

discriminate is a tactic that searches for primitive contradictions in the context and immediately solve the goal if it finds one (for assume a false statement, you can prove anything).

If you could revise
the fundmental principles of
computer system design
to improve security...

... what would you change?

Coq