def u32_refines

bend-collections-laws-math@1.0.0.0 · proofs/lib/lemmas/proofs/word_comparison.bend:44

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

44def u32_refines(a: U32, b: U32) -> {U32.cmp(a, b) == Nat.cmp(U32.to_nat(a), U32.to_nat(b)) : Cmp}:
45  match a b:
46    case U32{+x} U32{+y}:
47      %Equal.sym(Nat, Word.to_nat(32n, x), S.unsigned(32n, x), N.primitive_word_interpretation(32n, x)) : {U32.cmp(U32{x}, U32{y}) == Nat.cmp(_, Word.to_nat(32n, y)) : Cmp}
48      %Equal.sym(Nat, Word.to_nat(32n, y), S.unsigned(32n, y), N.primitive_word_interpretation(32n, y)) : {U32.cmp(U32{x}, U32{y}) == Nat.cmp(S.unsigned(32n, x), _) : Cmp}
49      refines(32n, x, y)