如何使用这些归纳法而不在coq中取消设置阳性检查?

问题描述 投票:0回答:1

[使用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
1个回答
1
投票

不,你不能。您的类型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.
© www.soinside.com 2019 - 2024. All rights reserved.