假设以下特定情况。
我们有一个平等的定义：
Inductive eqwal {A : Type} (x : A) : A -> Prop :=
eqw_refl : eqwal x x.
和豌豆坚果：
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.
现在我们要证明零从正确的角度是中性的。总结：
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.
问题是您nawt使用sortProp而不是Typeor进行定义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，因为勒柯克强加给你如何使用的东西，住在限制Prop。例如，不可能显示与zewro的不同sawc zewro。
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句