1 import Base 2 import ./nat.bend as MNat 3 4 # The empty list is a right identity for append: xs ++ [] = xs. 5 law append_nil: 6 for -a: Quant 7 for -A: Kind(a) 8 for xs: List 9 {List.append(a, A, xs, Nil{}) == xs : List} 10 11 def append_nil(a, A, xs): 12 match xs: 13 case Nil{}: 14 {==} 15 case h <> t: 16 %append_nil(a, A, t) : {h <> List.append(a, A, t, Nil{}) == h <> _ : List} 17 {==} 18 19 # The empty list is a left identity for append: [] ++ xs = xs. 20 law nil_append: 21 for -a: Quant 22 for -A: Kind(a) 23 for -xs: List 24 {List.append(a, A, Nil{}, xs) == xs : List} 25 26 def nil_append(a, A, xs): 27 {==} 28 29 # Append is associative: (xs ++ ys) ++ zs = xs ++ (ys ++ zs). 30 law append_assoc: 31 for -a: Quant 32 for -A: Kind(a) 33 for xs: List 34 for -ys: List 35 for -zs: List 36 {List.append(a, A, List.append(a, A, xs, ys), zs) == List.append(a, A, xs, List.append(a, A, ys, zs)) : List} 37 38 def append_assoc(a, A, xs, ys, zs): 39 match xs: 40 case Nil{}: 41 {==} 42 case h <> t: 43 %append_assoc(a, A, t, ys, zs) : {h <> List.append(a, A, List.append(a, A, t, ys), zs) == h <> _ : List} 44 {==} 45 46 # The length of an append is the sum of the lengths. 47 law length_append: 48 for -a: Quant 49 for -A: Kind(a) 50 for xs: List 51 for -ys: List 52 {List.length(a, A, List.append(a, A, xs, ys)) == Nat.add(List.length(a, A, xs), List.length(a, A, ys)) : Nat} 53 54 def length_append(a, A, xs, ys): 55 match xs: 56 case Nil{}: 57 {==} 58 case h <> t: 59 %length_append(a, A, t, ys) : {1n+List.length(a, A, List.append(a, A, t, ys)) == 1n+_ : Nat} 60 {==} 61 62 def internal_reverse_go_append(a, -A: Kind(a), xs: List, -ys: List, -acc: List) -> {List.reverse.go(a, A, xs, List.append(a, A, ys, acc)) == List.append(a, A, List.reverse.go(a, A, xs, ys), acc) : List}: 63 match xs: 64 case Nil{}: 65 {==} 66 case h <> t: 67 internal_reverse_go_append(a, A, t, h <> ys, acc) 68 69 # The reverse accumulator loop appends the reversed list to the accumulator. 70 law reverse_go_spec: 71 for -a: Quant 72 for -A: Kind(a) 73 for xs: List 74 for -acc: List 75 {List.reverse.go(a, A, xs, acc) == List.append(a, A, List.reverse(a, A, xs), acc) : List} 76 77 def reverse_go_spec(a, A, xs, acc): 78 match xs: 79 case Nil{}: 80 {==} 81 case h <> t: 82 internal_reverse_go_append(a, A, t, h <> Nil{}, acc) 83 84 def internal_reverse_append_go(a, -A: Kind(a), xs: List, -ys: List, -acc: List) -> {List.reverse.go(a, A, List.append(a, A, xs, ys), acc) == List.reverse.go(a, A, ys, List.reverse.go(a, A, xs, acc)) : List}: 85 match xs: 86 case Nil{}: 87 {==} 88 case h <> t: 89 internal_reverse_append_go(a, A, t, ys, h <> acc) 90 91 # Reversing an append reverses and swaps the parts: reverse (xs ++ ys) = reverse ys ++ reverse xs. 92 law reverse_append: 93 for -a: Quant 94 for -A: Kind(a) 95 for xs: List 96 for ys: List 97 {List.reverse(a, A, List.append(a, A, xs, ys)) == List.append(a, A, List.reverse(a, A, ys), List.reverse(a, A, xs)) : List} 98 99 def reverse_append(a, A, xs, ys): 100 Equal.trans(List, List.reverse(a, A, List.append(a, A, xs, ys)), List.reverse.go(a, A, ys, List.reverse(a, A, xs)), List.append(a, A, List.reverse(a, A, ys), List.reverse(a, A, xs)), internal_reverse_append_go(a, A, xs, ys, Nil{}), reverse_go_spec(a, A, ys, List.reverse(a, A, xs))) 101 102 def internal_reverse_go_go(a, -A: Kind(a), xs: List, -acc: List) -> {List.reverse.go(a, A, List.reverse.go(a, A, xs, acc), Nil{}) == List.reverse.go(a, A, acc, xs) : List}: 103 match xs: 104 case Nil{}: 105 {==} 106 case h <> t: 107 internal_reverse_go_go(a, A, t, h <> acc) 108 109 # Reversing twice gives the list back. 110 law reverse_reverse: 111 for -a: Quant 112 for -A: Kind(a) 113 for xs: List 114 {List.reverse(a, A, List.reverse(a, A, xs)) == xs : List} 115 116 def reverse_reverse(a, A, xs): 117 internal_reverse_go_go(a, A, xs, Nil{}) 118 119 def internal_length_reverse_go(a, -A: Kind(a), xs: List, -acc: List, +n: Nat, e: {List.length(a, A, acc) == n : Nat}) -> {List.length(a, A, List.reverse.go(a, A, xs, acc)) == Nat.add(n, List.length(a, A, xs)) : Nat}: 120 match xs: 121 case Nil{}: 122 %Equal.sym(Nat, Nat.add(n, 0n), n, MNat.add_zero(n)) : {List.length(a, A, acc) == _ : Nat} 123 e 124 case h <> t: 125 %Equal.sym(Nat, Nat.add(n, 1n+List.length(a, A, t)), 1n+Nat.add(n, List.length(a, A, t)), MNat.add_succ(n, List.length(a, A, t))) : {List.length(a, A, List.reverse.go(a, A, t, h <> acc)) == _ : Nat} 126 internal_length_reverse_go(a, A, t, h <> acc, 1n+n, Equal.cong(Nat, Nat, k => 1n+k, List.length(a, A, acc), n, e)) 127 128 # Reversing preserves the length. 129 law length_reverse: 130 for -a: Quant 131 for -A: Kind(a) 132 for xs: List 133 {List.length(a, A, List.reverse(a, A, xs)) == List.length(a, A, xs) : Nat} 134 135 def length_reverse(a, A, xs): 136 internal_length_reverse_go(a, A, xs, Nil{}, 0n, {==}) 137 138 # A right fold over an append folds the first part onto the fold of the second. 139 law foldr_append: 140 for ~a: Quant 141 for ~A: Kind(a) 142 for ~B: Type 143 for ~f: A -> B -> B 144 for xs: List 145 for -ys: List 146 for -z: B 147 {List.foldr(~a, ~A, ~B, ~f, List.append(a, A, xs, ys), z) == List.foldr(~a, ~A, ~B, ~f, xs, List.foldr(~a, ~A, ~B, ~f, ys, z)) : B} 148 149 def foldr_append(a, A, B, f, xs, ys, z): 150 match xs: 151 case Nil{}: 152 {==} 153 case h <> t: 154 %foldr_append(~a, ~A, ~B, ~f, t, ys, z) : {f(h, List.foldr(~a, ~A, ~B, ~f, List.append(a, A, t, ys), z)) == f(h, _) : B} 155 {==} 156 157 # Taking n elements and appending the rest after dropping n gives the list back. 158 law take_append_drop: 159 for -a: Quant 160 for -A: Kind(a) 161 for xs: List 162 for n: Nat 163 {List.append(a, A, List.take(a, A, xs, n), List.drop(a, A, xs, n)) == xs : List} 164 165 def take_append_drop(a, A, xs, n): 166 match xs n: 167 case Nil{} _: 168 {==} 169 case h <> t 0n: 170 {==} 171 case h <> t 1n+p: 172 %take_append_drop(a, A, t, p) : {h <> List.append(a, A, List.take(a, A, t, p), List.drop(a, A, t, p)) == h <> _ : List} 173 {==} 174 175 # Mapping preserves the length. 176 law length_map: 177 for ~A: Type 178 for ~B: Type 179 for ~f: A -> B 180 for xs: List 181 {List.length(&1, B, List.map(~A, ~B, ~f, xs)) == List.length(&1, A, xs) : Nat} 182 183 def length_map(A, B, f, xs): 184 match xs: 185 case Nil{}: 186 {==} 187 case h <> t: 188 %length_map(~A, ~B, ~f, t) : {1n+List.length(&1, B, List.map(~A, ~B, ~f, t)) == 1n+_ : Nat} 189 {==} 190 191 # Mapping over an append maps each part: map f (xs ++ ys) = map f xs ++ map f ys. 192 law map_append: 193 for ~A: Type 194 for ~B: Type 195 for ~f: A -> B 196 for xs: List 197 for -ys: List 198 {List.map(~A, ~B, ~f, List.append(&1, A, xs, ys)) == List.append(&1, B, List.map(~A, ~B, ~f, xs), List.map(~A, ~B, ~f, ys)) : List} 199 200 def map_append(A, B, f, xs, ys): 201 match xs: 202 case Nil{}: 203 {==} 204 case h <> t: 205 %map_append(~A, ~B, ~f, t, ys) : {f(h) <> List.map(~A, ~B, ~f, List.append(&1, A, t, ys)) == f(h) <> _ : List} 206 {==} 207 208 # Mapping twice is mapping the composition: map g (map f xs) = map (g . f) xs. 209 law map_map: 210 for ~A: Type 211 for ~B: Type 212 for ~C: Type 213 for ~f: A -> B 214 for ~g: B -> C 215 for xs: List 216 {List.map(~B, ~C, ~g, List.map(~A, ~B, ~f, xs)) == List.map(~A, ~C, ~(x => g(f(x))), xs) : List} 217 218 def map_map(A, B, C, f, g, xs): 219 match xs: 220 case Nil{}: 221 {==} 222 case h <> t: 223 %map_map(~A, ~B, ~C, ~f, ~g, t) : {g(f(h)) <> List.map(~B, ~C, ~g, List.map(~A, ~B, ~f, t)) == g(f(h)) <> _ : List} 224 {==} 225 226 # --- generated: _sym twins (tools/mathlib/twins.ts), do not edit --- 227 228 # The empty list is a right identity for append: xs ++ [] = xs, reversed to rewrite toward the simple side. 229 law append_nil_sym: 230 for -a: Quant 231 for -A: Kind(a) 232 for xs: List 233 {xs == List.append(a, A, xs, Nil{}) : List} 234 235 def append_nil_sym(a, A, xs): 236 Equal.sym(List, List.append(a, A, xs, Nil{}), xs, append_nil(a, A, xs)) 237 238 # The empty list is a left identity for append: [] ++ xs = xs, reversed to rewrite toward the simple side. 239 law nil_append_sym: 240 for -a: Quant 241 for -A: Kind(a) 242 for -xs: List 243 {xs == List.append(a, A, Nil{}, xs) : List} 244 245 def nil_append_sym(a, A, xs): 246 Equal.sym(List, List.append(a, A, Nil{}, xs), xs, nil_append(a, A, xs)) 247 248 # Append is associative: (xs ++ ys) ++ zs = xs ++ (ys ++ zs), reversed to rewrite toward the simple side. 249 law append_assoc_sym: 250 for -a: Quant 251 for -A: Kind(a) 252 for xs: List 253 for -ys: List 254 for -zs: List 255 {List.append(a, A, xs, List.append(a, A, ys, zs)) == List.append(a, A, List.append(a, A, xs, ys), zs) : List} 256 257 def append_assoc_sym(a, A, xs, ys, zs): 258 Equal.sym(List, List.append(a, A, List.append(a, A, xs, ys), zs), List.append(a, A, xs, List.append(a, A, ys, zs)), append_assoc(a, A, xs, ys, zs)) 259 260 # The length of an append is the sum of the lengths, reversed to rewrite toward the simple side. 261 law length_append_sym: 262 for -a: Quant 263 for -A: Kind(a) 264 for xs: List 265 for -ys: List 266 {Nat.add(List.length(a, A, xs), List.length(a, A, ys)) == List.length(a, A, List.append(a, A, xs, ys)) : Nat} 267 268 def length_append_sym(a, A, xs, ys): 269 Equal.sym(Nat, List.length(a, A, List.append(a, A, xs, ys)), Nat.add(List.length(a, A, xs), List.length(a, A, ys)), length_append(a, A, xs, ys)) 270 271 # The reverse accumulator loop appends the reversed list to the accumulator, reversed to rewrite toward the simple side. 272 law reverse_go_spec_sym: 273 for -a: Quant 274 for -A: Kind(a) 275 for xs: List 276 for -acc: List 277 {List.append(a, A, List.reverse(a, A, xs), acc) == List.reverse.go(a, A, xs, acc) : List} 278 279 def reverse_go_spec_sym(a, A, xs, acc): 280 Equal.sym(List, List.reverse.go(a, A, xs, acc), List.append(a, A, List.reverse(a, A, xs), acc), reverse_go_spec(a, A, xs, acc)) 281 282 # Reversing an append reverses and swaps the parts: reverse (xs ++ ys) = reverse ys ++ reverse xs, reversed to rewrite toward the simple side. 283 law reverse_append_sym: 284 for -a: Quant 285 for -A: Kind(a) 286 for xs: List 287 for ys: List 288 {List.append(a, A, List.reverse(a, A, ys), List.reverse(a, A, xs)) == List.reverse(a, A, List.append(a, A, xs, ys)) : List} 289 290 def reverse_append_sym(a, A, xs, ys): 291 Equal.sym(List, List.reverse(a, A, List.append(a, A, xs, ys)), List.append(a, A, List.reverse(a, A, ys), List.reverse(a, A, xs)), reverse_append(a, A, xs, ys)) 292 293 # Reversing twice gives the list back, reversed to rewrite toward the simple side. 294 law reverse_reverse_sym: 295 for -a: Quant 296 for -A: Kind(a) 297 for xs: List 298 {xs == List.reverse(a, A, List.reverse(a, A, xs)) : List} 299 300 def reverse_reverse_sym(a, A, xs): 301 Equal.sym(List, List.reverse(a, A, List.reverse(a, A, xs)), xs, reverse_reverse(a, A, xs)) 302 303 # Reversing preserves the length, reversed to rewrite toward the simple side. 304 law length_reverse_sym: 305 for -a: Quant 306 for -A: Kind(a) 307 for xs: List 308 {List.length(a, A, xs) == List.length(a, A, List.reverse(a, A, xs)) : Nat} 309 310 def length_reverse_sym(a, A, xs): 311 Equal.sym(Nat, List.length(a, A, List.reverse(a, A, xs)), List.length(a, A, xs), length_reverse(a, A, xs)) 312 313 # A right fold over an append folds the first part onto the fold of the second, reversed to rewrite toward the simple side. 314 law foldr_append_sym: 315 for ~a: Quant 316 for ~A: Kind(a) 317 for ~B: Type 318 for ~f: A -> B -> B 319 for xs: List 320 for -ys: List 321 for -z: B 322 {List.foldr(~a, ~A, ~B, ~f, xs, List.foldr(~a, ~A, ~B, ~f, ys, z)) == List.foldr(~a, ~A, ~B, ~f, List.append(a, A, xs, ys), z) : B} 323 324 def foldr_append_sym(a, A, B, f, xs, ys, z): 325 Equal.sym(B, List.foldr(~a, ~A, ~B, ~f, List.append(a, A, xs, ys), z), List.foldr(~a, ~A, ~B, ~f, xs, List.foldr(~a, ~A, ~B, ~f, ys, z)), foldr_append(~a, ~A, ~B, ~f, xs, ys, z)) 326 327 # Taking n elements and appending the rest after dropping n gives the list back, reversed to rewrite toward the simple side. 328 law take_append_drop_sym: 329 for -a: Quant 330 for -A: Kind(a) 331 for xs: List 332 for n: Nat 333 {xs == List.append(a, A, List.take(a, A, xs, n), List.drop(a, A, xs, n)) : List} 334 335 def take_append_drop_sym(a, A, xs, n): 336 Equal.sym(List, List.append(a, A, List.take(a, A, xs, n), List.drop(a, A, xs, n)), xs, take_append_drop(a, A, xs, n)) 337 338 # Mapping preserves the length, reversed to rewrite toward the simple side. 339 law length_map_sym: 340 for ~A: Type 341 for ~B: Type 342 for ~f: A -> B 343 for xs: List 344 {List.length(&1, A, xs) == List.length(&1, B, List.map(~A, ~B, ~f, xs)) : Nat} 345 346 def length_map_sym(A, B, f, xs): 347 Equal.sym(Nat, List.length(&1, B, List.map(~A, ~B, ~f, xs)), List.length(&1, A, xs), length_map(~A, ~B, ~f, xs)) 348 349 # Mapping over an append maps each part: map f (xs ++ ys) = map f xs ++ map f ys, reversed to rewrite toward the simple side. 350 law map_append_sym: 351 for ~A: Type 352 for ~B: Type 353 for ~f: A -> B 354 for xs: List 355 for -ys: List 356 {List.append(&1, B, List.map(~A, ~B, ~f, xs), List.map(~A, ~B, ~f, ys)) == List.map(~A, ~B, ~f, List.append(&1, A, xs, ys)) : List} 357 358 def map_append_sym(A, B, f, xs, ys): 359 Equal.sym(List, List.map(~A, ~B, ~f, List.append(&1, A, xs, ys)), List.append(&1, B, List.map(~A, ~B, ~f, xs), List.map(~A, ~B, ~f, ys)), map_append(~A, ~B, ~f, xs, ys)) 360 361 # Mapping twice is mapping the composition: map g (map f xs) = map (g . f) xs, reversed to rewrite toward the simple side. 362 law map_map_sym: 363 for ~A: Type 364 for ~B: Type 365 for ~C: Type 366 for ~f: A -> B 367 for ~g: B -> C 368 for xs: List 369 {List.map(~A, ~C, ~(x => g(f(x))), xs) == List.map(~B, ~C, ~g, List.map(~A, ~B, ~f, xs)) : List} 370 371 def map_map_sym(A, B, C, f, g, xs): 372 Equal.sym(List, List.map(~B, ~C, ~g, List.map(~A, ~B, ~f, xs)), List.map(~A, ~C, ~(x => g(f(x))), xs), map_map(~A, ~B, ~C, ~f, ~g, xs))