证明长度 (h::l) = 1 + 长度 l答案

【问题标题】：Prove length (h::l) = 1 + length l证明长度 (h::l) = 1 + 长度 l
【发布时间】：2015-11-25 07:47:41
【问题描述】：

我对这些看似微不足道的证明感到困惑。

例如，在归纳的情况下，如果我假设标题中的属性并且我想显示：

length (h'::h::l) = 1 + length (h::l)

我从这里去哪里？这显然是正确的，但我不知道在不证明某种引理的情况下我可以采取哪些步骤。比如我可以说

length ([h']@(h::l)) = 1 + length (h::l)

但是现在我必须证明一些类似的东西

length (l1@l2) = length l1 + length l2

当我需要证明引理时，我无法理解，尤其是在看似微不足道的证明中。

【问题讨论】：

我投票结束这个问题，因为它是一个数学问题，而不是一个编程问题。
它与编程课程有关，它是ocaml中程序的证明。我不同意。
@wvdz 参见类型理论：命题是类型，证明是程序。也许添加一个 Coq 标签。

标签： ocaml proof induction proof-of-correctness

【解决方案1】：

当您证明程序的正确性时，您通常会使用一些实现。如果您将采用简单的实现，那么证明也将是微不足道的。假设我们有以下实现：

let rec length = function
  | [] -> 0
  | x::xs -> 1 + length xs

我们有证明义务：

length (x::xs) = 1 + length xs

我们使用结构归纳来证明这一点。我假设，该列表被定义为

type 'a list = 
  | Nil 
  | Cons ('a,'a list)

而[] 是Nil 的语法糖，而x::xs 是Cons (x,xs) 的语法糖

所以我们逐案分析。我们只有一个适用案例，所以我们以案例为例

  | x::xs -> 1 + length xs

用右手边重写length (x::xs)，我们得到：

  1 + legnth xs = 1 + length xs

这可以通过= 运算符的反身性来证明。（如果它在你的逻辑中是自反的）。

注意：上面的实现是微不足道的。在OCaml标准库List.length中实现如下：

let rec length_aux len = function
    [] -> len
  | a::l -> length_aux (len + 1) l

let length l = length_aux 0 l

这里的证明义务length (x::xs) = 1 + length xs 产生了证明length_aux 0 (x::xs) = 1 + length_aux 0 xs 的义务。这不那么琐碎。

【讨论】：

【解决方案2】：

我首先要说的是，长度是由归纳定义的，void的长度是0，length(h::l) = 1 + length(l)。

然后，串联也由归纳定义，[]@l=l 和 [h]@l = h::l。

length 是一个将 @ 映射到 + 的函数：证明是使用上述属性的归纳证明。您继续对 l1 进行归纳：当 l1 为空时，属性 length(l1@l2) = length(l1)+length(l2) （归纳公理）。然后假设该属性对于长度为 n 的 l1 是正确的，您想证明它对于 n+1 是正确的。 length(h::l1@l2) = 1 + length(l1@l2) （感谢长度定义）。然后通过归纳假设，你length(l1@l2) = length(l1)+length(l2)，你得出结论。

【讨论】：