模式匹配不是专用类型

Question

我在Coq中玩，试图创建一个排序列表。我只是想要一个函数，它[1,2,3,2,4]一个列表并返回类似Sorted [1,2,3,4]的东西 - 即去掉不好的部分，但实际上并没有对整个列表进行排序。

我想我会从定义一个类型 (m n : nat) -> option (m <= n) 的函数lesseq开始，然后我可以很容易地进行模式匹配。也许这是一个坏主意。

我现在遇到的问题的症结是（片段，底部的整个功能）

Fixpoint lesseq (m n : nat) : option (m <= n) :=
    match m with
        | 0 => match n with
            | 0 => Some (le_n 0)
            ...

不是类型检查; 它说它期待一个option (m <= n)，但Some (le_n 0)有类型 option (0 <= 0) 。我不明白，因为显然在这种情况下m和n都是零，但我不知道如何告诉Coq。

整个函数是：

Fixpoint lesseq (m n : nat) : option (m <= n) :=
    match m with
    | 0 => match n with
        | 0 => Some (le_n 0)
        | S n_  => None
        end
    | S m_  => match n with
        | 0 => None
        | S _   => match lesseq m_ n with
                | Some x=> le_S m n x
                | None  => None
                end
            end
    end.

也许我正在超越自己，只需要在解决这个问题之前继续阅读。

Answer 1

你可能想要定义以下函数（即使你正确地注释了它，你[le_S m n x]也没有你想要的类型）：

     Fixpoint lesseq (m n : nat) : option (m <= n) :=
     match n with
     | 0 =>
         match m with
         | 0 => Some (le_n 0)
         | S m0 => None
         end
     | S p =>
         match lesseq m p with
         | Some l => Some (le_S m p l)
         | None => None
         end
     end.

但正如您已经注意到的，类型检查器不够聪明，无法猜测当您破坏出现在结果。您必须按以下方式注释匹配：

     Fixpoint lesseq (m n : nat) : option (m <= n) :=
     match n return (option (m <= n)) with
     | 0 =>
         match m return (option (m <= 0)) with
         | 0 => Some (le_n 0)
         | S m0 => None
         end
     | S p =>
         match lesseq m p with
         | Some l => Some (le_S m p l)
         | None => None
         end
     end.

如果您真的想了解模式，请参阅参考手册匹配适用于依赖类型。如果你觉得不够勇敢为此，您宁愿使用策略机制来构建您的证明。（"精炼"策略是一个很好的工具）。

     Definition lesseq m n : option (m <= n).
     refine (fix lesseq (m : nat) (n : nat) {struct n} := _).
     destruct n.
     destruct m.
     apply Some; apply le_n.
     apply None.
     destruct (lesseq m n).
     apply Some.
     apply le_S.
     assumption.
     apply None.
     Defined.

顺便说一句，我认为你的函数不会真正有帮助（即使这是一个好主意），因为您需要证明以下引理： 引理lesseq_complete： forall m n， lesseq m n <> None -> m> n.

这就是人们使用Coq.Arith.Compare_dec的原因。玩得愉快。

Answer 2

你是想写这个函数作为练习还是只为了实现你的更大目标？在后一种情况下，您应该查看标准库，其中充满了决策函数，可以在这里完成工作，Coq.Arith.Compare_dec;例如，请参阅le_gt_dec。

另请注意，您提出的功能只会为您提供信息是否m <= n。对于模式匹配，总和类型{ ... } + { ... }更有用，为您提供两种可能的情况来处理。