coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Forbiding Qed to compute

From: Pierre Casteran <pierre.casteran AT labri.fr>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Forbiding Qed to compute
Date: Tue, 25 Apr 2017 08:55:52 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.casteran AT labri.fr; spf=None smtp.mailfrom=pierre.casteran AT labri.fr; spf=None smtp.helo=postmaster AT v-zimmta03.u-bordeaux.fr
Ironport-phdr: 9a23:7rS9kRyOcFPlB7XXCy+O+j09IxM/srCxBDY+r6Qd1OwTIJqq85mqBkHD//Il1AaPBtSHraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze6/9pncbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRH2iCkJKj03/m/ZhcN/kK1VrwmspwB9zoPOfI2ZKPRzc6HbcNgHRWRBRMFRVylZD42mbosAEfABPfxGoILguVYBtwC+BRWyC+P10DBIgGL90Koi0+QgDw7GxhYgEMwUvHvIttr1L7sSXv6vzKbSyzXOdPdW1i3m54jScxAtu/+MXahpfMfX1EIhFBvFg02NpYHqPT6ZzPoBv3WH4+Z6S+6jlm4qpxtyrzWh3ssgl4bEi4APxlza6Cl13Jw5KN6iREN0YtOpFoZbuTuAOItsWMwiRnlluCYkxb0Cvp62ZDYKxI0mxh7ebvyHdpSI7Qj/WOufOzt4mWtpd6m4hxao7Eev1PfzVtS70VpQoCpFiMHAtnEL1xPN9siKUuZx80ij1DqVyQzf9/1ILVoqmabGK5Mt2L09m5QLvUTGBCD2mUH2jKGMdkUj/+il8/znYrT4qZ+GLY97lBvyPbg0lcykHeQ3LBIOUHKd+emn0L3s51b2QK9LjvEsnKnZqojWJd4Hqa6hHw9VzoEj5g6jADehydQUhGUILFZYeB2clIXpIFHPIPXgDfilmViskTFrx+rHPrL7GJnNIGLDw//deuN27FcZww4ux5gL7JVNT7oFPfjbW0nrtdWeAAVvYCKuxOOyMNRwzJkTEUmGGbOUKqrU+QuQ5+81OeTKb4YOpDvnIv4N4/fkl35/l0VLLvrh5ocedH3tRqcuGE6ee3e52to=

Hi,

I wrote a small proof on fast growing functions (Wainer's hierarchy).

The statement is F_3 (2) > F_omega (2). The proof term is not so big, but it contains several occurrences of (f_2 23), which is known as greater than 2^23.

The problem may come from the fact that all these subterms are computed after Qed, thus I had to interrupt after some time. Is there an option for preventing Coq to expand function calls ?

Pierre

[Coq-Club] Forbiding Qed to compute, Pierre Casteran, 04/25/2017
- Re: [Coq-Club] Forbiding Qed to compute, Laurent Thery, 04/25/2017
- Re: [Coq-Club] Forbiding Qed to compute, Guillaume Melquiond, 04/25/2017
  - Re: [Coq-Club] Forbiding Qed to compute, Pierre Casteran, 04/25/2017