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

Question

我在处理这些看似微不足道的证明时遇到了麻烦。

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

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

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

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

但现在我必须按照

的思路证明一些事情

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

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

Answer 1

我先说，length是归纳法定义的，void的length为0，length(h::l) = 1 + length(l).

然后，连接也由归纳法定义，[]@l=l，和[h]@l = h::l。

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

Answer 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)

和[]是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的义务。这不那么琐碎。

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

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

ocaml

proof

induction

proof-of-correctness