如何以不同的方式进行归纳？

Question

我正在用 Coq 做一个练习，试图证明一个列表是否等于它的倒数，它是一个回文。以下是我如何定义回文：

Inductive pal {X : Type} : list X -> Prop :=
  | emptypal : pal []
  | singlpal : forall x, pal [x]
  | inducpal : forall x l, pal l -> pal (x :: l ++ [x]).

这是定理：

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

根据我的定义，我需要在提取前尾元素时进行归纳，但显然 coq 不会让我这样做，如果我强制它这样做，它会给出一个归纳结果绝对没有任何意义：

Proof.
  intros X l H. remember (rev l) as rl. induction l, rl.
  - apply emptypal.
  - inversion H.
  - inversion H.
  - (* stuck *)

上下文：

1 subgoals
X : Type
x : X
l : list X
x0 : X
rl : list X
Heqrl : x0 :: rl = rev (x :: l)
H : x :: l = x0 :: rl
IHl : x0 :: rl = rev l -> l = x0 :: rl -> pal l
______________________________________(1/1)
pal (x :: l)

显然，归纳上下文是非常错误的。有什么办法可以解决归纳问题吗？

Answer 1

我在这里提出的解决方案可能不是最短的，但我认为这是很自然的。

我的解决方案是在 list 上定义一个专门针对您的问题的归纳原理。

考虑自然数。不仅有标准归纳法 nat_ind 证明 P 0 和 forall n, P n -> P (S n)。但是还有其他归纳方案，例如强归纳lt_wf_ind，或者证明P 0、P 1和forall n, P n -> P (S (S n))的两步归纳。如果标准的归纳方案不足以证明你想要的属性，你可以尝试另一个。

我们可以对列表做同样的事情。如果标准归纳方案 list_ind 还不够，我们可以编写另一个有效的方案。在这个思路中，我们为列表定义了一个类似于nat上的两步归纳的归纳原理（我们将使用nat上的两步归纳来证明这个归纳方案的有效性），其中我们需要证明三种情况：P []、forall x, P [x]和forall x l x', P l -> P (x :: l ++ [x'])。该方案的证明是困难的部分。应用它来推导您的定理非常简单。

我不知道两步归纳方案是否是标准库的一部分，所以我将其作为公理引入。

Axiom nat_ind2 : forall P : nat -> Prop, P 0 -> P 1 ->
  (forall n : nat, P n -> P (S (S n))) -> forall n : nat, P n.

然后我们证明我们想要的归纳方案

Lemma list_ind2 : forall {A} (P : list A -> Prop) (P_nil : P [])
  (P_single : forall x, P [x])
  (P_cons_snoc : forall x l x', P l -> P (x :: l ++ [x'])),
  forall l, P l.
Proof.
  intros. remember (length l) as n. symmetry in Heqn. revert dependent l.
  induction n using nat_ind2; intros.
  - apply length_zero_iff_nil in Heqn. subst l. apply P_nil.
  - destruct l; [discriminate|]. simpl in Heqn. inversion Heqn; subst.
    apply length_zero_iff_nil in H0. subst l. apply P_single.
  - destruct l; [discriminate|]. simpl in Heqn.
    inversion Heqn; subst. pose proof (rev_involutive l) as Hinv.
    destruct (rev l). destruct l; discriminate. simpl in Hinv. subst l.
    rewrite app_length in H0.
    rewrite PeanoNat.Nat.add_comm in H0. simpl in H0. inversion H0.
    apply P_cons_snoc. apply IHn. assumption.
Qed.

使用这个归纳原理，你应该可以很容易地得出结论。

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

如何以不同的方式进行归纳？

How to do induction differently?

coq