Skip to content

Instantly share code, notes, and snippets.

@NicolasT
Created May 2, 2011 21:50
Show Gist options
  • Save NicolasT/952451 to your computer and use it in GitHub Desktop.
Save NicolasT/952451 to your computer and use it in GitHub Desktop.
Coq definitions and proofs of several functors
Require Import Coq.Program.Basics.
Open Local Scope program_scope.
Definition id (A: Type) (e: A): A := e.
Module Type FUNCTOR.
Set Implicit Arguments.
Parameter F: forall (A: Type), Type.
Parameter fmap: forall (A B: Type), (A -> B) -> F A -> F B.
Axiom associativity: forall (A B C: Type) (f: A -> B) (g: B -> C) (e: F A),
fmap (g ∘ f) e = fmap g (fmap f e).
Axiom identity: forall (A: Type) (e: F A),
fmap (id A) e = e.
End FUNCTOR.
Inductive Identity (A: Type): Type :=
| Id: A -> Identity A.
Module IdentityFunctor <: FUNCTOR.
Set Implicit Arguments.
Definition F := Identity.
Definition fmap (A B: Type) (f: A -> B) (e: F A): F B :=
match e with
| Id a => Id B (f a)
end.
Lemma associativity: forall (A B C: Type) (f: A -> B) (g: B -> C) (e: F A),
fmap (fun x: A => g (f x)) e = fmap g (fmap f e).
Proof.
intros.
induction e.
simpl.
reflexivity.
Qed.
Lemma identity: forall (A: Type) (e: F A),
fmap (id A) e = e.
Proof.
intros.
induction e.
simpl.
reflexivity.
Qed.
End IdentityFunctor.
Inductive Maybe (A: Type): Type :=
| Nothing: Maybe A
| Just: A -> Maybe A.
Module MaybeFunctor <: FUNCTOR.
Set Implicit Arguments.
Definition F := Maybe.
Definition fmap (A B: Type) (f: A -> B) (e: F A): F B :=
match e with
| Nothing => Nothing B
| Just a => Just B (f a)
end.
Lemma associativity: forall (A B C: Type) (f: A -> B) (g: B -> C) (e: F A),
fmap (g ∘ f) e = fmap g (fmap f e).
Proof.
intros.
induction e.
simpl.
reflexivity.
simpl.
reflexivity.
Qed.
Lemma identity: forall (A: Type) (e: F A),
fmap (id A) e = e.
Proof.
intros.
induction e.
simpl.
reflexivity.
simpl.
reflexivity.
Qed.
End MaybeFunctor.
Inductive List (A: Type): Type :=
| Nil: List A
| Cons: A -> List A -> List A.
Module ListFunctor <: FUNCTOR.
Set Implicit Arguments.
Definition F := List.
Fixpoint fmap (A B: Type) (f: A -> B) (e: F A) {struct e}: F B :=
match e with
| Nil => Nil B
| Cons a b => Cons B (f a) (fmap f b)
end.
Lemma associativity: forall (A B C: Type) (f: A -> B) (g: B -> C) (e: F A),
fmap (g ∘ f) e = fmap g (fmap f e).
Proof.
intros.
induction e.
simpl.
reflexivity.
simpl.
rewrite IHe.
reflexivity.
Qed.
Lemma identity : forall (A : Type) (e: F A),
fmap (id A) e = e.
Proof.
intros.
induction e.
simpl.
reflexivity.
simpl.
rewrite IHe.
reflexivity.
Qed.
End ListFunctor.
Recursive Extraction IdentityFunctor MaybeFunctor ListFunctor.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment