11

这是我对回文的归纳定义：

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.

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

假设l0是一个任意列表，使得l0 = rev l0. 那么以下三种情况之一必须成立。l0有：

(a) 零元素，在这种情况下，根据定义它是回文。

(b) 一个元素，在这种情况下，根据定义，它也是一个回文。

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

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

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

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

4

2 回答 2

15

这是一个很好的例子，其中“直接”归纳根本不能很好地工作，因为您不是直接在尾部进行递归调用，而是在尾部的一部分上进行。在这种情况下，我通常建议用列表的长度来说明你的引理，而不是在列表本身上。然后你可以专攻它。那将是这样的：

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.
于 2014-06-23T11:47:11.900 回答
3

你也可以从一种有根据的归纳中推导出你的归纳原理。

Notation " [ ] " := nil : list_scope.
Notation " [ x1 ; .. ; x2 ] " := (cons x1 .. (cons x2 nil) ..) : list_scope.
Open Scope list_scope.

Conjecture C1 : forall t1 f1 p1, (forall x1, (forall x2, f1 x2 < f1 x1 -> p1 x2) -> p1 x1) -> forall x1 : t1, p1 x1.
Conjecture C2 : forall t1 p1, p1 [] -> (forall x1 l1, p1 ([x1] ++ l1)) -> forall l1 : list t1, p1 l1.
Conjecture C3 : forall t1 p1, p1 [] -> (forall x1 l1, p1 (l1 ++ [x1])) -> forall l1 : list t1, p1 l1.
Conjecture C4 : forall t1 (x1 x2 : t1) l1, length l1 < length ([x1] ++ l1 ++ [x2]).

Theorem T1 : forall t1 p1,
  p1 [] ->
  (forall x1, p1 [x1]) ->
  (forall x1 x2 l1, p1 l1 -> p1 ([x1] ++ l1 ++ [x2])) ->
  forall l1 : list t1, p1 l1.
Proof.
intros t1 p1 h1 h2 h3.
induction l1 as [l1 h4] using (C1 (list t1) (@length t1)).
induction l1 as [| x1 l1] using C2.
eapply h1.
induction l1 as [| x2 l1] using C3.
simpl.
eapply h2.
eapply h3.
eapply h4.
eapply C4.
Qed.

C1您可以通过首先将假设应用于结论，然后对 使用结构归纳f1 x1，然后使用关于 的一些事实来证明猜想<。

要证明C3没有归纳假设，您首先对 使用案例分析is_empty l1，然后使用事实is_empty l1 = true -> l1 = []和is_empty l1 = false -> l1 = delete_last l1 ++ [get_last l1](get_last将需要默认值)。

于 2014-06-23T14:10:44.243 回答