モナド、命題、証明、引き算

mpl.v

Set Implicit Arguments.
Unset Strict Implicit.

Class Setoid :=
  {
    carrier: Type;
    equal: carrier -> carrier -> Prop
  }.
Coercion carrier: Setoid >-> Sortclass.
Notation "x == y" := (equal x y) (at level 90, no associativity).

Class Category :=
  {
    obj: Type;
    hom: obj -> obj -> Setoid;
    comp: forall {X Y Z: obj}, hom X Y -> hom Y Z -> hom X Z;
    id: forall (X: obj), hom X X
  }.
Coercion obj: Category >-> Sortclass.
Coercion hom: Category >-> Funclass.
Notation "g \o{ C } f" := (comp (Category:=C) f g) (at level 60, right associativity).
Notation "g \o f" := (g \o{_} f) (at level 60, right associativity).
Notation "'Id' X" := (id X) (at level 60, right associativity).

Class Kleisli (C: Category)(T: C -> C) :=
  {
    pure: forall {X: C}, C X (T X);
    bind: forall {X Y: C}, C X (T Y) -> C (T X) (T Y)
  }.

Class KPL (C D: Category)(T: C -> C)(K: Kleisli T)(pred: C -> D) :=
  {
    sbst: forall {X Y: C}, C X (T Y) -> D (pred Y) (pred X)
  }.

Instance function (X Y: Type): Setoid :=
  {
    carrier := X -> Y;
    equal f g := forall x, f x = g x
  }.

Instance Types: Category :=
  {
    obj := Type;
    hom X Y := function X Y;
    comp X Y Z f g x := g (f x);
    id X x := x
  }.

Instance Maybe: Kleisli (C:=Types) option :=
  {
    pure X x := Some x;
    bind X Y f m := match m with Some x => f x | _ => None end
  }.

Module Pred.
  Definition type (X: Type) := X -> Prop.
  Definition impl {X: Type}(P Q: type X) := forall x, P x -> Q x.
  Arguments impl {X}(P Q) /.
  Definition not {X: Type}(P: type X) := forall x, ~ P x.
  Definition and {X: Type}(P Q: type X) := forall x, P x /\ Q x.
  Definition or {X: Type}(P Q: type X) := forall x, P x \/ Q x.
  Definition True := fun {X: Type}(_: X) => True.
  Definition False := fun {X: Type}(_: X) => False.
End Pred.
Notation predicate := Pred.type.

Generalizable Variables X Y Z x y z.
Instance MaybePL: KPL Maybe `(predicate X) :=
  {
    sbst X Y f P x := match f x with Some y => P y | _ => False end
  }.

Notation "m >>= f" := (bind (C:=Types) f m) (at level 55, left associativity).
Notation "x <- m ; p" := (m >>= fun x => p) (at level 60, right associativity).
Notation "x <-: m ; p" := (x <- pure m ; p ) (at level 60, right associativity).
Notation "f # P " := (sbst (C:=Types) f P) (at level 45, right associativity).
Notation "f >> g" := (bind (C:=Types) g \o{Types} f) (at level 42, right associativity).
Notation "P <= Q" := (Pred.impl P Q) (at level 70, no associativity).
Notation "[ x <~ P ] ; m ; [ y ~> Q ]" := ((fun x => P) <= (fun x => m) # (fun y => Q)) (at level 95).

Require Import Arith.
Fixpoint dif (n m: nat){struct m} :=
  match n, m with
  | S n', S m' => dif n' m'
  | _, 0 => Some n
  | 0, S _ => None
  end.

(* success *)
Goal
  forall n,
    [x <~ (x = S n)];
    y <-: (S x);
    dif y 2;
    [z ~> z = n].
Proof.
  simpl; intros; subst.
  destruct n; ring.
Qed.

(* failure *)
Goal
  forall P,
    ~ ([x <~ (x = 0)];
       y <-: (S x);
       dif y 2;
       [_ ~> P]).
Proof.
  simpl; intros P H; generalize (H _ (eq_refl _)); simpl; auto.
Qed.