时间戳

首页 > 解决方案 > 宇宙与 sumbool 不一致

coq - 宇宙与 sumbool 不一致

问题描述

我已经定义并证明了以下引理：

    NM.In k m -> {NM.In k m0}+{NM.In k m1}.

我还可以证明一个对称引理：

    {NM.In k m0}+{NM.In k m1} -> NM.In k m

但是，当我尝试将它们合并为一个时：

    NM.In k m <-> {NM.In k m0}+{NM.In k m1}.

我收到以下错误：

The term "sumbool (@NM.In CarrierA k m0) (@NM.In CarrierA k m1)" has type 
"Set" while it is expected to have type "Prop" (universe inconsistency: Cannot enforce
Set = Prop).

这怎么可能解决？

标签： coq

解决方案

正如丹尼尔指出的那样，问题在于<->连接词只将命题作为论据，而sumbool生活在Set. 这可以通过几种方式规避：您可以替换sumbool为or，或者您可以替换iff为与计算相关的连接词：

Variables A B C : Prop.

Check (({A} + {B} -> C) * (C -> {A} + {B}))%type.

推荐阅读