~/bend-docscommunity

proofs/math/natural/inverse.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/inverse.bend as Inverse

8 imports
import Base
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as A
import ../../../src/math/natural.bend as M
import ./arith.bend as R
import ./gcd.bend as G
import ./lcm.bend as LC

Definitions

def bg source · line 19 · raw

@bz:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.Bezout -> Nat

def bc source · line 24 · raw

@bz:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.Bezout -> Nat

def cong_add_r source · line 31 · raw

@+mp:Nat -> @+x:Nat -> @+y:Nat -> @+y2:Nat -> @+e:{Nat.mod(y, 1n+mp) == Nat.mod(y2, 1n+mp) : Nat} -> {Nat.mod(Nat.add(x, y), 1n+mp) == Nat.mod(Nat.add(x, y2), 1n+mp) : Nat}

def cong_mul_r source · line 35 · raw

@+mp:Nat -> @+x:Nat -> @+y:Nat -> @+y2:Nat -> @+e:{Nat.mod(y, 1n+mp) == Nat.mod(y2, 1n+mp) : Nat} -> {Nat.mod(Nat.mul(x, y), 1n+mp) == Nat.mod(Nat.mul(x, y2), 1n+mp) : Nat}

def shift source · line 40 · raw

@+z:Nat -> @+c:Nat -> @+k:Nat -> @+mm:Nat -> @+e:{Nat.add(c, k) == mm : Nat} -> {Nat.add(Nat.add(z, c), k) == Nat.add(mm, z) : Nat}

(z + c) + k == M + z when c + k == M

def add_cancel_mod source · line 44 · raw

@+mp:Nat -> @+x:Nat -> @+y:Nat -> @+c:Nat -> @+e:{Nat.mod(Nat.add(x, c), 1n+mp) == Nat.mod(Nat.add(y, c), 1n+mp) : Nat} -> {Nat.mod(x, 1n+mp) == Nat.mod(y, 1n+mp) : Nat}

x + c == y + c (mod m) gives x == y (mod m): add m - (c mod m) to both

def sub_plus source · line 66 · raw

@+m:Nat -> @+t:Nat -> @+h:{Nat.is_lt(t, m) == True{} : Bool} -> {Nat.add(Nat.sub(m, t), t) == m : Nat}

u + t == m for t < m, u = m - t

def inv_step_ok source · line 70 · raw

@+mp:Nat -> @+a:Nat -> @+r0:Nat -> @+s0:Nat -> @+rp:Nat -> @+s1:Nat -> @+h0:{Nat.mod(Nat.mul(a, s0), 1n+mp) == Nat.mod(r0, 1n+mp) : Nat} -> @+h1:{Nat.mod(Nat.mul(a, s1), 1n+mp) == Nat.mod(1n+rp, 1n+mp) : Nat} -> {Nat.mod(Nat.mul(a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.inv_step(1n+mp, Nat.div(r0, 1n+rp), s0, s1)), 1n+mp) == Nat.mod(Nat.mod(r0, 1n+rp), 1n+mp) : Nat}

one extended-Euclid step keeps the invariant

def inv_inv source · line 97 · raw

@fuel:Nat -> @+mp:Nat -> @+a:Nat -> @+r0:Nat -> @+s0:Nat -> @+r1:Nat -> @+s1:Nat -> @+h0:{Nat.mod(Nat.mul(a, s0), 1n+mp) == Nat.mod(r0, 1n+mp) : Nat} -> @+h1:{Nat.mod(Nat.mul(a, s1), 1n+mp) == Nat.mod(r1, 1n+mp) : Nat} -> {Nat.mod(Nat.mul(a, bc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.inv_go(fuel, 1n+mp, r0, s0, r1, s1))), 1n+mp) == Nat.mod(bg(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.inv_go(fuel, 1n+mp, r0, s0, r1, s1)), 1n+mp) : Nat}

def inv_r source · line 109 · raw

