coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Fixpoint "decreasing on 1st argument" notification

From: raffaello.giulietti AT supsi.ch
To: coq-club AT inria.fr
Subject: [Coq-Club] Fixpoint "decreasing on 1st argument" notification
Date: Thu, 8 Jun 2017 14:38:14 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=raffaello.giulietti AT supsi.ch; spf=Pass smtp.mailfrom=raffaello.giulietti AT supsi.ch; spf=Pass smtp.helo=postmaster AT ti-edu.ch
Ironport-phdr: 9a23:gjSwIRI9+9cqrpRygtmcpTZWNBhigK39O0sv0rFitYgQLPTxwZ3uMQTl6Ol3ixeRBMOAuq0C07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9ZDeZwdFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhicaOTAn82/ZhMJ/g61HrxyuvBF/34zZbZuJOPZicK7Qf9UXTndBUMZLUCxBB5uxb5EVAOoPM+ZXtZfyp18KrRu5HwWsC+LvyiJMhn/3w6I6z/ghEQDd0Qw7AtIOqG/UrNTvOKgOUeC4yrTDwzbbb/5OxDvw7IjFfgo8rfyOXL98a9fdxEsuGg/fk1mdq5HpMjWI3eoXqWeb9fBvVee3hm4ntQ5xpj+vy98wionIn44a1E3L9ThjzIkpJd20UE97Ydi6H5tMryyWKo97T8M4T211uis3y6cKtYO5cSUL0pgr2hzSZ+Gff4iN+B3jVeKRITlihHJifbKynwyy/lKuyu3yTMa7zlJKri5CktXWuXAN1gHT6syGSvRj4kehxTeP2hvI6uFZOUA0jqvbJ4Q9zb4wjpYTq1jMHjfqmEXqi6+bblkr+u+x6+j+frrmooKcOJRvhwHlMqUun9S/Dv4iPggPWWib4+W826f58U33WrUZxsExx6LeqdXRIdkRjq+/GQ5clIg5uDilCDLzyt0Wk3AKKFZCPh2GkozoNk3SIdjjEO+kghKnkGQ4j8vaN6HsV82eZkPIl63sKO5w

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

[Coq-Club] Fixpoint "decreasing on 1st argument" notification, raffaello . giulietti, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Gaetan Gilbert, 06/08/2017
  - Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, raffaello . giulietti, 06/08/2017
    - Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Beta Ziliani, 06/08/2017
      - Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, raffaello . giulietti, 06/08/2017
      - Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Abhishek Anand, 06/08/2017
      - Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Morrisett, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Dominique Larchey-Wendling, 06/08/2017
  - Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Beta Ziliani, 06/08/2017
    - Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, raffaello . giulietti, 06/08/2017
      - Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Dominique Larchey-Wendling, 06/08/2017