使用Coq证明可逆列表是回文。

Question

这是我关于回文的归纳定义：

Inductive pal { X : Type } : list X -> Prop :=
  | pal0 : pal []
  | pal1 : forall ( x : X ), pal [x]
  | pal2 : forall ( x : X ) ( l : list X ), pal l -> pal ( x :: l ++ [x] ).

我想证明的定理来自Software Foundations：

Theorem rev_eq_pal : forall ( X : Type ) ( l : list X ),
  l = rev l -> pal l.

我的证明的非正式概述如下：

假设 l0 是一个任意列表，满足 l0 = rev l0。那么以下三种情况之一必定成立。对于 l0：

(a) 元素个数为零，则根据定义它是一个回文。

(b) 元素个数为一，则根据定义它也是一个回文。

(c) 元素个数大于等于二，则存在某个元素 x 和某个列表 l1，使得 l0 = x :: l1 ++ [x]，且满足 l1 = rev l1。

现在，由于 l1 = rev l1，以下三种情况之一必定成立...

由于每次迭代分析的列表长度都会减少 2，因此递归情况分析将终止任何有限列表 l0。如果它对于任何列表 ln 终止，那么从 l0 到 ln 的所有外部列表也均为回文，因为通过在回文两端添加两个相同的元素构造出的列表也是回文。

我认为这个推理是正确的，但我不确定如何将其形式化。它可以转变成 Coq 中的一个证明吗？对所使用的策略进行一些解释将特别有帮助。

- user287393

Answer 1

这是一个很好的例子，其中“直接”归纳根本不起作用，因为您不会直接在尾部进行递归调用，而是在尾部的一部分上进行递归调用。在这种情况下，我通常建议使用列表的长度来陈述引理，而不是列表本身。然后您可以将它专门化。可能会是这样：

Lemma rev_eq_pal_length: forall (X: Type) (n: nat) (l: list X), length l <= n -> l = rev l -> pal l.
Proof.
(* by induction on [n], not [l] *)
Qed.

Theorem rev_eq_pal: forall (X: Type) (l: list X), l = rev l -> pal l.
Proof.
(* apply the previous lemma with n = length l *)
Qed.

如果需要，我可以帮助你更详细地了解，只需要留下评论。

祝好运！

V.

编辑：为了帮助你，我需要以下引理来完成这个证明，你可能也需要它们。

Lemma tool : forall (X:Type) (l l': list X) (a b: X),                                                                                                         
            a :: l = l' ++ b :: nil -> (a = b /\ l = nil) \/ exists k, l = k ++ b :: nil.

Lemma tool2 : forall (X:Type) (l1 l2 : list X) (a b: X),                                                                                                         
     l1 ++ a :: nil = l2 ++ b :: nil -> a = b /\ l1 = l2.

- Vinz

Answer 2

你可以从良基归纳的形式中推导出你的归纳原理。

Notation " [ ] " := nil : list_scope.
Notation " [ x1 ; .. ; x2 ] " := (cons x1 .. (cons x2 nil) ..) : list_scope.
Open Scope list_scope.

Conjecture C1 : forall t1 f1 p1, (forall x1, (forall x2, f1 x2 < f1 x1 -> p1 x2) -> p1 x1) -> forall x1 : t1, p1 x1.
Conjecture C2 : forall t1 p1, p1 [] -> (forall x1 l1, p1 ([x1] ++ l1)) -> forall l1 : list t1, p1 l1.
Conjecture C3 : forall t1 p1, p1 [] -> (forall x1 l1, p1 (l1 ++ [x1])) -> forall l1 : list t1, p1 l1.
Conjecture C4 : forall t1 (x1 x2 : t1) l1, length l1 < length ([x1] ++ l1 ++ [x2]).

Theorem T1 : forall t1 p1,
  p1 [] ->
  (forall x1, p1 [x1]) ->
  (forall x1 x2 l1, p1 l1 -> p1 ([x1] ++ l1 ++ [x2])) ->
  forall l1 : list t1, p1 l1.
Proof.
intros t1 p1 h1 h2 h3.
induction l1 as [l1 h4] using (C1 (list t1) (@length t1)).
induction l1 as [| x1 l1] using C2.
eapply h1.
induction l1 as [| x2 l1] using C3.
simpl.
eapply h2.
eapply h3.
eapply h4.
eapply C4.
Qed.

您可以通过先将假设应用于结论，然后在f1 x1上使用结构归纳，然后使用关于<的一些事实来证明猜想C1。

要证明没有归纳假设的C3，您首先需要对is_empty l1进行情况分析，然后使用事实is_empty l1 = true -> l1 = []和is_empty l1 = false -> l1 = delete_last l1 ++ [get_last l1]（其中get_last需要一个默认值）。

- user3551663