证明可逆清单是Coq中的回文 [英] Proving that a reversible list is a palindrome in Coq

问题描述

这是我对回文症的归纳定义:

Here is my inductive definition of palindromes:

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

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

And the theorem I want to prove, from Software Foundations:

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

我对证明的非正式概述如下:

My informal outlines of the proof are as follows:

假设l0是一个任意列表，例如l0 = rev l0.然后，以下三种情况之一必须成立. l0具有:

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

(a)零元素，在这种情况下，顾名思义就是回文.

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

(b)一个元素，在这种情况下，顾名思义也是回文.

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

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

(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.

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

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

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

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中将其转换为证明吗?有关使用战术如何工作的一些解释将特别有帮助.

I think the reasoning is sound, but I'm not sure how to formalize it. Can it be turned into a proof in Coq? Some explanations of how the tactics used work would be especially helpful.

推荐答案

这是一个很好的示例，其中直接"归纳根本无法正常工作，因为您没有直接在尾部进行递归调用，而是在<尾巴的strong>部分.在这种情况下，我通常建议用列表的长度而不是列表本身来说明您的引理.然后，您可以对其进行专门化.就像这样:

This is a nice example where "direct" induction does not work well at all because you don't directly make the recursive call on the tail, but on part of the tail. In such cases, I usually advice to state your lemma with the length of the list, not on the list itself. You can then specialize it. That would be something like:

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.

如有必要，我可以为您提供更多详细信息.

I can help you in more detail if necessary, just leave a comment.

祝你好运！

V.

为了帮助您，我需要以下引理进行证明，您可能也需要它们.

just to help you, I needed the following lemmas to make this proof, you might need them too.

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.

这篇关于证明可逆清单是Coq中的回文的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！