为什么不能对结论中使用的术语进行归纳？

Question

假设以下特定场景.

我们有一个平等的定义:

Inductive eqwal {A : Type} (x : A) : A -> Prop :=
    eqw_refl : eqwal x x.

和peano nats:

Inductive nawt : Prop :=
    | zewro : nawt
    | sawc  : nawt -> nawt.

我们在nat上定义了加法:

Fixpoint plaws (m n : nawt) : nawt :=
    match m with
      | zewro => n
      | sawc m' => sawc (plaws m' n)
    end.

现在我们想证明零从正确的wrt中立.总结:

Theorem neutral_r : forall n : nawt, eqwal (plaws n zewro) n.

可悲的是,以下证明文件的最后一行说" 错误:n用于结论. ".

Proof.
intros.
induction n. - this is the culprit

官方文档中的错误并不多,我有点困惑 - 为什么会出现这种错误？

使用标准库,我可以轻松地证明这个定理:

Theorem neutral_r : forall n : nat,
  n + 0 = n.
Proof.
  induction n; try reflexivity.
  cbn; rewrite IHn; reflexivity.
Qed.

Answer 1

问题是您nawt使用sort Prop而不是Type或来定义Set.默认情况下,为命题生成的归纳原则不允许我们证明这些命题的证明.考虑生成的默认归纳原则nawt:

Check nawt_ind.
> nawt_ind : forall P : Prop, P -> (nawt -> P -> P) -> nawt -> P

因为nawt_ind量化超过Prop,而不是超过nat -> Prop,我们不能用它来证明你的目标.

解决方案是设置一些更改Coq默认行为的选项,如下面的脚本所示.

Inductive eqwal {A : Type} (x : A) : A -> Prop :=
    eqw_refl : eqwal x x.

Unset Elimination Schemes.

Inductive nawt : Prop :=
    | zewro : nawt
    | sawc  : nawt -> nawt.

Scheme nawt_ind := Induction for nawt Sort Prop.

Set Elimination Schemes.

Fixpoint plaws (m n : nawt) : nawt :=
    match m with
      | zewro => n
      | sawc m' => sawc (plaws m' n)
    end.

Theorem eqwal_sym {A : Type} (x y : A) : eqwal x y -> eqwal y x.
Proof. intros H. destruct H. constructor. Qed.

Theorem neutral_r : forall n : nawt, eqwal (plaws n zewro) n.
Proof.
intros. induction n as [|n IH]; simpl.
- constructor.
- apply eqwal_sym in IH. destruct IH. constructor.
Qed.

该Elimination Schemes选项使Coq自动生成数据类型和命题的归纳原则.在这个脚本中,我只是将其关闭,并使用该Scheme命令生成正确的感应原理nawt.为了使induction策略起作用,重要的是给这个原则命名nawt_ind:这是由Coq生成的默认名称,并且是induction在被调用时查找的名称.

话虽这么说,我通常建议不要定义一种自然数Prop而不是Type,因为Coq限制你如何使用生活中的东西Prop.例如,不可能表明与之zewro不同sawc zewro.