<div dir="ltr"><div><div><div><div>Pardon my ignorance, but I don't understand why anyone would accept the definition of "empty".  The datatype D is not recursive; it's basically of the form<br><br></div>data D : Set where<br></div>  c : X -> D<br><br></div>for some fixed type X, which just happens to be large in this case.  So its induction principle says that we get a map D -> Y whenever we have a map X -> Y.  What justifies any sort of recursive call?<br></div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Mar 8, 2017 at 2:59 PM, Stefan Monnier <span dir="ltr"><<a href="mailto:monnier@iro.umontreal.ca" target="_blank">monnier@iro.umontreal.ca</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">>   data D : Set where<br>
>     c : (f : (A : Set) → A → A) → D<br>
>   -- Structural recursion with  f args < c f  is no longer valid.<br>
>   -- We should not be able to demonstrated that D is empty.<br>
<br>
</span>Coq lets us define this datatype (in Prop).<br>
<span class=""><br>
>   empty : D → ⊥<br>
>   empty (c f) = empty (f D (c f))<br>
<br>
</span>But rejects this definition:<br>
<br>
    Error:<br>
    Recursive definition of empty is ill-formed.<br>
    In environment<br>
    empty : D -> False<br>
    x : D<br>
    f : forall A : Prop, A -> A<br>
    Recursive call to empty has principal argument equal to<br>
    "f D (c f)" instead of a subterm of "x".<br>
    Recursive definition is:<br>
    "fun x : D => match x with<br>
                  | c f => empty (f D (c f))<br>
                  end".<br>
<br>
Not sure exactly what is the rule they use to decide whether a recursive<br>
call is considered as valid structural recursion.  I suspect it depends<br>
on the notion of a "large inductive type" or something along these lines.<br>
<span class="HOEnZb"><font color="#888888"><br>
<br>
        Stefan<br>
</font></span><div class="HOEnZb"><div class="h5"><br>
______________________________<wbr>_________________<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" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>