[Agda] A correctness proof for pattern matching without K

[Martin Escardo]

Very nice. I am looking forward to testing it with my without-K files.
Such a development was long overdue.
Martin

On 10/03/14 14:28, Jesper Cockx wrote:
> 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
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

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