proofs/math/typed/f64sqw.bend
bend-collections-laws-math@1.0.0.0 · 27 lines · 3 definitions
1import Base
2import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
3import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC
4import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend as FC
5
6
7
8def ltz(+l: Nat) -> {Nat.is_lt(0n, l) == Bool.not(Nat.is_eq(l, 0n)) : Bool}:
9 match l:
10 case 0n:
11 {==}
12 case 1n+ +lp:
13 {==}
14
15def eq_comm(+a: Nat, +b: Nat) -> {Nat.is_eq(a, b) == Nat.is_eq(b, a) : Bool}:
16 Equal.trans(Bool, Nat.is_eq(a, b), Cmp.is_eq(SF.flip(Nat.cmp(a, b))), Nat.is_eq(b, a), FC.eqflip(Nat.cmp(a, b)), Equal.cong(Cmp, Bool, c => Cmp.is_eq(c), SF.flip(Nat.cmp(a, b)), Nat.cmp(b, a), NC.cmp_flip(a, b)))
17
18def and_comm(+a: Bool, +b: Bool) -> {Bool.and(a, b) == Bool.and(b, a) : Bool}:
19 match a b:
20 case True{} True{}:
21 {==}
22 case True{} False{}:
23 {==}
24 case False{} True{}:
25 {==}
26 case False{} False{}:
27 {==}