<div dir="ltr"><div><div>Maxime: To be honest, I'm not sure what the intuition behind my fix is either. However, it is exactly what I need in order to apply structural recursion in my translation of pattern matching to eliminators (see
<a href="http://people.cs.kuleuven.be/~jesper.cockx/Without-K/Pattern-matching-without-K.pdf">http://people.cs.kuleuven.be/~jesper.cockx/Without-K/Pattern-matching-without-K.pdf</a>).
I'm afraid I don't really understand your criterion for Coq either. I thought univalence was only proven sound in combination with the standard eliminators, and not with sized types?<br><br></div>Dan: Your examples are instances of issue 59 (<a href="https://code.google.com/p/agda/issues/detail?id=59">https://code.google.com/p/agda/issues/detail?id=59</a>), which was fixed by inlining "with" and "rewrite" for the purpose of termination checking. However, at least for "rewrite" this inlining actually did bad things when --without-K was enabled. For example, the following was accepted in 2.3.2:<br>
<pre>==================================================
{-# OPTIONS --without-K #-}<br>open import Relation.Binary.PropositionalEquality
data Zero : Set where
data WOne : Set where wrap : (Zero → WOne) → WOne
FOne = Zero → WOne
postulate
iso : WOne ≡ FOne
foo : WOne → Zero
foo (wrap f) rewrite (sym iso) = foo f
BOOM : Zero
BOOM = foo (wrap (λ ()))
==================================================<br></pre>I'm not sure if the inlining of "with" also causes problems, but on the other hand I don't have a proof that it is sound either. So I decided to disable the inlining entirely (when --without-K is enabled). It would be interesting to take a look at the desuraging of "with" by Agda to see how they differ from your manual desugaring. Does anyone know if this is possible?<br>
<br></div>Jesper<br></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Jul 9, 2014 at 11:43 PM, Dan Licata <span dir="ltr"><<a href="mailto:drl@cs.cmu.edu" target="_blank">drl@cs.cmu.edu</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Jesper,<br>
<br>
Today I got the development version of Agda. There are some examples that I think should work. They termination-check with without-K turned off but not with it on.<br>
<br>
See the functions tagged with<br>
NO_TERMINATION_CHECK<br>
<br>
in<br>
<br>
<a href="https://github.com/dlicata335/hott-agda/blob/master/lib/Int.agda" target="_blank">https://github.com/dlicata335/hott-agda/blob/master/lib/Int.agda</a><br>
<a href="https://github.com/dlicata335/hott-agda/blob/master/lib/loopspace/Truncation.agda" target="_blank">https://github.com/dlicata335/hott-agda/blob/master/lib/loopspace/Truncation.agda</a><br>
<br>
One issue seems to have to do with absurd patterns; for example, if I do something like this (TLevel's are like natural numbers, with -2 being like 0, so S - is not less than it)<br>
<br>
foo : {C : _} (x y : TLevel) -> x <tl y -> C<br>
foo (S x) (S y) lt = foo x y {!!}<br>
foo (S y) -2 lt with lt<br>
foo (S y) -2 lt | ()<br>
foo _ _ _ = {!!}<br>
<br>
then the clause with the absurd pattern fails the termination checker (?).<br>
<br>
Another seems to have something to do with 'with'; e.g. a function<br>
<br>
1<=pos : (p : Positive) → tl 1 <=tl (tlp p)<br>
1<=pos One = Inr id<br>
1<=pos (S n) with 1<=pos n<br>
... | Inl lt = Inl (ltSR lt)<br>
... | Inr eq = transport (λ x → tl 1 <=tl S x) eq (Inl ltS)<br>
<br>
which is clearly structural recursive on p fails. But if I write out the 'with' explicitly it's fine.<br>
<br>
I think I could get all of these to pass by writing out the 'with's explicitly, but perhaps there is a way to change the termination checker so that it accepts them?<br>
<span class="HOEnZb"><font color="#888888"><br>
-Dan<br>
</font></span><div class="HOEnZb"><div class="h5"><br>
On Jul 1, 2014, at 12:59 PM, Dan Licata <<a href="mailto:dlicata@wesleyan.edu">dlicata@wesleyan.edu</a>> wrote:<br>
<br>
> Hi Jesper,<br>
><br>
> Thanks for the nice explanation! I don't think this restriction should be much of an issue for HoTT, because we tend to stick closer to the eliminators (e.g. for higher inductives that's all we know how to do), so in the examples I can think of ftrue/ffalse are already applications of eliminators, rather than direct recursive calls.<br>
><br>
> I'll try my library on it next time I have a chance to upgrade agda.<br>
><br>
> -Dan<br>
><br>
><br>
> On Jul 1, 2014, at 12:00 AM, Jesper Cockx <<a href="mailto:Jesper@sikanda.be">Jesper@sikanda.be</a>> wrote:<br>
><br>
>> The current restriction is quite simple: for a function to be<br>
>> structurally recursive on an argument x of type T, the type T must be<br>
>> a data type *before* any matching has been done. In particular, this<br>
>> prohibits structural recursion on 'deep' arguments and universe-like<br>
>> constructions such as the one in my previous mail. I don't know what<br>
>> the current situation is on the Coq side of things, maybe someone else<br>
>> can clarify?<br>
>><br>
>> Jesper<br>
>><br>
>> On 6/30/14, Dan Licata <<a href="mailto:dlicata@wesleyan.edu">dlicata@wesleyan.edu</a>> wrote:<br>
>>> great! is there a way to explain what the restriction is? Has Coq fixed<br>
>>> this bug yet, and if so, how does your solution compare to theirs?<br>
>>><br>
>>> -Dan<br>
>>><br>
>>> On Jun 27, 2014, at 12:26 PM, Jesper Cockx <<a href="mailto:Jesper@sikanda.be">Jesper@sikanda.be</a>> wrote:<br>
>>><br>
>>>> Yes, this restriction is to address the incompatibility of the termination<br>
>>>> checker with univalence. As a side-effect, many functions on universes no<br>
>>>> longer pass the termination check, for example (by Andreas):<br>
>>>> T : Bool -> Set<br>
>>>> T true = Nat<br>
>>>> T false = List Nat<br>
>>>><br>
>>>> f : (x : Bool) -> T x -> Set<br>
>>>> f true zero = Nat<br>
>>>> f true (suc x) = f true x<br>
>>>> f false nil = Nat<br>
>>>> f false (x :: xs) = f false xs<br>
>>>> For the moment, such definitions have to be unfolded manually:<br>
>>>> f : (x : Bool) -> T x -> Set<br>
>>>> f true = ftrue<br>
>>>> where<br>
>>>> ftrue : Nat -> Set<br>
>>>> ftrue zero = Nat<br>
>>>> ftrue (suc x) = ftrue x<br>
>>>> f false = ffalse<br>
>>>> where<br>
>>>> ffalse : List Nat -> Set<br>
>>>> ffalse nil = Nat<br>
>>>> ffalse (x :: xs) = ffalse xs<br>
>>>> However, due to a mistake I made in the fix, the termination checker a<br>
>>>> complains much more than necessary when --without-K is enabled. This has<br>
>>>> now been fixed in the development version:<br>
>>>> <a href="https://code.google.com/p/agda/issues/detail?id=1214&can=1" target="_blank">https://code.google.com/p/agda/issues/detail?id=1214&can=1</a>. I'll check the<br>
>>>> other errors in Nils' library later. If you have any specific examples<br>
>>>> that you think should be accepted, please send them to me and I'll see<br>
>>>> what I can do.<br>
>>>><br>
>>>> Jesper<br>
>>>><br>
>>>><br>
>>>> On Fri, Jun 27, 2014 at 6:52 AM, Dan Licata <<a href="mailto:dlicata@wesleyan.edu">dlicata@wesleyan.edu</a>> wrote:<br>
>>>> Is this restriction addressing the "termination checker + propositional<br>
>>>> univalence inconsistency" issue, or something else?<br>
>>>><br>
>>>> -Dan<br>
>>>><br>
>>>> On Jun 21, 2014, at 1:44 PM, Jesper Cockx <<a href="mailto:Jesper@sikanda.be">Jesper@sikanda.be</a>> wrote:<br>
>>>><br>
>>>>> I suppose by 'people working on this issue', you mean Andreas and me? I'm<br>
>>>>> not currently working on this problem, but I could be convinced to if the<br>
>>>>> current hack turns out to be too inconvenient. However, I have two<br>
>>>>> problems before I can start working on a fix:<br>
>>>>><br>
>>>>> - The current theory of pattern matching doesn't allow induction on<br>
>>>>> 'deep' arguments, i.e. ones that only get an inductive type after pattern<br>
>>>>> matching on some other arguments. So the theory would have to be<br>
>>>>> extended.<br>
>>>>><br>
>>>>> - I don't have a lot of experience with the termination checker, so I'm<br>
>>>>> not confident to mess with it. It seems that in order to fix this<br>
>>>>> problem, the termination checker would need some type information, as<br>
>>>>> well as information about the substitutions performed by the previous<br>
>>>>> case splits.<br>
>>>>><br>
>>>>> If anyone can help me with (one of) these problems, I'd like to work<br>
>>>>> together on it. Otherwise I'll try to get a better understanding by<br>
>>>>> myself, but then it might take a long time.<br>
>>>>><br>
>>>>> Jesper<br>
>>>>><br>
>>>>><br>
>>>>> On Fri, Jun 20, 2014 at 7:13 PM, Andrés Sicard-Ramírez <<a href="mailto:asr@eafit.edu.co">asr@eafit.edu.co</a>><br>
>>>>> wrote:<br>
>>>>><br>
>>>>> On 20 June 2014 09:07, Brent Yorgey <<a href="mailto:byorgey@seas.upenn.edu">byorgey@seas.upenn.edu</a>> wrote:<br>
>>>>> but is the code I linked now expected to<br>
>>>>> fail termination checking?<br>
>>>>><br>
>>>>> Using the --without-K option? I don't know. This is an open issue and<br>
>>>>> people working on this issue know that the current behaviour is too<br>
>>>>> restrictive. I don't know if they are working in a better solution<br>
>>>>> right now.<br>
>>>>><br>
>>>>> --<br>
>>>>> Andrés<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>
>>>>><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>
>>>><br>
>>>><br>
>>><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>
<br>
</div></div></blockquote></div><br></div>