coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] "check_not_nested" error with Function

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Cc: Bruno Grenet <bruno.grenet AT lirmm.fr>
Subject: Re: [Coq-Club] "check_not_nested" error with Function
Date: Wed, 5 Aug 2020 10:59:29 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f42.google.com
Ironport-phdr: 9a23:GbO76hMVCi21LIxtgmol6mtUPXoX/o7sNwtQ0KIMzox0I//9rarrMEGX3/hxlliBBdydt6sazbWG+Pm4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCe8bL9oLhi7rgrdutQKjYB/Nqs/1xzFr2dSde9L321oP1WTnxj95se04pFu9jlbtuwi+cBdT6j0Zrw0QrNEAjsoNWA1/9DrugLYTQST/HscU34ZnQRODgPY8Rz1RJbxsi/9tupgxCmXOND9QL4oVTi+6apgVQTlgzkbOTEn7G7Xi9RwjKNFrxKnuxx/2JPfbIWMOPZjYq/RYdYWSGxcVchTSiNBGJuxYIQBD+UDPehWoYrzqUYQoxSiCgehH//vyiZSi3PqwaE2z+YsHAfb1wIgBdIOt3HUoc3vOqcTT++11rPIwiveZP5I3jf99ZLIcgwgof6SQLJ7bM3cyVEuFwzblFWQs5LqMymJ2eQKrmib9fZgVeOxhG46sAxxrT2vyd0tionNnI4a1lfE9SBgzYszONa3R1J1b8S+H5tMqyGVKZF2QsU6Tm9muSs31LILtJ24cSYKyJkqxwLTZuCEfoWW4hzvSuifLzh6iX9he7+ymRK//VW+x+P8VcS50khGoyhLnNTCuH4A0QHY5MaASvt45Eih2DCP2hjc6uFFPUA0lbfbJIU7zrEskZoTtFzPHi7zmEX5ka+WbF8o9fSv6+TiZLjtu5ySN5dshw3gLqgjntazDOc4PwQUQmSW+OWx2Kfs8EHnRrhBk+c4nbPDsJ/AIMQWvq65DBFR0oYk8xu/Ci2p0NUcnXUeLVJFfw+Lg5HnO1zBPvz0F/i/g1OrkDdkw/DJIKftDYnKLnjGiLvhfLB95FBAyAcr09xT+5ZZBqsCLf/zQEP9qd3VAx4jPwG73errENB92ZkfWWKLDK+ZKqTSsVqQ6+I3IumDepUVuCzjJPQ/+/HuimI5mUUBfamow5QXdWu1HvtjI0qDYHrshs0NHnsNvgo7VODqkkGNUSZPZ3auWKIx/i00CIW/DYvaWo+thKGB0zygE51NZmFGD0iMHm3ye4WFXfcMciOSLdV7njwKT7jyA7MmgDqprUfRz6dtZr7f/TRdvpb+3vB04ffSnFc872onId6a1jS1TmxuhG5AbDgrxrx+rFE1nk+C3LJijrpTEsFJ+/JETy81MJfdy6pxDNWkCVGJRcuAVFvzGobuOjo2VN9khoZWOx8sSeXntQjK2m+RO5FQkrWKAJIu9aeFhir+Is98zzDN06xz1gB6EPsKDnWvg+tEzyaWH5TAyhzLmKOjdKBa1ynIpj/akDi++XpAWQs1ap3rGHASYkyM8Ib870LGCr6pUPEpblEHxsmFJa9HLNbuiAceSQ==

Sorry for the late answer. This error is raised when Function detects
nested recursive calls, which it does not support.

It seems indeed that in your definition the second recursive call
makes use (in decreasing position) of the results of the first one.

If you really need nested calls you may want to try the Equations
plugin (https://github.com/mattam82/Coq-Equations).

Best regards,
Pierre

Le jeu. 23 juil. 2020 à 08:30, Timothée Defourné
<tdefourne AT clipper.ens.fr> a écrit :
>
> Hello,
>
> I'm having an issue I don't understand with Coqtail, in the following
> function defined with the Function command : https://i.imgur.com/sW3EYLG.png
>
> I get the error : on expr : quo (ceiling (NQ_div2 (deg R0))) R0
> check_not_nested: failure R0, from the recursive call in the highlighted
> line.
>
>
> I have never seen this error before and researching it yields no result.
> Does anyone have an idea what it means ? I believe I can work out what
> exactly went wrong if I just know what the error means.
>
> Also, if it helps, making the function end immediately after the
> highlighted line raises no error, but ending it after the second pattern
> matching raises the same error.
>
>
> Thanks in advance,
>
> Timothée Defourné
>

Re: [Coq-Club] "check_not_nested" error with Function, Pierre Courtieu, 08/05/2020