如何进行不同的感应？

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.