Proof that safeHead is natural

safeHead_is_natural.v

Require Import List.
Import ListNotations.
Require Import FunInd.
Require Import Coq.Init.Datatypes.

Inductive Maybe (A:Type) : Type :=
  | Just : A -> Maybe A
  | Nothing : Maybe A.

Arguments Just {A} a.
Arguments Nothing {A}.

Class Functor (F : Type -> Type) := {
  fmap : forall {A B : Type}, (A -> B) -> F A -> F B
}.

#[local]
Instance Maybe_Functor : Functor Maybe :=
{
  fmap A B f x := match x with
                   | Nothing => Nothing
                   | Just y => Just (f y)
                   end
}.

Fixpoint fmap_list {A B : Type} (f: A -> B) (xs: list A) : list B :=
  match xs with
  | nil => nil
  | cons y ys => cons (f y) (fmap_list f ys)
  end.

#[local]
Instance List_Functor : Functor list := {
  fmap A B f l := fmap_list f l
}.

Definition safeHead {A : Type} (l : list A): Maybe A :=
  match l with
  | [] => Nothing
  | x :: _ => Just x
  end.

Functional Scheme safeHead_ind := Induction for safeHead Sort Prop.

Lemma safeHead_is_natural :
  forall (A B : Type) (f : A -> B) (l : list A),
     fmap f (safeHead l) = safeHead (fmap f l).
Proof.
  intros A B f l.
  functional induction (safeHead l); simpl.
  - (* Case: l = [] *)
    (* The safeHead of an empty list is Nothing, and mapping any function over *)
    (* Nothing gives Nothing. On the other hand, mapping any function over an *)
    (* empty list gives an empty list and applying safeHead to an empty list *)
    (* gives Nothing. Hence in this case, both sides of the equation are Nothing *)
    (* which makes them equal. *)
    reflexivity.
  - (* Case: l = x :: ls for some x and ls *)
    (* The safeHead of a list beginning with x is Just x, and mapping f over *)
    (* Just x gives Just (f x). On the other hand, mapping f over a list *)
    (* beginning with x gives a list beginning with f x and applying safeHead *)
    (* to this new list gives Just (f x). Hence in this case, both sides of *)
    (* the equation are Just (f x) which makes them equal. *)
    reflexivity.
Qed.