Coq proof that the Selection monad is an applicative and a monad

Question

I am pretty new to coq and I have so far managed to only prove things that are I can also prove by hand. So when I came across the Selection monad and decided to implement it in haskell, I thought it would be a good excercise but I got stuck. Could someone provide an example of a proof in coq that the selection monad is an applicative and a monad? Here is a haskell implementation of the functor.

newtype Sel r a = Sel { runSel :: (a -> r) -> a }

instance Functor (Sel r) where
  fmap ab (Sel ara) = Sel (ab . ara . (. ab))

Extra thanks if you can also also prove the monad laws.

EDIT: Here is my proof that the functor exists:

Definition sel (R A : Type) := (A -> R) -> A.

Theorem functor_exists : forall (R A B : Type),
    (A -> B) -> sel R A -> sel R B.
  intros R A B. unfold sel. intros AB ARA BR.
  apply AB. apply ARA. intro. apply BR. apply AB. exact X.
  Qed.

When I first started to use Coq, I reimplemented the definitions and lemmas from this "tutorial" and then switched to other (more interesting) monads. — ichistmeinname
I have done those but I can't seem to do much beyond that. I thought this one would be quite simple to a seasoned coq-ist, that's why I posted, but I might be wrong. — fakedrake
But then I guess that you can provide the Coq code, so that one can see the specific case where you get stuck? — ichistmeinname
I edited my post with my proof that the functor exists. I am just running in circles about the applicative. — fakedrake

gallais gallais · Accepted Answer · 2017-02-09T20:01:56

You don't have to use tactics because it's Coq: you can use it as a programming language in a way that is fairly similar to Haskell.

First, because R is going to be a variable present all the time in this section, we can make the notations a bit lighter by mentioning it once and for all:

Section SelMon.
Variable (R : Type).

We can then replicate your definition of sel (without the R variable because it's already in context). And write fmap as a nice definition rather than a proof using tactics:

Definition sel (A : Type) := (A -> R) -> A.

Definition fmap {A B : Type} (f : A -> B) (s : sel A) : sel B :=
  fun br => f (s (fun a => br (f a))).

The next step to prove that you have an applicative is to provide a pure method. Well it's easy enough: we can use a constant function.

Definition pure {A : Type} (a : A) : sel A :=
  fun _ => a.

Then it gets a bit hairy. I'd advise you to start with join and then derive bind (and app from it) using the canonical constructions:

Definition join {A : Type} (ssa : sel (sel A)) : sel A.
Admitted.

Definition bind {A B : Type} (sa : sel A) (asb : A -> sel B) : sel B.
Admitted.

Definition app {A B : Type} (sab : sel (A -> B)) (sa : sel A) : sel B.
Admitted.

Once you're done with these, you can close the section and R will be added as a parameter to all of your definitions.

End SelMon.

Coq proof that the Selection monad is an applicative and a monad

1 Answers