order.bend
bend-mathlib@0.8.0.0 · 130 lines · 0 definitions
1# bend-mathlib/order.bend: abstract preorder/total-order facts over a Bool comparator ~le.
2import Base
3import bend-mathlib@0.8.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# Nat calls of the laws above: --verdict takes a ~ constant's model from a call of its law (PLAN F38).
88def internal_nat_le_total(a: Nat, b: Nat) -> {Bool.or(Nat.is_le(a, b), Nat.is_le(b, a)) == True{} : Bool}:
89 match a b:
90 case 0n 0n:
91 {==}
92 case 0n 1n+q:
93 {==}
94 case 1n+p 0n:
95 {==}
96 case 1n+p 1n+q:
97 internal_nat_le_total(p, q)
98
99def internal_nat_le_trans3(+a: Nat, +b: Nat, +c: Nat, +d: Nat, ab: MNat.le(a, b), bc: MNat.le(b, c), cd: MNat.le(c, d)) -> MNat.le(a, d):
100 le_trans3(~Nat, ~Nat.is_le, ~MNat.le_trans, a, b, c, d, ab, bc, cd)
101
102def internal_nat_le_trans4(+a: Nat, +b: Nat, +c: Nat, +d: Nat, +e: Nat, ab: MNat.le(a, b), bc: MNat.le(b, c), cd: MNat.le(c, d), de: MNat.le(d, e)) -> MNat.le(a, e):
103 le_trans4(~Nat, ~Nat.is_le, ~MNat.le_trans, a, b, c, d, e, ab, bc, cd, de)
104
105def internal_nat_le_antisymm_eq(+a: Nat, +b: Nat, ab: MNat.le(a, b), ba: MNat.le(b, a)) -> {a == b : Nat}:
106 le_antisymm_eq(~Nat, ~Nat.is_le, ~MNat.le_antisymm, a, b, ab, ba)
107
108def internal_nat_le_total_true(+a: Nat, +b: Nat) -> {Bool.or(Nat.is_le(a, b), Nat.is_le(b, a)) == True{} : Bool}:
109 le_total_true(~Nat, ~Nat.is_le, ~internal_nat_le_total, a, b)
110
111def internal_nat_le_total_of_not_le(+a: Nat, +b: Nat, h: {Nat.is_le(a, b) == False{} : Bool}) -> MNat.le(b, a):
112 le_total_of_not_le(~Nat, ~Nat.is_le, ~internal_nat_le_total, a, b, h)
113
114# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
115
116# Totality as a Bool disjunction, reversed to rewrite toward the simple side.
117law le_total_true_sym:
118 for ~A: Data
119 for ~le: A -> A -> Bool
120 for ~le_total: @x: A -> @y: A -> {Bool.or(le(x, y), le(y, x)) == True{} : Bool}
121 for +a: A
122 for +b: A
123 {True{} == Bool.or(le(a, b), le(b, a)) : Bool}
124
125def le_total_true_sym(A, le, le_total, a, b):
126 Equal.sym(Bool, Bool.or(le(a, b), le(b, a)), True{}, le_total_true(~A, ~le, ~le_total, a, b))
127
128# Calls of the twins, as the calls above the generated section make of their laws (PLAN F38).
129def internal_nat_le_total_true_sym(+a: Nat, +b: Nat) -> {True{} == Bool.or(Nat.is_le(a, b), Nat.is_le(b, a)) : Bool}:
130 le_total_true_sym(~Nat, ~Nat.is_le, ~internal_nat_le_total, a, b)