[Agda] A correctness proof for pattern matching without K

[Jesper Cockx]

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.


On Wed, Apr 2, 2014 at 2:24 PM, Martin Escardo <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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140402/3eb48c6a/attachment.html