[Agda] A correctness proof for pattern matching without K

[Jesper Cockx]

Dear all,

Some people might be interested that I finished the correctness proof for
pattern matching without K. It proves the following:

Let us restrict the unification algorithm used during case splitting in two
ways:
- It is not allowed to delete equations of the form "x = x".
- When applying injectivity on an equation "c us = c vs" of type "D pars
ixs", the datatype indices ixs (but not the parameters pars) should be
*self-unifiable*, i.e. unification of ixs with itself should succeed (while
still following these two restrictions).
Let f be a function defined by dependent pattern matching (i.e. it has a
valid case tree and is structurally recursive), where all case splits
follow the restrictions above. Then we can translate f to a definition
using only eliminators (*without* using the K axiom).

The motivation for these two restrictions, as well as the proof, can be
found in our submission to ICFP '14 called "Pattern matching without K",
available here <http://people.cs.kuleuven.be/%7Ejesper.cockx/Without-K/>.
The same page also contains a link to the updated implementation of my
--new-without-K flag, which enforces the two restrictions to the
unification algorithm above.

Here are some examples that are rejected by the current --without-K flag,
but are accepted by --new-without-K:

{-# OPTIONS --new-without-K #-}
module Counterexamples where

open import Data.Nat
open import Relation.Binary.PropositionalEquality

≤-self : (m : ℕ) → m ≤ m → ⊤
≤-self .zero (lz .zero) = tt
≤-self .(suc m) (ls m .m p) = tt

sum-right : (k l m : ℕ) → k ≡ (l + m) → ⊤
sum-right .(l + m) l m refl = tt

Compared to the regular --without-K, it now also handles parameters much
better. For example, the following is rejected by --without-K but accepted
by --new-without-K:

open import Data.List

head-≡ : {A : Set} {x y : A} {xs ys : List A} →
        x ∷ xs ≡ y ∷ ys → x ≡ y
head-≡ refl = refl

In fact, we place no restrictions on the parameters at all. On the other
hand, injectivity of indexed data still poses a problem:

open import Data.Fin using (Fin) renaming (zero to fz; suc to fs)

drop-fs : ∀ {n} (x y : Fin n) → fs x ≡ fs y → x ≡ y
drop-fs x .x refl = refl
-- Error: Cannot eliminate reflexive equation n = n of type ℕ because K has
been disabled.
-- when checking that the pattern refl has type fs x ≡ fs y

Be aware that this definition is rejected by the regular --without-K flag
as well. However, this kind of problem occurs somewhat more often than
before because of the second restriction to the unification algorithm. This
restriction is a necessary evil to solve the bug discussed in a previous
mail <https://lists.chalmers.se/pipermail/agda/2014/006367.html>, but I'll
be the first to agree that it seems overly restrictive.  In practice, I
don't usually run into this problem, but YMMV. I have tested my
implementation on Nils' --without-K library (
http://www.cse.chalmers.se/~nad/repos/equality/) without encountering any
problems. The easiest way to solve this problem, seems to add (manual or
automatic) detection of types that satisfy K on their own (i.e. homotopy
sets), for example ℕ. I'll probably be working on this in the future, but
in my opinion the implementation is already very usable right now.

All questions, remarks, and suggestions are very welcome.

Best regards,
Jesper Cockx
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140310/6f3a585e/attachment.html