1	import Base
2	import ./class.bend as C
3	
4	# nat.bend: Nat arithmetic and order laws.
5	#
6	#   import ./nat.bend as Nat
7	#   Nat.ord(), Nat.add_sg()      # instances for class.bend
8	#
9	# Equations put the side a caller rewrites away on the right: `%e : P`
10	# replaces e's right side in the goal with its left side.
11	
12	# plain binders, so it fits C.Semigroup's assoc field
13	law add_assoc:
14	  for a: Nat
15	  for b: Nat
16	  for c: Nat
17	  {Nat.add(a, Nat.add(b, c)) == Nat.add(Nat.add(a, b), c) : Nat}
18	
19	def add_assoc(a, b, c):
20	  match a:
21	    case 0n:
22	      {==}
23	    case 1n+p:
24	      %add_assoc(p, b, c) : {1n+Nat.add(p, Nat.add(b, c)) == 1n+_ : Nat}
25	      {==}
26	
27	# a <= b, as a type: Unit when it holds, Empty when it does not.
28	def LE(a: Nat, b: Nat) -> Data:
29	  match a b:
30	    case 0n y:
31	      Unit
32	    case 1n+x 0n:
33	      Empty
34	    case 1n+x 1n+y:
35	      LE(x, y)
36	
37	# a < b. LT(i, 0n) computes to Empty.
38	def LT(a: Nat, b: Nat) -> Data:
39	  LE(1n+a, b)
40	
41	law le_refl:
42	  for a: Nat
43	  LE(a, a)
44	
45	def le_refl(a):
46	  match a:
47	    case 0n:
48	      Unit{}
49	    case 1n+p:
50	      le_refl(p)
51	
52	law le_step:
53	  for a: Nat
54	  LE(a, 1n+a)
55	
56	def le_step(a):
57	  match a:
58	    case 0n:
59	      Unit{}
60	    case 1n+p:
61	      le_step(p)
62	
63	law le_trans:
64	  for a: Nat
65	  for b: Nat
66	  for c: Nat
67	  for ab: LE(a, b)
68	  for bc: LE(b, c)
69	  LE(a, c)
70	
71	def le_trans(a, b, c, ab, bc):
72	  match a b c:
73	    case 0n b c:
74	      Unit{}
75	    case 1n+x 0n c:
76	      match ab:
77	    case 1n+x 1n+y 0n:
78	      match bc:
79	    case 1n+x 1n+y 1n+z:
80	      le_trans(x, y, z, ab, bc)
81	
82	# a - k <= a (Nat.sub stops at 0)
83	law sub_le:
84	  for a: Nat
85	  for k: Nat
86	  LE(Nat.sub(a, k), a)
87	
88	def sub_le(a, k):
89	  match a k:
90	    case 0n 0n:
91	      Unit{}
92	    case 0n 1n+q:
93	      Unit{}
94	    case 1n+p 0n:
95	      le_refl(1n+p)
96	    case 1n++p 1n++q:
97	      le_trans(Nat.sub(p, q), p, 1n+p, sub_le(p, q), le_step(p))
98	
99	# Compares a and b and returns the proof of the side that holds.
100	def le_case(a: Nat, b: Nat) -> Or(LE(a, b), LE(b, a)):
101	  match a b:
102	    case 0n y:
103	      Inl{Unit{}}
104	    case 1n+x 0n:
105	      Inr{Unit{}}
106	    case 1n+x 1n+y:
107	      le_case(x, y)
108	
109	# Motives that refute {False{} == True{}} and {True{} == False{}}.
110	law IsFalse:
111	  for c: Bool
112	  Type
113	
114	def IsFalse(c):
115	  match c:
116	    case False{}:
117	      Unit
118	    case True{}:
119	      Empty
120	
121	law IsTrue:
122	  for c: Bool
123	  Type
124	
125	def IsTrue(c):
126	  match c:
127	    case True{}:
128	      Unit
129	    case False{}:
130	      Empty
131	
132	# The two outcomes of Nat.is_lt as LE proofs. Base's min, max and clamp
133	# branch on is_lt.
134	law le_of_is_lt:
135	  for a: Nat
136	  for b: Nat
137	  for e: {Nat.is_lt(a, b) == True{} : Bool}
138	  LE(a, b)
139	
140	def le_of_is_lt(a, b, e):
141	  match a b:
142	    case 0n y:
143	      Unit{}
144	    case 1n+x 0n:
145	      %e : IsFalse(_)
146	      Unit{}
147	    case 1n+x 1n+y:
148	      le_of_is_lt(x, y, e)
149	
150	law ge_of_not_lt:
151	  for a: Nat
152	  for b: Nat
153	  for e: {Nat.is_lt(a, b) == False{} : Bool}
154	  LE(b, a)
155	
156	def ge_of_not_lt(a, b, e):
157	  match a b:
158	    case 0n 0n:
159	      Unit{}
160	    case 0n 1n+y:
161	      %e : IsTrue(_)
162	      Unit{}
163	    case 1n+x 0n:
164	      Unit{}
165	    case 1n+x 1n+y:
166	      ge_of_not_lt(x, y, e)
167	
168	# Nat ordered by LE
169	def ord() -> C.Ord<Nat>:
170	  C.Ord{LE, le_case}
171	
172	# Nat under addition
173	def add_sg() -> C.Semigroup<Nat>:
174	  C.Semigroup{Nat.add, add_assoc}