def injective

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/u32.bend:45

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

45def injective(+a: U32, +b: U32, +e: {U32.to_nat(a) == U32.to_nat(b) : Nat}) -> {a == b : U32}:
46  match a b:
47    case U32{+x} U32{+y}:
48      Equal.cong(Word(32n), U32, w => U32{w}, x, y,
49        Equal.trans(Word(32n), x, S.from_nat(32n, S.unsigned(32n, x)), y,
50          Equal.sym(Word(32n), S.from_nat(32n, S.unsigned(32n, x)), x, word_from_unsigned(x)),
51          Equal.trans(Word(32n), S.from_nat(32n, S.unsigned(32n, x)), S.from_nat(32n, S.unsigned(32n, y)), y,
52            Equal.cong(Nat, Word(32n), v => S.from_nat(32n, v), S.unsigned(32n, x), S.unsigned(32n, y),
53              Equal.trans(Nat, S.unsigned(32n, x), U32.to_nat(U32{x}), S.unsigned(32n, y),
54                Equal.sym(Nat, U32.to_nat(U32{x}), S.unsigned(32n, x), to_nat_word(x)),
55                Equal.trans(Nat, U32.to_nat(U32{x}), U32.to_nat(U32{y}), S.unsigned(32n, y), e, to_nat_word(y)))),
56            word_from_unsigned(y))))