coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] 16 Bit Unsigned Integer Library

From: mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] 16 Bit Unsigned Integer Library
Date: Thu, 2 Dec 2021 11:43:56 +1100
Authentication-results: mail2-smtp-roc.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-ed1-f49.google.com
Ironport-data: A9a23:G5fYbqn4F32pG6tN3NxO6lzo5gzoJ0RdPkR7XQ2eYbTBsI5bpz1Tz2JOWWiCPfzcZmfwe4okO4qxp0gC65PVztQyTQBl3Hw8FHgiRejtVY3IdB+oV8+xBpSeFxw/t512huEtnanYd1eEzvuWGuWn/SYUOZ2gHOKmUbeeYnkpHmeIdQ944f5ds75h6mJXqYPha++9kYuaT/z3YDdJ6RYsWo4nw/7rRCdUgRjHkGhwUmrSyhx8lAS2e3E9VPrzLEwqRpfyatE88uWSH44vwFwll1418SvBCvv9+lr6WkgDQ7qXMATXz3QKCu6thR9NoiF02aE+XBYeQR0P2nPZwpYrkIUL6c3YpQQBZsUgnMwYThpVCCFiPLJP4r6BIHm+rcm7wEjPcn+qyPJrZK0zFdJHo7gmWjAmGfswcWhRNHhvndmey7WiD+Jom84LN9juJIpZu3d6zDifA+xOfHxpa7GSsIUegyNp05gIReKEMpJfM2s+NQCbNkUJZ0NIXbsguMytolX/VxxRjm6PgZQ2xnyKlFkhlOX5WDbOUtmDRMEQk0rB42yariL2BRYVMNHZwj2Amk9AT9TnxUvTML/+3pXhnhKrvLGS+oDXIBgfVF/+rPXgz0DiCpRQLEsb/idopq83nKBuZrERQDXgyENofDZFMzaTLwH+wA6Iw6vQpQ2eAwDoixZfPcc+upZeqSMCjze0chCAOdCrmLKQQHOZsLyTqFte/AB9wXAqPUc5cOfO3zUvTEzfQP4CohaP3ZNZVuHIJAw=
Ironport-hdrordr: A9a23:j/PQdqvgpQuj8bsL+aWv0/OU7skDE9V00zEX/kB9WHVpm6uj+fxG/c576faaskdzZJhNo7290cq7Lk80i6QU3WB5B97LNzUO01HFEGgN1+Hf/wE=
Ironport-phdr: A9a23:/sIIYBJF974gjUposNmcuKNmWUAX0o4c3iYr45Yqw4hDbr6kt8y7ehCFvLMz0BSTBs3y0LFts6LuqafuWGgNs96qkUspV9hybSIDktgchAc6AcSIWgXRJf/uaDEmTowZDAc2t360PlJIF8ngelbcvmO97SIIGhX4KAF5Ovn5FpTdgsipyuy+4ZzebgpHiDajb755MQm7oxjWusQKm4VpN7w/ygHOontGeuRWwX1nKFeOlBvi5cm+4YBu/T1It/0u68BPX6P6f78lTbNDFzQpL3o15MzwuhbdSwaE+2YRXX8XkhpMBAjF8Q36U5LsuSb0quZxxC+XNtDwQLspWzqt8r1rRQfnhykHOTA383zZhNJsg69Auh2tuwZyzpTIbI2JNvdzeL7Wc9MARWpGW8ZcTylBAp6/b4QRFOoBPftTr5X8p1oAtxS+HwisD/7oxz9Nm3/23rM10/8hEQHa3QwhEcgBsG7VrNnvNacSUOG1zLXNzTjYYPNW3C3y6InMchw7vf6MWrdwfNPXxEIyGAzLkk+eppb5PzOJyOsNqW6b4vJuWO+siWMqpAB8rzuuy8kilIXEhYYYxkzE+Ch53Ys4JNm1RU9mbdOgEZZdtCWXOop1T84jTWxkpCI3x7wFtJO4eiUB1Zopxxnaa/OdcoiI5AruVOeXITdihXJqYqizhxio8UWm1+byVdG03U5UoiZZltTArHMA2hzJ5sSZVvdw/V2t1DmL2g3V9+pKO1o7lbDBJJ4k2rMwloQcsUDEHiLunUX5lq6WdkE99ue29uvrf6zqppGTOoJwkA3+PaMumsuwAeQ8LAcCRXSU+eO51LH7/E35RqtFjuEun6XHrJzXId4Xq625DgNPzIov9xWyAy2p3dkchXUHKUhKeBODj4jnIVHOJ/X4AO+6g1Sxkzdk2evGPr39ApXMIHnMiq3hfbdn505dyQozzMxf55dPB7EOJfL8QE7xtNjCAhAlNAy0xv7rCM9h2YMGRWKPHqiZPbvOvl+P/+IjOvWDZIsIuDnmMPUl/P7vjXohmVAHZ6Wp3J0XaGq5Hvt8OUmZb2Ds0Z89FjIBuRN7R+j3gnWDVyRSbjC8RfES/DY+XYe7DorYRsixgaOIxibzSphLZW1dCkyNDn7ydsOFWvYQbQqdJ8ZglnoPUr33GNxp7g2nqAKvk+kvFeHT4CBN7foLO/B64uTSkVc58jkmVqx1MkmIRmBw224EHno4gPE5rkt6xVOOl6N/hq4AfTS2z/xMWwY+c5Xbyr4iY+0=

I am looking for 16 bit unsigned integer library in Coq and I found this library [1] but at the very top it says, “This library has been deprecated since Coq version 8.10”, so I am curious about the other alternatives.

One way, at the top of my head, I can do this by

Record UInt16 := mk_uint { val: N; 0 <= val < 2^16} and define all the needed functions and proofs but before that I would like see the existing solutions.

Best,

Mukesh

[1] https://coq.inria.fr/library/Coq.Numbers.Cyclic.Int31.Int31.html

[Coq-Club] 16 Bit Unsigned Integer Library, mukesh tiwari, 12/02/2021
- Re: [Coq-Club] 16 Bit Unsigned Integer Library, Pierre-Yves Strub, 12/02/2021
- Re: [Coq-Club] 16 Bit Unsigned Integer Library, Xavier Leroy, 12/02/2021
  - Re: [Coq-Club] 16 Bit Unsigned Integer Library, mukesh tiwari, 12/03/2021
    - Re: [Coq-Club] 16 Bit Unsigned Integer Library, Ana Borges, 12/07/2021
      - Re: [Coq-Club] 16 Bit Unsigned Integer Library, mukesh tiwari, 12/09/2021