Agda 中的构造函数是否不相交？ （或者如何反驳 inj₁ x ≡ inj₂ y）

Question

我还需要一个引理来证明 inj₁ x ≡ inj₂ y 作为关于 Agda 中不相交联合类型 (⊎) 的更大定理的一部分是荒谬的。

这个结果直接来自 ⊎ 的两个构造函数，即 inj₁ 和 inj₂，它们是不相交的。 是阿格达的案例？如何证明？

这是完整的引理：

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Sum


lemma : ∀ {a b} {A : Set a} {B : Set b} {x : A} {y : B} → ¬ inj₁ x ≡ inj₂ y
lemma eq = ?

Answer 1

数据类型构造函数不相交。我会说这是 Agda 类型系统元理论中的一个定理。

你可以尝试 case eq 证明 (C-c C-c)，Agda 会发现矛盾：

lemma : ∀ {a b} {A : Set a} {B : Set b} {x : A} {y : B} → ¬ inj₁ x ≡ inj₂ y
lemma ()

这愉快地进行了类型检查。