Commit 1705a724 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Upgrade some sessions to shapes v5, fix bench

parent b784014f
module Toom
use import array.Array
use import map.Map
use import mach.c.C
use import ref.Ref
use import
use array.Array
use map.Map
use mach.c.C
use ref.Ref
use import as Limb
use import int.Int
use import int.Power
use import valuation.Valuation
use import int.ComputerDivision
use import types.Types
use import lemmas.Lemmas
use import compare.Compare
use import util.Util
use import add.Add
use import sub.Sub
use import mul.Mul
use import logical.Logical
use int.Int
use int.Power
use valuation.Valuation
use int.ComputerDivision
use types.Types
use lemmas.Lemmas
use compare.Compare
use util.Util
use add.Add
use sub.Sub
use mul.Mul
use logical.Logical
let constant toom22_threshold : int32 = 20
module Valuation
use import int.Int
use import int.Power
use import int.ComputerDivision
use int.Int
use int.Power
use int.ComputerDivision
use export number.Divisibility
use import number.Prime
use import number.Coprime
use number.Prime
use number.Coprime
use export number.Parity
let rec function valuation (n p: int)
......@@ -115,7 +115,7 @@ module Valuation
lemma valuation_mod: forall n p. 1 <= n -> 1 < p -> (mod n p = 0 <-> valuation n p > 0)
lemma valuation_decomp_aux: forall n p. 1 <= n -> 1 < p ->
lemma valuation_decomp: forall n p. 1 <= n -> 1 < p ->
n = (power p (valuation n p)) * (div n (power p (valuation n p)))
by divides (power p (valuation n p)) n
This source diff could not be displayed because it is too large. You can view the blob instead.
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment