モナド、命題、証明、交わり半束

mpl.v

Set Implicit Arguments.
Unset Strict Implicit.

Require Import Setoids.Setoid Morphisms.
Generalizable All Variables.

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

Class Map (X Y: Setoid) :=
  {
    map: X -> Y;
    substitute: Proper ((==) ==> (==)) map
  }.
Coercion map: Map >-> Funclass.
Existing Instance substitute.

Instance Map_setoid (X Y: Setoid): Setoid :=
  {
    carrier := Map X Y;
    equal f g := forall x, f x == g x
  }.
Proof.
  split.
  - intros f x; reflexivity.
  - intros f g Heq x; symmetry; apply Heq.
  - intros f g h H H' x; transitivity (g x); [apply H | apply H'].
Defined.

Instance Map_comp {X Y Z: Setoid}(f: Map X Y)(g: Map Y Z): Map X Z :=
  {
    map x := g (f x)
  }.
Proof.
  intros x y Heq; repeat apply substitute; auto.
Defined.

Instance Map_id (X: Setoid): Map X X :=
  {
    map x := x
  }.
Proof.
  intros x y Heq; auto.
Defined.

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;

    comp_subst:
      forall (X Y Z: obj)(f f': hom X Y)(g g': hom Y Z),
        f == f' -> g == g' -> comp f g == comp f' g';

    comp_assoc:
      forall {X Y Z W: obj}(f: hom X Y)(g: hom Y Z)(h: hom Z W),
        comp f (comp g h) == comp (comp f g) h;

    comp_id_dom:
      forall {X Y: obj}(f: hom X Y),
        comp (id X) f == f;

    comp_id_cod:
      forall {X Y: obj}(f: hom X Y),
        comp f (id Y) == f
  }.
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);

    bind_pure:
      forall {X: C},
        bind (pure (X:=X)) == id (T X);

    pure_bind:
      forall {X Y: C}(f: hom X (T Y)),
        bind f \o pure == f;

    bind_bind:
      forall {X Y Z: C}(f: hom X (T Y))(g: hom Y (T Z)),
        bind g \o bind f == bind (bind g \o f)
  }.

Class SemiLattice  :=
  {
    sl_setoid: Setoid;
    sl_binop: sl_setoid -> sl_setoid -> sl_setoid;

    sl_binop_subst: Proper ((==) ==> (==) ==> (==)) sl_binop;

    sl_binop_refl:
      forall (x: sl_setoid),
        sl_binop x x == x;
    sl_binop_comm:
      forall (x y: sl_setoid),
        sl_binop x y == sl_binop y x;
    sl_binop_assoc:
      forall (x y z: sl_setoid),
        sl_binop x (sl_binop y z) == sl_binop (sl_binop x y) z
  }.
Coercion sl_setoid: SemiLattice >-> Setoid.
Existing Instance sl_binop_subst.

Class SLMap (A B: SemiLattice) :=
  {
    slmap: Map A B;
    slmap_binop:
      forall (x y: A),
        slmap (sl_binop x y) == sl_binop (slmap x) (slmap y)
  }.
Coercion slmap: SLMap >-> Map.
Existing Instance slmap.

Instance SLMap_setoid (A B: SemiLattice): Setoid :=
  {
    carrier := SLMap A B;
    equal f g := equal (Setoid:=Map_setoid A B) f g
  }.
Proof.
  split.
  - intros f x; reflexivity.
  - intros f g Heq x; symmetry; apply Heq.
  - intros f g h H H' x; transitivity (g x); [apply H | apply H'].
Defined.

Instance SLMap_comp
         {A B C: SemiLattice}(f: SLMap A B)(g: SLMap B C): SLMap A C :=
  {
    slmap := Map_comp f g
  }.
Proof.
  simpl; intros.
  repeat rewrite slmap_binop.
  reflexivity.
Defined.

Instance SLMap_id (A: SemiLattice): SLMap _ _ :=
  {
    slmap := Map_id A
  }.
Proof.
  simpl; intros; reflexivity.
Defined.

Instance SL: Category :=
  {
    obj := SemiLattice;
    hom := SLMap_setoid;
    comp := @SLMap_comp;
    id := SLMap_id
  }.
Proof.
  - simpl; intros.
    rewrite (H x), (H0).
    reflexivity.
  - simpl; intros; reflexivity.
  - simpl; intros; reflexivity.
  - simpl; intros; reflexivity.
Defined.

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

    sbst_subst: forall (X Y: C), Proper ((==) ==> (==)) (@sbst X Y);

    sbst_comp:
      forall (X Y Z: C)(f: hom X (T Y))(g: hom Y (T Z)),
        sbst f \o sbst g == sbst (bind g \o f);

    sbst_id:
      forall (X: C),
        sbst (pure (X:=X)) == id (pred X)
  }.
Existing Instance sbst_subst.

Instance function (X Y: Type): Setoid :=
  {
    carrier := X -> Y;
    equal f g := forall x, f x = g x
  }.
Proof.
  split.
  - intros f x; auto.
  - intros f g Heq x; auto.
  - intros f g h Heqfg Heqgh x.
    rewrite Heqfg; apply Heqgh.
Defined.

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
  }.
Proof.
  - simpl; intros.
    rewrite H, H0; auto.
  - simpl; intros; auto.
  - simpl; intros; auto.
  - simpl; intros; auto.
Defined.

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
  }.
Proof.
  - simpl; intros X [x|]; auto.
  - simpl; intros X Y f x; auto.
  - simpl; intros X Y Z f g [x|]; auto.
