order.bend
bend-mathlib@0.5.0.0 · 99 lines · 0 definitions
1# bend-mathlib/order.bend: abstract preorder/total-order facts over a Bool comparator ~le.
2import Base
3import bend-mathlib@0.5.0.0/nat.bend as MNat
4
5# A chain of three comparisons composes.
6law le_trans3:
7 for ~A: Data
8 for ~le: A -> A -> Bool
9 for ~le_trans: @x: A -> @y: A -> @z: A -> {le(x, y) == True{} : Bool} -> {le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}
10 for +a: A
11 for +b: A
12 for +c: A
13 for +d: A
14 for ab: {le(a, b) == True{} : Bool}
15 for bc: {le(b, c) == True{} : Bool}
16 for cd: {le(c, d) == True{} : Bool}
17 {le(a, d) == True{} : Bool}
18
19def le_trans3(A, le, le_trans, a, b, c, d, ab, bc, cd):
20 le_trans(a, c, d, le_trans(a, b, c, ab, bc), cd)
21
22# A chain of four comparisons composes.
23law le_trans4:
24 for ~A: Data
25 for ~le: A -> A -> Bool
26 for ~le_trans: @x: A -> @y: A -> @z: A -> {le(x, y) == True{} : Bool} -> {le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}
27 for +a: A
28 for +b: A
29 for +c: A
30 for +d: A
31 for +e: A
32 for ab: {le(a, b) == True{} : Bool}
33 for bc: {le(b, c) == True{} : Bool}
34 for cd: {le(c, d) == True{} : Bool}
35 for de: {le(d, e) == True{} : Bool}
36 {le(a, e) == True{} : Bool}
37
38def le_trans4(A, le, le_trans, a, b, c, d, e, ab, bc, cd, de):
39 le_trans(a, d, e, le_trans3(A, le, le_trans, a, b, c, d, ab, bc, cd), de)
40
41# Antisymmetry gives equality.
42law le_antisymm_eq:
43 for ~A: Data
44 for ~le: A -> A -> Bool
45 for ~le_antisymm: @x: A -> @y: A -> {le(x, y) == True{} : Bool} -> {le(y, x) == True{} : Bool} -> {x == y : A}
46 for +a: A
47 for +b: A
48 for ab: {le(a, b) == True{} : Bool}
49 for ba: {le(b, a) == True{} : Bool}
50 {a == b : A}
51
52def le_antisymm_eq(A, le, le_antisymm, a, b, ab, ba):
53 le_antisymm(a, b, ab, ba)
54
55# Totality as a Bool disjunction.
56law le_total_true:
57 for ~A: Data
58 for ~le: A -> A -> Bool
59 for ~le_total: @x: A -> @y: A -> {Bool.or(le(x, y), le(y, x)) == True{} : Bool}
60 for +a: A
61 for +b: A
62 {Bool.or(le(a, b), le(b, a)) == True{} : Bool}
63
64def le_total_true(A, le, le_total, a, b):
65 le_total(a, b)
66
67def internal_or_of_false_right(a: Bool, b: Bool, h: {Bool.or(a, b) == True{} : Bool}, ha: {a == False{} : Bool}) -> {b == True{} : Bool}:
68 match a:
69 case False{}:
70 h
71 case True{}:
72 Empty.absurd({b == True{} : Bool}, MNat.internal_false_ne_true(Equal.sym(Bool, True{}, False{}, ha)))
73
74# The other side of a total order holds when one side fails.
75law le_total_of_not_le:
76 for ~A: Data
77 for ~le: A -> A -> Bool
78 for ~le_total: @x: A -> @y: A -> {Bool.or(le(x, y), le(y, x)) == True{} : Bool}
79 for +a: A
80 for +b: A
81 for h: {le(a, b) == False{} : Bool}
82 {le(b, a) == True{} : Bool}
83
84def le_total_of_not_le(A, le, le_total, a, b, h):
85 internal_or_of_false_right(le(a, b), le(b, a), le_total(a, b), h)
86
87# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
88
89# Totality as a Bool disjunction, reversed to rewrite toward the simple side.
90law le_total_true_sym:
91 for ~A: Data
92 for ~le: A -> A -> Bool
93 for ~le_total: @x: A -> @y: A -> {Bool.or(le(x, y), le(y, x)) == True{} : Bool}
94 for +a: A
95 for +b: A
96 {True{} == Bool.or(le(a, b), le(b, a)) : Bool}
97
98def le_total_true_sym(A, le, le_total, a, b):
99 Equal.sym(Bool, Bool.or(le(a, b), le(b, a)), True{}, le_total_true(~A, ~le, ~le_total, a, b))