def sif_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64mont.bend:78

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natlight.bend as AQ

78# sub_if: r < 2 m gives r mod m
79def sif_c(+bp: Nat, +m: WU.U64, +r: WU.U64, +hM: {SW.value(m) == 1n+bp : Nat}, +hr: {Nat.is_lt(SW.value(r), Nat.add(1n+bp, 1n+bp)) == True{} : Bool}, +c: Bool, +hc: {X.le(m, r) == c : Bool}) -> {SW.value(X.sub_if(r, m, c)) == Nat.mod(SW.value(r), 1n+bp) : Nat}:
80  match c:
81    case True{}:
82      +hle0 = Equal.trans(Bool, Nat.is_le(SW.value(m), SW.value(r)), X.le(m, r), True{}, Equal.sym(Bool, X.le(m, r), Nat.is_le(SW.value(m), SW.value(r)), WA.le_value(m, r)), hc)
83      +hle = L.subst(Nat, z => {Nat.is_le(z, SW.value(r)) == True{} : Bool}, SW.value(m), 1n+bp, hM, hle0)
84      +es = Equal.trans(Nat, SW.value(X.sub(r, m)), Nat.sub(SW.value(r), SW.value(m)), Nat.sub(SW.value(r), 1n+bp), WA.sub_value(r, m, hle0), Equal.cong(Nat, Nat, z => Nat.sub(SW.value(r), z), SW.value(m), 1n+bp, hM))
85      +x = Nat.sub(SW.value(r), 1n+bp)
86      +hx = N.sub_lt(SW.value(r), 1n+bp, 1n+bp, hle, hr)
87      +er = Equal.trans(Nat, Nat.add(Nat.mul(1n, 1n+bp), x), Nat.add(1n+bp, x), SW.value(r), Equal.cong(Nat, Nat, z => Nat.add(z, x), Nat.mul(1n, 1n+bp), 1n+bp, AQ.mul1(1n+bp)), N.sub_add(SW.value(r), 1n+bp, hle))
88      +em = Equal.trans(Nat, Nat.mod(SW.value(r), 1n+bp), Nat.mod(Nat.add(Nat.mul(1n, 1n+bp), x), 1n+bp), x, Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), SW.value(r), Nat.add(Nat.mul(1n, 1n+bp), x), Equal.sym(Nat, Nat.add(Nat.mul(1n, 1n+bp), x), SW.value(r), er)), NR.mod_of(1n, bp, x, hx))
89      Equal.trans(Nat, SW.value(X.sub(r, m)), x, Nat.mod(SW.value(r), 1n+bp), es, Equal.sym(Nat, Nat.mod(SW.value(r), 1n+bp), x, em))
90    case False{}:
91      +hle0 = Equal.trans(Bool, Nat.is_le(SW.value(m), SW.value(r)), X.le(m, r), False{}, Equal.sym(Bool, X.le(m, r), Nat.is_le(SW.value(m), SW.value(r)), WA.le_value(m, r)), hc)
92      +hl = L.subst(Nat, z => {Nat.is_lt(SW.value(r), z) == True{} : Bool}, SW.value(m), 1n+bp, hM, N.not_le_lt(SW.value(m), SW.value(r), hle0))
93      Equal.sym(Nat, Nat.mod(SW.value(r), 1n+bp), SW.value(r), NR.mod_of(0n, bp, SW.value(r), hl))