Defined.

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

Instance Pred_setoid (X: Type): Setoid :=
  {
    carrier := predicate X;
    equal P Q := forall x, P x <-> Q x
  }.
Proof.
  split.
  - intros P x; tauto.
  - intros P Q H; symmetry; auto.
  - intros P Q R H H' x; transitivity (Q x); auto.
Defined.

Instance Pred_SL (X: Type): SemiLattice :=
  {
    sl_setoid := Pred_setoid X;
    sl_binop := Pred.and (X:=X)
  }.
Proof.
  - simpl; intros P P' Hp Q Q' Hq x; simpl.
    rewrite Hp, Hq.
    tauto.
  - simpl; tauto. 
  - simpl; tauto. 
  - simpl; tauto. 
Defined.

Inductive Preds :=
| preds (X: Type)(P: predicate X).
Definition base (p: Preds) := match p with preds x _ => x end.
Definition pr (p: Preds): predicate (base p) := match p with preds _ x => x end.
Coercion pr: Preds >-> predicate.

Instance Monotone (P Q: Preds): Setoid := function (base P) (base Q).

Instance PoSets: Category :=
  {
    obj := Preds;
    hom P Q := Monotone P Q;
    comp X Y Z f g := g \o f;
    id P := id (base P)
  }.
Proof.
  - simpl; intros.
    rewrite H, H0; auto.
  - simpl; intros; auto.
  - simpl; intros; auto.
  - simpl; intros; auto.
Defined.

Program Instance MaybeKPL: KPL Maybe (fun X: Type => Pred_SL X) :=
  {
    sbst X Y f :=
      {|
        slmap :=
          {|
            map := fun P x => match f x with Some y => P y | _ => False end
          |}
      |}
  }.
Next Obligation.
  simpl; intros P Q H x.
  destruct (f x) as [y|]; auto.
  split; auto.
Qed.
Next Obligation.
  rename x into P, y into Q, x0 into x.
  destruct (f x) as [y|]; tauto.
Qed.
Next Obligation.
  intros f g H Q x; simpl.
  rewrite <- H.
  destruct (f x) as [y|]; tauto.
Qed.
Next Obligation.
  rename x into R, x0 into x.
  destruct (f x) as [y|]; tauto.
Qed.
Next Obligation.
  tauto.
Qed.


Notation "m >>= f" := (bind (C:=Types) f m) (at level 53, 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.pord P Q) (at level 70, no associativity).
Notation "[ x <~ P ] ; m ; [ y ~> Q ]" := ((fun x => P) -=> (fun x => x <- m; pure x) # (fun y => Q)) (at level 95).
Notation "'for' x 'with' P  ; 'result' y 'of' m ; 'satisfies' Q" := ([x<~P];m;[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,
    for x with x = S n;
    result z of
           (y <-: (S x);
            dif y 2);
    satisfies z = n.
Proof.
  simpl; intros; subst.
  destruct n; ring.
Qed.


Lemma le_ind':
  forall (P : nat -> nat -> Prop),
    (forall n, P 0 n) ->
    (forall n m : nat, P n m -> P (S n) (S m)) ->
    forall n m : nat, le n m -> P n m.
Proof.
  intros.
  revert m H1; induction n.
  - intros; apply H.
  - destruct m.
    + intro H1; inversion H1.
    + intro Hle; apply H0, IHn, le_S_n; auto.
Qed.

Require Import Omega.
Goal
  for x with (2 <= x);
  result z of
         (mx <-: x * x;
          px <-: x + x;
          pure (px, mx));
  satisfies let (px,mx) := z in px <= mx.
Proof.
  simpl.
  intros.
  elim H; simpl; auto.
  intros.
  rewrite plus_comm; simpl.
  rewrite mult_comm; simpl.
  omega.
Qed.

Goal
  for nm with (let (n,m) := nm:nat*nat in n <= m);
  result z of (let (n,m) := nm:nat*nat in dif m n);
  satisfies 0 <= z.
Proof.
  simpl; intros [n m] Hle; simpl in *.
  pattern n, m; apply le_ind'; auto; clear Hle n m.
  destruct n; simpl; auto with arith.
Qed.


Lemma hcomp:
  forall {X Y Z: Type}(P: predicate X)(Q: predicate Y)(R: predicate Z)
         (f: X -> option Y)(g: Y -> option Z),
    (for x with P x; result y of f x; satisfies Q y) ->
    (for y with Q y; result z of g y; satisfies R z) ->
    (for x with P x; result z of y <- f x; g y; satisfies R z).
Proof.
  simpl; intros.
  generalize (H _ H1); destruct (f x) as [y|]; auto; intros.
  generalize (H0 _ H2); destruct (g y) as [z|]; auto.
Qed.


Goal
    for x with 2 <= x;
    result z of
           (mx <-: x * x;
            px <-: x + x;
            dif mx px);
    satisfies 0 <= z.
Proof.
  change
    (for x with 2 <= x;
     result z of
            (mx <-: x * x;
             px <-: x + x;
             pm <-: (px,mx);     (* intermediate parameter *)
             let (p,m) := pm:_*_ in dif m p);
     satisfies 0 <= z).
  eapply hcomp.
  - apply Unnamed_thm0.
  - apply Unnamed_thm1.
Qed.

(* failure *)
Goal
  forall P,
    ~ (for x with x = 0;
       result _ of y <-: (S x); dif y 2;
       satisfies P).
Proof.
  simpl; intros P H; generalize (H _ (eq_refl _)); simpl; auto.
Qed.