def q_one

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/eqf.bend:34

import Base
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/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend as G

34# w mod p == 0 gives A == B: the quotient q has w == q p, and q is 1
35def q_one(+pp: Nat, +A: Nat, +B: Nat, +q: Nat, +hA: {Nat.is_lt(A, 1n+pp) == True{} : Bool}, +hB: {Nat.is_lt(B, 1n+pp) == True{} : Bool}, +hw: {Nat.add(Nat.mul(q, 1n+pp), B) == Nat.add(A, 1n+pp) : Nat}) -> {A == B : Nat}:
36  match q:
37    case 0n:
38      +P = {1n+pp : Nat}
39      +c = L.subst(Nat, z => {Nat.is_le(P, z) == True{} : Bool}, Nat.add(A, P), B, Equal.sym(Nat, B, Nat.add(A, P), hw), G.le_add_l(A, P))
40      Empty.absurd({A == B : Nat}, L.true_not_false(Nat.is_lt(B, P), hB, N.le_not_lt(B, P, c)))
41    case 1n:
42      +P = {1n+pp : Nat}
43      +h2 = Equal.trans(Nat, Nat.add(P, B), Nat.add(Nat.mul(1n, P), B), Nat.add(A, P), Equal.cong(Nat, Nat, z => Nat.add(z, B), P, Nat.mul(1n, P), Equal.sym(Nat, Nat.mul(1n, P), P, NA.add_zero(P))), hw)
44      NR.add_cancel(P, A, B, Equal.sym(Nat, Nat.add(P, B), Nat.add(P, A), Equal.trans(Nat, Nat.add(P, B), Nat.add(A, P), Nat.add(P, A), h2, NA.add_comm(A, P))))
45    case 2n+ +r:
46      +P = {1n+pp : Nat}
47      +big = Nat.add(P, Nat.add(P, Nat.add(Nat.mul(r, P), B)))
48      +h2 = Equal.trans(Nat, big, Nat.add(Nat.mul(2n+r, P), B), Nat.add(A, P), Equal.sym(Nat, Nat.add(Nat.mul(2n+r, P), B), big, Equal.trans(Nat, Nat.add(Nat.add(P, Nat.add(P, Nat.mul(r, P))), B), Nat.add(P, Nat.add(Nat.add(P, Nat.mul(r, P)), B)), big, NA.add_assoc(P, Nat.add(P, Nat.mul(r, P)), B), Equal.cong(Nat, Nat, z => Nat.add(P, z), Nat.add(Nat.add(P, Nat.mul(r, P)), B), Nat.add(P, Nat.add(Nat.mul(r, P), B)), NA.add_assoc(P, Nat.mul(r, P), B)))), hw)
49      +l1 = N.le_add_left(P, Nat.add(P, Nat.add(Nat.mul(r, P), B)), P, N.le_add_right(P, Nat.add(Nat.mul(r, P), B)))
50      +l2 = L.subst(Nat, z => {Nat.is_le(Nat.add(P, P), z) == True{} : Bool}, big, Nat.add(A, P), h2, l1)
51      +l3 = N.lt_le_trans(Nat.add(A, P), Nat.add(P, P), Nat.add(A, P), N.lt_add_r2(A, P, P, hA), l2)
52      Empty.absurd({A == B : Nat}, L.true_not_false(Nat.is_lt(Nat.add(A, P), Nat.add(A, P)), l3, N.lt_irrefl(Nat.add(A, P))))