[Coq] Scala PartialFunction is Monoid

「Scala の PartialFunction が orElse の演算に関して monoid になっているのでは？」という stackoverflow の議論 Scala PartialFunction can be Monoid? について twitter 上で目にしたので証明してみた。
Scala の PartialFunction[A,B] は失敗する関数と考えれば A -> option B と考えて良い。
Coq は外延性の公理を入れないと、(fun x => f x) = f が言えないので、ライブラリ Logic.FunctionalExtensionality を Import してるとか extensionality というタクティックを使ってるとかが目新しいぐらいで、他は単に型クラス定義してインスタンスが公理を満たすのを証明するだけ。

Section PartialFunctionMonoid.
(* See http://stackoverflow.com/questions/9067904/scala-partialfunction-can-be-monoid *)
 
Require Import Logic.FunctionalExtensionality.
 
Class Monoid(T:Type) := {
  op : T -> T -> T;
  e : T;
  left_id : forall t, op e t = t;
  right_id : forall t, op t e = t;
  assoc : forall t u v, op (op t u) v = op t (op u v)
}.
 
Variable A B:Type.
Definition pf := A -> option B.
Definition orElse(f g:pf):pf :=
fun a => match (f a) with
  | None => g a
  | Some b => Some b
  end.       
 
Instance pf_monoid : Monoid pf := {
  op := orElse;
  e := (fun a => None)
}.
Proof.
  intros. unfold orElse. simpl.
  extensionality a. auto.
 intros. unfold orElse.
 extensionality a. destruct (t a); auto.
intros. unfold orElse. extensionality a.
destruct (t a); auto.
Defined.
 
End PartialFunctionMonoid.