<div dir="ltr">Indeed in Coq we statically compute the possible recursive calls at the definition of the inductive type, independently of its use. In this case Agda is "fooled" because it thinks that [f] is a valid subterm (of type [D]) of [x : D], while Coq simply doesn't categorize [f] as a subterm when checking the guardedness/structural recursion criterion.</div><br><div class="gmail_quote"><div dir="ltr">On Thu, Mar 9, 2017 at 11:37 AM Michael Shulman <<a href="mailto:shulman@sandiego.edu">shulman@sandiego.edu</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr" class="gmail_msg"><div class="gmail_msg"><div class="gmail_msg"><div class="gmail_msg"><div class="gmail_msg">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 class="gmail_msg"><br class="gmail_msg"></div>data D : Set where<br class="gmail_msg"></div>  c : X -> D<br class="gmail_msg"><br class="gmail_msg"></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 class="gmail_msg"></div><div class="gmail_msg"><br class="gmail_msg"></div></div><div class="gmail_extra gmail_msg"><br class="gmail_msg"><div class="gmail_quote gmail_msg">On Wed, Mar 8, 2017 at 2:59 PM, Stefan Monnier <span dir="ltr" class="gmail_msg"><<a href="mailto:monnier@iro.umontreal.ca" class="gmail_msg" target="_blank">monnier@iro.umontreal.ca</a>></span> wrote:<br class="gmail_msg"><blockquote class="gmail_quote gmail_msg" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="gmail_msg">>   data D : Set where<br class="gmail_msg">
>     c : (f : (A : Set) → A → A) → D<br class="gmail_msg">
>   -- Structural recursion with  f args < c f  is no longer valid.<br class="gmail_msg">
>   -- We should not be able to demonstrated that D is empty.<br class="gmail_msg">
<br class="gmail_msg">
</span>Coq lets us define this datatype (in Prop).<br class="gmail_msg">
<span class="gmail_msg"><br class="gmail_msg">
>   empty : D → ⊥<br class="gmail_msg">
>   empty (c f) = empty (f D (c f))<br class="gmail_msg">
<br class="gmail_msg">
</span>But rejects this definition:<br class="gmail_msg">
<br class="gmail_msg">
    Error:<br class="gmail_msg">
    Recursive definition of empty is ill-formed.<br class="gmail_msg">
    In environment<br class="gmail_msg">
    empty : D -> False<br class="gmail_msg">
    x : D<br class="gmail_msg">
    f : forall A : Prop, A -> A<br class="gmail_msg">
    Recursive call to empty has principal argument equal to<br class="gmail_msg">
    "f D (c f)" instead of a subterm of "x".<br class="gmail_msg">
    Recursive definition is:<br class="gmail_msg">
    "fun x : D => match x with<br class="gmail_msg">
                  | c f => empty (f D (c f))<br class="gmail_msg">
                  end".<br class="gmail_msg">
<br class="gmail_msg">
Not sure exactly what is the rule they use to decide whether a recursive<br class="gmail_msg">
call is considered as valid structural recursion.  I suspect it depends<br class="gmail_msg">
on the notion of a "large inductive type" or something along these lines.<br class="gmail_msg">
<span class="m_-703960079366861716HOEnZb gmail_msg"><font color="#888888" class="gmail_msg"><br class="gmail_msg">
<br class="gmail_msg">
        Stefan<br class="gmail_msg">
</font></span><div class="m_-703960079366861716HOEnZb gmail_msg"><div class="m_-703960079366861716h5 gmail_msg"><br class="gmail_msg">
_______________________________________________<br class="gmail_msg">
Agda mailing list<br class="gmail_msg">
<a href="mailto:Agda@lists.chalmers.se" class="gmail_msg" target="_blank">Agda@lists.chalmers.se</a><br class="gmail_msg">
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" class="gmail_msg" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br class="gmail_msg">
</div></div></blockquote></div><br class="gmail_msg"></div>
_______________________________________________<br class="gmail_msg">
Agda mailing list<br class="gmail_msg">
<a href="mailto:Agda@lists.chalmers.se" class="gmail_msg" target="_blank">Agda@lists.chalmers.se</a><br class="gmail_msg">
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" class="gmail_msg" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br class="gmail_msg">
</blockquote></div>