[Agda] A correctness proof for pattern matching without K

[Martin Escardo]

On 02/04/14 13:15, Jesper Cockx wrote:
> The translation to eliminators uses the generic "no confusion" property
> of constructors from "A few constructions on constructors" by Conor et
> al. (2006). This property is defined by a two-level construction, so it
> needs (at least) the first universe Set. For the _+_ type, the
> construction looks like this:
>
> +-NoConfusion : {X₀ X₁ : Set} → X₀ + X₁ → X₀ + X₁ → Set
> +-NoConfusion (in₀ x) (in₀ y) = x ≡ y
> +-NoConfusion (in₀ x) (in₁ y) = ∅
> +-NoConfusion (in₁ x) (in₀ y) = ∅
> +-NoConfusion (in₁ x) (in₁ y) = x ≡ y

But x and y live in different types. Are you sure you mean x ≡ y?

> +-noConfusion : {X₀ X₁ : Set} (x y : X₀ + X₁) → x ≡ y → +-NoConfusion x y
> +-noConfusion (in₀ x) .(in₀ x) refl = refl
> +-noConfusion (in₁ x) .(in₁ x) refl = refl
>
> Both can easily written using the eliminators for _+_ and _≡_, see the
> paper for details. Now the definition of sum-disjoint from +-noConfusion
> is easy:
>
> sum-disjoint : {X Y : Set} {x : X} {y : Y} → in₀ x ≡ in₁ y → ∅
> sum-disjoint {x = x} {y = y} = +-noConfusion (in₀ x) (in₁ y)
>
> The actual translation looks much more complicated because it has to
> deal with possible multiple case splits and recursive calls, but the
> result is essentially the same.

Ok, I understand, modulo the x ≡ y issue.

Martin