4

I need one more lemma showing that inj₁ x ≡ inj₂ y is absurd as part of a larger theorem about disjoint union types (⊎) in Agda.

This result would follow directly from the two constructors for ⊎, namely inj₁ and inj₂, being disjoint. Is that the case in Agda? How do I prove it?

Here is the complete lemma:

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 = ?
phadej
  • 11,947
  • 41
  • 78
curiousleo
  • 296
  • 1
  • 7

1 Answers1

6

The data type constructors are disjoint. I'd say it's a theorem in Agda's type-system meta-theory.

You can try to case the eq proof (C-c C-c), and Agda will find the contradiction:

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

This happily type-checks.

phadej
  • 11,947
  • 41
  • 78
  • Haha, no way! I really ought to have tried that. Thanks. – curiousleo Jan 31 '15 at 12:25
  • 3
    You can also use large elimination to prove false with no primitive absurd patterns. The basic is that you can write a function that takes your `inj₁` to `⊤` and `inj₂` to `⊥`. You can then use `subst` with that function to "cast" a trivially obtainable value of type `⊤` to a `⊥`. – copumpkin Feb 05 '15 at 06:30