coq - 模式匹配不专门类型

我在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显然都是零，但是我不知道该如何告诉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.也许我正在超越自己，只需要继续阅读就可以解决这个问题。 最佳答案 您可能想定义以下函数(即使您正确注释了该函数，[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 无-> m> n。这就是为什么人们使用Coq.Arith.Compare_dec的原因。玩得开心。关于coq - 模式匹配不专门类型，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/6097501/