Kata

(This is part of a series of 'Verified' kata, where a classical algorithm problem is posed, the specification is formalized, the algorithm is implemented, and you're asked to prove the algorithm's correctness. Check out the collection of all 'Verified' kata)

Background

Some time ago there was 'The great theorem prover showdown' by Hillel Wayne. The goal was to challenge the notion that purely functional code is easier to reason than imperative code. The challenge was to write formally verified purely functional algorithms and compare them to the formally verified imperative Dafny code provided. Although the author of this kata does not necessarily agree with all points in the blog post, the challenges are well selected and are good exercises in formal proving/verification no matter imperative or functional. We're doing one today.

(You can check out all Theorem prover showdown kata as a collection).

(I have asked and obtained permission to turn the challenges into Codewars kata.)

The problem

We want to collect the unique elements of a list into a new list. No particular order required.

We would like to verify that the original list and the new list have the following properties:

• An element is in the original list, if and only if it's in the new list.
• The new list does not have duplicates.

The algorithm

This is naive but it will work for our purposes: Starting from an empty list, add each element into it if it's not already in it, otherwise discard it.

The formalization

We will just use a straightforward recursion to implement it.

Note: in_dec checks if an element is in a list. The Nat.eq_dec argument is provided for in_dec to know how to compare elements for equality.

Fixpoint list_unique (xs : list nat) : list nat :=
  match xs with
  | [] => []
  | x :: rest =>
      let next := list_unique rest
      in if in_dec Nat.eq_dec x next
        then next
        else x :: next
  end.

And the theorems you need to prove are:

Theorem list_unique_bidir : forall x xs,
  In x xs <-> In x (list_unique xs).
Proof. (* FILL IN HERE *) Admitted.

Theorem list_unique_NoDup : forall xs,
  NoDup (list_unique xs).
Proof. (* FILL IN HERE *) Admitted.

Hints

• The documentation of Lists contains the definition of In, NoDup, etc.

Preloaded code

From Coq Require Import List Arith.
Import ListNotations.

Fixpoint list_unique (xs : list nat) : list nat :=
  match xs with
  | [] => []
  | x :: rest =>
      let next := list_unique rest
      in if in_dec Nat.eq_dec x next
        then next
        else x :: next
  end.