我可以告诉Coq从n到n + 2进行归纳吗？

Question

我试图看看是否可以evenb n = true <-> exists k, n = double k从https://softwarefoundations.cis.upenn.edu/lf-current/Logic.html证明,而不涉及奇数.我尝试过以下内容:

Theorem evenb_double_k : forall n,
  evenb n = true -> exists k, n = double k.
Proof.
  intros n H. induction n as [|n' IHn'].
  - exists 0. reflexivity.
  - (* stuck *)

但显然感应一次只能起作用一个自然数,exists k : nat, S n' = double k显然不可证明.

n' : nat
H : evenb (S n') = true
IHn' : evenb n' = true -> exists k : nat, n' = double k
______________________________________(1/1)
exists k : nat, S n' = double k

有没有办法让感应从n到n + 2？

Answer 1

有一种叫做的策略fix.我将尝试解释高级别的情况,因为我认为这是一个很酷的黑客,但要警告这fix是一把双刃剑,通常不建议使用:它取决于Coq的真正低级细节,这使得证明非常脆弱,当它们中断时,错误信息很难理解.

fix foo i,哪里foo是一个新的变量,并且i是一个整数,是一个适用于至少有i参数的目标的策略(例如,forall n, evenb n = true -> ...有两个:n和证明evenb n = true),并假定你试图证明的目标,命名为新的假设foo.(是的,你没有看错.)

Theorem evenb_double_k : forall n,
  evenb n = true -> exists k, n = double k.
Proof.
  fix self 1.

(*

1 subgoal (ID 17)

  self : forall n : nat,
         evenb n = true -> exists k : nat, n = double k
  ============================
  forall n : nat, evenb n = true -> exists k : nat, n = double k

 *)

当然,有一个问题:这个假设必须应用于一个适当的子项n(这是目标的第一个参数,这就是fix self 1平均值的数字参数,我们说第一个参数是减少的参数).什么是适当的子项n？这是一个只有通过破坏才能获得的价值,n至少一次.

请注意,如果您仍然决定self直接应用假设,Coq不会立即抱怨(n这不是一个适当的子项).Coq仅检查"子项"要求Qed.编辑:您也可以随时使用该命令Guarded进行检查.

  apply self. (* seems fine, all goals done. *)
Qed. (* ERROR! *)

您可以近似地将其想象fix为强诱导的一种形式,其中self对所有小于当前项的术语给出归纳假设(),而不仅仅是直接的前辈.然而,这种"次要"关系实际上并没有出现在声明中self.(这种特殊性是制造fix低级别,危险策略的原因.)

在fix你通常想要destruct减少参数之后.这是fix允许您的证明遵循结构的地方evenb.下面,我们立即再次破坏S.所以,我们得到三种情况:n = O,n = S O,n = S (S n')对于一些n' : nat.

第一种情况很容易,第二种情况是空洞的,第三种情况是需要"诱导假设" self的地方n'.

Proof.
  fix self 1.
  intros n.
  destruct n as [| [| n']].
  - exists 0; reflexivity.
  - discriminate.
  - simpl. intro H.
    apply self in H.
    destruct H as [k Hk].
    exists (S k).
    rewrite Hk; reflexivity.
Qed.

一些推理是相当通用的,它可以被拉出到一个自定义的感应原理甚至nats,这具体是另一个Theorem.

Theorem even_ind :
  forall (P : nat -> Prop),
    P O ->
    (forall n, evenb n = true -> P n -> P (S (S n))) ->
    forall n, evenb n = true -> P n.

将它与标准感应原理nat相比较,实际上也是一个定理,命名为nat_ind.这是induction战术在引擎盖下使用的.

About nat_ind.

(* nat_ind :
     forall P : nat -> Prop,
       P 0 ->
       (forall n : nat, P n -> P (S n)) ->
       forall n : nat, P n
 *)

归纳步骤中的nat_ind去从n到S n,而对于诱导步骤even_ind,从去n到S (S n),并有一个额外的假设说,我们的数字是偶数.

的证明even_ind遵循类似的结构evenb_double_k,尽管它是比较抽象的,因为它概括了所有谓词P上nat.

Proof.
  intros P HO HSS.
  fix self 1.
  intros n.
  destruct n as [| [| n']].
  - intro; apply HO.
  - discriminate.
  - intros H. apply HSS.
    + apply H.
    + apply self.
      apply H.
Qed.

这里的另一种方法是根本不使用fix(因为它应该避免),但保持induction原始来证明替代even_ind原则.这很好nat,但对于一些复杂的归纳类型,默认的归纳原理太弱,手写fix是唯一的方法.

最后,回到过去evenb_double_k,我们可以使用新的归纳原理apply even_ind,而不是fix或induction.现在,我们只得到两个有意义的案件,O并S (S n')在那里n'为偶数.

Theorem evenb_double_k' : forall n,
  evenb n = true -> exists k, n = double k.
Proof.
  apply even_ind.
  - exists 0. reflexivity.
  - intros n H [k Hk].
    exists (S k).
    rewrite Hk.
    reflexivity.
Qed.

本答案中使用的定义:

Fixpoint evenb n :=
  match n with
  | S (S n') => evenb n'
  | S O => false
  | O => true
  end.

Fixpoint double k :=
  match k with
  | O => O
  | S k' => S (S (double k'))
  end.

Answer 2

是的,一点没错!让我们从这个答案中使用归纳原理.

From Coq Require Import Arith.

Lemma pair_induction (P : nat -> Prop) :
  P 0 -> P 1 ->
  (forall n, P n -> P (S n) -> P (S (S n))) ->
  forall n, P n.
Proof.
  intros H0 H1 Hstep n.
  enough (P n /\ P (S n)) by easy.
  induction n; intuition.
Qed.

现在我们可以像这样使用新原理(我用stdlib对应的方式切换非标准函数,以便编译所有内容):

Theorem evenb_double_k : forall n,
  Nat.even n = true -> exists k, n = Nat.double k.
Proof.
  intros n Ev.
  induction n as [| |n IHn _] using pair_induction.
  (* the rest of the proof has been removed to not spoil the fun *)
Qed.