Do.v

(** 
 * Do do notation with Notation
 Haskell の do 記法はモナディックな計算を [<-] を使って命令的に記述するためのもの。
 つまり、 do 内部の記述は解釈の仕方が外部と異なる。

 ここでは、 Coq の Arguments コマンドや Notation コマンドを用いて同様のコンセプトを実現する。
 すなわち、Coq に於ける Monad の do 記法を実装する。
 **)

Set Implicit Arguments.
Unset Strict Implicit.

(** 
 [$] 記法をとりあえず定義。
 **)
Notation "f $ x" := (f x) (at level 65, right associativity, only parsing).

(** 
 モナド用の記法は [monad_scope] の中でのみ使えるようにする。
 デリミタを設定し、スコープを開いておく。
 **)
Delimit Scope monad_scope with monad.
Open Scope monad_scope.

(** 
 今回は形だけの Monad を使う。
 モナド則付きの Monad でも全く同じことができる。
 **)
Class Monad (T: Type -> Type) :=
  {
    ret: forall {X: Type}, X -> T X;
    bind: forall {X Y: Type}, (X -> T Y) -> (T X -> T Y)
  }.
Bind Scope monad_scope with Monad.

(**
 [bind] 用の記法 [>>=], [>>] は特定のスコープに依存せず使えるようにしておく。
 **)
Notation "m >>= f" := (bind f m) (at level 50, left associativity)
Notation "m >> n" := (m >>= (fun _ => n)) (at level 50, left associativity).

(** 
 [<-] は　[monad_scope] の中でのみ使えるようにする。
 format オプションを使って、表示の際には ; で改行されるようにする。
 p を [monad_scope] の中で解釈するよう指定することを忘れずに。
 **)
Notation "x <- m ; p" := (m >>= fun x => p%monad) (at level 68, right associativity, format "'[' x  <-  '[v' m ']' ; '//' '[' p ']' ']'"): monad_scope.

(** 
 例示用に Maybe モナド
 **)
Instance Maybe: Monad option :=
  {
    ret X x := Some x;
    bind X Y f m := match m with Some x => f x | _ => None end
  }.


(** 
 今は [monad_scope] の中にいるので、 [<-] は利用可能。
 **)
Check (forall p q: nat,
          (x <- ret p;
           y <- ret q;
           ret $ x*y)
          = ret $ p*q).

(** 
 [monad_scope] を閉じるとダメ。
 **)
Close Scope monad_scope.
Fail Check (forall p q: nat,
               (x <- ret p;
                y <- ret q;
                ret $ x*y)
               = ret $ p*q).
(* The command has indeed failed with message: *)
(* => Error: Unknown interpretation for notation "_ <- _ ; _". *)

(** 
 恒等函数と [Arguments] コマンドによるスコープ指定を組み合わせる。
 函数 Do の引数 m を [monad_scope] にて解釈するように指定した。
 **)
Definition Do {X: Type}(m: X) := m.
Arguments Do {X}(m)%monad.

(** 
 Do の引数として与えれば [<-] が使える。
 **)
Check (forall p q: nat,
          Do (x <- ret p;
              y <- ret q;
              ret $ x*y)
          = ret $ p*q).

(**
 [do] はタクティクなので函数の名前は [Do] にしたが、ちょっと工夫して [do] と括弧で表現できるように。
 format の使い方は訊くかリファレンスマニュアルを参照しましょう。
 **)
(**
 level は = よりも優先度が低くなるよう 70 未満に設定する。
 ただし、 [<-] よりも優先度は高めに。
 **)
Notation "'do[' m ]":= (Do m) (at level 69, format "do[  '[  ' m ']'  ]").

Check (forall p q: nat,
          do[ x <- ret p;
              y <- ret q;
              ret $ x * y ]
          = ret $ p * q).

(**
 unfoldo := do 専用 unfold タクティク(なくても全く問題ない)。
 **)
Ltac unfoldo := unfold Do.
Goal (forall p q: nat,
          do[ x <- ret p;
              y <- ret q;
              ret $ x * y ]
          = ret $ p * q).
  do 2 intro; simpl.
  unfoldo.                      (* 使わずとも [reflexivity] は通る。 *)
  reflexivity.
Save testlemma.                 (* Goal で証明を始めたあと、 Qed の代わりに Save 使えば名前を付けられるよ。 *)