1	import Base
2	
3	# String, word and character comparison lemmas and two natural-addition
4	# lemmas, split out of native_map.bend so that code which only needs these
5	# does not import the lemmas about Base's Map internals.
6	
7	law boolean_compare_self:
8	  for b: Bool
9	  {Bool.cmp(b, b) == EQ{} : Cmp}
10	def boolean_compare_self(b):
11	  match b:
12	    case False{}:
13	      {==}
14	    case True{}:
15	      {==}
16	
17	law word_compare_self:
18	  for n: Nat
19	  for w: Word(n)
20	  {Word.cmp(n, w, w) == EQ{} : Cmp}
21	def word_compare_self(n, w):
22	  match n:
23	    case 0n:
24	      {==}
25	    case 1n+p:
26	      match w:
27	        case WCon{+b, t}:
28	          Equal.trans(Cmp, Word.cmp.fin(b, b, Word.cmp(p, t, t)), Bool.cmp(b, b), EQ{},
29	            Equal.cong(Cmp, Cmp, x => Word.cmp.fin(b, b, x), Word.cmp(p, t, t), EQ{}, word_compare_self(p, t)),
30	            boolean_compare_self(b))
31	
32	law character_compare_self:
33	  for c: Char
34	  {Char.cmp(c, c) == ((c, c), EQ{}) : (Char & Char) & Cmp}
35	def character_compare_self(c):
36	  match c:
37	    case Chr{U32{w}}:
38	      %word_compare_self(32n, w) : {((Chr{U32{w}}, Chr{U32{w}}), Word.cmp(32n, w, w)) == ((Chr{U32{w}}, Chr{U32{w}}), _) : (Char & Char) & Cmp}
39	      {==}
40	
41	law string_compare_self:
42	  for s: String
43	  {String.cmp(s, s) == ((s, s), EQ{}) : (String & String) & Cmp}
44	def string_compare_self(s):
45	  match s:
46	    case SNil{}:
47	      {==}
48	    case SCon{h, t}:
49	      %Equal.sym((Char & Char) & Cmp, Char.cmp(h, h), ((h, h), EQ{}), character_compare_self(h)) : {String.cmp.fin(t, t, _) == ((SCon{h, t}, SCon{h, t}), EQ{}) : (String & String) & Cmp}
50	      %Equal.sym((String & String) & Cmp, String.cmp(t, t), ((t, t), EQ{}), string_compare_self(t)) : {String.cmp.rec(h, h, _) == ((SCon{h, t}, SCon{h, t}), EQ{}) : (String & String) & Cmp}
51	      {==}
52	
53	def comparison_identity(-A: Type, a: A, b: A, c: Cmp) -> Type:
54	  match c:
55	    case LT{}:
56	      Unit
57	    case EQ{}:
58	      {a == b : A}
59	    case GT{}:
60	      Unit
61	
62	law word_comparison_step:
63	  for n: Nat
64	  for a: Word(n)
65	  for b: Word(n)
66	  for c: Cmp
67	  for x: Bool
68	  for y: Bool
69	  for proof: comparison_identity(Word(n), a, b, c)
70	  comparison_identity(Word(1n+n), WCon{x, a}, WCon{y, b}, Word.cmp.fin(x, y, c))
71	def word_comparison_step(n, a, b, c, x, y, proof):
72	  match c:
73	    case LT{}:
74	      Unit{}
75	    case GT{}:
76	      Unit{}
77	    case EQ{}:
78	      match x y:
79	        case False{} False{}:
80	          Equal.cong(Word(n), Word(1n+n), t => WCon{False{}, t}, a, b, proof)
81	        case True{} True{}:
82	          Equal.cong(Word(n), Word(1n+n), t => WCon{True{}, t}, a, b, proof)
83	        case False{} True{}:
84	          Unit{}
85	        case True{} False{}:
86	          Unit{}
87	
88	law word_comparison_identity:
89	  for n: Nat
90	  for a: Word(n)
91	  for b: Word(n)
92	  comparison_identity(Word(n), a, b, Word.cmp(n, a, b))
93	def word_comparison_identity(n, a, b):
94	  match n:
95	    case 0n:
96	      match a b:
97	        case WNil{} WNil{}:
98	          {==}
99	    case 1n+ +p:
100	      match a b:
101	        case WCon{x, +at} WCon{y, +bt}:
102	          word_comparison_step(p, at, bt, Word.cmp(p, at, bt), x, y, word_comparison_identity(p, at, bt))
103	
104	law comparison_lift:
105	  for -A: Type
106	  for -B: Type
107	  for f: A -> B
108	  for a: A
109	  for b: A
110	  for c: Cmp
111	  for proof: comparison_identity(A, a, b, c)
112	  comparison_identity(B, f(a), f(b), c)
113	def comparison_lift(A, B, f, a, b, c, proof):
114	  match c:
115	    case LT{}:
116	      Unit{}
117	    case GT{}:
118	      Unit{}
119	    case EQ{}:
120	      Equal.cong(A, B, f, a, b, proof)
121	
122	def comparison_result_identity(-A: Type, r: (A & A) & Cmp) -> Type:
123	  ((a, b), c) = r
124	  comparison_identity(A, a, b, c)
125	
126	law character_comparison_identity:
127	  for a: Char
128	  for b: Char
129	  comparison_result_identity(Char, Char.cmp(a, b))
130	def character_comparison_identity(a, b):
131	  match a b:
132	    case Chr{U32{+x}} Chr{U32{+y}}:
133	      comparison_lift(Word(32n), Char, w => Chr{U32{w}}, x, y, Word.cmp(32n, x, y), word_comparison_identity(32n, x, y))
134	
135	law string_comparison_rec_identity:
136	  for h: Char
137	  for r: (String & String) & Cmp
138	  for proof: comparison_result_identity(String, r)
139	  comparison_result_identity(String, String.cmp.rec(h, h, r))
140	def string_comparison_rec_identity(h, r, proof):
141	  match r:
142	    case Tuple{Tuple{a, b}, c}:
143	      comparison_lift(String, String, t => SCon{h, t}, a, b, c, proof)
144	
145	law string_comparison_fin_identity:
146	  for t1: String
147	  for t2: String
148	  for hc: (Char & Char) & Cmp
149	  for hp: comparison_result_identity(Char, hc)
150	  for tp: comparison_result_identity(String, String.cmp(t1, t2))
151	  comparison_result_identity(String, String.cmp.fin(t1, t2, hc))
152	def string_comparison_fin_identity(t1, t2, hc, hp, tp):
153	  match hc:
154	    case Tuple{Tuple{h1, h2}, LT{}}:
155	      Unit{}
156	    case Tuple{Tuple{h1, h2}, GT{}}:
157	      Unit{}
158	    case Tuple{Tuple{h1, h2}, EQ{}}:
159	      %hp : comparison_result_identity(String, String.cmp.rec(h1, _, String.cmp(t1, t2)))
160	      string_comparison_rec_identity(h1, String.cmp(t1, t2), tp)
161	
162	law string_comparison_identity:
163	  for a: String
164	  for b: String
165	  comparison_result_identity(String, String.cmp(a, b))
166	def string_comparison_identity(a, b):
167	  match a b:
168	    case SNil{} SNil{}:
169	      {==}
170	    case SNil{} SCon{h, t}:
171	      Unit{}
172	    case SCon{h, t} SNil{}:
173	      Unit{}
174	    case SCon{+h1, +t1} SCon{+h2, +t2}:
175	      string_comparison_fin_identity(t1, t2, Char.cmp(h1, h2), character_comparison_identity(h1, h2), string_comparison_identity(t1, t2))
176	
177	def comparison_tag(-A: Type, r: (A & A) & Cmp) -> Cmp:
178	  (pair, c) = r
179	  c
180	
181	law string_comparison_shape_step:
182	  for h1: Char
183	  for h2: Char
184	  for t1: String
185	  for t2: String
186	  for c: Cmp
187	  for tp: {String.cmp(t1, t2) == ((t1, t2), comparison_tag(String, String.cmp(t1, t2))) : (String & String) & Cmp}
188	  {String.cmp.fin(t1, t2, ((h1, h2), c)) == ((SCon{h1, t1}, SCon{h2, t2}), comparison_tag(String, String.cmp.fin(t1, t2, ((h1, h2), c)))) : (String & String) & Cmp}
189	def string_comparison_shape_step(h1, h2, t1, t2, c, tp):
190	  match c:
191	    case LT{}:
192	      {==}
193	    case GT{}:
194	      {==}
195	    case EQ{}:
196	      %Equal.sym((String & String) & Cmp, String.cmp(t1, t2), ((t1, t2), comparison_tag(String, String.cmp(t1, t2))), tp) : {String.cmp.rec(h1, h2, _) == ((SCon{h1, t1}, SCon{h2, t2}), comparison_tag(String, String.cmp.rec(h1, h2, _))) : (String & String) & Cmp}
197	      {==}
198	
199	law string_comparison_shape:
200	  for a: String
201	  for b: String
202	  {String.cmp(a, b) == ((a, b), comparison_tag(String, String.cmp(a, b))) : (String & String) & Cmp}
203	def string_comparison_shape(a, b):
204	  match a b:
205	    case SNil{} SNil{}:
206	      {==}
207	    case SNil{} SCon{h, t}:
208	      {==}
209	    case SCon{h, t} SNil{}:
210	      {==}
211	    case SCon{Chr{U32{+x}}, +t1} SCon{Chr{U32{+y}}, +t2}:
212	      string_comparison_shape_step(Chr{U32{x}}, Chr{U32{y}}, t1, t2, Word.cmp(32n, x, y), string_comparison_shape(t1, t2))
213	
214	law string_comparison_original_identity:
215	  for +a: String
216	  for +b: String
217	  comparison_identity(String, a, b, comparison_tag(String, String.cmp(a, b)))
218	def string_comparison_original_identity(a, b):
219	  %string_comparison_shape(a, b) : comparison_result_identity(String, _)
220	  string_comparison_identity(a, b)
221	
222	law string_equal_from_comparison:
223	  for a: String
224	  for b: String
225	  for e: {comparison_tag(String, String.cmp(a, b)) == EQ{} : Cmp}
226	  {a == b : String}
227	def string_equal_from_comparison(a, b, e):
228	  %e : comparison_identity(String, a, b, _)
229	  string_comparison_original_identity(a, b)
230	
231	law string_equal_comparison:
232	  for a: String
233	  for b: String
234	  for e: {a == b : String}
235	  {String.cmp(a, b) == ((a, b), EQ{}) : (String & String) & Cmp}
236	def string_equal_comparison(a, b, e):
237	  %e : {String.cmp(a, _) == ((a, _), EQ{}) : (String & String) & Cmp}
238	  string_compare_self(a)
239	
240	# First-difference base and common-prefix reduction laws for the existing
241	law natural_add_associative:
242	  for a: Nat
243	  for b: Nat
244	  for c: Nat
245	  {Nat.add(a, Nat.add(b, c)) == Nat.add(Nat.add(a, b), c) : Nat}
246	def natural_add_associative(a, b, c):
247	  match a:
248	    case 0n:
249	      {==}
250	    case 1n+p:
251	      Equal.cong(Nat, Nat, x => 1n+x, Nat.add(p, Nat.add(b, c)), Nat.add(Nat.add(p, b), c), natural_add_associative(p, b, c))
252	
253	law natural_add_right_zero:
254	  for a: Nat
255	  {Nat.add(a, 0n) == a : Nat}
256	def natural_add_right_zero(a):
257	  match a:
258	    case 0n:
259	      {==}
260	    case 1n+p:
261	      Equal.cong(Nat, Nat, x => 1n+x, Nat.add(p, 0n), p, natural_add_right_zero(p))
262