6

我在 Coq 中玩耍，试图创建一个排序列表。我只想要一个接受列表[1,2,3,2,4]并返回类似内容的函数Sorted [1,2,3,4]- 即取出坏部分，但实际上并未对整个列表进行排序。

我想我会先定义一个lesseqtype的函数(m n : nat) -> option (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)有 type 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.

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

4

2 回答 2

7

您可能想要定义以下函数（即使您正确注释它，您 [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 <> None -> m > n.

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

于 2011-05-23T14:29:23.073 回答
6

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

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

于 2011-05-23T14:09:31.030 回答