@fuel:Nat -> @+m:Nat -> @+r0:Nat -> @+s0:Nat -> @+r1:Nat -> @+s1:Nat -> {bg(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.inv_go(fuel, m, r0, s0, r1, s1)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.gcd_go(fuel, r0, r1) : Nat}

the remainders are Euclid's

def unwrap source · line 122 · raw

@r:Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.MathError, Nat> -> Nat

def is_done source · line 129 · raw

@r:Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.MathError, Nat> -> Bool

def mod_self source · line 136 · raw

@+mp:Nat -> {Nat.mod(1n+mp, 1n+mp) == 0n : Nat}

def inv_bz source · line 141 · raw

@+a:Nat -> @+mp:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.Bezout

the extended-Euclid state mod_inverse(a, m) ends in

def inv_bezout source · line 144 · raw

@+a:Nat -> @+mp:Nat -> {Nat.mod(Nat.mul(a, bc(inv_bz(a, mp))), 1n+mp) == Nat.mod(bg(inv_bz(a, mp)), 1n+mp) : Nat}

def inv_km source · line 151 · raw

@+a:Nat -> @+mp:Nat -> Nat

the final remainder divides m and a

def inv_ka source · line 154 · raw

@+a:Nat -> @+mp:Nat -> Nat

def inv_dvd_m source · line 157 · raw

@+a:Nat -> @+mp:Nat -> {1n+mp == Nat.mul(inv_km(a, mp), bg(inv_bz(a, mp))) : Nat}

def inv_dvd_a2 source · line 163 · raw

@+a:Nat -> @+mp:Nat -> @+g:Nat -> @+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/math/natural/gcd.Wit -> @p:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/math/natural/gcd.divides_both(1n+mp, Nat.mod(a, 1n+mp), g, w) -> {a == Nat.mul(Nat.add(Nat.mul(Nat.div(a, 1n+mp), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/math/natural/gcd.wl(w)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/math/natural/gcd.wr(w)), g) : Nat}

def inv_dvd_a source · line 167 · raw

@+a:Nat -> @+mp:Nat -> {a == Nat.mul(inv_ka(a, mp), bg(inv_bz(a, mp))) : Nat}

def done_bz source · line 174 · raw

@+mp:Nat -> @+a:Nat -> @+bz:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.Bezout -> @+hinv:{Nat.mod(Nat.mul(a, bc(bz)), 1n+mp) == Nat.mod(bg(bz), 1n+mp) : Nat} -> @+x:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.inv_fin(1n+mp, bz) == Done{x} : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.MathError, Nat>} -> Pair({Nat.mod(Nat.mul(a, x), 1n+mp) == Nat.mod(1n, 1n+mp) : Nat}, {Nat.is_lt(x, 1n+mp) == True{} : Bool})

def inverse_done source · line 186 · raw

@+a:Nat -> @+mp:Nat -> @+x:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.mod_inverse(a, 1n+mp) == Done{x} : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.MathError, Nat>} -> Pair({Nat.mod(Nat.mul(a, x), 1n+mp) == Nat.mod(1n, 1n+mp) : Nat}, {Nat.is_lt(x, 1n+mp) == True{} : Bool})

mod_inverse(a, m) == Done{x}: a x == 1 (mod m) and x < m (Mathlib ZMod.mul_inv_of_unit)

def fail_bz source · line 189 · raw

@+mp:Nat -> @+bz:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.Bezout -> @+km:Nat -> @+em:{1n+mp == Nat.mul(km, bg(bz)) : Nat} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.inv_fin(1n+mp, bz) == Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.NotInvertible{}} : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.MathError, Nat>} -> {Nat.is_le(2n, bg(bz)) == True{} : Bool}

def inverse_fail source · line 200 · raw

@+a:Nat -> @+mp:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.mod_inverse(a, 1n+mp) == Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.NotInvertible{}} : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.MathError, Nat>} -> Pair({Nat.is_le(2n, bg(inv_bz(a, mp))) == True{} : Bool}, Pair({a == Nat.mul(inv_ka(a, mp), bg(inv_bz(a, mp))) : Nat}, {1n+mp == Nat.mul(inv_km(a, mp), bg(inv_bz(a, mp))) : Nat}))

mod_inverse(a, m) == Fail{NotInvertible}: g >= 2 divides a and m, so a and m are not coprime (Mathlib Nat.Coprime, ZMod.unitOfCoprime)

def inverse_zero source · line 203 · raw

@+a:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.mod_inverse(a, 0n) == Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.ZeroDivision{}} : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.MathError, Nat>}