(** * Computation in Coq
Dan Christensen, UWO, June 7, 2016
Outline:
- Recursive functions
- Proving things about recursive functions
- Lists and nested recursive functions
- Trees and more complicated recursive functions
- Program Extraction
- Using recursive functions to prove things (a.k.a. reflection)
- Efficiency
- Endnotes
#

#
This web page is generated from a Coq source file using coqdoc.
You can view this file and the Coq source file via
#http://jdc.math.uwo.ca/HoTT#.
Direct link: #computation.v#.
Tested with Coq 8.4. *)
(** ** First example *)
Require Import Bool Arith.
Definition nonzero (n : nat) : bool :=
match n with
| 0 => false
| S m => true
end.
(** In an interactive session, the following would display the
result of "running" this function. *)
Compute nonzero 0. (* [false : bool] *)
Compute nonzero 3. (* [true : bool] *)
(** "Computation" in Coq is simply the process of using definitional
equality to simplify a term until it is in normal form, e.g.
[nonzero 3 => nonzero (S (S (S 0))) => true].
*)
(** ** Recursive functions
Note that [match] is a primitive concept in Coq, which when combined with
[Fixpoint] is equivalent to the induction principles associated to inductive types.
Thus, they can be used to make recursive functions.
*)
Fixpoint factorial (n : nat) : nat :=
match n with
| 0 => 1
| S m => n * factorial m
end.
Compute factorial 7. (* [5040 : nat] *)
Definition factorial_ex1 : factorial 7 = 7*6*5*4*3*2*1 := eq_refl.
(** It is essential for logical consistency that all functions terminate
on all inputs. For example, the following would type check, but doesn't
terminate, so Coq doesn't accept the definition. *)
Fail Fixpoint loop (n : nat): Empty_set := loop n.
(* Error: Recursive call to loop has principal argument equal to
"n" instead of a subterm of "n". *)
(** If it were accepted, then [loop 0] would be of type [Empty_set]. Oops.
For Coq to accept a definition using [Fixpoint], there must
be an argument of your function so that all of your recursive
calls pass in a proper subterm of that argument.
For example, [m] is a proper subterm of [S m].
We'll get to more advanced examples of recursion soon.
*)
(** ** Aside: Laziness
Coq is in general lazy about computation. It does it when needed
to check the type of a term, e.g. checking that [eq_refl] has type
[factorial 7 = 7*6*5*4*3*2*1], but otherwise leaves things alone. This laziness
is crucial for efficiency.
For example, [factorial 9] causes a stack overflow on my machine, but
the following examples type check without a problem. *)
Definition factorial_ex2 : factorial 100 = factorial 100 := eq_refl.
Definition factorial_ex3 : nat := factorial 100.
(** ** Proving things about recursive functions
Here's another recursive function, which divides by 2 and rounds down.
Note that it calls itself on a sub-sub-term of its input. *)
Fixpoint div2 (n : nat) :=
match n with
| 0 => 0
| S 0 => 0
| S (S p) => S (div2 p)
end.
(** We ask Coq to create an induction principle for this function. *)
Functional Scheme div2_ind := Induction for div2 Sort Prop.
(** We use this to prove a Lemma. The cases match the cases in div2.
We could also use ordinary induction, twice. *)
Lemma div2_le : forall n, div2 n * 2 <= n.
Proof.
intro n.
functional induction div2 n.
- (* Goal: [0 * 2 <= 0] *)
auto.
- (* Goal: [0 * 2 <= 1] *)
auto.
- (* Goal: [(S (div2 p)) * 2 <= S (S p)] *)
(* Given: [IHN0 : div2 p * 2 <= p] *)
simpl.
(* Goal: [S (S (div2 p * 2)) <= S (S p)] *)
auto with arith.
Qed.
(** ** Lists
Lists are defined in this way. *)
Inductive mylist (A : Type) :=
| mynil : mylist A
| mycons : A -> mylist A -> mylist A.
Definition mylist_ex1 : mylist nat := mycons nat 0 (mycons nat 1 (mynil nat)).
(** We'll use Coq's list type, which comes with nice notations. *)
Require Import List.
Import ListNotations.
Definition list_ex1 : list nat := [1; 2; 4; 3].
Definition list_ex2 : list nat := 1 :: 2 :: 4 :: 3 :: nil.
Definition list_ex_eq : list_ex1 = list_ex2 := eq_refl.
Fixpoint last {A : Type} (default : A) (lst : list A) : A :=
match lst with
| nil => default
| hd :: nil => hd
| hd :: tail => last default tail
end.
Compute last 0 list_ex1. (* [3 : nat] *)
(** [last] is inductively defined by structural recursion on the argument [lst].
[tail] is a proper subterm of the list [head :: tail]. *)
(** ** Nested structural recursion
Now suppose I want to write a function that merges two sorted lists
of natural numbers into a new sorted list. A naive try would be: *)
Fail Fixpoint merge (l1 l2 : list nat) : list nat :=
match l1 with
| nil => l2
| h1 :: t1 => match l2 with
| nil => l1
| h2 :: t2 =>
if leb h1 h2 then
h1 :: merge t1 l2
else
h2 :: merge l1 t2
end
end.
(* Error: Cannot guess decreasing argument of fix. *)
(** Here's one way to accomplish this. *)
Fixpoint merge (l1 l2 : list nat) : list nat :=
match l1 with
| nil => l2
| h1 :: t1 => (fix merge_aux (l2' : list nat) :=
match l2' with
| nil => l1
| h2 :: t2 =>
if leb h1 h2 then
h1 :: merge t1 l2'
else
h2 :: merge_aux t2
end) l2
end.
(** The inner recursive function [merge_aux] is the "merge with [l1]" function.
It is created each time we reach that spot, adapted to the particular [l1] we
have then. It calls the outer [merge] and itself recursively. The outer
[merge] has [l1] decreasing, and the inner [merge_aux] has [l2'] decreasing. *)
Compute merge [1; 3; 3; 6] [0; 1; 2; 5; 7].
(* [[0; 1; 1; 2; 3; 3; 5; 6; 7] : list nat] *)
(** ** Trees
We'll study a type of trees whose nodes are labelled with natural numbers,
and whose children are ordered. *)
Inductive tree :=
node : nat -> list tree -> tree.
(** One parent node, with three children nodes. *)
Definition tree_ex1 : tree :=
node 7 [node 6 nil; node 3 nil; node 3 nil].
(** Node 4 has two children, and the second of those has three children. *)
Definition tree_ex2 : tree :=
node 4 [node 2 nil; tree_ex1].
(** Return label of the "leftmost" leaf node. *)
Fixpoint leftmost_leaf (t : tree) : nat :=
match t with
| node n nil => n
| node n (child::rest) => leftmost_leaf child
end.
(** Coq considers [child] a subterm of [node n (child::rest)], so accepts the above. *)
Compute leftmost_leaf tree_ex1. (* [6 : nat] *)
Compute leftmost_leaf tree_ex2. (* [2 : nat] *)
(** This function searches through the tree for a node with a particular label. *)
Fixpoint occur (m : nat) (t : tree) : bool :=
match t with
| node n children =>
if beq_nat m n then true
else (fix occur_list (m' : nat) (l : list tree) : bool :=
match l with
| nil => false
| hd::tl => orb (occur m' hd) (occur_list m' tl)
end) m children
end.
(** We need nested recursion, because we need to search the tail list.
One could try calling [occur m (node n tl)], but [node n tl] isn't a subterm. *)
Compute occur 2 tree_ex2. (* [true : bool] *)
Compute occur 9 tree_ex2. (* [false : bool] *)
(** Another approach is a recursive function defined from the start to
look through a _list_ of trees. *)
Fail Fixpoint occur_list (m : nat) (l : list tree) {struct l} : bool :=
match l with
| nil => false
| (node n children)::tl => beq_nat m n || occur_list m children || occur_list m tl
end.
(* Error: Recursive call to occur_list has principal argument equal to
"children" instead of "tl". *)
(** I don't know why Coq accepts [child] as a subterm of [node n (child::rest)]
but not [children] as a subterm of [(node n children)::tl]. If it had worked,
one would then define: *)
Fail Definition occur' (m : nat) (t : tree) : bool := occur_list m [t].
(** In situations like this, it is sometimes fruitful to change the definition of the type. *)
Inductive tree' :=
node' : nat -> forest -> tree'
with forest :=
| fnil : forest
| fcons : tree' -> forest -> forest.
(** We have defined _mutually inductive_ types, with [forest] essentially the
same as [list tree].
Now Coq will accept: *)
Fixpoint occur_forest (m : nat) (l : forest) : bool :=
match l with
| fnil => false
| fcons (node' n children) tl => beq_nat m n || occur_forest m children || occur_forest m tl
end.
Definition occur' (m : nat) (t :tree') : bool := occur_forest m (fcons t fnil).
(** One can also define _mutually recursive_ functions over mutually inductive types.
The above two could be better organized in this way. *)
(** ** More complicated recursion
Sometimes recursion isn't structural. Then you need to prove to Coq that
your function terminates. One way is to specify an argument [X] of type [T]
and a _measure_ function [m : T -> nat] such that [m X] decreases on each
recursive call.
*)
Require Import Recdef.
Function log2 (n : nat) {measure (fun m => m) n} : nat :=
match n with
| S (S n') => S (log2 (div2 n))
| _ => 0
end.
Proof.
(* Goal: [forall n n0 n' : nat, n0 = S n' -> n = S (S n') -> div2 (S (S n')) < S (S n')] *)
intros n n0 n'.
intros H1 H2.
(* Goal: [div2 (S (S n')) < S (S n')] *)
auto with arith. (* I'm surprised this works! *)
Defined.
(** [Program Fixpoint] is another tool for defining a function using a
measure. It is more flexible, in that the measure can depend on several
arguments. (It's also an expression, rather than a function.) And the
code it produces is more concise and faster, at least in one example I
tested ([game_half_sum]).
[Function] doesn't allow nested recursion, mutual recursion, dependent types,
or higher order functions.
[Program Fixpoint] allows most or all of these, but doesn't generate
as many inductive principles. *)
(** ** Code extraction
Once you've defined a function (and possibly proved it correct), you can
extract code in a variety of languages. The extraction procedure is smart
enough to throw away _proofs_ that don't affect the result. *)
Extraction Language Ocaml.
Extraction "log2.ml" log2. (* See #log2.ml# *)
(** One can also extract to Haskell and Scheme. An _entire C compiler_,
called CompCert, has been written in Coq, proved to be correct relative to
a specification, and extracted to Ocaml! *)
(* Added later: See
https://www.irif.univ-paris-diderot.fr/~letouzey/download/letouzey_extr_cie08.pdf
for more about extraction (and recursion in general). And see the game_sum example.
Note that the extracted code is generally much faster than running the code in Coq. *)
(** ** Proof using reflection
The rough idea is to prove something by translating it into a question that becomes
true by definitional equality. Here is a toy example. *)
Inductive Even : nat -> Prop :=
| Even_O : Even 0
| Even_SS : forall n, Even n -> Even (S (S n)).
Goal Even 0.
exact Even_O.
Qed.
Goal Even 4.
exact (Even_SS 2 (Even_SS 0 Even_O)).
Qed.
(** We can even use [repeat constructor] to prove that large numbers are Even. *)
Lemma by_constructor_1024 : Even 1024.
Proof.
repeat constructor. (* 1.5s *)
Defined. (* 1.6s *)
(** The time is roughly _quadratic_ in the value! For [Even 2n], we get
[n] nested occurrences of [Even_SS], but each of those requires an argument [m]
which in unary requires [m] constructors. *)
(** An alternative approach. *)
Fixpoint is_even (n : nat) : bool :=
match n with
| 0 => true
| 1 => false
| S (S n') => is_even n'
end.
(** Soundness theorem. Proved using [match], to mirror the function. *)
Fixpoint is_even_sound (n : nat) : is_even n = true -> Even n :=
match n return is_even n = true -> Even n with
| 0 => fun _ => Even_O
| 1 => fun pf : false = true => match pf with eq_refl => tt end
| S (S n') => fun pf : is_even n' = true => Even_SS _ (is_even_sound n' pf)
end.
(** Notice how we are using computational properties of [is_even] to make
the types match up. This is why decidability of definitional equality
is essential for type checking.
(The second line is pretty confusing, as is the proof
that you can Print. I can explain on the board later if there is time.) *)
(* begin hide *)
(* To explain the second line above, consider a similar situation. *)
Definition test (pf : false = true) : False :=
match pf with eq_refl => tt end.
(* If you print the result, you'll see that the match has a dependent return type. *)
Print test.
(* Here's the Book-HoTT style of explaining this.
Consider the type family over bool sending [b] to [false = b].
This defines a fibration over bool with total space Sigma_b (false = b).
Since one endpoint is free, the induction principal for identity types applies.
So consider the type family over Sigma_b (false = b) sending (b, pf) to
[if b then False else Unit]. (False is what we call Empty.)
This defines a fibration over Sigma_b (false = b), and to get a section,
it's enough to say where (false, eq_refl) goes. So we send it to tt : Unit.
Then, if we have a term (true, pf), the second will send it to (true, pf, foo),
where foo : False.
I think this blog post treats similar aspects of the match command:
http://homes.cs.washington.edu/~jrw12/dep-destruct.html
*)
(* end hide *)
Lemma by_reflection_1024 : Even 1024.
Proof.
apply is_even_sound.
(* Goal: [is_even 1024 = true] *)
reflexivity. (* 0.005s *)
Defined. (* 0.02s *)
Lemma by_reflection_big : Even 16384.
Proof.
apply is_even_sound.
reflexivity. (* 0.09s *)
Defined. (* 0.27s *)
(** The speed is because the proof term is concise. *)
Print by_reflection_1024. (* [is_even_sound 1024 eq_refl : Even 1024] *)
(** Coq doesn't need to fully evaluate that proof term to check its type. (Laziness!)
But if it did, it would obtain the same proof term we got the other way. *)
Goal by_reflection_1024 = by_constructor_1024.
reflexivity.
Qed.
(** ** A more substantial example of reflection: commutative monoids
The point of reflection isn't really speed. It's the ability to
have Coq automatically handle tedious proofs. *)
Section cmonoid.
Variable A : Set.
Variable e : A.
Variable m : A -> A -> A.
Infix "+" := m.
Hypothesis identl : forall a, e + a = a.
Hypothesis identr : forall a, a + e = a.
Hypothesis assoc : forall a b c, (a + b) + c = a + (b + c).
Hypothesis comm : forall a b, a + b = b + a.
(** Consider a theorem such as: *)
Theorem monoid_ex1 (a b c : A) : (a + e) + (e + (b + (c + b))) = (e + (b + b) + (c + (a + e))).
Abort.
(** The proof would be a bit tedious. *)
(** To reason about such equalities, we create a syntactic representation of them
that we can manipulate in gallina. We use natural numbers to index variables. *)
Inductive mexp : Type :=
| E : mexp
| Var : nat -> mexp
| Add : mexp -> mexp -> mexp.
(** For example, the following represent the above expressions, with different variables. *)
Definition LHS : mexp := (Add (Add (Var 0) E) (Add E (Add (Var 1) (Add (Var 2) (Var 1))))).
Definition RHS : mexp := (Add (Add E (Add (Var 1) (Var 1))) (Add (Var 2) (Add (Var 0) E))).
(** Next, we write an interpretation function, given variables [var n] of type [A]. *)
Variable var : nat -> A.
Fixpoint mdenote (me : mexp) : A :=
match me with
| E => e
| Var v => var v
| Add me1 me2 => mdenote me1 + mdenote me2
end.
Compute mdenote LHS. (* [var 0 + e + (e + (var 1 + (var 2 + var 1))) : A] *)
Compute mdenote RHS. (* [e + (var 1 + var 1) + (var 2 + (var 0 + e)) : A] *)
(** We will normalize expressions by first flattening them into lists (dropping E),
which takes care of associativity and identity, and then sorting the result, to take
care of commutativity. *)
Fixpoint flatten (me : mexp) : list nat :=
match me with
| E => nil
| Var n => n :: nil
| Add me1 me2 => flatten me1 ++ flatten me2
end.
Require Import Sorting.
Import NatSort.
Definition sort_and_flatten (me : mexp) : list nat :=
sort (flatten me).
(** Given a list of variable indices, we can get also interpret it. *)
Fixpoint mldenote (ls : list nat) : A :=
match ls with
| nil => e
| n :: tail => var n + mldenote tail
end.
Compute mldenote (sort_and_flatten LHS). (* [var 0 + (var 1 + (var 1 + (var 2 + e))) : A] *)
Compute mldenote (sort_and_flatten RHS). (* [var 0 + (var 1 + (var 1 + (var 2 + e))) : A] *)
(** This might be a bit tricky to prove. *)
Theorem sort_and_flatten_correct : forall me, mdenote me = mldenote (sort_and_flatten me).
Admitted.
(** Now it is easy to prove the main soundness result. *)
Theorem cmonoid_reflect : forall me1 me2,
mldenote (sort_and_flatten me1) = mldenote (sort_and_flatten me2)
-> mdenote me1 = mdenote me2.
Proof.
intros; repeat rewrite sort_and_flatten_correct; assumption.
Qed.
(** Now look at the motivating example again: *)
Theorem cmonoid_ex1 : (var 0 + e) + (e + (var 1 + (var 2 + var 1)))
= ((e + (var 1 + var 1)) + (var 2 + (var 0 + e))).
Proof.
exact (cmonoid_reflect LHS RHS eq_refl).
Qed.
(** It is still a bit tedious to write down LHS and RHS, but it's a
purely mechanical process to translate the expressions in the
statement into the syntactic type we created. In fact, one can create
a tactic that does this for you. See the references at the end, and
also the tactics built into Coq, like [ring] and [omega]. *)
(** Reflection is a very powerful tool. It is the basis for the SSReflect
library, which was developed for the proof of the Four Colour Theorem, by
Gonthier's team. *)
End cmonoid.
(** ** Efficiency (only if I have time to spare)
Here's an example illustrating a strategy for efficient recursion. *)
Fixpoint divonacci (n : nat) : nat :=
match n with
| 0 => 2
| 1 => 2
| S ((S n'') as n') => divonacci n' + div2 (divonacci n'')
end.
Compute map divonacci [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10].
(* [[2; 2; 3; 4; 5; 7; 9; 12; 16; 22; 30] : list nat] *)
Compute divonacci 34. (* [53134 : nat], 5.0s *)
(** Do the iteration [n] times, starting with [dn''] and [dn']. *)
Fixpoint divonacci_aux (n : nat) (dn' dn'' : nat): nat :=
match n with
| 0 => dn''
| 1 => dn'
| S n' => divonacci_aux n' (dn' + div2 dn'') dn'
end.
Definition divonacci_fast (n : nat) : nat := divonacci_aux n 2 2.
Compute map divonacci_fast [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10].
(* [[2; 2; 3; 4; 5; 7; 9; 12; 16; 22; 30] : list nat] *)
Compute divonacci_fast 34. (* [53134 : nat], 0.2s *)
(** More generally, recursive calls can often be eliminated using
an appropriate data structure to record past or pending work. *)
(** ** Endnotes
- There are a variety of evaluation techniques, such as [Eval compute],
[Eval vm_compute], [Eval lazy], etc. See Section 8.7 of the reference manual.
[Compute] is short for [Eval vm_compute in].
- There are many tutorials about recursive functions in Coq, but some
have questionable examples. I borrowed from one due to Benjamin Grégoire:
# http://www.di.ens.fr/~zappa/teaching/coq/ecole11/summer/lectures/lec9.pdf #
- My example of reflection is based on a blog post of Gregory Malecha:
#https://gmalecha.github.io/reflections/2015/10/03/computational-reflection-primer/.

#
I also combined ideas from
#http://poleiro.info/posts/2015-04-13-writing-reflective-tactics.html#
and
#http://adam.chlipala.net/cpdt/html/Reflection.html#.
- Good tutorials on recursive functions and proving their correctness, with
sorting as important examples:
# Eric Kidd, blog post,
Ömer Ağacan, blog post,
Coq in a Hurry, Bertot,
Altenkirch, Lecture 7. #
Sorting is also part of the Coq standard library.
- Another good reference on Inductive types, induction principles, recursive functions, etc. is the
# Inductive Types #
chapter of Adam Chlipala's online book.
*)
(* begin hide *)
(*
The settings below are handy for when giving a talk, since my beamer
remote can be used to move forward and back through the Coq file.
This undoes the bindings shown below:
(progn
(local-set-key (kbd "") nil)
(local-set-key (kbd "") nil))
This redoes them:
(progn
(local-set-key (kbd "") 'proof-assert-next-command-interactive)
(local-set-key (kbd "") 'proof-undo-last-successful-command))
Various paths to cut and paste or eval:
(setq coq-prog-name "/usr/bin/coqtop")
(setq coq-prog-name "/home/jdc/math/me/homotopy-type-theory/UniMath/sub/coq/bin/coqtop")
(setq coq-prog-name "/home/jdc/math/me/homotopy-type-theory/HoTT/hoqtop")
*** Local Variables: ***
*** eval: (local-set-key (kbd "") 'proof-assert-next-command-interactive) ***
*** eval: (local-set-key (kbd "") 'proof-undo-last-successful-command) ***
*** coq-prog-name: "/usr/bin/coqtop" ***
*** End:***
*)