Агда: могу ли я доказать, что типы с разными конструкторами не пересекаются? - PullRequest
Новая
       65

Агда: могу ли я доказать, что типы с разными конструкторами не пересекаются?

3 голосов
/ 12 января 2020

Если я пытаюсь доказать, что 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 имеют разные (type) конструкторы.

Есть ли способ доказать что-то подобное в Agda? Или неравенства, связанные с типами в Agda, просто не поддерживаются?

1 Ответ

6 голосов
/ 12 января 2020

Единственный способ доказать, что два набора в Агде различны, - это использовать их различия с точки зрения мощности. Если у них один и тот же кардинал, вы не можете ничего доказать: это было бы несовместимо с кубическим.

Вот доказательство того, что 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₂ ())
...