proofs/u32_comparison.bend source
proofs/u32_comparison.bend on the hub · documented module
import Basedef digit(bit: Bool,n: Nat) -> Nat: match bit: case False{}: Nat.double(n) case True{}: 1n+Nat.double(n)law digits: for +a: Nat for +b: Nat for +ab: Bool for +bb: Bool {Nat.cmp(digit(ab,a),digit(bb,b)) == Word.cmp.fin(ab,bb,Nat.cmp(a,b)) : Cmp}def digits(a,b,ab,bb): match a b ab bb: case 0n 0n False{} False{}: {==} case 0n 0n False{} True{}: {==} case 0n 0n True{} False{}: {==} case 0n 0n True{} True{}: {==} case 0n 1n+bp False{} False{}: {==} case 0n 1n+bp False{} True{}: {==} case 0n 1n+bp True{} False{}: {==} case 0n 1n+bp True{} True{}: {==} case 1n+ap 0n False{} False{}: {==} case 1n+ap 0n False{} True{}: {==} case 1n+ap 0n True{} False{}: {==} case 1n+ap 0n True{} True{}: {==} case 1n+ap 1n+bp False{} False{}: digits(ap,bp,False{},False{}) case 1n+ap 1n+bp False{} True{}: digits(ap,bp,False{},True{}) case 1n+ap 1n+bp True{} False{}: digits(ap,bp,True{},False{}) case 1n+ap 1n+bp True{} True{}: digits(ap,bp,True{},True{})law word: for +n: Nat for +a: Word(n) for +b: Word(n) {Word.cmp(n,a,b) == Nat.cmp(Word.to_nat(n,a),Word.to_nat(n,b)) : Cmp}def word(n,a,b): match n: case 0n: {==} case 1n+ +p: match a b: case WCon{False{},+at} WCon{False{},+bt}: %Equal.sym(Cmp,Nat.cmp(digit(False{},Word.to_nat(p,at)),digit(False{},Word.to_nat(p,bt))),Word.cmp.fin(False{},False{}, Nat.cmp(Word.to_nat(p,at),Word.to_nat(p,bt))),digits(Word.to_nat(p,at),Word.to_nat(p,bt),False{},False{})) : {Word.cmp.fin(False{}, False{},Word.cmp(p,at,bt)) == _ : Cmp} %word(p,at,bt) : {Word.cmp.fin(False{},False{},Word.cmp(p,at,bt)) == Word.cmp.fin(False{},False{},_) : Cmp} {==} case WCon{False{},+at} WCon{True{},+bt}: %Equal.sym(Cmp,Nat.cmp(digit(False{},Word.to_nat(p,at)),digit(True{},Word.to_nat(p,bt))),Word.cmp.fin(False{},True{}, Nat.cmp(Word.to_nat(p,at),Word.to_nat(p,bt))),digits(Word.to_nat(p,at),Word.to_nat(p,bt),False{},True{})) : {Word.cmp.fin(False{}, True{},Word.cmp(p,at,bt)) == _ : Cmp} %word(p,at,bt) : {Word.cmp.fin(False{},True{},Word.cmp(p,at,bt)) == Word.cmp.fin(False{},True{},_) : Cmp} {==} case WCon{True{},+at} WCon{False{},+bt}: %Equal.sym(Cmp,Nat.cmp(digit(True{},Word.to_nat(p,at)),digit(False{},Word.to_nat(p,bt))),Word.cmp.fin(True{},False{}, Nat.cmp(Word.to_nat(p,at),Word.to_nat(p,bt))),digits(Word.to_nat(p,at),Word.to_nat(p,bt),True{},False{})) : {Word.cmp.fin(True{}, False{},Word.cmp(p,at,bt)) == _ : Cmp} %word(p,at,bt) : {Word.cmp.fin(True{},False{},Word.cmp(p,at,bt)) == Word.cmp.fin(True{},False{},_) : Cmp} {==} case WCon{True{},+at} WCon{True{},+bt}: %Equal.sym(Cmp,Nat.cmp(digit(True{},Word.to_nat(p,at)),digit(True{},Word.to_nat(p,bt))),Word.cmp.fin(True{},True{}, Nat.cmp(Word.to_nat(p,at),Word.to_nat(p,bt))),digits(Word.to_nat(p,at),Word.to_nat(p,bt),True{},True{})) : {Word.cmp.fin(True{}, True{},Word.cmp(p,at,bt)) == _ : Cmp} %word(p,at,bt) : {Word.cmp.fin(True{},True{},Word.cmp(p,at,bt)) == Word.cmp.fin(True{},True{},_) : Cmp} {==}law uint: for +a: U32 for +b: U32 {U32.cmp(a,b) == Nat.cmp(U32.to_nat(a),U32.to_nat(b)) : Cmp}def uint(a,b): match a b: case U32{x} U32{y}: word(32n,x,y)def lt(+a: U32,+b: U32) -> {U32.is_lt(a,b) == Nat.is_lt(U32.to_nat(a),U32.to_nat(b)) : Bool}: %uint(a,b) : {Cmp.is_lt(U32.cmp(a,b)) == Cmp.is_lt(_) : Bool} {==}def le(+a: U32,+b: U32) -> {U32.is_le(a,b) == Nat.is_le(U32.to_nat(a),U32.to_nat(b)) : Bool}: %uint(a,b) : {Cmp.is_le(U32.cmp(a,b)) == Cmp.is_le(_) : Bool} {==}def eq(+a: U32,+b: U32) -> {U32.is_eq(a,b) == Nat.is_eq(U32.to_nat(a),U32.to_nat(b)) : Bool}: %uint(a,b) : {Cmp.is_eq(U32.cmp(a,b)) == Cmp.is_eq(_) : Bool} {==}def ge(+a: U32,+b: U32) -> {U32.is_ge(a,b) == Nat.is_ge(U32.to_nat(a),U32.to_nat(b)) : Bool}: %uint(a,b) : {Cmp.is_ge(U32.cmp(a,b)) == Cmp.is_ge(_) : Bool} {==}