Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Proving p: Z is prime for large p

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proving p: Z is prime for large p


Chronological Thread 
  • From: roux cody <cody.roux AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Proving p: Z is prime for large p
  • Date: Mon, 4 Apr 2022 21:14:32 -0400
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=cody.roux AT gmail.com; spf=Pass smtp.mailfrom=cody.roux AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk1-f181.google.com
  • Ironport-data: A9a23:6eNmlqCE6a7VVBVW/xPlw5YqxClBgxIJ4kV8jS/XYbTApG8jgmBWm mcWCzrXbKyKYWf1etx/YNuy8UwFucPQn4JjOVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA +E2MISowBUcFyeEzvuVGuG96yE6jMlkf5KkYAL+EnkZqTRMFWFw0XqPp8Zj2tQy2YThX1vX0 T/Pi5S31GGNi2Yc3l08sPrrRCNH5JwebxtF1rCWTakjUG72zxH5PrpHTU2CByeQrr1vIwKPb 72rIIdVUY/u10xF5tuNyt4Xe6CRK1LYFVDmZnF+A8BOjvXez8A/+v5TCRYSVatYo2ygns1Uy dJXj6STdC0gHofshroxcSANRkmSPYUekFPGCX22sMjW0U6fNnW1k6woA0YxMokVvO1wBAmi9 9RCcGFLPk3F3bjvhuvrE4GAhex7RCXvFIgYtmAm1zbEHd4pRJnCR+PB4towMDIY3ZgWRKyHP 5pxhTxHNwXLZSYQBAwuUtE5rrmOun+veCBjtwfAzUYwyzGLkFYZPKLWGNHSY5mBQdhftl2Jo 3rPuWX/GBATctKFoQdp6Vqpj+7L2D34AcccTe3hsPFth1KXyyoYDxh+uUaHTeeR02e/RvdeL FYuwgkTh6ES3my1EPXfZkjtyJKbhSI0V91VGuw8zQiCzKvI/gqUblToqBYRN7TKU+dmFVQXO k+1c8DBXmMw7eXEIZ6J3vLF8mPoYHl9wXoqPHdcFWM4D8/fTJbfZy8jo/5mGa+xy8P2QHT+m mDT6ic5gLoXgIgA0KDTEbH7b9CE9sWhou0dvF2/soeZAuVROd7Ni2uAtAmz0Bq4BNzFJmRtR VBd8yRk0MgADIuWiAuGS/gXEbei6p6taWOA0AY2TsV/rW/xoxZPmLy8Bhkuey+F1e5UKVfUj LP75Gu9GbcPZCv7NPcpC25PI51yl/O8SrwJqcw4nvIXOsQrHON21C5pYkGU0gjQfLsEwMkC1 WOgWZ/0Vx4yUPw5pBLvH7d1+eZymkgWmD2OLbimkEzP+efPPBa9FOZeWHPTP7FRxP3e/G39r Y0EX+PUkEU3bQELSnCJmWLlBQxXdyhT6FGfg5A/S9Nv1SI9QTt7VqCIne16E2Gn9owM/tr1E riGchcw4DLCabfvcG1ms1hvN+HiW4hRt3U+MXB+NFqkwSlxboOm7aNZfJwyJOF1+OtmxP9yb v8EZ8TQWqQVGmqbo2wQPcvnsYhvVBW3ngbRbSeoZT4IeZQ/FQHE/9nTeBTiqXsVBS2tuMpi+ LCtj1uJQZcKSwl4ItzRbfajkwG4sXQHybB9WkLJJp9Yf0C1qNpmLCn4j/kWJcAQKEWblmHKi VrOWRpB/LvDuY449tXNlJuolYbxHrssBFdeEkna8a2yanvX82+l9olKD7SFcDXbY2Xrofnwa OhQycb8B/0JhlN9tYRxTuRwxqUk6tqz/rJXw1g2HHjPaFj3WLpsLmPcgZtKv6xJg6Fa4E64A xLWvNZdPrqNNYXuF1tIfFgpaeGK1Pc1nDjO7KRqfB+runcvpLfXA19POxSsiTBGKOcnOo0Sx +p86tUd7Bayi0Z3P9va3DpY8X+Aci4JX6k97M1IBYbqjk81yQgHb8WMU2n555aAb9gKOU4ve 2fGiK3HjrVa50zDb3tjSiSXjLQF3cwD6EJQ0VsPB1WVgd6Z1PU56xtcrGYsRQNPwxQbju9+N wCH7aGuyXliItupuCRCY4xoMwRIBRnc5E+ojlVQxDSfQE6vWWjAamY6PI5hOazfH310JlBmE HOwkQ4JkgoGuOn+2yIzXQhurPmLoRlZ6FjZgM7+dyiaN8BSXNcm65NCoUIHrhLmBYU6g0ivS SyGOgpvQfWTCBP8aJHXx2VXOXr8hfxEyKF/rSldwZ40
  • Ironport-hdrordr: A9a23:TetjH68PAhX2MPSTdu5uk+DhI+orL9Y04lQ7vn2ZKCYlC/Bw8v rFoB11726QtN98YgBDpTnEAtjifZq+z/9ICOsqTNOftWDd0QPCEGgh1+vfKlbbakrDH4BmpM FdmmtFZOEYz2IWsS832maF+h8bruW6zA==
  • Ironport-phdr: A9a23:wFnykRO2Wf+hdei35aAl6nYDBxdPi9zP1u491JMrhvp0f7i5+Ny6Z QqDv68r1QCSFtmAo9t/yMPu+5j6XmIB5ZvT+FsjS7drEyE/tMMNggY7C9SEA0CoZNTjbig9A dgQHAQ9pyLzPkdaAtvxaEPPqXOu8zESBg//NQ1oLejpB4Lelcu62/6s95HJfglFhjSwbbx9I Ri4sA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S 6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5 KlpVRDokj8KODE38G7VisJ+gqFVrg+/qRNj2IPbep2ZOeBkc6/BYd8XR2xMVdtRWSxbBYO8a pMCD/AGPeZFoIj2ukcBrRyjCgisGejizSNHhnjr0qw6yeghCwbG3BEvHt8Vv3TUqc/6NKYWU eyv0KbIyjDDYupQ1Dzg54fGbgovruuQXbJsb8XR008vGhvEg1ieqIHoOy+Z2/gOvmWf4OdtU eGihmEnpQxwrTWixckihIbNi48LxF7J+it0zZsrKdC7VEJ2fcCpHZVOuyyaMYZ9X80sQ2Ztu Ckgy70Gv4a2fCcLyJQ7xx7fdueIf5KU7RLkUeadOTl5hHNmeLK+nxa971WvyuzmWcWu11ZKt CVFn9/RvX4Ozxze8taLRud580u72juC1xrf5v9aLUwpj6bXNp0szqM2m5EOq0rMBDX2l1/zj KKOdkUr5Oyo6+P/b7XjvJCcNot0hhjgMqQth8CzGOo4PhUNUmSG4+i827rj/Ur2QLVOkPI6i LXWsJffJcgDp665BRFa0po75hqhEzur1M4UkHoHIV5fZh6LkZXlN0vTLP37EPuzm1Gsny1qx /DCML3hGJLNLn3bnbj9erZy9k5dxBApzdBY+pJVBaoMIP32WkDrtdzYCgU1PBCzw+biENl90 JgRVnqVAqCFKKPSrUOI5uU3LuWRfIMVoiryK+A55/7yin80gUMSfa6w3ZcOdH+4GulmLF6Cb Hr3gtYBFH8KsRAkQOzrjl2CSz9TaGyoU6Iy/DFoQL6hWIzEX8WmhKGL9Ca9BJxfIG5cWX6WF nK9bYKZS78Hby6DaptqlTAVE6KmVp8J2hSntQu8wL1ieLmHshYEvI7ugYAmr9bYkgs/oGQc5 6W11miMSzsxhWYUX3os26s5p0Vhy1CF2Kw+gvpCFNUV6ekaGhwiO8v6yOp3Q8v3RhqHZs2AH V2hTsTgGzYsXvo+xtYPZwB2HNDxxgvb0X+SCqQO36eOGIRy96vd23brIMMowHHKxe87iEQ2a sRKPGyiwKV48lubHJbHxmOekavibqEAxGjN+WOEmHKJp11dWRVsXL/tWHkeYg7Iro286BqSF vmhDrMoNgYHwsmHQkdTQvvui1gOBPLqOdCEJnm0h3/1HxGDgLWFcIvtfWwZmiTbEkkN1Q4Jr z6AMkAlCyGtrni7bnQmHE/zY07q7eh1qW+qBk4ywQaQakR91r2zshcLjP2YQvkX0/oKoiAk4 zlzGV+82ZrRBb/i70Jqe6lNJ8k6/Udv2mfQtgg7NZulbuhjilMYbwVrrhb2zRwkQo5EkMUss DYr1F8ocfPegA4HLWnBm8mgY+6ySCG65h2kZq/I10uL1d+X/v1K8/EksxD5uwrvEEM+8nJh2 t0T0n2G55yMAhBBNPC5Gksx6RV+oKnXJycn4IaBn3ZrPbjyqDjfy/omAeIkzlCreNIVY8bmX EfiVtYXAcSjMrlgkF+lf1QeO/1C3KExNsKiMfCB3eT4dPYllzWgg2Nd5Yl72U/Z7CtwRNnD2 JMdyu2Z1A+KP9vlpG+oqdu/2YVNZDVIW3G61TChHolaIKt7YYcMD26qZcyx3NR3wZD3CTZU8 1uqBlVO38HMG1LaZFvxzEtK0lkHiXOikCq8iTdzlnklo7Ge0yrH3+n5PEBfaygbGS841w6qe Njtx9kBFFCldQ0oiAeo6SOYj+BAqaJzInOSCUZEci7qLn1zB665t76MeclKu9sjtSRaVvj5Y EjPEOas5UtHlXm5Ri0HlGloElPi8o/0lBF7lm+HeXN6rX6DPNp12Q+a/tvXA/hYwjsBQiB8z zjRHFm1edezrrD239/OtP6zU2W5W9hday7umMmLsyeqo3dtHA2XkPW6m9mhGg8/m3yetZEiR WDToRDwb5O+na+9PfMhZE51FHfz7sN7Hsd1lY561/RykTAKw56S+3QAi2L6N95WjLn/YHQ6T jkO29fJ4QLh1R4rPjeTyon+THnY3tp5aozwfDYNwixkpZMvau/c/PlekCByuFb9sQ/Bfa03g GIG0fV3oH8C37NS5Ux0n33bWOxNWxEfZ3CklgzUvY7i6v8MPyD2L+D2jA0nzLXDRPmDul0OB ii/I894W3c2toIlaBrNyCGhtN+iIoWBK4JL8EXTyU+IjvAJes1r0KNWw3M2YySl+iR1roxzx R12gcPl4M7ecTgrpOThRUcGfjztO5FKomGr1PkB2JbQh8f1R91gAmlZBcSzC6v5THRK86ygb ljrcnV0q2/HS+CHTEnPtQE/9SKJS9fyaDmWPCVLl4w8AkTNYhUO2kZMG2xr1p8hSlLwnZKnK hwooGtLoAa/80opqKogIRD7Vi23SB6ATDAyRdDfKRNX6lsH/ELJKYmE6ek1GShE/5qnpQjLK 2qBZg0OA3tbEkqDT0vuOLWj/7yiu6CRG/a+Iv3SYL6Ptf0WVvGGwoiq25dn+DDEP9uGP31rB fk2kkRZWnUxF8PckjQJAysZ8kCFJ9acvwu58zZro9qX9f3qXEfx5tLKBeICaJNg/Be5harFP OmVxW54JTteypIQ1CrIxbwYjztww2llczigF6hFtDaYFvqB3P8KSURBMmUqZJIbisB0lhNAM sPalN7vg7txj/pvTkxASUSkgMaiI8oDP2C6MlrDQkeNLrWPYzPRkKSVKeuxT6NdiOJMuli+o zGeRgXoOTiS0SPuSgCHPuRFjSXdNxtb8tLYEF4lGS34QdTqZwfuesdwliEzyKYoi2niMGcdN X1icBoIoOTAtGVXhfJwH2EH5X1gZ7rh+W7R/6zTLZAYtuFuCyJ/mrdB4Xg0/LBS6TlNWP1/n Ca6RjtGrFSvk+3JwT1iAkImQtdjgYuKuQB8Ovyc+MAQADDL+xUC6WjWABMP9YMN4jLHtKVZy 9yJn6X2em4qzg==
  • Ironport-sdr: 9WE8I2mr8zM79FCIhXDTGy12SB035nTpe5jOiq+UhjCN1Ave9/dWAoSeVYuUPkQWrvljWz32Rr 5ZsfFBg+hzpXuYrteBwbSikFSzTwa8D4PcPSGm/ZMtESiOjgMxa4WQfj+5Cri/w0vDnpXYf0nj 1kCegEK5vt40kM96IdXoweXV0duVN9IF5x3/z9vN5X54zZUs5PkSZ2+rPYHYSMtvifGOqaWfxB BsYknzYtgnP66ESzDoKC895caqo+CdDfk+kO4s7CudwYeY/9hhCw8H6WF27Raajm+v5K05d2nS w8dfyf2lurmg6v3tJmrnUldJ

I'm sure someone will have already posted this by the time I send it, but here's a nice approach from a few years ago that probably still compiles: https://github.com/thery/coqprime originally from Werner, Gregoire and Thierry, which formalizes this: https://en.wikipedia.org/wiki/Pocklington_primality_test

The idea involves running (fast) C code to generate *certificates*, which then are checked by verified Coq code in P time.

This is actually the "right" way to do it IMHO, since AKS is still pretty slow as far as I know.



On Mon, Apr 4, 2022 at 4:06 PM Timothy Carstens <intoverflow AT gmail.com> wrote:
Let p: Z be a 32-bit positive literal. Suppose p happens to be prime. What’s the best way in Coq to prove that it’s prime?

The standard library provides a definition of primality for Z, and even provides a decision procedure, but the decision procedure does not seem very fast.

At a glance it appears mathcomp-extras provides a proof of the AKS primality test, but I’m a mathcomp novice and to my novice eyes their definition appears to be for nat (not N or Z).

Does anyone have a trick for this?

Thanks in advance,
-t




Archive powered by MHonArc 2.6.19+.

Top of Page