证明可逆列表是 Coq 中的回文答案

【问题标题】：Proving that a reversible list is a palindrome in Coq证明可逆列表是 Coq 中的回文
【发布时间】：2014-08-13 08:08:55
【问题描述】：

这是我对回文的归纳定义：

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] ).

以及我想证明的定理，来自软件基础：

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

我的证明的非正式大纲如下：

假设l0 是一个任意列表，例如l0 = rev l0。那么以下三种情况之一必须成立。 l0 有：

(a) 零个元素，在这种情况下，根据定义它是回文。

(b) 一个元素，在这种情况下，根据定义它也是一个回文。

(c) 两个或更多元素，在这种情况下，l0 = x :: l1 ++ [x] 用于某些元素x 和某些列表l1 使得l1 = rev l1。

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

对于任何有限列表l0，递归案例分析将终止，因为分析的列表的长度在每次迭代中都会减少 2。如果它对任何列表ln 终止，则其直到l0 的所有外部列表也是回文，因为通过在回文的任一端附加两个相同元素构造的列表也是回文。

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

【问题讨论】：

标签： coq palindrome theorem-proving logical-foundations

【解决方案1】：

你也可以从一种有根据的归纳中推导出你的归纳原理。

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需要一个默认值）。

【讨论】：

【解决方案2】：

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

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.

如有需要，我可以为您提供更详细的帮助，请发表评论。

祝你好运！

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

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.

【讨论】：