def eq_c

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/u32laws.bend:83

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/u32.bend as U
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend as A
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L

83# U32 equality is equality of the values
84def eq_c(+x: U32, +y: U32, +c: Bool, +hc: {U32.is_eq(x, y) == c : Bool}, +d: Bool, +hd: {Nat.is_eq(v(x), v(y)) == d : Bool}) -> {c == d : Bool}:
85  match c d:
86    case True{} True{}:
87      {==}
88    case False{} False{}:
89      {==}
90    case True{} False{}:
91      +e = A.eq_of(x, y, hc)
92      +hd2 = L.subst(U32, z => {Nat.is_eq(v(x), v(z)) == False{} : Bool}, y, x, Equal.sym(U32, x, y, e), hd)
93      Empty.absurd({True{} == False{} : Bool}, true_ne_false(Equal.trans(Bool, True{}, Nat.is_eq(v(x), v(x)), False{}, Equal.sym(Bool, Nat.is_eq(v(x), v(x)), True{}, N.is_eq_refl(v(x))), hd2)))
94    case False{} True{}:
95      +e = U.injective(x, y, N.eq_from_is_eq(v(x), v(y), hd))
96      +hc2 = L.subst(U32, z => {U32.is_eq(x, z) == False{} : Bool}, y, x, Equal.sym(U32, x, y, e), hc)
97      Empty.absurd({False{} == True{} : Bool}, true_ne_false(Equal.trans(Bool, True{}, U32.is_eq(x, x), False{}, Equal.sym(Bool, U32.is_eq(x, x), True{}, A.eq_refl(x)), hc2)))