osa1

Coq exercises for beginners

July 12, 2014 - Tagged as: coq, en.

Formalizing abstractions/data structures and proving theorems about them in Coq is so much fun. I made up some simple exercises that consist of encoding some abstractions and laws we know from algebra and functional programming and then proving that some particular set + some operations on that set obeys the laws.

Using my amazing(!) JavaScript skills, I set up some “show/hide answer” buttons after each exercise. Exercises are easy, but the latter ones are relatively harder. Some abstractions/laws are inspired by Haskell.

Please note that I’m a beginner so my solutions probably have some flaws if you want to use them in large-scale verified programs :) I’m currently learning about typeclasses and records of Coq and I’m open to suggestions for improvements.

In exercises, when we talk that an abstraction should obey some laws, you need to enforce it in construction. e.g. You need to make constructors in a way that user would have to prove that the data structure + operations obey the laws.

Require Import List.
Import ListNotations.

Open Scope list_scope.

Exercise 1

A semigroup is a set together with an associative binary function. For example, natural numbers and addition function form a semigroup, because we know/can prove that addition function is associative. More precisely: (in Coq syntax)

forall (n1 n2 n3 : nat), n1 + (n2 + 3) = (n1 + n2) + n3.

Encode semigroups in Coq.

Inductive semigroup (A : Type) (Op : A -> A -> A) : Prop :=
| Semigroup_intro :
    (forall (a1 a2 a3 : A), Op a1 (Op a2 a3) = Op (Op a1 a2) a3) -> semigroup A Op.

Now prove that lists together with append operation form a semigroup. Use standard Coq lists and app function.

Theorem list_semigroup : forall A, semigroup (list A) (@app A).
Proof.
  intro. apply Semigroup_intro. intros.
  induction a1.
  + reflexivity.
  + simpl. f_equal. induction a2; auto.
Qed.

Exercise 2

A monoid is a semigroup with an identity element. In our addition example, identity element is 0, because when applied to the monoid function(addition) as first or second argument, results is the other argument:

forall (n : nat), 0 + n = n /\ n + 0 = n.

Encode monoids in Coq.

Inductive monoid A Op (sg : semigroup A Op) (U : A) : Prop :=
| Monoid_intro :
    semigroup A Op -> (forall (a : A), Op U a = Op a U /\ Op U a = a) -> monoid A Op sg U.

Now prove that lists with empty list as unit element together with the proof that lists are monoids as we proved in previous exercise, form a monoid.

Theorem list_monoid : forall A, monoid (list A) (@app A) (@list_semigroup A) [].
Proof.
  intro. apply Monoid_intro. apply list_semigroup.
  intro. split.
  + rewrite app_nil_r. reflexivity.
  + reflexivity.
Qed.

Exercise 3

In this exercise and exercise 4, we’ll be talking about Haskell definitions of abstractions, instead of algebra definitions. (although they may coincide)

A functor is a type with one argument(in Haskell terms, a type with kind * -> *) and a function, together with some laws. If you’re unfamiliar with functors of Haskell, you may want to skip this, or read Typeclassopedia.

A Coq definition would use these to encode functors:

Functor type: F : Type -> Type
Functor operation: forall t1 t2, (t1 -> t2) -> f t1 -> f t2 (let’s call it fmap)

A functor should obey these laws:

fmap id = id
fmap (fun x => g (h x)) = fun x => (fmap g (fmap h x))

Encode functors in Coq.

Inductive functor (F : Type -> Type) : (forall t1 t2, (t1 -> t2) -> f t1 -> f t2) -> Prop :=
| Functor_intro
    (fmap : forall t1 t2, (t1 -> t2) -> F t1 -> F t2)
    (l1   : forall t f, fmap t t id f = f)
    (l2   : forall t1 t2 t3, forall (f : F t1) (p : t2 -> t3) (q : t1 -> t2),
              fmap t1 t3 (fun a => p (q a)) f = fmap t2 t3 p (fmap t1 t2 q f)) :
    functor F fmap.

Now prove that lists with standard map function form a functor.

Theorem list_functor : functor list map.
Proof.
  apply Functor_intro.
  + intros. induction f. reflexivity. simpl. rewrite IHf. reflexivity.
  + intros. induction f. reflexivity. simpl. f_equal. apply IHf.
Qed.

Exercise 4

A monad is a functor with two more operations; let’s call bind and lift and some more laws. In Coq syntax: (F is our functor type)

bind: forall t1 t2, F t1 -> (t1 -> F t2) -> F t2
lift: forall t, t -> F t

Laws:

Left identity: forall t1 t2 a f, bind t1 t2 (lift t1 a) f = f a
Right identity: right_id : forall t m, bind t t m (lift t) = m
Associativity: forall t1 t2 t3 m f g, bind t2 t3 (bind t1 t2 m f) g = bind t1 t3 m (fun x => bind t2 t3 (f x) g)

Encode monads in Coq.

