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: mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Proving p: Z is prime for large p
  • Date: Tue, 5 Apr 2022 11:16:04 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mukeshtiwari.iiitm AT gmail.com; spf=Pass smtp.mailfrom=mukeshtiwari.iiitm AT gmail.com; spf=None smtp.helo=postmaster AT mail-ej1-f53.google.com
  • Ironport-data: A9a23:/MBjo6Cdq+9i2xVW/+3lw5YqxClBgxIJ4kV8jS/XYbTApD10g2ECm zAaXW+Bb62LNzH8fI8gad6//RkDvp7QzN5kOVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA +E2MISowBUcFyeEzvuVGuG96yE6jMlkf5KkYAL+EnkZqTRMFWFw0XqPp8Zj2tQy2YThXlvU0 T/Pi5S31GGNi2Yc3l08sPrrRCNH5JwebxtF1rCWTakjUG72zxH5PrpHTU2CByeQrr1vIwKPb 72rIIdVUY/u10xF5tuNyt4Xe6CRK1LYFVDmZnF+A8BOjvXez8A/+v5TCRYSVatYoweSjYhQx 9kOjpHqbiYGLL3hnNU0cDANRkmSPYUekFPGCX22sMjWwk+fNnWxmLNhC0Y5OYBe8eFyaY1M3 aZAeXZdM1bZ3rLwnenTpupE3qzPKOHuIYASoXF8zC7QF/dgQJHCX6Di6tpR3TN2jcdLdRrbT 5NBN2M2MEicC/FJEnYuE6MvrsuHvUX2XGBquF+Kn/N0vkGGmWSd15C0aIaPEjCQfu1emV/dr Wbb9UziExQCPZqezyCE+zSinIfycTjTXYsTEPi19KcvjgDIgGMUDxISWB2wpvzRZlOCt8x3G VcGogshoesJ+RaMb/bvTzC8kVenl0tJMzZPKNES5AaIw6vSxg+WAGkYUzJMAODKUudmGlTGM XfZz7vU6SxTXK69Ei3Cq+/Fxd+mEW1Ecj9YPH5soR4tuoG7+OkOYgTzosGP+ZNZY/XwEDD0h j2I9W0w2u5VgskM2KG2u1vAhlpAR6QlrCZlt207vUr/tmuVgbJJgaT2tTA3Ct4ece6koqGp5 iRspiRnxLlm4WuxvCKMWv4RO7qi+uyINjbR6XY2QcVwr238pyD5JtwIiN2bGKuPGpZbEdMOS B+D0T69GLcOVJdXRfMvM9PoU5pCIVbITIy/DayLBjaxXnSBXFbfoHsGib+40Gfqn0wh+ZzTy r/KGftA+U0yUPw9pBLvH7l1+eZynkgWnDqPLbimkUnP+efBPBa9FOZdWHPTP7tRxP7V8G39r YwDX+PUkE43eLOlMkHqHXs7dw9iwY4TXsCo9aS6t4erfmJbJY3WI6SIm+l8JNU5wf89eyWh1 ijVZ3K0AWHX3RXvQThmoFg5AF82dZog/389IwI2OlOkhyoqbYq1vfUQcpI2ef8s8+k6lax4S PwMesOhBPVTS2Sfq25NM8Wl9IEyJg62gQ+uPja+ZGdtcpNlQTvP8IC2cwbq8h4IESfq59A1p Ket11+ATJdaH1ZiAc/aZeiB1VS0uXRByut+U1GZcNZWcUTotoNtLnWp3PMwJsgNLzTFxyebh 17GW0dG+bGVrtZsotfThK2Co4O4KMdEHxJXTzvB8LK7FSjG5W78k4JNVeC/ezqCBm75/aOVY /oMk6PxPfgBq1Z9s4RmFoFtw69jtcDkoKVXz1g9EXjGMwarB7dnLiXU1MVDrPcWlLpQuA/zV 0DWv9cHYvOGP8TqFFNXLw0gN7zR2fYRkzjUzPI0PESqu3MtreTfCR1fb0uWlShQDLppK4d5k +0vj8gbtl6kgR0wP9fa0y1ZqzaWInobX/l1v50WGtWw2A8iy1UHbJ6FTyGru9eAbNJDNkRsK TiR3fKQi7NZz0vEUnwyCXmdgrYH1MpW4EhHnA0YOlCEutvZnftrjhdfxjI6E1ZOxRJd3uMvZ 2VmOiWZ/0lVE+uEWSSCY4ytJ+2FLBiQ+0i0xllQ0WOEFA+nUWvCKGB7MuGIlKzcH6SwYRADl Ix0Ck68OdopQC019iQ3UE9h7ffkSLSdMyXczdu/EZ3t84YSOFLYb2zHWYbMgxTiCMI1wkbAo IGGOQq2hbLTbUYtnkHwN2VWOXn8hvxJyKyujMyNJJ80IFw=
  • Ironport-hdrordr: A9a23:tvtrv67AUsOOdls/BAPXwPHXdLJyesId70hD6qkRc20tTiX8ra qTdZsgpHrJYVoqKRMdcJW7Scq9qBDnlKKdg7NhWYtKNTOO0ACVxcNZjbcKqAeQfBEWmNQts5 uIsJITNDQzNzVHZArBjzVQ2uxP/OW6
  • Ironport-phdr: A9a23:tsxzjBQDy19mPQK+ihEKFUsp/9psohGVAWYlg6HPa5pwe6iut67vI FbYra00ygOTB8OCtK4P0bKempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yN s1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffRtEiCCgbb5wI xi6ohvdutULioZ+N6g9zQfErGFVcOpM32NoIlyTnxf45siu+ZNo7jpdtfE8+cNeSKv2Z6s3Q 6BWAzQgKGA1+dbktQLfQguV53sTSXsZnxxVCAXY9h76X5Pxsizntuph3SSRIMP7QawoVTmk8 qxmTgLjhiUaOD4j6GzYhcJwg6BbrhyvpBJx3pDab52OOfVkYq/QZ8kXSXZdUstTUSFKH4Oyb 5EID+oEJetYqpT9p1gQohulBQmnGf/vyj5Gh3Dsx6060vkqHAbD3Aw9HNIBrm/UrNXpNKcTX +G61rPIzTTZY/NX2Df96ZTIchU6rPGDWLJ/a8vRyU01GwzZiVWQrJXoMjWI3esCr2aV9fBvV f6zi2E5sQFxpCCiy9ojhITVmo4YyE3I+Dh5zosoJtC1RlB2bcK5HZZOqS2XN4V7T8c/T2x1p Cs217ILtIC5cSUL1pgqyRrSZv+ZfoWO/xntWuGRITJii3JkfrKynxmy8Um8yu38S8m7y0xGo TZCktnJsH0Gyh/d6tCfR/dj4kus3SyD2gPT5+1eP0w4iKnWJ4Qhz7M+kJcYrF7NETXsmErsi a+bbkUk9fas6+Tgerjmo4WTN45wig3nLKsumNGzDf02MgUOUWWX4+u81Lrk/U32RLVFkOc6n bXesJDfPcgbp6i5DBFJ0os79RqzEzOr3M4bkHQHNl5JZg+LgovzN1zOLv30FfK/jE6tkDdvy fDGJLrhApDVI3jGjbfhfqhy61VcyAovzNBe6YhbCqsAIP7pW0/xtd3YDgM8MwGvzObnDc9y1 oIaWW6VHqCZN6bSvUeO5u00O+aMfpMauC7hK/g54P7jlWI1lUcHfaa1xZsXdGy4HvN+LkqFZ nrsm84NHnsOvgojV+Pnk0aCUD5WZ3aqRa0w/DA7CIS8DYfCXI+hmrKB3D3oVqFRM2tBExWHF WriX4SCQfYFLiyIceF7lTlRUKWiRpQhnQ2vqwbgyvIzK/fX9zYYqZP83cJ0oezSlA033TNxB sWZlWqKSjcnzSszWzYq0fUn8gRGwVCZ3P0g6xQ5Pdla5vcSFxw/KYaZ1OtiTdb7RgPGeN6ND legWNSvRz8rHZoq29FbRUF7Fp25iwzbmTKwCuoQir+GH5wo873VxXm3Jsd813Pu26wojl1gS cxKZiW9nqAqzwHIHMbSllmB0aOjdKASxinIoWKezmeVvF1ZTwdqUOPEXHEDY2PZqN344gXJS Lr9Qa8/PF5nzsiPYrBPdsWvjVhCQ6L7P8/CZmuqh2qqLROBx7fJYYizPmtAh2PSD08Llw1V9 nGDXeQnLgGmpW+WTDlnFFa0Jljp7fE7s3SjCEk90wCNaURlkbuz4B8cw/KGGbsV2foftSEtp i8Rfh711s/KC9eGuwtqfblNKdI77lBd0GvFtgt7dpW+JqFmj1Qafkx5pUTrnxlwD4xBl4Ato hZIhEJ3NKGVy1NddiyRx5G2O7zWNmza8xWmaqqQ0VbbkZ6X9qoJ9PUkugD7pgj6cyhqu35j0 tRTzz6d/sCQVFtUAc+3CB9nsUUh9NS4KmEn6ojZ1GNhK/yxuz7GgJcyAfc9jw2nZ5FZOb+FE wn7F4sbAdKvIaokgQvMDFpMMeZM+aozJ87jeeGB3fvhOftjkSmmkWVY6Zp8lEON9jZ5YuHN1 pcBhfqf20HUMlW0xEfkqc3xlY1eMHsXA2my0ij4BZFYfKw0fIcKFWKGLMi+x9E4jJnoES09l hbrFxYN38mnfgCXZlr20FhL1EgZlnegnDOx0z1+lzxBQrO35CXV2KyicRMGPjUOX2x+lRL3J pDyidkGXU+uZgxvlR2/5E+8ybIJ7Kh4KmDSRw9PcU2UZylnT6i9rbqeYtFG8pJusCRWTOGUb lWTS7q7qBwfmy/uBGpRwjkneiri4M2o2UwnzjjEfDAu9zLQYqQSjV/H6cbZROJN0zZOXyR+h TTNRxC9M9Sv4dSIhsLGu+G6WXimU84bei3qwIWc8SqjsDcyUFvvwrbpw42hTFNptE2zn8NnX ijJshvmN4zi1qDhdPliYlEtH1jkrcxzBoB5lII0wpAWw3kTwJuPrh9l2S/+N8tW3aXmYT8DX zkOlpTQ/Qvow01/L22A3YO/V3Sc3s5JaNyzY2dQ0SU4pZMvau/c/PlfkC15r0Dt5wfMYvVmn isc1vI06TgbguAVvSIiyyycBvYZGkwSbkmO31yYqtu5qqtQfmOmd7O9gVF/kd6WB7aHughAW Xz9d8RqDWpq4854Kl6JzGzr59SuZozLddxK/E7x8V+In61PJZk2jPZPmSd3JTe3oyg+0+Bix R12gcPh4c7eej0rpv7mREYfbGG9ZttPqG+xy/wFxYDPgdjpRtI4S1BpFNPpVa76TmxU7Ky9c V7ISHpm8j+aAeaNQ1HZshs36SKXVcjsbSnfJWFFn4o4AkDBYhUO2kZMG2xq+/xxXgGymJ6+L AEgvG1Xvhig7UISguNwa0umCjeZ/Vj3LGdyEN/FdVJX9l0QvhiOd5XPsqQrWXkfp8PEzkTFK 3THNV4QXCdZBwrdXQClZv73upHB67TKXLPgaaaeJ+zf86oGEK7ZjZO3jtk8pmjKbJ7eeCI4S aV8gxsmPzgxDc3dn39npzU/sSXLYobboR69/nYytcWj6LHwXxqp44KTCrxUONEp+hasgK7FO fTCzCB+YS1V0J8B3xqqgPAWwUIShidydjKsDaVItCjDS7jVk7NWCBhTYj16Nc9B5aYxlgdXP suThtTw379+xvk7bjUNHUTmgd2sbNcWLnuVMVrGAAOGNu3DK2CQhc7wZqy4RPtbi+AV/xy8t DCHElPyazSOkz66MnLneepIjSydIFlfoNTnKkcrWTWlFou2LEDgY7oVxXUszLY5h23HLzsZO Dl4KAZWq6GIqDhfmrN5EnBA6XxsKa+FnTyY5q/WMMVz07MjDyJqmuZd+Hl/xaFS6XQOQeF2l TDSst9xqkun1OiOyyZieBVLozdPwomMuA8xXMeRvokFQnvC8B8XuC+IDA8WotJ+FtD1k6VZy 9yKmaCqbTkfqJTb+swTA8WSI8WCeilEU1KhCHvfCw0LSiSuPGfUihlGkf2cwXaSq4Aztpnmn JdmolpzW1k8F/dcAUNgToRqyHhfUTYtkLrdh8kNtyPWRPj5QcxbutXKVKvXD6i0bjmeirZAa l0Dxraqdewu
  • Ironport-sdr: xbjKbk6SRb6L+dgH1DRrRHMujWPadOSGK8j6bRqOZtfkgkBA99cuXwpHro0FpHgGsiSAwcbD+F V+158BUNhDeotjvPjqOUjx5uMv6eEe6Ul3SU7KHu5cOzno2b7R1AcRqndoNRmCAd1uxecr1fzO Jo3lLkQzmNmXJ48Z+3kRVbGILB7kExGi/qadsyI846SFoz6+LK96uNu1ldGwQhcShQpeSBRMzg YmlXUh9fr50GAe0ysA1sEoD4HERMoRJA17gYq/90zPI/xqJCd8cQY/53VYNiUejxXvQjbAahF4 Q2szR/p0YNhzbzOb6tD8Uy4m

Hi Tim,

It’s not exactly you are looking for but have a look at Rabin Miller formalisation [1]. It has some benchmarks at the end of the file, which does not look very promising given that you wanted to assert primality of 32 bit number. The other way, which is already suggested by Roux, is to use Coq-prime. 

Best, 
Mukesh

[1] https://github.com/coqtail/coqtail/blob/master/src/Arith/MillerRabin.v

On Mon, 4 Apr 2022 at 21:06, 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