[使用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
解决问题,而不是取消设置阳性检查?
不,你不能。您的类型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.