时间戳

首页 > 解决方案 > 如何在不取消 coq 中的积极性检查的情况下使用这些归纳法？

coq - 如何在不取消 coq 中的积极性检查的情况下使用这些归纳法？

问题描述

要使用 以简单的方式编写Inductive，我有如下代码。

Inductive T :=
  | t0
  | t1 (a b : T)
  | ..
  | tk (P : T->Prop) (t : T)
  | tn (P : T->T->Prop) (t : T)
  | ..
  end
.

但是，我必须Unset Positivity Checking使用T，也不能Fixpoint使用T. 我可以使用替代方案，例如bool代替Prop. 这就是我的代码现在的样子。

Inductive有没有办法使用而不是取消设置积极性检查来解决问题？

标签： coq

解决方案

你不能。您的类型T太大以至于破坏了逻辑的一致性。

Unset Positivity Checking.

Inductive T := tk (P : T -> bool).

Definition shaves x :=
  match x with tk f => f x end.

Definition barber :=
  tk (fun x => negb (shaves x)).

Goal False.
Proof.
assert (negb (shaves barber) = shaves barber).
{ change (negb (negb (shaves barber)) = shaves barber).
  now destruct shaves. }
now destruct shaves.
Qed.

推荐阅读