The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

On Thu, Jun 8, 2017 at 9:42 AM, Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr> wrote:

Le 08/06/2017 à 14:38, raffaello.giulietti AT supsi.ch a écrit :
> 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".

I suppose that during type-checking, Coq performs some kind of reduction
and sees that 0 * z n reduces to 0 (definition of mult) ... hence there
is no recursive sub-call.

On the contrary, the following fails

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

Exactly. The other day, Gil Hur pass me an example of this. The official answer AFAIK is that "Coq is not Strongly Normalizing, but it is Weakly Normalizing. That is ---together with the property of Uniqueness of Normal Forms--- for every reduction scheme either it terminates in THE normal form of the term, or it loops forever. And, for soundness, that's good enough".