~/bend-docscommunity

order.bend checks

raw source on the hub · import bend-mathlib@0.7.0.0/order.bend as Order

bend-mathlib/order.bend: abstract preorder/total-order facts over a Bool comparator ~le.

2 imports
import Base
import ./nat.bend as MNat

Laws

law le_trans3 provedsource · line 6 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @-le_trans:(@x:A -> @y:A -> @z:A -> @_:{le(x, y) == True{} : Bool} -> @_:{le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}) -> @+a:A -> @+b:A -> @+c:A -> @+d:A -> @ab:{le(a, b) == True{} : Bool} -> @bc:{le(b, c) == True{} : Bool} -> @cd:{le(c, d) == True{} : Bool} -> {le(a, d) == True{} : Bool}

A chain of three comparisons composes.

law le_trans4 provedsource · line 23 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @-le_trans:(@x:A -> @y:A -> @z:A -> @_:{le(x, y) == True{} : Bool} -> @_:{le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}) -> @+a:A -> @+b:A -> @+c:A -> @+d:A -> @+e:A -> @ab:{le(a, b) == True{} : Bool} -> @bc:{le(b, c) == True{} : Bool} -> @cd:{le(c, d) == True{} : Bool} -> @de:{le(d, e) == True{} : Bool} -> {le(a, e) == True{} : Bool}

A chain of four comparisons composes.

law le_antisymm_eq provedsource · line 42 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @-le_antisymm:(@x:A -> @y:A -> @_:{le(x, y) == True{} : Bool} -> @_:{le(y, x) == True{} : Bool} -> {x == y : A}) -> @+a:A -> @+b:A -> @ab:{le(a, b) == True{} : Bool} -> @ba:{le(b, a) == True{} : Bool} -> {a == b : A}

Antisymmetry gives equality.

law le_total_true provedsource · line 56 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @-le_total:(@x:A -> @y:A -> {Bool.or(le(x, y), le(y, x)) == True{} : Bool}) -> @+a:A -> @+b:A -> {Bool.or(le(a, b), le(b, a)) == True{} : Bool}

Totality as a Bool disjunction.

law le_total_of_not_le provedsource · line 75 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @-le_total:(@x:A -> @y:A -> {Bool.or(le(x, y), le(y, x)) == True{} : Bool}) -> @+a:A -> @+b:A -> @h:{le(a, b) == False{} : Bool} -> {le(b, a) == True{} : Bool}

The other side of a total order holds when one side fails.

law le_total_true_sym provedsource · line 90 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @-le_total:(@x:A -> @y:A -> {Bool.or(le(x, y), le(y, x)) == True{} : Bool}) -> @+a:A -> @+b:A -> {True{} == Bool.or(le(a, b), le(b, a)) : Bool}

Totality as a Bool disjunction, reversed to rewrite toward the simple side.

Definitions

def internal_or_of_false_right source · line 67 · raw

@a:Bool -> @b:Bool -> @h:{Bool.or(a, b) == True{} : Bool} -> @ha:{a == False{} : Bool} -> {b == True{} : Bool}