proofs/nat_division.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/nat_division.bend as Nat_division

Characterize Base.Nat.divmod by quotient/remainder and remainder bounds.

3 imports

import Base
import ./natural_addition.bend as Addition
import ./word_encoding.bend as WordEncoding

Laws

law bump_go provedsource · line 54 · raw

@+n:Nat -> @+m:Nat -> @+d:Nat -> @+r:Nat -> {Nat.divmod.go(n, m, 1n+d, r) == bump(Nat.divmod.go(n, m, d, r)) : Pair(Nat, Nat)}

law cycle provedsource · line 71 · raw

@+m:Nat -> @+tail:Nat -> @+d:Nat -> @+r:Nat -> {Nat.divmod.go(Nat.add(1n+m, tail), m, d, r) == Nat.divmod.go(tail, Nat.add(m, r), 1n+d, 0n) : Pair(Nat, Nat)}

law quotient_remainder provedsource · line 95 · raw

@+q:Nat -> @+r:Nat -> @+b:Nat -> @+positive:{Nat.is_lt(0n, b) == True{} : Bool} -> @+bounded:{Nat.is_lt(r, b) == True{} : Bool} -> {Nat.divmod(Nat.add(Nat.mul(q, b), r), b) == (q, r) : Pair(Nat, Nat)}

Definitions

def lt_zero source · line 6 · raw

@+n:Nat -> {Nat.is_lt(n, 0n) == False{} : Bool}

def lt_succ_le source · line 13 · raw

@+n:Nat -> @+m:Nat -> @h:{Nat.is_lt(n, 1n+m) == True{} : Bool} -> {Nat.is_le(n, m) == True{} : Bool}

def go_small source · line 25 · raw

@+n:Nat -> @+m:Nat -> @+d:Nat -> @+r:Nat -> @h:{Nat.is_le(n, m) == True{} : Bool} -> {Nat.divmod.go(n, m, d, r) == (d, Nat.add(n, r)) : Pair(Nat, Nat)}

def small source · line 37 · raw

@+r:Nat -> @+b:Nat -> @h:{Nat.is_lt(r, b) == True{} : Bool} -> {Nat.divmod(r, b) == (0n, r) : Pair(Nat, Nat)}

def bump source · line 46 · raw

@pair:Pair(Nat, Nat) -> Pair(Nat, Nat)

def bumped_quotient source · line 50 · raw

@pair:Pair(Nat, Nat) -> {Pair.fst(Nat, Nat, bump(pair)) == 1n+Pair.fst(Nat, Nat, pair) : Nat}

def add_divisor source · line 85 · raw

@+a:Nat -> @+b:Nat -> @h:{Nat.is_lt(0n, b) == True{} : Bool} -> {Nat.divmod(Nat.add(b, a), b) == bump(Nat.divmod(a, b)) : Pair(Nat, Nat)}

def unique source · line 114 · raw

@+a:Nat -> @+b:Nat -> @+q:Nat -> @+r:Nat -> @e:{a == Nat.add(Nat.mul(q, b), r) : Nat} -> @positive:{Nat.is_lt(0n, b) == True{} : Bool} -> @bounded:{Nat.is_lt(r, b) == True{} : Bool} -> {Nat.divmod(a, b) == (q, r) : Pair(Nat, Nat)}