U64div.neg_quot: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend as U64div
Lines 293-317 of bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend&start_line=293&end_line=317

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/src/wide.bend as W
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/division_quotient.bend as DQ
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend as AR
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/modular_negation.bend as MN
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/negation_magnitude.bend as NM
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_value.bend as WV

# negate, divide the magnitude, negate back: the specification's quotient of
# a negative word, at every width
def neg_quot(+n: Nat, +w: Word(n), +d: U32, +hnz: {W.is_zero(n, w) == False{} : Bool}) -> {Word.inc(n, Word.not(n, S.unsigned_quotient(n, Word.inc(n, Word.not(n, w)), d))) == S.negative_quotient(n, w, d) : Word(n)}:
  match n w:
    case 0n WNil{}:
      {==}
    case 1n+p WCon{+bit, +tail}:
      +m = {1n+p : Nat}
      +ww = {WCon{bit, tail} : Word(1n+p)}
      +x = Word.inc(m, Word.not(m, ww))
      +dn = U32.to_nat(d)
      +sc = S.scale_binary(m, 1n)
      +q = Nat.div(S.unsigned(m, x), dn)
      +hx = NM.magnitude(m, ww, hnz)
      +hq = N.le_lt_trans(q, S.unsigned(m, x), sc, AR.div_le(S.unsigned(m, x), dn), WD.lt1(m, 1n, {==}, S.unsigned(m, x), WD.wb(m, 1n, {==}, x)))
      +hqv = WV.from_nat_value(m, q, L.subst(Nat, z => {Nat.is_lt(q, z) == True{} : Bool}, sc, Nat.pow(2n, m), NM.scale_power(m), hq))
      +e1 = Equal.cong(Word(m), Word(m), z => Word.inc(m, Word.not(m, z)), S.unsigned_quotient(m, x, d), S.from_nat(m, q), DQ.specification_equation(m, x, d))
      +e2 = MN.negation_refines(m, S.from_nat(m, q))
      +e3 = Equal.cong(Nat, Word(m), z => S.from_nat(m, Nat.sub(sc, z)), S.unsigned(m, S.from_nat(m, q)), q, hqv)
      +e4 = Equal.cong(Nat, Word(m), z => S.from_nat(m, Nat.sub(sc, Nat.div(z, dn))), S.unsigned(m, x), Nat.sub(sc, S.unsigned(m, ww)), hx)
      +e5 = Equal.cong(Nat, Word(m), z => S.from_nat(m, Nat.sub(z, Nat.div(Nat.sub(z, S.unsigned(m, ww)), dn))), sc, Nat.pow(2n, m), NM.scale_power(m))
      Equal.trans(Word(m), Word.inc(m, Word.not(m, S.unsigned_quotient(m, x, d))), Word.inc(m, Word.not(m, S.from_nat(m, q))), S.negative_quotient(m, ww, d), e1,
        Equal.trans(Word(m), Word.inc(m, Word.not(m, S.from_nat(m, q))), S.from_nat(m, Nat.sub(sc, S.unsigned(m, S.from_nat(m, q)))), S.negative_quotient(m, ww, d), e2,
          Equal.trans(Word(m), S.from_nat(m, Nat.sub(sc, S.unsigned(m, S.from_nat(m, q)))), S.from_nat(m, Nat.sub(sc, q)), S.negative_quotient(m, ww, d), e3,
            Equal.trans(Word(m), S.from_nat(m, Nat.sub(sc, q)), S.from_nat(m, Nat.sub(sc, Nat.div(Nat.sub(sc, S.unsigned(m, ww)), dn))), S.negative_quotient(m, ww, d), e4, e5))))

Uses (31):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.pow
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Nil
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.inc
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.not
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend&name=div_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/division_quotient.bend&name=specification_equation
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/modular_negation.bend&name=negation_refines
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/negation_magnitude.bend&name=magnitude
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/negation_magnitude.bend&name=scale_power
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_value.bend&name=from_nat_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=from_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=negative_quotient
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=scale_binary
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=unsigned
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=unsigned_quotient
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/src/wide.bend&name=is_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_lt_trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=lt1
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=wb