<div dir="ltr"><div><div><div><div><div><div>Hi Pierre,<br><br></div>I've encountered the same problem with the following example:<br><br><div style="margin-left:40px">drop-fs : ∀ {o} (x y : Fin o) → fs x ≡ fs y → x ≡ y<br>
</div><div style="margin-left:40px">drop-fs x .x refl = refl<br></div><br></div>With my new flag enabled, this gives the following error:<br><br><div style="margin-left:40px">Cannot eliminate reflexive equation o = o of type ℕ because K has<br>
been disabled.<br>when checking that the pattern refl has type fs x ≡ fs y<br></div><br></div>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:<br>
<br><div style="margin-left:40px">add-suc : {m n : ℕ} → m ≡ n → suc m ≡ suc n<br>add-suc refl = refl<br><br>drop-suc : {m n : ℕ} → suc m ≡ suc n → m ≡ n<br>drop-suc refl = refl<br><br>add-drop-lemma : {m n : ℕ} (q : suc m ≡ suc n) → add-suc (drop-suc q) ≡ q<br>
add-drop-lemma refl = refl<br><br>K-for-ℕ : {n : ℕ} → (P : n ≡ n → Set) → P refl → (q : n ≡ n) → P q<br>K-for-ℕ {zero} P p refl = p<br>K-for-ℕ {suc n} P p q = J (λ q _ → P q) aux (add-drop-lemma q) <br> where<br> aux : P (add-suc (drop-suc q))<br>
aux = K-for-ℕ {n} (λ q → P (add-suc q)) p (drop-suc q)<br></div><br></div>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...<br>
<br></div>Best,<br></div>Jesper<br> </div><div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Nov 22, 2013 at 2:45 PM, Pierre Boutillier <span dir="ltr"><<a href="mailto:pierre.boutillier@pps.univ-paris-diderot.fr" target="_blank">pierre.boutillier@pps.univ-paris-diderot.fr</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
I'm working on this problem from the other side. I'm in Coq so I know<br>
that I don't have K but I try to push the pattern matching compiler<br>
further and further. (Sketch of that can been seen at<br>
<a href="http://gallium.inria.fr/blog/a-new-Coq-tactic-for-inversion/" target="_blank">http://gallium.inria.fr/blog/a-new-Coq-tactic-for-inversion/</a> )<br>
If I knew a way to characterize the pattern matching problems my<br>
algorithm is able to tackle, my phd would have already been sent to its<br>
reviewers. Consequently, I'm really really interested by the condition<br>
you propose! :-)<br>
<br>
In fact, I give up on giving a characterisation and I claim that my<br>
algorithm works correctly if its type-checking in your (Agda) setting<br>
does not use variable - variable equality! That's correct (so I can only<br>
argue for your proposal) but not complete. I share with you my<br>
archenemy. The problem:<br>
<br>
{-# OPTIONS --without-K #-}<br>
<br>
module jouet where<br>
<br>
data nat : Set where<br>
O : nat<br>
S : (n : nat) -> nat<br>
<br>
data fin : nat -> Set where<br>
F1 : (n : nat) -> fin (S n)<br>
FS : {n : nat} (f : fin n) -> fin (S n)<br>
<br>
data finEq : {m : nat} -> fin m -> fin m -> Set where<br>
F1Eq : {m : nat} -> finEq (F1 m) (F1 m)<br>
FSEq : {m : nat} {f1 f2 : fin m} -> finEq f1 f2 -> finEq (FS f1) (FS<br>
f2)<br>
<br>
invertFSEq : {n : nat} {f1 f2 : fin n} -> finEq (FS f1) (FS f2) -><br>
finEq f1 f2<br>
invertFSEq x = {!x!}<br>
<br>
does NOT imply K. (crazy people could read above the CIC term for it<br>
found by my algorithm) But Agda is also right when it says:<br>
/tmp/jouet.agda:18,16-20<br>
The variables<br>
n<br>
n<br>
f1<br>
n<br>
f2<br>
in the indices<br>
{_}<br>
FS f1<br>
FS f2<br>
are not distinct (note that parameters count as constructor<br>
arguments)<br>
when checking that the expression ? has type finEq .f1 .f2<br>
<br>
So I'm stuck! I tried to shake my hands and say "unlinearity driven by<br>
the type of the inductive family are not K, others are" but I didn't<br>
succeed to find a convincing formulation.<br>
<br>
Definition diag_x1 (x1 : nat__) : Fin__ x1 -> Type :=<br>
case x1 predicate fun (n2 : nat__) => Fin__ n2 -> Type of<br>
|O: fun (_ : Fin O) => True<br>
|S: fun (x0 : nat__) => fun (f1' : Fin__ (S_ x0)) =><br>
forall (f2 : Fin__ (S_ x0)), FinEq__ (S_ x0) f1' f2 -> Type<br>
end.<br>
<br>
Definition diag_x2 (x2 : nat__) : Fin__ x2 -> Type :=<br>
case x2 predicate fun (n3 : nat__) => Fin__ n3 -> Type of<br>
|O: fun (_ : Fin__ O_) => True<br>
|S: fun (x0 : nat__) => fun (f2' : Fin__ (S_ x0)) => forall (f1'' :<br>
Fin__ x0),<br>
FinEq__ (S_ x0) (FS_ x0 f1'') f2' -> Type<br>
end.<br>
<br>
Definition diag_H (n0 : nat__) : forall (f1 f2 : Fin__ n), FinEq__ n f1<br>
f2 -> Type :=<br>
case n0 predicate fun (n1 : nat__) => forall (f4 f5 : Fin__ n1), FinEq__<br>
n1 f4 f5 -> Type of<br>
|O: fun (f4 f5 : Fin__ O_) (_ : FinEq__ O f4 f5) => True__<br>
|S: fun (x : nat) => fun (f4 : Fin (S x)) =><br>
case f4 predicate _diag_x1 of<br>
|F1: fun (n1 : nat__) => fun (f5 : Fin__ (S_ n1))<br>
(_ : FinEq__ (S_ n1) (F1_ n1) f5) => True__<br>
|FS: fun (n1 : nat__) (f5 : Fin__ (S n1)) => fun (f6 : Fin__ (S n1))<br>
=><br>
(case f6 predicate _diag_x2 of<br>
|F1: fun (n2 : nat__) => fun (f7 : Fin n2)<br>
(_ : FinEq (S n2) (FS n2 f7) (F1 n2)) => True<br>
|FS: fun (n2 : nat__) (f7 : Fin__ n2) => fun (f8 : Fin__ n2)<br>
(_ : FinEq__ (S_ n2) (FS_ n2 f8) (FS_ n2 f7)) =><br>
FinEq__ n2 f8 f7<br>
end f5)<br>
end<br>
end.<br>
<br>
Definition invert_H (n : nat__) (f1 f2 : Fin__ n)<br>
(H : FinEq__ (S_ n) (FS_ n f1) (FS_ n f2)) : FinEq__ n f1 f2 :=<br>
case H predicate fun (n0 : nat__) (f f0 : Fin__ n0) (H' : FinEq__ n0 f<br>
f0) => _diag_n f f0 H' of<br>
|F1Eq: fun (_ : nat__) => I<br>
|FSEq: fun (m : nat__) (f' f'' : Fin__ m) (H0 : FinEq__ m f' f'') => H0<br>
end.<br>
<br>
Le vendredi 22 novembre 2013 à 13:34 +0100, Jesper Cockx a écrit :<br>
<div class="HOEnZb"><div class="h5">> Dear all,<br>
><br>
> Lately I have been working on a proof of correctness for the<br>
> --without-K flag in Agda (someone should do it, right?). The proof<br>
> itself is not quite ready for prime time, but during my investigations<br>
> I actually discovered a more general (and, in my eyes, simpler)<br>
> formulation of pattern matching without K. In order to play around<br>
> with this idea, I implemented a new flag to Agda. Since a good number<br>
> of people here seem interested in this subject, I thought I'd share<br>
> it.<br>
><br>
> The idea is as follows: Suppose we want to split on a variable x of<br>
> type "D us" for some data type D with constructors "c_j : Delta_j -> D<br>
> vs_j". Instead of putting certain syntactic restrictions on the<br>
> indices "us" (as in the current implementation of --without-K), we<br>
> limit the algorithm for unification of "us" with "vs_j". We do this by<br>
> refusing to deleting reflexive equations of the form "x = x" where x<br>
> is a variable. All other unification steps (solution, injectivity,<br>
> disjointness, and acyclicity) keep working as usual. So for example,<br>
> we allow unifying "suc x" with "suc zero" or "suc x" with "suc<br>
> y" (where y != x), but not "suc x" with "suc x". This should rule out<br>
> any definitions that depend on K (if my proof is correct). It is also<br>
> more general than the current implementation, since the current<br>
> implementation guarantees that we will never encounter "x = x" during<br>
> unification.<br>
><br>
> In the attachment, you can find a patch to darcs agda. At the moment,<br>
> it adds a new flag called --new-without-K that restricts the<br>
> unification algorithm as described above. Here is an example of the<br>
> error message:<br>
> K : (A : Set) (x : A) → (p : x ≡ x) → p ≡ refl<br>
> K A x refl = refl<br>
><br>
> Cannot eliminate reflexive equation x = x of type A because K<br>
> has<br>
> been disabled.<br>
> when checking that the pattern refl has type x ≡ x<br>
> One advantage is that this solves the problem where you can split on a<br>
> variable of type "something ≡ x", but not "x ≡ something" (see<br>
> <a href="https://lists.chalmers.se/pipermail/agda/2013/005407.html" target="_blank">https://lists.chalmers.se/pipermail/agda/2013/005407.html</a> and<br>
> <a href="https://lists.chalmers.se/pipermail/agda/2013/005428.html" target="_blank">https://lists.chalmers.se/pipermail/agda/2013/005428.html</a>). For<br>
> example, the following examples typecheck with --new-without-K enabled<br>
> (but not with the old --without-K):<br>
> foo : (k l m : ℕ) → k ≡ l + m → {!!}<br>
> foo .(l + m) l m refl = {!!}<br>
><br>
> bar : (n : ℕ) → n ≤ n → {!!}<br>
> bar .zero z≤n = {!!}<br>
> bar .(suc m) (s≤s {m} p) = {!!}<br>
> I also added two tests to /test/succeed and /test/fail.<br>
><br>
> What I'd like you to do, is:<br>
> 1. Try out my modification on your favorite examples,<br>
> 2. Tell me what you think,<br>
> 3. If you think it's good, add it to the main Agda branch.<br>
><br>
> Best regards,<br>
> Jesper Cockx<br>
</div></div><div class="HOEnZb"><div class="h5">> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>