coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Vincent Siles <vincent.siles AT ens-lyon.org>
To: Coq-Club Club <coq-club AT inria.fr>
Subject: [Coq-Club] Example of terminating function that are not accepted by Coq
Date: Wed, 19 Dec 2018 13:53:40 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=vincent.siles AT ens-lyon.org; spf=None smtp.mailfrom=SRS0=Laii=O4=ens-lyon.org=vincent.siles AT bounce.ens-lyon.org; spf=Pass smtp.helo=postmaster AT sonata.ens-lyon.org
Ironport-phdr: 9a23:pl+U8hIqGvmOTdCSktmcpTZWNBhigK39O0sv0rFitYgeLPXxwZ3uMQTl6Ol3ixeRBMOHs6IC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwZFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QKsqUjq+8ahkVB7oiD8GNzEn9mHXltdwh79frB64uhBz35LYbISTOfFjfK3SYMkaSHJOUchRWSJPAZ6yYZUTAOcaJ+lUs5PwqkESoReiBwShAv7kxD9Shn/x2K03y+suEQDA3AM8Ad0OtmjUp8joOqcTVeC60rLIxijEYvNI2Df97pTHfQ4nofGQR75wasvRyU0xGAPelVift4rlPyiM2uQJs2mb6OxgWfioi249pAF8uz6izdovhInRno8Z11/J+TljzIs3J9C0UlN3bN+lHZdKqi2XOYh7Tts8T210vCs20L4LtJ6hcCQXyZkqxgTTZvyIfoWO/xntTvyeIS1ii3JgYL+/hwi98UynyuDkTcm011BKoTBZktbWrHwCyRrT6tOeRvt5/kah3jCP2xrU6uFeLkA4javbK5g/zb4sjpcfrEvOEjPslEj0jqKabFgo9+mp5uj9f7nrqJyRO5dxig7kM6QunsK/Af4/MggLR2WV5Piy2qD/8UDhRrtFlPw2kqjBvZ7DKskWvrC2AwlO0oo67xa+DzCm0NICkXkANlJFdwqKj5boO1HIPP/3E/G/g0i2nDdwxvDGOqPuAo7WI3fYl7fhYLB95FJCxwYp099f4YlUBqgFIPPzXU/xssbUDhgjMwy72+rnEsly1psCWWKTBa+UKL/dsViR5u42P+aMYJIVty3mJvg+5//uiGc5lkUHcamo25sXcnG4Ee58L0WXe3q/yusGREwNp08VSPHgwHaGTDQbM321Ruc34iwxIIOgF4bKAI631u+vxiC+S6NXYGtLDEzEKnbsep7MD+kNbimfJNMniT0AWKOJRok6kBW/swm8zKBoeLmHshYEvI7ugYAmr9bYkgs/oHktV5zEgjO9Clpsl2ZNfAcYmaV2oEhz0FCGi/EqiftFE9deof5PSUI+JJnaietgBIKqA16TTpKyUF+jB+6eL3QpVNton40DZV04H8SliFbExSX4W+ZIxYzOP4Q99+fn51a0J8t5zCyfhrImiVA6S41CM3bjgr948U7UHYGbykg=

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,

[Coq-Club] Example of terminating function that are not accepted by Coq, Vincent Siles, 12/19/2018
- Re: [Coq-Club] Example of terminating function that are not accepted by Coq, Klaus Ostermann, 12/19/2018
  - Re: [Coq-Club] Example of terminating function that are not accepted by Coq, Siddharth Bhat, 12/19/2018
    - Re: [Coq-Club] Example of terminating function that are not accepted by Coq, Xuanrui Qi, 12/19/2018
      - Re: [Coq-Club] Example of terminating function that are not accepted by Coq, Robbert Krebbers, 12/19/2018
      - Re: [Coq-Club] Example of terminating function that are not accepted by Coq, Thorsten Altenkirch, 12/19/2018
      - Re: [Coq-Club] Example of terminating function that are not accepted by Coq, Klaus Ostermann, 12/19/2018
        
        Re: [Coq-Club] Example of terminating function that are not accepted by Coq, Xuanrui Qi, 12/19/2018
        
        Re: [Coq-Club] Example of terminating function that are not accepted by Coq, Xuanrui Qi, 12/19/2018
    - Re: [Coq-Club] Example of terminating function that are not accepted by Coq, Jan Bessai, 12/19/2018
      - Re: [Coq-Club] Example of terminating function that are not accepted by Coq, Thorsten Altenkirch, 12/19/2018