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

Question

所以我试图定义一个列表长度函数的尾递归版本，并证明该函数与"length"相同函数下面是我的代码。当证明被卡住

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中将类型标记为隐式，这样它的可读性更强，你不觉得吗?