1	# bend-mathlib/order.bend: abstract preorder/total-order facts over a Bool comparator ~le.
2	import Base
3	import ./nat.bend as MNat
4	
5	# A chain of three comparisons composes.
6	law 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	
19	def 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.
23	law 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	
38	def 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.
42	law 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	
52	def 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.
56	law 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	
64	def le_total_true(A, le, le_total, a, b):
65	  le_total(a, b)
66	
67	def 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.
75	law 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	
84	def 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.
90	law 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	
98	def 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))