[Agda] A different implementation of --without-K

[Pierre Boutillier]

Hi,

I'm working on this problem from the other side. I'm in Coq so I know
that I don't have K but I try to push the pattern matching compiler
further and further. (Sketch of that can been seen at
http://gallium.inria.fr/blog/a-new-Coq-tactic-for-inversion/ )
If I knew a way to characterize the pattern matching problems my
algorithm is able to tackle, my phd would have already been sent to its
reviewers. Consequently, I'm really really interested by the condition
you propose! :-)

In fact, I give up on giving a characterisation and I claim that my
algorithm works correctly if its type-checking in your (Agda) setting
does not use variable - variable equality! That's correct (so I can only
argue for your proposal) but not complete. I share with you my
archenemy. The problem:

{-# OPTIONS --without-K #-}

module jouet where

data nat : Set where
  O : nat
  S : (n : nat) -> nat

data fin : nat -> Set where
  F1 : (n : nat) -> fin (S n)
  FS : {n : nat} (f : fin n) -> fin (S n)

data finEq : {m : nat} -> fin m -> fin m -> Set where
  F1Eq : {m : nat} -> finEq (F1 m) (F1 m)
  FSEq : {m : nat} {f1 f2 : fin m} -> finEq f1 f2 -> finEq (FS f1) (FS
f2)

invertFSEq : {n : nat} {f1 f2 : fin n} ->  finEq (FS f1) (FS f2) ->
finEq f1 f2
invertFSEq x = {!x!}

does NOT imply K. (crazy people could read above the CIC term for it
found by my algorithm) But Agda is also right when it says:
/tmp/jouet.agda:18,16-20
The variables
  n
  n
  f1
  n
  f2
in the indices
  {_}
  FS f1
  FS f2
are not distinct (note that parameters count as constructor
arguments)
when checking that the expression ? has type finEq .f1 .f2

So I'm stuck! I tried to shake my hands and say "unlinearity driven by
the type of the inductive family are not K, others are" but I didn't
succeed to find a convincing formulation.

Definition diag_x1 (x1 : nat__) : Fin__ x1 -> Type :=
case x1 predicate fun (n2 : nat__) => Fin__ n2 -> Type of
|O: fun (_ : Fin O) => True
|S: fun (x0 : nat__) => fun (f1' : Fin__ (S_ x0)) =>
   forall (f2 : Fin__ (S_ x0)), FinEq__ (S_ x0) f1' f2 -> Type
end.

Definition diag_x2 (x2 : nat__) : Fin__ x2 -> Type :=
case x2 predicate fun (n3 : nat__) => Fin__ n3 -> Type of
|O: fun (_ : Fin__ O_) => True
|S: fun (x0 : nat__) => fun (f2' : Fin__ (S_ x0)) => forall (f1'' :
Fin__ x0),
     FinEq__ (S_ x0) (FS_ x0 f1'') f2' -> Type
end.

Definition diag_H (n0 : nat__) : forall (f1 f2 : Fin__ n), FinEq__ n f1
f2 -> Type :=
case n0 predicate fun (n1 : nat__) => forall (f4 f5 : Fin__ n1), FinEq__
n1 f4 f5 -> Type of
|O: fun (f4 f5 : Fin__ O_) (_ : FinEq__ O f4 f5) => True__
|S: fun (x : nat) => fun (f4 : Fin (S x)) =>
    case f4 predicate _diag_x1 of
    |F1: fun (n1 : nat__) => fun (f5 : Fin__ (S_ n1))
          (_ : FinEq__ (S_ n1) (F1_ n1) f5) => True__
    |FS: fun (n1 : nat__) (f5 : Fin__ (S n1)) => fun (f6 : Fin__ (S n1))
=>
        (case f6 predicate _diag_x2 of
        |F1: fun (n2 : nat__) => fun (f7 : Fin n2)
            (_ : FinEq (S n2) (FS n2 f7) (F1 n2)) => True
        |FS: fun (n2 : nat__) (f7 : Fin__ n2) => fun (f8 : Fin__ n2)
            (_ : FinEq__ (S_ n2) (FS_ n2 f8) (FS_ n2 f7)) =>
            FinEq__ n2 f8 f7
        end f5)
    end
end.

Definition invert_H (n : nat__) (f1 f2 : Fin__ n)
 (H : FinEq__ (S_ n) (FS_ n f1) (FS_ n f2)) : FinEq__ n f1 f2 :=
case H predicate fun (n0 : nat__) (f f0 : Fin__ n0) (H' : FinEq__ n0 f
f0) => _diag_n f f0 H' of
|F1Eq: fun (_ : nat__) => I
|FSEq: fun (m : nat__) (f' f'' : Fin__ m) (H0 : FinEq__ m f' f'') => H0
end.

Le vendredi 22 novembre 2013 à 13:34 +0100, Jesper Cockx a écrit :
> Dear all,
> 
> Lately I have been working on a proof of correctness for the
> --without-K flag in Agda (someone should do it, right?). The proof
> itself is not quite ready for prime time, but during my investigations
> I actually discovered a more general (and, in my eyes, simpler)
> formulation of pattern matching without K. In order to play around
> with this idea, I implemented a new flag to Agda. Since a good number
> of people here seem interested in this subject, I thought I'd share
> it.
> 
> The idea is as follows: Suppose we want to split on a variable x of
> type "D us" for some data type D with constructors "c_j : Delta_j -> D
> vs_j". Instead of putting certain syntactic restrictions on the
> indices "us" (as in the current implementation of --without-K), we
> limit the algorithm for unification of "us" with "vs_j". We do this by
> refusing to deleting reflexive equations of the form "x = x" where x
> is a variable. All other unification steps (solution, injectivity,
> disjointness, and acyclicity) keep working as usual. So for example,
> we allow unifying "suc x" with "suc zero" or "suc x" with "suc
> y" (where y != x), but not "suc x" with "suc x". This should rule out
> any definitions that depend on K (if my proof is correct). It is also
> more general than the current implementation, since the current
> implementation guarantees that we will never encounter "x = x" during
> unification.
> 
> In the attachment, you can find a patch to darcs agda. At the moment,
> it adds a new flag called --new-without-K that restricts the
> unification algorithm as described above. Here is an example of the
> error message:
>         K : (A : Set) (x : A) → (p : x ≡ x) → p ≡ refl
>         K A x refl = refl
>         
>         Cannot eliminate reflexive equation x = x of type A because K
>         has 
>         been disabled.
>         when checking that the pattern refl has type x ≡ x
> One advantage is that this solves the problem where you can split on a
> variable of type "something ≡ x", but not "x ≡ something" (see
> https://lists.chalmers.se/pipermail/agda/2013/005407.html and
> https://lists.chalmers.se/pipermail/agda/2013/005428.html). For
> example, the following examples typecheck with --new-without-K enabled
> (but not with the old --without-K):
>         foo : (k l m : ℕ) → k ≡ l + m → {!!}
>         foo .(l + m) l m refl = {!!} 
>         
>         bar : (n : ℕ) → n ≤ n → {!!}
>         bar .zero z≤n = {!!}
>         bar .(suc m) (s≤s {m} p) = {!!}
> I also added two tests to /test/succeed and /test/fail.
> 
> What I'd like you to do, is:
> 1. Try out my modification on your favorite examples,
> 2. Tell me what you think,
> 3. If you think it's good, add it to the main Agda branch.
> 
> Best regards,
> Jesper Cockx 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda