The Coq mailing list

[Christian Doczkal <doczkal AT ps.uni-saarland.de>]

Dear Georges Gonthier, dear Coq-Club

First of all, thank you for your quick reply. The paper [1], to which I
was referring, defines a syntactic "guarded by destructors" condition
for fix. As far as I can tell, this condition does not handle the case
of div/mod. However, there appears to be an extended version in the form
of an LIP research report that I was unable to obtain.

I found a later paper from Giménez [2], where termination of fix is
ensured by typing conditions. The paper employs guarded types and an
order relation on types. The motivating example in this paper is a
structurally recursive version of div.

Now I'm curious whether Coq uses a type based approach for termination
checking as proposed in [2] or a syntactic condition closer to [1],
extended to cover div/mod. The Coq manual only references [1]. 

I would be thankful for any clarification.


-- 
Regards
Christian


[1] E. Giménez. Codifying guarded definitions with recursive schemes. In
Types'94 : Types for Proofs and Programs, volume 996 of Lecture Notes in
Computer Science. Springer-Verlag, 1994. Extended version in LIP
research report 95-07, ENS Lyon.

[2] E. Giménez. Structural recursive definitions in type theory. In 
Automata, Languages and Programming, volume 1443 of Lecture Notes in
Computer Science. Springer-Verlag, 1998.

Am Freitag, den 08.04.2011, 17:14 +0000 schrieb Georges Gonthier:
> This behavior is actually covered by [2], which defines two notions:
> "structurally smaller than" and "structurally smaller than or equal to".
>   minus x y, as defined in the ssr library, is "structurally smaller than 
> or equal to" x,
> because x is the structural argument of minus, and all match branches 
> return either x or a proper recursive call to minus. This is not the case 
> for minus', as 0 is syntactically unrelated to x (even though it is 
> provably equal to x in that branch!).
> 
> Georges
> 
> -----Original Message-----
> From: Christian Doczkal 
>Â [mailto:doczkal AT ps.uni-saarland.de]
>  
> Sent: 08 April 2011 17:22
> To: Coq-Club
> Subject: [Coq-Club] Guard Condition
> 
> Dear Coq-Club.
> 
> The guard condition for "fix" appears to be under active
> development [1]. I would be interested in the exact guard condition
> implemented in Coq 8.3. 
> 
> Is there any document (besides the Coq sources) where the details of the
> guard condition are explained? The Coq manual refers to [2], but this
> seems to be only part of what is implemented. 
> 
> The particular example I found rather stunning is the recursive version
> of mod (ported from the Ssreflect libraries).
> 
> Fixpoint minus (x y : nat) : nat :=
>   match x, y with
>     | _, O => x
>     | O, _ => x
>     | S x', S y' => minus x' y'
>   end.
> 
> Fixpoint mod' x y {struct x} :=
>   match minus x y  with
>     | O => x
>     | S x' => mod' x' y
>   end.
> 
> Definition mod  (x y : nat) : nat := mod' x (minus y (S O)).
> 
> I would be happy if someone could explain why mod' is accepted (It seems
> to not be covered by [2]). Furthermore, I would like to understand why
> the above definition of mod' is not accepted if we replace minus by the
> following semantically equivalent version:
> 
> Fixpoint minus (x y : nat) : nat :=
>   match x, y with
>     | _, O => x
>     | O, _ => O (* x changed to O *)
>     | S x', S y' => minus x' y'
>   end.
> 
> Thanks in advance.
> 
> Regards
> Christian
> 
> 
> [1] Pierre Boutillier, Subject: Re: [Coq-Club] Destruct vs. inversion
> https://sympa-roc.inria.fr/wws/arc/coq-club/2011-04/msg00027.html
> 
> [2] E. Gimenez "Codifying guarded definitions with recursive schemes"
> 
> 
>