这是我对回文的归纳定义：
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是一个任意列表，使得l0 = rev l0。那么以下三种情况之一必须成立。l0 has:
(a) 零个元素，在这种情况下，根据定义它是回文。
(b) 一个元素，在这种情况下，根据定义它也是回文。
(c) 两个或更多元素，在这种情况下l0 = x :: l1 ++ [x]对于某些元素x和一些清单l1这样l1 = rev l1.
现在，自从l1 = rev l1，下列三种情况之一必须成立...
对于任何有限列表，递归案例分析都将终止l0因为每次迭代分析的列表长度都会减少 2。如果它终止于任何列表ln，其所有外部列表直到l0也是回文，因为通过在回文两端附加两个相同元素构建的列表也是回文。
我认为推理是合理的，但我不确定如何将其形式化。它可以在 Coq 中转化为证明吗？对所使用的策略如何发挥作用的一些解释会特别有帮助。
这是一个很好的例子，其中“直接”归纳根本不能很好地工作，因为您不是直接在尾部进行递归调用，而是在part尾巴的。在这种情况下，我通常建议用列表的长度来陈述你的引理，而不是在列表本身上。然后你可以专门化它。那会是这样的：
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.
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
