Prove the paper's counts, levelization, depth bounds, recipe lengths and Section 6 in Rocq, and revise the paper
8397e00 | (* Machine arithmetic for the functions of PeanoNat.Nat, as ExtrOcamlNatInt gives it to those of Init.Nat; | |
| the values extracted stay far below 2^62. *) | |
| From Stdlib Require Import Arith Extraction ExtrOcamlBasic ExtrOcamlNatInt. | |
| Extract Inlined Constant PeanoNat.Nat.add => "(+)". | |
| Extract Inlined Constant PeanoNat.Nat.mul => "( * )". | |
| Extract Inlined Constant PeanoNat.Nat.sub => "(fun n m -> if n > m then n - m else 0)". | |
| Extract Inlined Constant PeanoNat.Nat.pred => "(fun n -> if n > 0 then n - 1 else 0)". | |
| Extract Inlined Constant PeanoNat.Nat.div => "(fun x y -> if y = 0 then 0 else x / y)". | |
| Extract Inlined Constant PeanoNat.Nat.modulo => "(fun x y -> if y = 0 then x else x mod y)". | |
| Extract Inlined Constant PeanoNat.Nat.div2 => "(fun n -> n / 2)". | |
| Extract Inlined Constant PeanoNat.Nat.even => "(fun n -> n land 1 = 0)". | |
| Extract Inlined Constant PeanoNat.Nat.odd => "(fun n -> n land 1 = 1)". | |
| Extract Inlined Constant PeanoNat.Nat.testbit => "(fun a n -> n < 62 && (a lsr n) land 1 = 1)". | |
| Extract Inlined Constant PeanoNat.Nat.max => "(fun n m -> if n < m then m else n)". | |
| Extract Inlined Constant PeanoNat.Nat.min => "(fun n m -> if n < m then n else m)". | |
| Extract Inlined Constant PeanoNat.Nat.eqb => "(=)". | |
| Extract Inlined Constant PeanoNat.Nat.leb => "(<=)". | |
| Extract Inlined Constant PeanoNat.Nat.ltb => "(<)". | |
| Extract Constant PeanoNat.Nat.pow => "(fun n m -> let rec p k = if k = 0 then 1 else n * p (k - 1) in p m)". | |
| Extract Constant PeanoNat.Nat.log2 => | |
| "(fun n -> let rec g k x = if x <= 1 then k else g (k + 1) (x lsr 1) in if n <= 0 then 0 else g 0 n)". | |
| Extract Constant PeanoNat.Nat.log2_up => | |
| "(fun a -> let rec g k x = if x = 0 then k else g (k + 1) (x lsr 1) in if a <= 1 then 0 else g 0 (a - 1))". | |