为什么不可能对结论中使用的术语进行归纳？ [英] Why is it impossible to perform induction on a term that is used in conclusion?

问题描述

假设以下特定情况。

我们有一个相等的定义：

We have a definition of equality:

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

和豌豆坚果：

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

我们在nat上定义加法：

We define addition on nats:

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

现在我们想证明零是正确的。求和：

And now we want to prove that zero is neutral from right wrt. summing:

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

遗憾的是，以下证明的最后一行说 错误：结论中使用了n。 。

Sadly the last line of the following proofscripts says "Error: n is used in conclusion.".

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

官方文档中的错误并不多，我有些困惑-为什么会发生此错误？

There is not much about the error in official documentation and I am somewhat confused - why does this error occur?

使用标准库，我可以轻松证明定理：

Using the standard library, I can prove the theorem easily:

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

推荐答案

问题是您定义了 nawt 排序为 Prop 而不是 Type 或 Set 。默认情况下，为命题生成的归纳原理不允许我们证明有关这些命题证明的任何信息。考虑为 nawt 生成的默认归纳原理：

The problem is that you defined nawt with sort Prop instead of Type or Set. By default, the induction principles generated for propositions do not allow us to prove anything about proofs of those propositions. Consider the default induction principle generated for nawt:

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

因为 nawt_ind 量化了 Prop ，并且不超过 nat->道具，我们不能用它来证明您的目标。

Because nawt_ind quantifies over Prop, and not over nat -> Prop, we cannot use it to prove your goal.

解决方案是设置一些更改Coq默认行为的选项，例如

The solution is to set a few options that change Coq's default behavior, as in the following script.

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 生成正确的归纳原理。为了使归纳法起作用，重要的是给该原理命名为 nawt_ind ：这是默认名称是由Coq生成的，并且是归纳在被调用时寻找的那个。

The Elimination Schemes option causes Coq to automatically generate induction principles for data types and propositions. In this script, I merely turned it off, and used the Scheme command to generate the correct induction principle for nawt. For the induction tactic to work, it is important to give this principle the name nawt_ind: this is the default name that is generated by Coq, and is the one that induction looks for when called.

通常建议不要在 Prop 中定义自然数类型，而不是在 Type 中定义自然数类型，因为Coq对使用方式施加了限制 Prop 中存储的内容。例如，不可能显示 zewro 与 sawc zewro 不同。

That being said, I would generally advise against defining a type of natural numbers in Prop instead of Type, because Coq imposes restrictions on how you can use things that live in Prop. For instance, it is impossible to show that zewro is different from sawc zewro.

这篇关于为什么不可能对结论中使用的术语进行归纳？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！