The Coq mailing list

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

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"