模式匹配不专门化类型

Question

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

我想我应该首先定义一个 (mn : nat) -> 类型的函数 lesseq选项 (m <= n)，然后我可以很容易地对其进行模式匹配。也许这是一个坏主意。

我现在遇到的问题的关键是（片段，底部的整个函数）

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 mnx] 也没有您想要的类型）：

     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 mn, lesseq mn <>;无 -> m＞名词

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

Answer 2

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

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