coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Example of terminating function that are not accepted by Coq

From: Jean-Francois Monin <jean-francois.monin AT univ-grenoble-alpes.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Example of terminating function that are not accepted by Coq
Date: Wed, 19 Dec 2018 18:09:24 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jean-francois.monin AT univ-grenoble-alpes.fr; spf=Pass smtp.mailfrom=jean-francois.monin AT univ-grenoble-alpes.fr; spf=None smtp.helo=postmaster AT zm-mta-out-1.u-ga.fr
Ironport-phdr: 9a23:mGxNfRSdA1zRYRqDNByNI7rJadpsv+yvbD5Q0YIujvd0So/mwa6yYRSN2/xhgRfzUJnB7Loc0qyK6/CmATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfbB/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/m/XhMJukaxVoxyhqBNjzIHJYo6aOuFzfr/Bcd4AWWZNQtxcWzJHD4ihb4UPFe0BPeNAoof5uVQBtx2+CRCsCuP10DBIgGP53ao70+Q6DArI2wsgH9QPsHTSsd74M6USXv6vw6nO1DnDYelW1i376IfUdRAhoOqMUah1ccrWz0kvFgXFg06NqYzjPjOVyP0Bs2eB7+V+U+KvjHUoqwVvrTS23MgsjpHJiZwOylze+yV52p84KNulQ0B4ed6pCIZcuiGEO4dsQM4vQXtktDgmxrEao5K2fCkHxIwjyhLDcfCKfJaE7gj+WOqMPTt0nm9pdbChixu07EOu0PfzVtOu31ZPtidFksfDtnQK1xHL68mHT+Jx/kK92TmVzgzT7fxEIVwtmabGMZIh36c8lpUJvkjZEC/2gl36jK6Qdko65uil8/nrb7X4qpOGNYJ5iBvyProylsCjG+g1MgkDU3Ce+eum1b3j+UP5QK9Njv0ziqTZso7VKt4dpqKgDQ9VyJws6xCjADeh0dQYhmMLLFdCeBKBjojpPUrDIO3+Dfe+nVSgiThrx+rYMb3nBZXCNXzDn6n4cbln705c0BQ8zctF65JaELENOOjzVVPptNzEEh85NBS5zPrgCNVkz48RRWaPArKCP67Jql+J5ucvI/GWa4MPuTb9LeIl5//0gnMjl18dZ/rh4ZxCY3ehW/9iPk+xYHz2g95HH31ZkBA5SbnIhVSEFBBJbnC5WKMnrhQ8DoOgRdPBS4mrxbKb1SGwGZxNIGVBDFGKOWrudpvBVO0BbiWYJsIkmzgcWKPnRZV3hkLmjxPz17cydrmcwSYfr5+2jIEktd2Wrgk78HlPN+rY1miMS29umWZSG20r2qFh5ENnx1GE26x1xvVcDdFIof1TAF5jaczsitdiAtW3YTrvO8+TQQz6EMigAC90Qcg8xdgEZ0s4EtG6gwuF0TD4W+ZIxYzOP4Q99+fn51a0J8t5zCychrskylw6S45IKHHj3+hisgfaQYDTwR2U

Well, even functions where no termination argument is known
can be expressed in Coq, and without (Set-)fuel. For instance,
the Syracuse/Collatz function. It is enough to add a precondition
saying that the argument is in the domain. Such an argument can be
inductively presented, as soon as you have an inductive definition
of the input-output relation. The trick works even with
complex schemes such as embedded recursion.
See the material presented by Dominique Larchey-Wendling at
the last TYPES'2018.

Best,
JF

On Wed, Dec 19, 2018 at 01:53:40PM +0100, Vincent Siles wrote:
> Hi !
> Today I've been asked if there are some examples of known terminating
> programs that can't be expressed at all in Coq. I know the usual 'fuel'
> encoding where one can add an integer to recurse on, and then prove that
> there always exists an integer big enough for the program to terminante.
> But are there examples that are not accepted by Coq even with such
> technics ?
> Best,
> V.

Re: [Coq-Club] Example of terminating function that are not accepted by Coq, (continued)
- Re: [Coq-Club] Example of terminating function that are not accepted by Coq, Jean-Francois Monin, 12/19/2018
  - [Coq-Club] Why Qwire was verified precisely in Coq?, José Manuel Rodriguez Caballero, 12/21/2018
    - Re: [Coq-Club] Why Qwire was verified precisely in Coq?, Robert Rand, 12/21/2018
      - Re: [Coq-Club] Why Qwire was verified precisely in Coq?, José Manuel Rodriguez Caballero, 12/21/2018