Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: raffaello.giulietti AT supsi.ch
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification
  • Date: Thu, 8 Jun 2017 14:54:23 +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:a8oidx2YWnkHVrX1smDT+DRfVm0co7zxezQtwd8ZsewRKPad9pjvdHbS+e9qxAeQG96KtLQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q89pDXYQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmlTkJNzA5/m/UhMJ/gq1UrxC9qBJw2IPUfIKYOeBicq/Bc94XR2xMVdtRWSxbBYO8apMCD/AbMuZWoYnyvUUBrR+6BQmrHu/vxT5IhmLy3a07zeshDR3G3A07EtIVrXTUtM71NKYIXe+pzKnFyyjIYfBO2Trl9YTFdhAsreuRUb9ycMfd01QjGgHEg1mKtIDoPS6Z2+IQuGaB9eVgT/igi2s/pgFxvDevwsAsh5HVhoIU01zL6zh2wJsvKdKkSE53ed+kEJ1OuCGGL4Z6X8cvTmFytConyLALuIS3cDUIxZkm3RLTdv6Kf5WQ7hLmTumRIDN4hHx/eLK4gha/6VKgxffyVsm6yllFsC5Fkt3LtnwX2BzT69WHSv98/ki/xTaPywHT5/pfIUApjarbMJ8hzqQsmZoTqUjDBDP5mF3qjK+KcUUp4vSn6+P+Yrn/upCcM5J0hRrlP6Q1ms2/BPw4PRIUU2ia/+S8zrzj8lfjTLVElP1l2pXe5ZvdPIEQorOzKw5TyIcqrRilXBm819FNh3AJIltIfBaAyYfoJlXPLezkDN+knky3kXFgx6OVdob9C4nAeyCQ2IzqeqxwvhZR
On 08/06/17 14:42, Dominique Larchey-Wendling 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.
>

Yes, this is my impression, too. And yes, I also tried reverting the
factors in the multiplication as a confirmation.

Thanks
Raffaello

Archive powered by MHonArc 2.6.18.

Top of Page