Proving insertion sort correct easily in Coq

Proving insertion sort in Coq.pdf

sort.v

(** * Proving insertion sort correct, easily *)

(** This is a PDF rendering of the gist by siraben at
$\href{https://gist.github.com/siraben/3fedfc2c5a242136a9bc6725064e9b7d}{\text{this
URL}}$.  I give an example of how to prove insertion sort correct
easily with $\href{https://coqhammer.github.io/}{\text{CoqHammer}}$.
CoqHammer is a proof automation tool, more details can be found from
the website.  What matters for us is that we can use it as an oracle
of sorts, just supplying it with the correct lemmas and letting it
finish the proof.  Whenever you see a call to a tactic such as
[sauto], [sfirstorder] and so on, those were found interactively by
running the [best] command first (possibly with some lemmas), then
copy/pasting the output.  While we could use [sauto] in most places,
these more restricted tactics help with performance.

From the standard library we will just import natural numbers and
lists. *)

Require Import Nat.
Require Import List.
(** The secret sauce: CoqHammer. *)

From Hammer Require Import Tactics.

Import ListNotations.
Open Scope nat.

(** * Sorted predicate *)
(** [Sorted] is a predicate on lists of natural numbers that expresses
sortedness.  It is defined as follows:
- [sorted_nil]: the empty list is sorted
- [sorted_singleton]: the list containing one element is sorted
- [sorted_cons]: let [n], [m], [p] be natural numbers such that $n\le m$ and [m::p] is sorted, then [n::m::p] is sorted *)

Inductive Sorted : list nat -> Prop :=
| sorted_nil : Sorted []
| sorted_singleton : forall n, Sorted [n]
| sorted_cons : forall n m p, n <= m -> Sorted (m :: p) -> Sorted (n :: m :: p).

(** * Inserting an element *)
(** Insert [n] into [l] just before the first number that is larger
than [n]. *)

Fixpoint insert n l :=
  match l with
  | [] => [n]
  | (x :: y) => if n <=? x then n :: x :: y else x :: insert n y
  end.

(** * Insert preserves sortedness *)
(** Let [l] be a sorted list, then [insert x l] is a sorted list.  We
proceed by induction on [l].  The base case is trivial.  For the
inductive case, we just perform case analysis on the tail again to
expose another element and use CoqHammer to finish the proof. *)

Lemma sorted_insert : forall x l, Sorted l -> Sorted (insert x l).
Proof.
  induction l.
  - sfirstorder.
  - destruct l; sblast.
Qed.

(** * Insertion sort *)
(** The definition of insertion sort, [sort], is straightforward.  For
the nil case, return nil, otherwise for [x :: l], recursively sort [l]
then insert [x] into the sorted tail. *)

Fixpoint sort l :=
  match l with
  | [] => []
  | x :: l => insert x (sort l)
  end.

(** * Correctness of [sort] *)
(** Let [l] be an arbitrary list.  Then [sort l] is sorted.  The proof
proceeds by induction on [l] and the use of the [sorted_insert]
lemma. *)

Lemma sort_sorts : forall l, Sorted (sort l).
Proof.
  induction l; sfirstorder use: sorted_insert.
Qed.

(** * Definition of permutation *)
(** Unlike a usual mathematical definition, we define permutations
inductively.  We have:
- nil is a permutation of nil
- if [l] is a permutation of [l'], then [x::l] is a permutation of [x::l']
- [x::y::l] is a permutation of [y::x::l]
- permutations are transitive
 *)

Inductive permutation {A} : list A -> list A -> Prop :=
| perm_nil : permutation [] []
| perm_cons : forall l l' x, permutation l l' -> permutation (x :: l) (x :: l')
| perm_swap : forall l x y, permutation (x :: y :: l) (y :: x :: l)
| perm_trans : forall a b c, permutation a b -> permutation b c -> permutation a c.

(** As an example, we can show that the list $[1,2]$ is a permutation of $[2,1]$ *)

Example permutation_ex1 : permutation [1;2] [2;1].
Proof. sfirstorder. Qed.

(** ** Symmetry of [permutation] *)

Lemma permutation_sym {A} : forall (a b : list A), permutation a b -> permutation b a.
Proof.
  intros a b Ha.
  induction Ha; sauto lq: on.
Qed.

(** ** [permutation] is respected by prepending with a list *)
(** If [tl] is a permutation of [tl'] then any list prepended to both
respects the relation. *)

Lemma permutation_app_head {A} : forall (l tl tl' : list A),
    permutation tl tl' -> permutation (l ++ tl) (l ++ tl').
Proof.
  intros l tl tl' H.
  induction l; sauto lq: on.
Qed.

(** ** [x::l] is a permutation of [insert x l] *)

Lemma insert_perm : forall x l, permutation (x :: l) (insert x l).
Proof.
  induction l; sauto q: on.
Qed.

(** ** [sort] produces a permutation of the input *)
(** For any list [l], sorting the list produces a permutation of [l].
The base case is trivial.  For the inductive case, we have to prove
that [permutation l (sort l)] implies [permutation (a :: l) (insert a
(sort l))].  We perform case analysis on l then use transitivity of
[permutation] and some other lemmas to finish the proof. *)

Lemma sort_perm : forall l, permutation l (sort l).
Proof.
  induction l.
  - sfirstorder.
  - simpl.
    sauto lq: on use: @perm_cons, @perm_trans, @permutation_sym, insert_perm.
Qed.

(** * General definition of a sorting algorithm *)
(** More generally, [f] is a sorting algorithm if the output is sorted
and a permutation of the original list. *)

Definition is_sorting_algorithm f := forall l, permutation l (f l) /\ Sorted (f l).

(** ** [sort] is a sorting algorithm *)
(** Finally, we can combine our lemmas to show that [sort] is a sorting algorithm. *)

Theorem insert_sort_is_sorting_algorithm : is_sorting_algorithm sort.
Proof.
  sfirstorder use: sort_perm, sort_sorts unfold: is_sorting_algorithm.
Qed.