Agda:我能证明具有不同构造函数的类型是不相交的吗?
Agda: can I prove that types with different constructors are disjoint?
如果我试图证明 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 类型的不等式?
在 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₂ ())
如果我试图证明 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 类型的不等式?
在 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₂ ())