coq - 如何通过归纳证明列表的相等性？

Question

我对 Coq 很陌生。假设在一些我想证明的假设下l1 = l2，这两个都是列表。如果我想以归纳方式证明它，我想知道什么是一般策略。

我不知道有什么方法可以同时进行l1归纳l2。如果我首先在 上进行归纳l1，那么我最终将不得不l1 = l2在假设下证明的尾部t1 = l2在哪里，这显然是错误的。t1l1

标签： coq

Answer 1

通常这取决于你有什么样的假设。但是，作为一般原则，如果要在对一个列表进行归纳时同步两个列表，则必须对另一个列表进行泛化。

induction l in l' |- *.

或者

revert l'.
induction l.

也可能是您对两者都有一些假设，l并且l'您可以对其进行归纳。例如，Forall2谓词同步两个列表：

Inductive Forall2 (A B : Type) (R : A -> B -> Prop) : list A -> list B -> Prop :=
| Forall2_nil : Forall2 R [] []
| Forall2_cons : forall (x : A) (y : B) (l : list A) (l' : list B), R x y -> Forall2 R l l' -> Forall2 R (x :: l) (y :: l')

如果您对此进行归纳，它将同时破坏两个列表。