examples/multiprecision/valuation.mlw

   1 module Valuation
   2
   3   use int.Int
   4   use int.Power
   5   use int.ComputerDivision
   6   use export number.Divisibility
   7   use number.Prime
   8   use number.Coprime
   9   use export number.Parity
  10
  11   let rec function valuation (n p: int)
  12     requires { 1 < p }
  13     requires { 1 <= n }
  14     variant { n }
  15     ensures { 0 <= result }
  16     ensures { divides (power p result) n }
  17   = if mod n p = 0
  18     then
  19       let d = div n p in
  20       let r = valuation d p in
  21       r+1
  22     else 0
  23
  24   lemma valuation_mul: forall n p. 1 <= n -> 1 < p
  25     -> valuation (n*p) p = 1 + valuation n p
  26        by mod (n*p) p = 0 so div (n*p) p = n
  27
  28   lemma power_ge_1: forall b e. 1 <= b -> 0 <= e -> 1 <= power b e
  29
  30   let rec lemma valuation_times_pow (n p k:int)
  31     requires { 1 <= n /\ 1 < p /\ 0 <= k }
  32     ensures  { valuation (n * power p k) p = k + valuation n p }
  33     variant  { k }
  34   =
  35     if k > 0
  36     then begin
  37       valuation_times_pow n p (k-1);
  38       assert { valuation (n * power p k) p
  39                = 1 + valuation (n * power p (k-1)) p
  40                by valuation (n * power p k) p
  41                = valuation (n * power p (k-1) * p) p
  42                = 1 + valuation (n * power p (k-1)) p }
  43     end
  44
  45   lemma valuation_split: forall n p. 1 <= n -> prime p ->
  46     let v = valuation n p in
  47     valuation (div n (power p v)) p = 0        (* only altergo proves this? *)
  48
  49   let lemma valuation_lower_bound (n p v:int)
  50     requires {  1 <= n /\ 1 < p /\ 0 <= v }
  51     requires { divides (power p v) n }
  52     ensures  { v <= valuation n p }
  53   =
  54     let q = div n (power p v) in
  55     assert { n = q * power p v };
  56     valuation_times_pow q p v
  57
  58   lemma valuation_pow: forall p k. 1 < p /\ 0 <= k -> valuation (power p k) p = k
  59
  60   let rec lemma valuation_monotonous (n c p:int)
  61     requires { 1 <= n /\ 1 <= c /\ 1 < p }
  62     ensures { valuation n p <= valuation (n*c) p }
  63     variant { n }
  64   = if mod n p = 0
  65     then begin
  66       let q = div n p in
  67       assert { n = p * q };
  68       valuation_monotonous q c p;
  69       assert { valuation n p = 1 + valuation q p };
  70       let m = q * c in
  71       assert { valuation (n * c) p = 1 + valuation m p
  72                by n * c = m * p
  73                so valuation (n*c) p = valuation (m*p) p
  74                   = 1 + valuation m p };
  75     end
  76
  77   lemma valuation_nondiv: forall n p. 1 <= n -> 1 < p ->
  78     valuation n p = 0 <-> not (divides p n)
  79
  80   lemma valuation_zero_prod: forall c1 c2 p. 1 <= c1 -> 1 <= c2 -> prime p ->
  81     valuation c1 p = 0 -> valuation c2 p = 0 -> valuation (c1 * c2) p = 0
  82
  83   let rec lemma valuation_times_nondiv (n c p:int)
  84     requires { 1 <= n /\ 1 <= c }
  85     requires { prime p }
  86     requires { valuation c p = 0 }
  87     ensures  { valuation (n*c) p = valuation n p }
  88     variant  { n }
  89   = if mod n p = 0
  90     then let d = div n p in
  91          valuation_times_nondiv d c p;
  92          assert { valuation (n*c) p
  93                   = valuation (d*c*p) p
  94                   = 1 + valuation (d*c) p
  95                   = 1 + valuation d p = valuation n p }
  96     else ()
  97
  98   lemma valuation_prod: forall n1 n2 p. 1 <= n1 -> 1 <= n2 -> prime p
  99     -> valuation (n1 * n2) p = valuation n1 p + valuation n2 p
 100     by let v1 = valuation n1 p in
 101        let v2 = valuation n2 p in
 102        let c1 = div n1 (power p v1) in
 103        let c2 = div n2 (power p v2) in
 104        n1 = power p v1 * c1
 105     so n2 = power p v2 * c2
 106     so valuation c1 p = 0
 107     so valuation c2 p = 0
 108     so valuation (c1 * c2) p = 0
 109     so n1 * n2 = power p v1 * power p v2 * (c1 * c2)
 110        = power p (v1+v2) * (c1 * c2)
 111     so let pow = power p (v1+v2) in
 112        let c = c1 * c2 in
 113        1 <= c1 so 1 <= c2 so 1 <= c
 114        so valuation (n1*n2) p = valuation (pow * c) p = valuation pow p =  v1 + v2
 115
 116   lemma valuation_mod: forall n p. 1 <= n -> 1 < p -> (mod n p = 0 <-> valuation n p > 0)
 117
 118   lemma valuation_decomp: forall n p. 1 <= n -> 1 < p ->
 119         n = (power p (valuation n p)) * (div n (power p (valuation n p)))
 120         by divides (power p (valuation n p)) n
 121
 122 end