def shln_mod.go

lawful-words@0.1.0.0 · proof_u32.bend:1088

import Base
import lawful-words@0.1.0.0/proof_nat.bend as N

1088def shln_mod.go(+x: Nat, +k: Nat, +m: Nat, +hm: {Nat.pow(2n, 32n) == m : Nat}, z: Bool, +ez: {Nat.is_le(k, 32n) == z : Bool}) ->
1089  {Nat.mod(Nat.mod(Nat.mul(x, Nat.pow(2n, k)), m), Nat.pow(2n, k)) == 0n : Nat}:
1090  match z:
1091    case True{}:
1092      %hm : {Nat.mod(Nat.mod(Nat.mul(x, Nat.pow(2n, k)), _), Nat.pow(2n, k)) == 0n : Nat}
1093      %Equal.sym(Nat, Nat.mod(Nat.mod(Nat.mul(x, Nat.pow(2n, k)), Nat.pow(2n, 32n)), Nat.pow(2n, k)), Nat.mod(Nat.mul(x, Nat.pow(2n, k)), Nat.pow(2n, k)),
1094          N.mod_mod_pow(Nat.mul(x, Nat.pow(2n, k)), k, 32n, ez)) :
1095        {_ == 0n : Nat}
1096      N.mul_mod(x, Nat.pow(2n, k))
1097    case False{}:
1098      +d = Nat.sub(k, 32n)
1099      +pd = Nat.pow(2n, d)
1100      +inner = {
1101        %N.le_sub_add(32n, k, N.lt_to_le(32n, k, N.not_le_lt(k, 32n, ez))) : {Nat.mod(Nat.mul(x, Nat.pow(2n, _)), m) == 0n : Nat}
1102        %Equal.sym(Nat, Nat.pow(2n, Nat.add(32n, d)), Nat.mul(Nat.pow(2n, 32n), pd), N.pow_add(2n, 32n, d)) :
1103          {Nat.mod(Nat.mul(x, _), m) == 0n : Nat}
1104        %Equal.sym(Nat, Nat.pow(2n, 32n), m, hm) : {Nat.mod(Nat.mul(x, Nat.mul(_, pd)), m) == 0n : Nat}
1105        %N.mul_comm(pd, m) : {Nat.mod(Nat.mul(x, _), m) == 0n : Nat}
1106        %N.mul_assoc(x, pd, m) : {Nat.mod(_, m) == 0n : Nat}
1107        N.mul_mod(Nat.mul(x, pd), m) : {Nat.mod(Nat.mul(x, Nat.pow(2n, k)), m) == 0n : Nat}}
1108      %Equal.sym(Nat, Nat.mod(Nat.mul(x, Nat.pow(2n, k)), m), 0n, inner) : {Nat.mod(_, Nat.pow(2n, k)) == 0n : Nat}
1109      N.mod_zero_l(Nat.pow(2n, k))