<div dir="ltr"><div><div><div><div><div><div><div><div><div><div>A little more analysis from my part. The injectivity rule in the EDPM paper has the following form (somewhat simplified):<br><br></div>m : s ≃ t -> P ⊢ injectivity m : c s ≃ c t -> P<br>
<br></div>
where ≃ is Conor's heterogeneous equality. As we all know, the elimination rule for heterogeneous equality is equivalent with K, so we should use the homogeneous equality instead:<br><br>m : s ≡ t -> P ⊢ injectivity m : c s ≡ c t -> P<br>
<br></div>Unfortunately, this turns out to be insufficient for pattern matching. What we need instead is a version of injectivity where P is dependent on the proof of c s ≡ c t:<br>
<br>m : (e : s ≡ t) -> P (cong c e) ⊢ injectivity m : (e : c s ≡ c t) -> P e<br><br></div>This works fine as long as the type of c is just a simple data type. When we consider indexed data types, we can no longer be sure that the equation c s ≡ c t is homogeneous. So an additional equation on the indices is introduced, and P is made dependent on it as well. So suppose for simplicity "D : U -> Set" is a data type with a single constructor "c : (x : A) -> D (u x)" and define "us := u s" and "ut := u t". We need this auxiliary function:<br>
<br>conf : (e : s ≡ t) → subst D (cong u e) (c s) ≡ c t<br>conf e = J (λ t e → subst D (cong u e) (c s) ≡ c t) e refl<br><br>Then we get the correct version of injectivity:<br>
<br></div>m : (e : s ≡ t) -> P (cong u e) (conf e) ⊢ injectivity m : (eu : us ≡ ut) (e : subst D eu (c s) ≡ c t) -> P eu e<br><br></div>This rule can be defined using only the standard eliminators for D and ≡, without K (ask me if you want to see the construction, I have it but it's quite long). <br>
<br>However, this is not the form of injectivity that is used in the pattern matching algorithm. Rather, it needs a version of injectivity where us and ut are *definitionally* equal. Ok, you say, in that case we can just fill in refl to get this:<br>
<br>m : (e : s ≡ t) -> P (cong u e) (conf e) ⊢ injectivity m : (e : c s ≡ c t) -> P refl e<br><br></div>The problem arises when we want to apply this rule to construct a function "? : (e : c s ≡ c t) -> P' e". Now in order to apply this rule, we need to find P such that P refl e = P' e (definitionally). In other words, to construct P we need to eliminate the first argument "eu : u ≡ u", which is generally speaking not possible without K.<br>
<br></div>In my example, I exploit this behaviour by choosing "P' : foo ≡ foo -> Set" to be defined by "P' e = e ≡ refl". You can see that we cannot construct a "P : (e : refl ≡ refl) -> subst Foo e foo ≡ foo -> Set" such that "P refl e ≡ P' refl" without using K. So we should not be able to apply injectivity in this situation, yet that is exactly what Agda is doing.<br>
<br></div>Best,<br></div>Jesper<br><div><div><div><div>
<div><div>
<div><br></div></div></div></div></div></div></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Jan 17, 2014 at 3:34 PM, Jesper Cockx <span dir="ltr"><<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div><div><span style="font-family:arial,helvetica,sans-serif">Andreas: my own version of --without-K has the same problem. However, I'm trying to fix it by doing something like parameter reconstruction for the indices: when applying the injectivity rule to the problem "foo ≡ foo", we should first solve the equation "refl ≡ refl" on the indices (here, both refl's have type "myPoint ≡ myPoint"). But this equation is already rejected by the current --without-K, thus excluding the problematic pattern matching on "foo ≡ foo". I'm still testing whether this doesn't introduce any other problems or excludes any good examples.</span><br>
<br></div>Matteo: the problem with allowing no pattern matching at all is that in Agda, we depend on pattern matching to define eliminators for data types. Another possibility would be to introduce an even more restrictive version of --without-K that requires all indices (and parameters too possibly?) to be *distinct* variables (so no constructors allowed). This would at least allow us to define the eliminator for each data type, but hopefully be simple enough to avoid any problems like this one.<br>
<br></div>Mattieu: The equation that's being eliminated is "foo ≡ foo", which is indeed the same as "refl ≡ refl" under the equivalence Foo-equiv. However unlike refl, the constructor foo has no parameters and no arguments, so a naive interpretation of injectivity would tell you that the only term of type "foo ≡ foo" is refl. However, this is ignoring the index of the type Foo. So in fact, we first need to solve the equation "refl ≡ refl" on the indices, which is impossible without K. <br>
<br></div>Best,<br></div>Jesper<br></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Jan 17, 2014 at 3:02 PM, Matteo Acerbi <span dir="ltr"><<a href="mailto:matteo.acerbi@gmail.com" target="_blank">matteo.acerbi@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello,<br>
<br>
I noticed that if the two postulates are replaced by<br>
<br>
module _ (mySpace : Set)(myPoint : mySpace) where<br>
<br>
(indent the rest)<br>
<br>
the problem seems to not appear (an error is reported).<br>
<br>
Maybe this gives some hints (I do not know).<br>
<br>
That said, I have a small proposal.<br>
<br>
Most of the times I use Agda for its *wonderful* dependent pattern<br>
matching facility, but every now and then I would like to forbid<br>
myself to use pattern matching at all, at least from inside a single<br>
file.<br>
<br>
I would like to have the possibility to get back to that file and make<br>
sure that I never used pattern matching in that code just by looking<br>
at the OPTIONS header.<br>
<br>
I think I would find a --no-pattern-matching option, which simply<br>
applied this restriction, but still allowed for importing modules<br>
whatever their options are, very convenient.<br>
<br>
For now I am just curious as to whether others are interested: would<br>
anyone else like such a --no-pattern-matching option?<br>
<br>
Cheers,<br>
Matteo<br>
<div><div><br>
On Fri, Jan 17, 2014 at 2:43 PM, Jesper Cockx <<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>> wrote:<br>
> I'm not relieved. The problem is still there.<br>
><br>
><br>
> On Fri, Jan 17, 2014 at 2:38 PM, Andreas Abel <<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>><br>
> wrote:<br>
>><br>
>> Can you explain, please?<br>
>><br>
>> You say you did not expect to be able to prove 'problem' from<br>
>> 'equiv-to-id' which you thought was univalence. Martin tells you that<br>
>> 'equiv-to-id' is a consequence of univalence. Now you are relieved. But<br>
>> still 'problem' follows from univalence. Why are you relieved now?<br>
>><br>
>> Sorry, I am a bit confused now...<br>
>> Andreas<br>
>><br>
>><br>
>> On 17.01.2014 13:39, Jesper Cockx wrote:<br>
>>><br>
>>> As Martin pointed out to me, my definition of equiv-to-id is not the<br>
>>> univalence axiom, but merely a (much weaker) consequence of it. Thank<br>
>>> you.<br>
>>><br>
>>> Best,<br>
>>> Jesper<br>
>>><br>
>>><br>
>>> On Fri, Jan 17, 2014 at 12:19 PM, Jesper Cockx <<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a><br>
>>> <mailto:<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>>> wrote:<br>
>>><br>
>>> Dear all,<br>
>>><br>
>>> Much to my own surprise, I encountered another problem with the<br>
>>> --without-K option. This is on the latest darcs version of Agda and<br>
>>> is unrelated to the termination checker. As far as I understand, the<br>
>>> unification algorithm is applying the injectivity rule too liberally<br>
>>> for data types indexed over indexed data. But maybe someone else can<br>
>>> give a better explanation?<br>
>>><br>
>>> === BEGIN CODE ===<br>
>>><br>
>>> {-# OPTIONS --without-K #-}<br>
>>><br>
>>> module YetAnotherWithoutKProblem where<br>
>>><br>
>>> -- First, some preliminaries to make this file self-contained.<br>
>>> data _≡_ {a} {A : Set a} (x : A) : A → Set where<br>
>>> refl : x ≡ x<br>
>>><br>
>>> subst : ∀ {a b} {A : Set a} {x : A} (B : (y : A) → Set b) →<br>
>>> {y : A} → x ≡ y → B x → B y<br>
>>> subst B refl b = b<br>
>>><br>
>>> record _≃_ (A B : Set) : Set where<br>
>>> constructor equiv<br>
>>> field<br>
>>> f : A → B<br>
>>> g : B → A<br>
>>> i : (x : A) → g (f x) ≡ x<br>
>>> j : (y : B) → f (g y) ≡ y<br>
>>><br>
>>> -- The univalence axiom.<br>
>>> postulate equiv-to-id : {A B : Set} → A ≃ B → A ≡ B<br>
>>><br>
>>> -- Now consider any concrete space 'mySpace' with a point 'myPoint'.<br>
>>> -- We will show that mySpace has no structure above dimension 2.<br>
>>> postulate mySpace : Set<br>
>>> postulate myPoint : mySpace<br>
>>><br>
>>> -- We define Foo in a way such that 'Foo e' is equivalent with 'refl<br>
>>> ≡ e'.<br>
>>> data Foo : myPoint ≡ myPoint → Set where<br>
>>> foo : Foo refl<br>
>>><br>
>>> Foo-equiv : {e : myPoint ≡ myPoint} → Foo e ≃ (refl ≡ e)<br>
>>> Foo-equiv = equiv f g i j<br>
>>> where<br>
>>> f : {e : myPoint ≡ myPoint} → Foo e → refl ≡ e<br>
>>> f foo = refl<br>
>>><br>
>>> g : {e : myPoint ≡ myPoint} → refl ≡ e → Foo e<br>
>>> g refl = foo<br>
>>><br>
>>> i : {e : myPoint ≡ myPoint} (m : Foo e) → g (f m) ≡ m<br>
>>> i foo = refl<br>
>>><br>
>>> j : {e : myPoint ≡ myPoint} (i : refl ≡ e) → f (g i) ≡ i<br>
>>> j refl = refl<br>
>>><br>
>>> -- Here comes the real problem: by injectivity, 'Foo e' is a set ...<br>
>>> test : {e : myPoint ≡ myPoint} → (a : Foo e) → (i : a ≡ a) → i ≡ refl<br>
>>> test foo refl = refl<br>
>>><br>
>>> -- ... hence by univalence, so is 'refl ≡ e'.<br>
>>> problem : {e : myPoint ≡ myPoint} → (a : refl ≡ e) → (i : a ≡ a) → i<br>
>>> ≡ refl<br>
>>> problem = subst (λ X → (x : X) → (i : x ≡ x) → i ≡ refl)<br>
>>> (equiv-to-id Foo-equiv)<br>
>>> test<br>
>>><br>
>>> === END CODE ===<br>
>>><br>
>>> All the best,<br>
>>> Jesper<br>
>>><br>
>>><br>
>>><br>
>>><br>
>>> _______________________________________________<br>
>>> Agda mailing list<br>
>>> <a href="mailto:Agda@lists.chalmers.se" target="_blank">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>
>> --<br>
>> Andreas Abel <>< Du bist der geliebte Mensch.<br>
>><br>
>> Theoretical Computer Science, University of Munich<br>
>> Oettingenstr. 67, D-80538 Munich, GERMANY<br>
>><br>
>> <a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br>
>> <a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a><br>
><br>
><br>
><br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">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>
</div></div></blockquote></div><br></div>
</div></div></blockquote></div><br></div>