The Coq mailing list

[Georges Gonthier <gonthier AT microsoft.com>]

  It was committed in the ssreflect library archive on February 14, 2008; my 
previous commit was on February 4, so it appeared somewhere in between. I 
coined it independently, which is not to say someone hadn't come up with it 
before.
   Georges

-----Original Message-----
From: Gert Smolka 
[mailto:smolka AT ps.uni-saarland.de]
 
Sent: 08 April 2011 19:38
To: Georges Gonthier; Coq-Club
Subject: Re: [Coq-Club] Guard Condition

I'm curious:  When did the "structurally" recursive version
of mod appearing below first appear?

Gert

Am 08.04.2011 19:14, 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"
>
>
>