<div dir="ltr"><div><div><div><div><div><div>Hi Pierre,<br><br></div>I&#39;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&#39;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">&lt;<a href="mailto:pierre.boutillier@pps.univ-paris-diderot.fr" target="_blank">pierre.boutillier@pps.univ-paris-diderot.fr</a>&gt;</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&#39;m working on this problem from the other side. I&#39;m in Coq so I know<br>
that I don&#39;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&#39;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&#39;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) -&gt; nat<br>
<br>
data fin : nat -&gt; Set where<br>
  F1 : (n : nat) -&gt; fin (S n)<br>
  FS : {n : nat} (f : fin n) -&gt; fin (S n)<br>
<br>
data finEq : {m : nat} -&gt; fin m -&gt; fin m -&gt; Set where<br>
  F1Eq : {m : nat} -&gt; finEq (F1 m) (F1 m)<br>
  FSEq : {m : nat} {f1 f2 : fin m} -&gt; finEq f1 f2 -&gt; finEq (FS f1) (FS<br>
f2)<br>
<br>
invertFSEq : {n : nat} {f1 f2 : fin n} -&gt;  finEq (FS f1) (FS f2) -&gt;<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&#39;m stuck! I tried to shake my hands and say &quot;unlinearity driven by<br>
the type of the inductive family are not K, others are&quot; but I didn&#39;t<br>
succeed to find a convincing formulation.<br>
<br>
Definition diag_x1 (x1 : nat__) : Fin__ x1 -&gt; Type :=<br>
case x1 predicate fun (n2 : nat__) =&gt; Fin__ n2 -&gt; Type of<br>
|O: fun (_ : Fin O) =&gt; True<br>
|S: fun (x0 : nat__) =&gt; fun (f1&#39; : Fin__ (S_ x0)) =&gt;<br>
   forall (f2 : Fin__ (S_ x0)), FinEq__ (S_ x0) f1&#39; f2 -&gt; Type<br>
end.<br>
<br>
Definition diag_x2 (x2 : nat__) : Fin__ x2 -&gt; Type :=<br>
case x2 predicate fun (n3 : nat__) =&gt; Fin__ n3 -&gt; Type of<br>
|O: fun (_ : Fin__ O_) =&gt; True<br>
|S: fun (x0 : nat__) =&gt; fun (f2&#39; : Fin__ (S_ x0)) =&gt; forall (f1&#39;&#39; :<br>
Fin__ x0),<br>
     FinEq__ (S_ x0) (FS_ x0 f1&#39;&#39;) f2&#39; -&gt; Type<br>
end.<br>
<br>
Definition diag_H (n0 : nat__) : forall (f1 f2 : Fin__ n), FinEq__ n f1<br>
f2 -&gt; Type :=<br>
case n0 predicate fun (n1 : nat__) =&gt; forall (f4 f5 : Fin__ n1), FinEq__<br>
n1 f4 f5 -&gt; Type of<br>
|O: fun (f4 f5 : Fin__ O_) (_ : FinEq__ O f4 f5) =&gt; True__<br>
|S: fun (x : nat) =&gt; fun (f4 : Fin (S x)) =&gt;<br>
    case f4 predicate _diag_x1 of<br>
    |F1: fun (n1 : nat__) =&gt; fun (f5 : Fin__ (S_ n1))<br>
          (_ : FinEq__ (S_ n1) (F1_ n1) f5) =&gt; True__<br>
    |FS: fun (n1 : nat__) (f5 : Fin__ (S n1)) =&gt; fun (f6 : Fin__ (S n1))<br>
=&gt;<br>
        (case f6 predicate _diag_x2 of<br>
        |F1: fun (n2 : nat__) =&gt; fun (f7 : Fin n2)<br>
            (_ : FinEq (S n2) (FS n2 f7) (F1 n2)) =&gt; True<br>
        |FS: fun (n2 : nat__) (f7 : Fin__ n2) =&gt; fun (f8 : Fin__ n2)<br>
            (_ : FinEq__ (S_ n2) (FS_ n2 f8) (FS_ n2 f7)) =&gt;<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&#39; : FinEq__ n0 f<br>
f0) =&gt; _diag_n f f0 H&#39; of<br>
|F1Eq: fun (_ : nat__) =&gt; I<br>
|FSEq: fun (m : nat__) (f&#39; f&#39;&#39; : Fin__ m) (H0 : FinEq__ m f&#39; f&#39;&#39;) =&gt; H0<br>
end.<br>
<br>
Le vendredi 22 novembre 2013 à 13:34 +0100, Jesper Cockx a écrit :<br>
<div class="HOEnZb"><div class="h5">&gt; Dear all,<br>
&gt;<br>
&gt; Lately I have been working on a proof of correctness for the<br>
&gt; --without-K flag in Agda (someone should do it, right?). The proof<br>
&gt; itself is not quite ready for prime time, but during my investigations<br>
&gt; I actually discovered a more general (and, in my eyes, simpler)<br>
&gt; formulation of pattern matching without K. In order to play around<br>
&gt; with this idea, I implemented a new flag to Agda. Since a good number<br>
&gt; of people here seem interested in this subject, I thought I&#39;d share<br>
&gt; it.<br>
&gt;<br>
&gt; The idea is as follows: Suppose we want to split on a variable x of<br>
&gt; type &quot;D us&quot; for some data type D with constructors &quot;c_j : Delta_j -&gt; D<br>
&gt; vs_j&quot;. Instead of putting certain syntactic restrictions on the<br>
&gt; indices &quot;us&quot; (as in the current implementation of --without-K), we<br>
&gt; limit the algorithm for unification of &quot;us&quot; with &quot;vs_j&quot;. We do this by<br>
&gt; refusing to deleting reflexive equations of the form &quot;x = x&quot; where x<br>
&gt; is a variable. All other unification steps (solution, injectivity,<br>
&gt; disjointness, and acyclicity) keep working as usual. So for example,<br>
&gt; we allow unifying &quot;suc x&quot; with &quot;suc zero&quot; or &quot;suc x&quot; with &quot;suc<br>
&gt; y&quot; (where y != x), but not &quot;suc x&quot; with &quot;suc x&quot;. This should rule out<br>
&gt; any definitions that depend on K (if my proof is correct). It is also<br>
&gt; more general than the current implementation, since the current<br>
&gt; implementation guarantees that we will never encounter &quot;x = x&quot; during<br>
&gt; unification.<br>
&gt;<br>
&gt; In the attachment, you can find a patch to darcs agda. At the moment,<br>
&gt; it adds a new flag called --new-without-K that restricts the<br>
&gt; unification algorithm as described above. Here is an example of the<br>
&gt; error message:<br>
&gt;         K : (A : Set) (x : A) → (p : x ≡ x) → p ≡ refl<br>
&gt;         K A x refl = refl<br>
&gt;<br>
&gt;         Cannot eliminate reflexive equation x = x of type A because K<br>
&gt;         has<br>
&gt;         been disabled.<br>
&gt;         when checking that the pattern refl has type x ≡ x<br>
&gt; One advantage is that this solves the problem where you can split on a<br>
&gt; variable of type &quot;something ≡ x&quot;, but not &quot;x ≡ something&quot; (see<br>
&gt; <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>
&gt; <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>
&gt; example, the following examples typecheck with --new-without-K enabled<br>
&gt; (but not with the old --without-K):<br>
&gt;         foo : (k l m : ℕ) → k ≡ l + m → {!!}<br>
&gt;         foo .(l + m) l m refl = {!!}<br>
&gt;<br>
&gt;         bar : (n : ℕ) → n ≤ n → {!!}<br>
&gt;         bar .zero z≤n = {!!}<br>
&gt;         bar .(suc m) (s≤s {m} p) = {!!}<br>
&gt; I also added two tests to /test/succeed and /test/fail.<br>
&gt;<br>
&gt; What I&#39;d like you to do, is:<br>
&gt; 1. Try out my modification on your favorite examples,<br>
&gt; 2. Tell me what you think,<br>
&gt; 3. If you think it&#39;s good, add it to the main Agda branch.<br>
&gt;<br>
&gt; Best regards,<br>
&gt; Jesper Cockx<br>
</div></div><div class="HOEnZb"><div class="h5">&gt; _______________________________________________<br>
&gt; Agda mailing list<br>
&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt; <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>