Inductive monad : (Type -> Type) -> Prop :=
| Monad_intro
    (F        : Type -> Type)
    (fmap     : forall t1 t2, (t1 -> t2) -> F t1 -> F t2)
    (Fp       : functor F fmap)
    (lift     : forall t, t -> F t)
    (bind     : forall t1 t2, F t1 -> (t1 -> F t2) -> F t2)
    (left_id  : forall t1 t2 a f, bind t1 t2 (lift t1 a) f = f a)
    (right_id : forall t m, bind t t m (lift t) = m)
    (assoc    : forall t1 t2 t3 m f g,
                  bind t2 t3 (bind t1 t2 m f) g = bind t1 t3 m (fun x => bind t2 t3 (f x) g)) :
    monad F.

Now prove that lists form a monad. You need to figure out what functions to use for lift and bind.

lift function:

(* I couldn't find this in stdlib so let's define *)
Definition singleton (A : Type) (x : A) := [x].

For bind, you can use standard flat_map function, but it’s argument order is reversed. So instead I rolled my own version:

Fixpoint concat {A : Type} (l : list (list A)) : list A :=
  match l with
  | []     => []
  | h :: t => app h (concat t)
  end.

(* I don't like argument order of flat_map in stdlib ... *)
Definition concatMap (A : Type) (B : Type) (l : list A) (f : A -> list B) : list B :=
  concat (map f l).

Now most involved proof in this exercises: (still very easy)

Theorem list_monad : monad list.
Proof.
  apply Monad_intro with (fmap := map) (lift := singleton) (bind := concatMap).
  + apply list_functor.
  + intros. unfold concatMap. simpl. rewrite app_nil_r. reflexivity.
  + intros. unfold concatMap. induction m.
    - reflexivity.
    - simpl. f_equal. apply IHm.
  + intros. induction m as [|h t].
    - reflexivity.
    - unfold concatMap in *. simpl. rewrite <- IHt. 
      assert (forall A (l1 : list (list A)) (l2 : list (list A)),
                concat l1 ++ concat l2 = concat (l1 ++ l2)) as H.
        intros. induction l1; auto.
          simpl. rewrite <- app_assoc. rewrite IHl1. auto.
      rewrite H. f_equal. rewrite map_app. reflexivity.
Qed.

Exercise 5

Prove that standard option type with some operations form a semigroup, monoid, functor and monad. You need to find relevant operations.

What restrictions do you need on options type argument? (A in option A) Does it need to form a monoid for option to form a monoid?

Definition map_option (A B : Type) (f : A -> B) (opt : option A) :=
  match opt with
  | None => None
  | Some t => Some (f t)
  end.

Definition append_option A OpA (sg : semigroup A OpA) (a b : option A) : option A :=
  match a, b with
  | None, None => None
  | None, Some b' => Some b'
  | Some a', None => Some a'
  | Some a', Some b' => Some (OpA a' b')
  end.

Theorem option_semigroup : forall A OpA (sg : semigroup A OpA),
  semigroup (option A) (append_option A OpA sg).
Proof.
  intros. apply Semigroup_intro. intros. destruct a1.
  + destruct a2.
    - destruct a3.
      * simpl. f_equal. inversion sg. apply H.
      * simpl. reflexivity.
    - destruct a3; simpl; reflexivity.
  + destruct a2; destruct a3; auto.
Qed.

Theorem option_monoid : forall A OpA (sg : semigroup A OpA),
  monoid (option A) (append_option A OpA sg) (option_semigroup A OpA sg) None.
Proof.
  intros. apply Monoid_intro. apply option_semigroup.
  intros. split. auto. destruct a; auto.
Qed.

Definition option_map A B (f : A -> B) (o : option A) : option B :=
  match o with
  | None => None
  | Some a => Some (f a)
  end.

Theorem option_functor : functor option option_map.
Proof.
  apply Functor_intro; intros; destruct f; auto.
Qed.

Definition option_bind A B (o1 : option A) (f : A -> option B) : option B :=
  match o1 with
  | None => None
  | Some a => f a
  end.

Theorem option_monad : monad option.
Proof.
  apply Monad_intro with (fmap := option_map) (lift := Some) (bind := option_bind).
  + apply option_functor.
  + intros. auto.
  + intros. destruct m; auto.
  + intros. destruct m; auto.
Qed.

Exercise 6

I only have a partial solution to this one and it’s not strictly a Coq exercise, but it’s still fun :)

A group is a monoid with inverse element of every element. In Coq syntax:

forall e, exists e_i -> op e e_1 = U

where op is monoid operation and U is unit of monoid.

Can you come up with a data structure that forms a group?

Someone at Coq IRC channel suggested diffs. Do you think a diff could form a group? What would associative operation, unit element, and inverse elements be?

Diffs don’t form a group. Composing two diffs is the merge operation, which is partial function. We can’t always merge two diffs. (merge conflicts)

So I don’t have an answer to this exercise, If you know examples to this one, please write at comments :)

(Show comments)