Agda:我能证明具有不同构造函数的类型是不相交的吗？
Agda:我能证明具有不同构造函数的类型是不相交的吗？
提问于 2020-01-13 03:31:41
如果我试图证明Nat和Bool在Agda中不相等：
open import Data.Nat
open import Data.Bool
open import Data.Empty
open import Relation.Binary.PropositionalEquality
noteq : ℕ ≡ Bool -> ⊥
noteq () 我得到了错误：
Failed to solve the following constraints:
Is empty: ℕ ≡ Bool我知道不可能对类型本身进行模式匹配，但令我惊讶的是，编译器没有看到Nat和Bool具有不同的(类型)构造函数。
在Agda中有没有办法证明这一点？或者是不支持Agda中涉及类型的不等式？
回答 1
Stack Overflow用户
回答已采纳
发布于 2020-01-13 04:13:48
证明两个集合在Agda中不同的唯一方法是利用它们在基数方面的差异。如果它们有相同的基数，那么你无法证明任何东西:这与立方是不兼容的。
下面是Nat和Bool不相等的一个证明：
open import Data.Nat.Base
open import Data.Bool.Base
open import Data.Sum.Base
open import Data.Empty
open import Relation.Binary.PropositionalEquality
-- Bool only has two elements
bool : (a b c : Bool) → a ≡ b ⊎ b ≡ c ⊎ c ≡ a
bool false false c = inj₁ refl
bool false b false = inj₂ (inj₂ refl)
bool a false false = inj₂ (inj₁ refl)
bool true true c = inj₁ refl
bool true b true = inj₂ (inj₂ refl)
bool a true true = inj₂ (inj₁ refl)
module _ (eq : ℕ ≡ Bool) where
-- if Nat and Bool are the same then Nat also only has two elements
nat : (a b c : ℕ) → a ≡ b ⊎ b ≡ c ⊎ c ≡ a
nat rewrite eq = bool
-- and that's obviously nonsense...
noteq : ⊥
noteq with nat 0 1 2
... | inj₁ ()
... | inj₂ (inj₁ ())
... | inj₂ (inj₂ ())页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/59707418
复制相关文章
相似问题
腾讯云开发者
