spec/lib/order.bend

bend-collections-laws-containers@1.0.0.0 · 20 lines · 0 definitions

1import Base
2
3# Total-order laws for a static comparator ~cmp : A -> A -> Cmp, the
4# precondition every ordered container states its contract under.
5#   flip:    cmp(b, a) = flip(cmp(a, b))
6#   antisym: cmp(a, b) = EQ  implies  a == b
7#   trans:   a <= b and b <= c  implies  a <= c     (<= is cmp in {LT, EQ})
8# The lemmas and the U32 / String instances are in proofs/lib/order.bend.
9
10def flipc(c: Cmp) -> Cmp:
11  match c:
12    case LT{}:
13      GT{}
14    case EQ{}:
15      EQ{}
16    case GT{}:
17      LT{}
18
19def Order(~A: Data, ~cmp: A -> A -> Cmp) -> Type:
20  (@+a: A -> @+b: A -> {cmp(b, a) == flipc(cmp(a, b)) : Cmp}) & ((@+a: A -> @+b: A -> @+e: {cmp(a, b) == EQ{} : Cmp} -> {a == b : A}) & (@+a: A -> @+b: A -> @+c: A -> @+ab: {Cmp.is_le(cmp(a, b)) == True{} : Bool} -> @+bc: {Cmp.is_le(cmp(b, c)) == True{} : Bool} -> {Cmp.is_le(cmp(a, c)) == True{} : Bool}))