Search code examples
functorcoqapplicativetheorem-proving

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

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.
Solution

  • 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.