模式匹配不是专业类型

Question

我在Coq玩,试图创建一个排序列表.我只是想要一个带有列表的函数,[1,2,3,2,4]并返回类似的东西Sorted [1,2,3,4]- 即取出坏的部分,但实际上并没有对整个列表进行排序.

我想我会先定义一个lesseq类型的函数(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)有类型option (0 <= 0).我不明白,因为很明显,两者m并n在这方面零,但我不知道如何告诉勒柯克说.

整个功能是:

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.

顺便说一句,我认为你的功能不会真正有用(即使它是一个好主意),因为你需要证明以下引理:Lemma lesseq_complete:forall mn,lesseq mn <> None - > m> ñ.

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

Answer 2

你想把这个功能写成练习还是只是为了实现更大的目标？在后一种情况下,你应该看看标准库,它充满了可以在这里完成工作的决策函数,Coq.Arith.Compare_dec ; 比如说le_gt_dec.

另请注意,您建议的功能只会为您提供信息m <= n.对于模式匹配,sum类型{ ... } + { ... }更有用,为您提供两种可能的处理方式.