Introduction

There is still a huge gap between the grammar of Coq and the real-world applications: even if we learned how to use Coq prove some mathematical theorems, lemmas, or other things, we may still find it hard to verify an algorithm and an application. This chapter is intended to illustrate how we use Coq to prove algorithms.

Basic Techniques for Comparisons and Permutations

Consider these algorithms and data structures:

• sort a finite sequence of numbers
• finite maps from numbers to arbitrary type data
• finite maps from any ordered type or arbitrary type data
• priority queues (heaps): finding or deleting the highest number in a set

To prove the correctness of such programs, we need to reason about comparison, and about whether two collections have the same contents. We first introduce tricks for comparisons and permutations, which are essential to proceeding with proofs of algorithms.

In addition, we may give examples of how to use creusot to help verify Rust-based algorithms, if possible. Also, we will directly import all the needed theorems and definitions from Coq’s standard library, rather than doing them ourselves.

Swapping

Sorting algorithms, in most cases, involve swapping two elements if they are out of order, so it is necessary for us to reason about it.

Definition swap_first_element(l : list nat) : list nat :=
	match l with
	| a :: b :: l' => if a >? b then b :: a :: l' else a :: b :: l'
	| _ => l
	end.

Apparently this is idempotent.

Theorem swap_is_idempotent : forall l,
  swap (swap l) = swap l.
Proof.
  intros. destruct l as [| lhs l].
  - reflexivity.
  - destruct l as [| rhs l].
    + reflexivity.
		(* We omit the detail of bdestruct. *)
    + simpl. bdestruct (lhs >? rhs).
      * simpl. bdestruct (rhs >? lhs). lia. trivial.
      * simpl. bdestruct (lhs >? rhs). lia. trivial.
Qed.

Permutations

Another useful fact about swap is that is does not add or remove elements from the list: the size of the list remains the same, but the content changes – the output may be the permutation of the original list, and Coq provides an inductive property in the standard library called Permutation.

Inductive Permutation {A : Type} : list A -> list A -> Prop :=
  | perm_nil : Permutation  
  | perm_skip : forall (x : A) (l l' : list A),
                Permutation l l' ->
                Permutation (x :: l) (x :: l')
  | perm_swap : forall (x y : A) (l : list A),
                Permutation (y :: x :: l) (x :: y :: l)
  | perm_trans : forall l l' l'' : list A,
                 Permutation l l' ->
                 Permutation l' l'' ->
                 Permutation l l''.

A lot of theorems are proved in Coq’s standard library.

Insertion Sort