在没有存在策略的情况下证明可逆列表是 Coq 中的回文

Question

作为软件基础的练习，我想证明以下定理：

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

pal 定义如下：

Inductive pal {X:Type} : list X -> Prop :=
| pal_nil : pal []
| pal_one : forall x, pal [x]
| pal_rec : forall x l, pal l -> pal (snoc(x:: l) x).

但是为了证明这一点，我想使用一个使用 exists 的引理来举例说明：

foral (l l':list X) (a b:X), a::l = l' ++[b] -> (a=b /\ l=[]) \/ exists k, l = k ++ [b].

其实我想提一点比l少的。但是使用 destruct 策略似乎没有帮助。

为什么我不想用exists是因为在阅读软件基础这本书的时候，我们还没有看到exists。当然，有人会告诉我 exists 可以看作是 forall，但这种形式很难使用。

那么没有这样的引理如何证明这个定理呢？我卡住了。

Answer 1

你不能通过对 l 的直接归纳来证明你的定理。

对于归纳步骤，归纳假设是pal l（清除前提后），你要证明pal (x :: l)。但是归纳假设明显与结论相矛盾（除非repeat x n = l），所以不可用。

看到这本书直到现在都没有提到更奇特的归纳法，而且这是一个 5 星练习，我认为可以肯定地得出结论，你可以更自由地进行这个练习。

看看this other question。

Answer 2

如前所述，使用列表的长度更容易证明这个定理：

Theorem rev_pal_aux {X:Type} : forall (l:list X) (n:nat) , length l<= n -> l = rev l -> pal l.

然后就可以开始对n进行归纳了。

避免 exists 的关键点是使用反转。对于此证明，可以对 x::l=rev x::l 之类的东西使用反转，然后对 rev l（对于某些 l）使用析构。这样，您将得到 x :: l = snoc (x0 :: l0) x（l0 是新的）。

(l0) 是关键。在l0上需要用到归纳假设

最后，我使用了以下引理（不太容易证明）：

Lemma length_snoc_aux {X:Type} : forall (l m:list X) (n:nat) (x:X), length l <= n -> l = snoc m x -> length m <= n.

Proving that a reversible list is a palindrome in Coq without exists tactic