[Agda] A correctness proof for pattern matching without K

[Jesper Cockx]

Martin,

Thank you for testing it on your Agda files, it's great to hear that it's
working for you.

On Wed, Apr 2, 2014 at 12:29 PM, Martin Escardo <m.escardo at cs.bham.ac.uk>wrote:

>
> (Wouldn't it be better if the patch simply made without-K work in your
> way, rather than require to change all files from without-K to
> new-without-K?)
>

Yes, but I kept the old version available for now for testing purposes and
to allow easy comparison between the two versions.


> I wonder what your automatic translation of my function in the above
> file to eliminators is. The reason I am asking is that what I prove
> above using pattern matching requires the use of a universe in MLTT.
> Does your automatic translation generate such a use of the universe?
>

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

+-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.


Jesper
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140402/f83bae2a/attachment-0001.html