[Agda] A correctness proof for pattern matching without K

[Martin Escardo]

On 02/04/14 13:30, Jesper Cockx wrote:
> No, they live in the same type: in the first clause, they both live in
> X₀, and in the last clause they both live in X₁. They do have different
> types in the two middle clauses, but there they are not equated.

Oh, sorry, of course. I was reading too quickly.

Nice.

Thanks,
Martin

>
>
> On Wed, Apr 2, 2014 at 2:24 PM, Martin Escardo <m.escardo at cs.bham.ac.uk
> <mailto:m.escardo at cs.bham.ac.uk>> wrote:
>
>
>
>     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
>
>

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe