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

我想证明的定理，来自软件基础:

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

我的证明的非正式概要如下:

Suppose l0 is an arbitrary list such that l0 = rev l0. Then one of the following three cases must hold. l0 has:

(a) zero elements, in which case it is a palindrome by definition.

(b) one element, in which case it is also a palindrome by definition.

(c) two elements or more, in which case l0 = x :: l1 ++ [x] for some element x and some list l1 such that l1 = rev l1.

Now, since l1 = rev l1, one of the following three cases must hold...

The recursive case analysis will terminate for any finite list l0 because the length of the list analyzed decreases by 2 through each iteration. If it terminates for any list ln, all of its outer lists up to l0 are also palindromes, since a list constructed by appending two identical elements at either end of a palindrome is also a palindrome.

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

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.

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

祝你好运!

五。

编辑:只是为了帮助您，我需要以下引理来证明这一点，您可能也需要它们。

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.