<div dir="ltr"><div><div>Maxime: To be honest, I&#39;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&#39;m afraid I don&#39;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 &quot;with&quot; and &quot;rewrite&quot; for the purpose of termination checking. However, at least for &quot;rewrite&quot; 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&#39;m not sure if the inlining of &quot;with&quot; also causes problems, but on the other hand I don&#39;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 &quot;with&quot; 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">&lt;<a href="mailto:drl@cs.cmu.edu" target="_blank">drl@cs.cmu.edu</a>&gt;</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&#39;s are like natural numbers, with -2 being like 0, so S - is not less than it)<br>
<br>
        foo : {C : _} (x y : TLevel) -&gt; x &lt;tl y -&gt; 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 &#39;with&#39;; e.g. a function<br>
<br>
    1&lt;=pos : (p : Positive) → tl 1 &lt;=tl (tlp p)<br>
    1&lt;=pos One = Inr id<br>
    1&lt;=pos (S n) with 1&lt;=pos n<br>
    ... | Inl lt = Inl (ltSR lt)<br>
    ... | Inr eq = transport (λ x → tl 1 &lt;=tl S x) eq (Inl ltS)<br>
<br>
which is clearly structural recursive on p fails.  But if I write out the &#39;with&#39; explicitly it&#39;s fine.<br>
<br>
I think I could get all of these to pass by writing out the &#39;with&#39;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 &lt;<a href="mailto:dlicata@wesleyan.edu">dlicata@wesleyan.edu</a>&gt; wrote:<br>
<br>
&gt; Hi Jesper,<br>
&gt;<br>
&gt; Thanks for the nice explanation!  I don&#39;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&#39;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>


