证明可逆列表是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)两个或更多元素,在这种情况下l0 = x :: l1 ++ [x]某些元素x和一些列表l1如此l1 = rev l1.

现在,因为l1 = rev l1,以下三个案件之一必须举行......

递归案例分析将针对任何有限列表终止,l0因为所分析列表的长度在每次迭代时减少2.如果它终止于任何列表ln,那么它的所有外部列表l0也都是回文,因为通过在回文的任一端附加两个相同元素构建的列表也是回文.

我认为推理是合理的,但我不确定如何将其形式化.它可以变成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.

如有必要,我可以更详细地帮助您,只需发表评论.

祝好运 !

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.