list-comprehension - Coq 中的列表推导式

Question

我想在 Coq 中使用 Monad 推导式。
因为我认为我很难实现需要 MonadPlus 的符号。如 [ x | x <- m, x < 4 ] ，我没有尝试实现这样的符号。
因此，我编写了以下代码。

Notation "[ e | x <- m1 , .. , y <- m2 ]"
  := (m1 >>= (fun x => .. (m2 >>= (fun y => e)) ..))
  (x closed binder, y closed binder).

但是，它不起作用，我收到了这个错误。

Error: m1 is expected to occur in binding position in the right-hand side.

我认为 Coq 解释了 "[ m | x <- m1 , .. , y <- m2 ]" (Coq 代码)为 "[ m | x <- ( m1 , .. , y ) <- m2 ]" (伪代码)。
但我没有解决这个问题的方法。任何帮助，将不胜感激。

Answer 1

我不知道 Notation 是否可以实现这样的事情只。我能得到的最接近的东西不是写 [ e | x <- mx , ... , y <- my ]一个必须写[ x <- mx , ... , y <- my | e ] .

你可以这样做:

Require Import List.

Fixpoint join {a : Type} (xss : list (list a)) : list a :=
match xss with
 | nil           => nil
 | (cons xs xss) => xs ++ join xss
end.

Definition bind {a b : Type} (xs : list a) (f : a -> list b) : list b :=
  join (map f xs).

Notation "[ e" :=  e (at level 3).
Notation "x '<-' mx '|' e ']'" := (bind mx (fun x => cons e nil))
  (at level 2).
Notation "x '<-' mx ',' f"     := (bind mx (fun x => f))
  (right associativity, at level 2).

你现在可以这样写:

Goal forall xs ys, { zs | zs = [ x <- xs, y <- map (plus x) ys | y - x ] }.

然而，脱糖版本看起来很糟糕，目标很难阅读。如果只是为了编程，那还好。您甚至可以添加一些额外的符号，例如范围的符号:

Fixpoint range0 (n : nat) : list nat :=
match n with
 | O   => cons O nil
 | S m => cons n (range0 m)
end.

Definition range (m n : nat) : list nat := map (plus m) (rev (range0 (n - m))).

Notation "m -- n ']'" := (range m n) (at level 2).

这让您可以编写以下内容:

Goal { xs | xs = [ x <- [ 1 -- 3 ]
                 , y <- [ 1 -- x ]
                 | x + y ] }.