在 Coq 中定义递归列表长度不确定我的函数是否错误并卡住了

Question

所以我试图定义列表长度函数的尾递归版本并证明该函数与“长度”函数相同下面是我的代码。证明时卡住了

Fixpoint length_tail (A: Type) (l: list A) (len: nat): nat :=
  match l, len with
  | [], len => len
  | _ :: t, len => length_tail _ t (1 + len)
end.

Example length_rev: forall {A: Type} {l1: list A}, 
  @length_tail _ l1 0 = @length _ l1.
Proof.
  intros.
  induction l1.
  - simpl. reflexivity.
  - simpl.
    rewrite <- IHl1.
    + simpl.
Admitted.

下面是“长度”的原始函数：

Fixpoint length (l:natlist) : nat :=
  match l with
  | nil => O
  | h :: t => S (length t)
  end.

如果有人可以提供帮助或提供一些提示，将不胜感激！！谢谢！

Answer 1

几件事：

首先，您在函数中对 l 和 len 累加器进行模式匹配，但您没有查看其形状，下面的方法也一样：

Fixpoint length_tail (A: Type) (l: list A) (len: nat): nat :=
  match l with
  | [] => len
  | _ :: t => length_tail _ t (1 + len)
  end.

其次，你面临的问题是你要用归纳法证明的引理不够通用。实际上，您假设累加器是 0，但正如您在递归调用中看到的那样，您有 1 + len（顺便说一句，它只是 S len），它永远不会相等至 0.

为了通过归纳法证明这一点，您需要证明一些更强的东西。通常，您希望根据 length l 给出一个等于 length_tail l len 的表达式，这样当用 0 实例化时，您会得到 length l.

对我来说，length_tail l len = len + length l 是个不错的候选人。在使用累加器证明函数的属性时，您将不得不经常这样做。

有几种方法可以解决这个问题：

你可以直接证明更一般的引理然后得到一个推论，它可能对其他事情有用。
你可以在你的证明中使用 assert 更强的引理，然后用它作为结论。
或者您可以 generalize 在您的证明中实现您的目标。我个人不会使用它，但我会展示它来说明可以做什么。

Fixpoint length_tail {A : Type} (l: list A) (len: nat): nat :=
  match l, len with
  | [], len => len
  | _ :: t, len => length_tail t (1 + len)
end.

Example length_rev : forall {A: Type} {l : list A},
  length_tail l 0 = length l.
Proof.
  intros A l.
  change (length l) with (0 + length l).
  generalize 0 as n.
  (* Now the goal is forall n : nat, length_tail l n = n + length l *)

请注意，我在 length_tail 中将类型标记为隐式类型，这样可读性更好，你不觉得吗？

在 Coq 中定义递归列表长度不确定我的函数是否错误并卡住了

Define list length in recursion in Coq Not sure if my function is wrong and got stuck

coq

coq-tactic

在 Coq 中定义递归列表长度 不确定我的函数是否错误并卡住了

Define list length in recursion in Coq Not sure if my function is wrong and got stuck

coq

coq-tactic

在 Coq 中定义递归列表长度不确定我的函数是否错误并卡住了