2

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

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

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

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

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

但现在我必须证明一些事情

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

当我需要证明引理时，我很难理解，尤其是在看起来几乎微不足道的证明中。

4

2 回答 2

2

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

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

我们有证明义务：

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

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

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

and[]是 的语法糖Nil，whilex::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。这是不那么微不足道的。

于 2015-11-25T12:57:45.210 回答
1

我首先要说的是，该长度是由归纳定义的，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)，你得出结论。

于 2015-11-25T12:16:00.130 回答