The Coq mailing list

[Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>]

Some evaluation strategies terminate. eg


Fixpoint z (n: nat): nat := 0 * z n.

Lemma foo n : z n = 0.
unfold z. cbn.
(* (fix z (n0 : nat) : nat := 0) n = 0 *)


I don't know why Coq tries to be smart with this though.

Gaëtan Gilbert

On 08/06/2017 14:38, 
raffaello.giulietti AT supsi.ch
 wrote:
> Hello,
>
> consider the following z function
>
> Fixpoint z (n: nat): nat := 0 * z n.
>
> which Coq accepts with the usual notification "decreasing on 1st argument".
>
> Well, I don't see that this recursive definition is "decreasing on 1st
> argument". Indeed, an invocation results in an infinite recursion, as
> witnessed by the Out of memory message:
>
> Compute z 0.
> Out of memory.
>
> I'd expect Coq to reject the definition (even if the smallest
> mathematical fixpoint is the unary function 0).
>
> What is really happening? Any clarification would help.
>
> Greetings
> Raffaello