proofs/math/natural/gcd.bend checks

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

6 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

Types

type Wit source · line 37 · raw

Data

the quotients a / g and b / g, by Euclid's recursion

W
```
@l:Nat -> @r:Nat -> Wit
```

Definitions

def dvd_mod source · line 16 · raw

@+bp:Nat -> @+a:Nat -> @+d:Nat -> @+ka:Nat -> @+kn:Nat -> @+ea:{a == Nat.mul(ka, d) : Nat} -> @+en:{1n+bp == Nat.mul(kn, d) : Nat} -> {Nat.mod(a, 1n+bp) == Nat.mul(Nat.sub(ka, Nat.mul(Nat.div(a, 1n+bp), kn)), d) : Nat}

d | a and d | n give d | a mod n: a mod n == (ka - q kn) d, q = a / n

def dvd_of_mod source · line 26 · raw

@+bp:Nat -> @+a:Nat -> @+d:Nat -> @+kn:Nat -> @+kr:Nat -> @+en:{1n+bp == Nat.mul(kn, d) : Nat} -> @+er:{Nat.mod(a, 1n+bp) == Nat.mul(kr, d) : Nat} -> {a == Nat.mul(Nat.add(Nat.mul(Nat.div(a, 1n+bp), kn), kr), d) : Nat}

d | n and d | a mod n give d | a: a == (q kn + kr) d

def wl source · line 40 · raw

@w:Wit -> Nat

def wr source · line 45 · raw

@w:Wit -> Nat

def wstep source · line 51 · raw

@+q:Nat -> @w:Wit -> Wit

from n == l g and a mod n == r g: a == (q l + r) g and n == l g

def ws source · line 56 · raw

@fuel:Nat -> @+a:Nat -> @+b:Nat -> Wit

def divides_both source · line 65 · raw

@+a:Nat -> @+b:Nat -> @+g:Nat -> @w:Wit -> Type

def step_both source · line 68 · raw

@+bp:Nat -> @+a:Nat -> @+g:Nat -> @w:Wit -> @ih:divides_both(1n+bp, Nat.mod(a, 1n+bp), g, w) -> divides_both(a, 1n+bp, g, wstep(Nat.div(a, 1n+bp), w))

def gcd_both source · line 75 · raw

@fuel:Nat -> @+a:Nat -> @+b:Nat -> @+hb:{Nat.is_le(b, fuel) == True{} : Bool} -> divides_both(a, b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.gcd_go(fuel, a, b), ws(fuel, a, b))

def dw source · line 89 · raw

@fuel:Nat -> @+a:Nat -> @+b:Nat -> @+ka:Nat -> @+kb:Nat -> Nat

the quotient g / d, for d | a (a == ka d) and d | b (b == kb d)

def gcd_greatest source · line 98 · raw

@fuel:Nat -> @+a:Nat -> @+b:Nat -> @+hb:{Nat.is_le(b, fuel) == True{} : Bool} -> @+d:Nat -> @+ka:Nat -> @+kb:Nat -> @+ea:{a == Nat.mul(ka, d) : Nat} -> @+eb:{b == Nat.mul(kb, d) : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.gcd_go(fuel, a, b) == Nat.mul(dw(fuel, a, b, ka, kb), d) : Nat}

def both_l source · line 111 · raw

@+a:Nat -> @+b:Nat -> @+g:Nat -> @w:Wit -> @p:divides_both(a, b, g, w) -> {a == Nat.mul(wl(w), g) : Nat}

def both_r source · line 115 · raw

@+a:Nat -> @+b:Nat -> @+g:Nat -> @w:Wit -> @p:divides_both(a, b, g, w) -> {b == Nat.mul(wr(w), g) : Nat}

def gcd_dvd_left source · line 119 · raw

@+a:Nat -> @+b:Nat -> {a == Nat.mul(wl(ws(b, a, b)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.gcd(a, b)) : Nat}

def gcd_dvd_right source · line 122 · raw

@+a:Nat -> @+b:Nat -> {b == Nat.mul(wr(ws(b, a, b)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.gcd(a, b)) : Nat}

def dvd_gcd source · line 125 · raw

@+a:Nat -> @+b:Nat -> @+d:Nat -> @+ka:Nat -> @+kb:Nat -> @+ea:{a == Nat.mul(ka, d) : Nat} -> @+eb:{b == Nat.mul(kb, d) : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.gcd(a, b) == Nat.mul(dw(b, a, b, ka, kb), d) : Nat}