[Agda] A different implementation of --without-K
Jesper Cockx
Jesper at sikanda.be
Fri Nov 22 15:20:22 CET 2013
Hi Pierre,
I've encountered the same problem with the following example:
drop-fs : ∀ {o} (x y : Fin o) → fs x ≡ fs y → x ≡ y
drop-fs x .x refl = refl
With my new flag enabled, this gives the following error:
Cannot eliminate reflexive equation o = o of type ℕ because K has
been disabled.
when checking that the pattern refl has type fs x ≡ fs y
The reason why drop-fs can still be proven (in a more complicated way) is
that ℕ is a (homotopy) set, i.e. it satisfies K even without assuming it as
an axiom:
add-suc : {m n : ℕ} → m ≡ n → suc m ≡ suc n
add-suc refl = refl
drop-suc : {m n : ℕ} → suc m ≡ suc n → m ≡ n
drop-suc refl = refl
add-drop-lemma : {m n : ℕ} (q : suc m ≡ suc n) → add-suc (drop-suc q) ≡ q
add-drop-lemma refl = refl
K-for-ℕ : {n : ℕ} → (P : n ≡ n → Set) → P refl → (q : n ≡ n) → P q
K-for-ℕ {zero} P p refl = p
K-for-ℕ {suc n} P p q = J (λ q _ → P q) aux (add-drop-lemma q)
where
aux : P (add-suc (drop-suc q))
aux = K-for-ℕ {n} (λ q → P (add-suc q)) p (drop-suc q)
If there were some way to automatically detect (some of) the types that are
sets, then we could use it to selectively eliminate reflexive equations x =
x when the type of x is a set. Maybe Hedberg's theorem (types with
decidable equality are sets) could be useful here...
Best,
Jesper
On Fri, Nov 22, 2013 at 2:45 PM, Pierre Boutillier <
pierre.boutillier at pps.univ-paris-diderot.fr> wrote:
> 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
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131122/a6eb2b5f/attachment-0001.html
More information about the Agda
mailing list