&gt;<br>
&gt; I&#39;ll try my library on it next time I have a chance to upgrade agda.<br>
&gt;<br>
&gt; -Dan<br>
&gt;<br>
&gt;<br>
&gt; On Jul 1, 2014, at 12:00 AM, Jesper Cockx &lt;<a href="mailto:Jesper@sikanda.be">Jesper@sikanda.be</a>&gt; wrote:<br>
&gt;<br>
&gt;&gt; The current restriction is quite simple: for a function to be<br>
&gt;&gt; structurally recursive on an argument x of type T, the type T must be<br>
&gt;&gt; a data type *before* any matching has been done. In particular, this<br>
&gt;&gt; prohibits structural recursion on &#39;deep&#39; arguments and universe-like<br>
&gt;&gt; constructions such as the one in my previous mail. I don&#39;t know what<br>
&gt;&gt; the current situation is on the Coq side of things, maybe someone else<br>
&gt;&gt; can clarify?<br>
&gt;&gt;<br>
&gt;&gt; Jesper<br>
&gt;&gt;<br>
&gt;&gt; On 6/30/14, Dan Licata &lt;<a href="mailto:dlicata@wesleyan.edu">dlicata@wesleyan.edu</a>&gt; wrote:<br>
&gt;&gt;&gt; great! is there a way to explain what the restriction is?  Has Coq fixed<br>
&gt;&gt;&gt; this bug yet, and if so, how does your solution compare to theirs?<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; -Dan<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; On Jun 27, 2014, at 12:26 PM, Jesper Cockx &lt;<a href="mailto:Jesper@sikanda.be">Jesper@sikanda.be</a>&gt; wrote:<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; Yes, this restriction is to address the incompatibility of the termination<br>
&gt;&gt;&gt;&gt; checker with univalence. As a side-effect, many functions on universes no<br>
&gt;&gt;&gt;&gt; longer pass the termination check, for example (by Andreas):<br>
&gt;&gt;&gt;&gt; T : Bool -&gt; Set<br>
&gt;&gt;&gt;&gt; T true = Nat<br>
&gt;&gt;&gt;&gt; T false = List Nat<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; f : (x : Bool) -&gt; T x -&gt; Set<br>
&gt;&gt;&gt;&gt; f true zero = Nat<br>
&gt;&gt;&gt;&gt; f true (suc x) = f true x<br>
&gt;&gt;&gt;&gt; f false nil = Nat<br>
&gt;&gt;&gt;&gt; f false (x :: xs) = f false xs<br>
&gt;&gt;&gt;&gt; For the moment, such definitions have to be unfolded manually:<br>
&gt;&gt;&gt;&gt; f : (x : Bool) -&gt; T x -&gt; Set<br>
&gt;&gt;&gt;&gt; f true = ftrue<br>
&gt;&gt;&gt;&gt; where<br>
&gt;&gt;&gt;&gt;   ftrue : Nat -&gt; Set<br>
&gt;&gt;&gt;&gt;   ftrue zero = Nat<br>
&gt;&gt;&gt;&gt;   ftrue (suc x) = ftrue x<br>
&gt;&gt;&gt;&gt; f false = ffalse<br>
&gt;&gt;&gt;&gt; where<br>
&gt;&gt;&gt;&gt;   ffalse : List Nat -&gt; Set<br>
&gt;&gt;&gt;&gt;   ffalse nil = Nat<br>
&gt;&gt;&gt;&gt;   ffalse (x :: xs) = ffalse xs<br>
&gt;&gt;&gt;&gt; However, due to a mistake I made in the fix, the termination checker a<br>
&gt;&gt;&gt;&gt; complains much more than necessary when --without-K is enabled. This has<br>
&gt;&gt;&gt;&gt; now been fixed in the development version:<br>
&gt;&gt;&gt;&gt; <a href="https://code.google.com/p/agda/issues/detail?id=1214&amp;can=1" target="_blank">https://code.google.com/p/agda/issues/detail?id=1214&amp;can=1</a>. I&#39;ll check the<br>
&gt;&gt;&gt;&gt; other errors in Nils&#39; library later. If you have any specific examples<br>
&gt;&gt;&gt;&gt; that you think should be accepted, please send them to me and I&#39;ll see<br>
&gt;&gt;&gt;&gt; what I can do.<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; Jesper<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; On Fri, Jun 27, 2014 at 6:52 AM, Dan Licata &lt;<a href="mailto:dlicata@wesleyan.edu">dlicata@wesleyan.edu</a>&gt; wrote:<br>
&gt;&gt;&gt;&gt; Is this restriction addressing the &quot;termination checker + propositional<br>
&gt;&gt;&gt;&gt; univalence inconsistency&quot; issue, or something else?<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; -Dan<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; On Jun 21, 2014, at 1:44 PM, Jesper Cockx &lt;<a href="mailto:Jesper@sikanda.be">Jesper@sikanda.be</a>&gt; wrote:<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; I suppose by &#39;people working on this issue&#39;, you mean Andreas and me? I&#39;m<br>
&gt;&gt;&gt;&gt;&gt; not currently working on this problem, but I could be convinced to if the<br>
&gt;&gt;&gt;&gt;&gt; current hack turns out to be too inconvenient. However, I have two<br>
&gt;&gt;&gt;&gt;&gt; problems before I can start working on a fix:<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; - The current theory of pattern matching doesn&#39;t allow induction on<br>
&gt;&gt;&gt;&gt;&gt; &#39;deep&#39; arguments, i.e. ones that only get an inductive type after pattern<br>
&gt;&gt;&gt;&gt;&gt; matching on some other arguments. So the theory would have to be<br>
&gt;&gt;&gt;&gt;&gt; extended.<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; - I don&#39;t have a lot of experience with the termination checker, so I&#39;m<br>
&gt;&gt;&gt;&gt;&gt; not confident to mess with it. It seems that in order to fix this<br>
&gt;&gt;&gt;&gt;&gt; problem, the termination checker would need some type information, as<br>
&gt;&gt;&gt;&gt;&gt; well as information about the substitutions performed by the previous<br>
&gt;&gt;&gt;&gt;&gt; case splits.<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; If anyone can help me with (one of) these problems, I&#39;d like to work<br>
&gt;&gt;&gt;&gt;&gt; together on it. Otherwise I&#39;ll try to get a better understanding by<br>
&gt;&gt;&gt;&gt;&gt; myself, but then it might take a long time.<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; Jesper<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; On Fri, Jun 20, 2014 at 7:13 PM, Andrés Sicard-Ramírez &lt;<a href="mailto:asr@eafit.edu.co">asr@eafit.edu.co</a>&gt;<br>
&gt;&gt;&gt;&gt;&gt; wrote:<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; On 20 June 2014 09:07, Brent Yorgey &lt;<a href="mailto:byorgey@seas.upenn.edu">byorgey@seas.upenn.edu</a>&gt; wrote:<br>
&gt;&gt;&gt;&gt;&gt; but is the code I linked now expected to<br>
&gt;&gt;&gt;&gt;&gt; fail termination checking?<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; Using the --without-K option? I don&#39;t know. This is an open issue and<br>
&gt;&gt;&gt;&gt;&gt; people working on this issue know that the current behaviour is too<br>
&gt;&gt;&gt;&gt;&gt; restrictive. I don&#39;t know if they are working in a better solution<br>
&gt;&gt;&gt;&gt;&gt; right now.<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; --<br>
&gt;&gt;&gt;&gt;&gt; Andrés<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; _______________________________________________<br>
&gt;&gt;&gt;&gt;&gt; Agda mailing list<br>
&gt;&gt;&gt;&gt;&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt;&gt;&gt;&gt;&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; _______________________________________________<br>
&gt;&gt;&gt;&gt;&gt; Agda mailing list<br>
&gt;&gt;&gt;&gt;&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt;&gt;&gt;&gt;&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt;<br>
&gt;<br>
&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>
</div></div></blockquote></div><br></div>