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	# Nat calls of the laws above: --verdict takes a ~ constant's model from a call of its law (PLAN F38).
88	def 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	
99	def 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	
102	def 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	
105	def 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	
108	def 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	
111	def 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.
117	law 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	
125	def 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).
129	def 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)