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

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.