1 import Base 2 import ./logic.bend as L 3 import ./nat.bend as N 4 import ../../spec/lib/common.bend as SC 5 6 # Lemmas about the specification list vocabulary (spec/common.bend). 7 8 def cons_cong(-A: Data, +h: A, +xs: List<&2, A>, +ys: List<&2, A>, +e: {xs == ys : List<&2, A>}) -> {Con{h, xs} == Con{h, ys} : List<&2, A>}: 9 Equal.cong(List<&2, A>, List<&2, A>, zs => Con{h, zs}, xs, ys, e) 10 11 def append_nil(-A: Data, +xs: List<&2, A>) -> {SC.append(A, xs, Nil{}) == xs : List<&2, A>}: 12 match xs: 13 case Nil{}: 14 {==} 15 case Con{+h, +t}: 16 cons_cong(A, h, SC.append(A, t, Nil{}), t, append_nil(A, t)) 17 18 def append_assoc(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>, +zs: List<&2, A>) -> {SC.append(A, SC.append(A, xs, ys), zs) == SC.append(A, xs, SC.append(A, ys, zs)) : List<&2, A>}: 19 match xs: 20 case Nil{}: 21 {==} 22 case Con{+h, +t}: 23 cons_cong(A, h, SC.append(A, SC.append(A, t, ys), zs), SC.append(A, t, SC.append(A, ys, zs)), append_assoc(A, t, ys, zs)) 24 25 def length_append(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>) -> {SC.length(A, SC.append(A, xs, ys)) == Nat.add(SC.length(A, xs), SC.length(A, ys)) : Nat}: 26 match xs: 27 case Nil{}: 28 {==} 29 case Con{+h, +t}: 30 N.succ_cong(SC.length(A, SC.append(A, t, ys)), Nat.add(SC.length(A, t), SC.length(A, ys)), length_append(A, t, ys)) 31 32 def snoc_append(-A: Data, +xs: List<&2, A>, +x: A) -> {SC.snoc(A, xs, x) == SC.append(A, xs, Con{x, Nil{}}) : List<&2, A>}: 33 match xs: 34 case Nil{}: 35 {==} 36 case Con{+h, +t}: 37 cons_cong(A, h, SC.snoc(A, t, x), SC.append(A, t, Con{x, Nil{}}), snoc_append(A, t, x)) 38 39 def length_snoc(-A: Data, +xs: List<&2, A>, +x: A) -> {SC.length(A, SC.snoc(A, xs, x)) == 1n+SC.length(A, xs) : Nat}: 40 match xs: 41 case Nil{}: 42 {==} 43 case Con{+h, +t}: 44 N.succ_cong(SC.length(A, SC.snoc(A, t, x)), 1n+SC.length(A, t), length_snoc(A, t, x)) 45 46 def length_replicate(-A: Data, +n: Nat, +x: A) -> {SC.length(A, SC.replicate(A, n, x)) == n : Nat}: 47 match n: 48 case 0n: 49 {==} 50 case 1n+p: 51 N.succ_cong(SC.length(A, SC.replicate(A, p, x)), p, length_replicate(A, p, x)) 52 53 def replicate_add(-A: Data, +m: Nat, +n: Nat, +x: A) -> {SC.append(A, SC.replicate(A, m, x), SC.replicate(A, n, x)) == SC.replicate(A, Nat.add(m, n), x) : List<&2, A>}: 54 match m: 55 case 0n: 56 {==} 57 case 1n+p: 58 cons_cong(A, x, SC.append(A, SC.replicate(A, p, x), SC.replicate(A, n, x)), SC.replicate(A, Nat.add(p, n), x), replicate_add(A, p, n, x)) 59 60 # ---- nth / update across append ---- 61 62 def nth_append_left(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>, +i: Nat, +h: {Nat.is_lt(i, SC.length(A, xs)) == True{} : Bool}) -> {SC.nth(A, SC.append(A, xs, ys), i) == SC.nth(A, xs, i) : Maybe<&2, A>}: 63 match xs i: 64 case Nil{} _: 65 Empty.absurd({SC.nth(A, ys, i) == None{} : Maybe<&2, A>}, N.lt_zero_absurd(i, h)) 66 case Con{h1, t} 0n: 67 {==} 68 case Con{h1, t} 1n+p: 69 nth_append_left(A, t, ys, p, h) 70 71 def nth_append_right(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>, +i: Nat, +h: {Nat.is_le(SC.length(A, xs), i) == True{} : Bool}) -> {SC.nth(A, SC.append(A, xs, ys), i) == SC.nth(A, ys, Nat.sub(i, SC.length(A, xs))) : Maybe<&2, A>}: 72 match xs i: 73 case Nil{} _: 74 %Equal.sym(Nat, Nat.sub(i, 0n), i, N.sub_zero(i)) : {SC.nth(A, ys, i) == SC.nth(A, ys, _) : Maybe<&2, A>} 75 {==} 76 case Con{h1, t} 0n: 77 Empty.absurd({SC.nth(A, SC.append(A, Con{h1, t}, ys), 0n) == SC.nth(A, ys, Nat.sub(0n, 1n+SC.length(A, t))) : Maybe<&2, A>}, L.false_true(h)) 78 case Con{h1, t} 1n+p: 79 nth_append_right(A, t, ys, p, h) 80 81 def update_append_left(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>, +i: Nat, +v: A, +h: {Nat.is_lt(i, SC.length(A, xs)) == True{} : Bool}) -> {SC.update(A, SC.append(A, xs, ys), i, v) == SC.append(A, SC.update(A, xs, i, v), ys) : List<&2, A>}: 82 match xs i: 83 case Nil{} _: 84 Empty.absurd({SC.update(A, ys, i, v) == SC.append(A, Nil{}, ys) : List<&2, A>}, N.lt_zero_absurd(i, h)) 85 case Con{h1, t} 0n: 86 {==} 87 case Con{+h1, t} 1n+p: 88 cons_cong(A, h1, SC.update(A, SC.append(A, t, ys), p, v), SC.append(A, SC.update(A, t, p, v), ys), update_append_left(A, t, ys, p, v, h)) 89 90 def update_append_right(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>, +i: Nat, +v: A, +h: {Nat.is_le(SC.length(A, xs), i) == True{} : Bool}) -> {SC.update(A, SC.append(A, xs, ys), i, v) == SC.append(A, xs, SC.update(A, ys, Nat.sub(i, SC.length(A, xs)), v)) : List<&2, A>}: 91 match xs i: 92 case Nil{} _: 93 %Equal.sym(Nat, Nat.sub(i, 0n), i, N.sub_zero(i)) : {SC.update(A, ys, i, v) == SC.update(A, ys, _, v) : List<&2, A>} 94 {==} 95 case Con{h1, t} 0n: 96 Empty.absurd({SC.update(A, SC.append(A, Con{h1, t}, ys), 0n, v) == SC.append(A, Con{h1, t}, SC.update(A, ys, Nat.sub(0n, 1n+SC.length(A, t)), v)) : List<&2, A>}, L.false_true(h)) 97 case Con{+h1, t} 1n+p: 98 cons_cong(A, h1, SC.update(A, SC.append(A, t, ys), p, v), SC.append(A, t, SC.update(A, ys, Nat.sub(p, SC.length(A, t)), v)), update_append_right(A, t, ys, p, v, h)) 99 100 def length_update(-A: Data, +xs: List<&2, A>, +i: Nat, +v: A) -> {SC.length(A, SC.update(A, xs, i, v)) == SC.length(A, xs) : Nat}: 101 match xs i: 102 case Nil{} _: 103 {==} 104 case Con{h1, t} 0n: 105 {==} 106 case Con{h1, t} 1n+p: 107 N.succ_cong(SC.length(A, SC.update(A, t, p, v)), SC.length(A, t), length_update(A, t, p, v)) 108 109 def nth_lt_length(-A: Data, +xs: List<&2, A>, +i: Nat, +x: A, +h: {SC.nth(A, xs, i) == Some{x} : Maybe<&2, A>}) -> {Nat.is_lt(i, SC.length(A, xs)) == True{} : Bool}: 110 match xs i: 111 case Nil{} _: 112 Empty.absurd({Nat.is_lt(i, 0n) == True{} : Bool}, L.none_some(A, x, h)) 113 case Con{h1, t} 0n: 114 {==} 115 case Con{h1, t} 1n+p: 116 nth_lt_length(A, t, p, x, h) 117 118 def nth_update_same(-A: Data, +xs: List<&2, A>, +i: Nat, +v: A, +h: {Nat.is_lt(i, SC.length(A, xs)) == True{} : Bool}) -> {SC.nth(A, SC.update(A, xs, i, v), i) == Some{v} : Maybe<&2, A>}: 119 match xs i: 120 case Nil{} _: 121 Empty.absurd({SC.nth(A, Nil{}, i) == Some{v} : Maybe<&2, A>}, N.lt_zero_absurd(i, h)) 122 case Con{h1, t} 0n: 123 {==} 124 case Con{h1, t} 1n+p: 125 nth_update_same(A, t, p, v, h) 126 127 def nth_none(-A: Data, +xs: List<&2, A>, +i: Nat, +h: {Nat.is_le(SC.length(A, xs), i) == True{} : Bool}) -> {SC.nth(A, xs, i) == None{} : Maybe<&2, A>}: 128 match xs i: 129 case Nil{} _: 130 {==} 131 case Con{x, t} 0n: 132 Empty.absurd({Some{x} == None{} : Maybe<&2, A>}, L.false_true(h)) 133 case Con{x, +t} 1n+p: 134 nth_none(A, t, p, h) 135 136 # Base List.append agrees with the specification append. 137 def base_append(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>) -> {List.append(&2, A, xs, ys) == SC.append(A, xs, ys) : List<&2, A>}: 138 match xs: 139 case Nil{}: 140 {==} 141 case Con{+h, +t}: 142 cons_cong(A, h, List.append(&2, A, t, ys), SC.append(A, t, ys), base_append(A, t, ys)) 143 144 def length_zero_nil(-A: Data, +xs: List<&2, A>, +h: {SC.length(A, xs) == 0n : Nat}) -> {xs == Nil{} : List<&2, A>}: 145 match xs: 146 case Nil{}: 147 {==} 148 case Con{x, t}: 149 Empty.absurd({Con{x, t} == Nil{} : List<&2, A>}, N.succ_zero(SC.length(A, t), h)) 150 151 # reverse.go(reverse.go(xs, a), b) == reverse.go(a, xs ++ b) 152 def rev_go_twice(-A: Data, +xs: List<&2, A>, +a: List<&2, A>, +b: List<&2, A>) -> {List.reverse.go(&2, A, List.reverse.go(&2, A, xs, a), b) == List.reverse.go(&2, A, a, SC.append(A, xs, b)) : List<&2, A>}: 153 match xs: 154 case Nil{}: 155 {==} 156 case Con{+h, +t}: 157 rev_go_twice(A, t, Con{h, a}, b) 158 159 def rev_rev(-A: Data, +xs: List<&2, A>) -> {List.reverse(&2, A, List.reverse.go(&2, A, xs, Nil{})) == xs : List<&2, A>}: 160 Equal.trans(List<&2, A>, List.reverse.go(&2, A, List.reverse.go(&2, A, xs, Nil{}), Nil{}), SC.append(A, xs, Nil{}), xs, rev_go_twice(A, xs, Nil{}, Nil{}), append_nil(A, xs)) 161 162 def nth_update_other(-A: Data, +xs: List<&2, A>, +i: Nat, +j: Nat, +v: A, +ne: {Nat.is_eq(i, j) == False{} : Bool}) -> {SC.nth(A, SC.update(A, xs, i, v), j) == SC.nth(A, xs, j) : Maybe<&2, A>}: 163 match xs i j: 164 case Nil{} _ _: 165 {==} 166 case Con{h, t} 0n 0n: 167 Empty.absurd({Some{v} == Some{h} : Maybe<&2, A>}, L.true_false(ne)) 168 case Con{h, t} 0n 1n+q: 169 {==} 170 case Con{h, t} 1n+p 0n: 171 {==} 172 case Con{h, +t} 1n+p 1n+q: 173 nth_update_other(A, t, p, q, v, ne) 174 175 # ---- snoc / reverse ---- 176 177 def append_snoc(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>, +x: A) -> {SC.append(A, xs, SC.snoc(A, ys, x)) == SC.snoc(A, SC.append(A, xs, ys), x) : List<&2, A>}: 178 match xs: 179 case Nil{}: 180 {==} 181 case Con{+h, +t}: 182 cons_cong(A, h, SC.append(A, t, SC.snoc(A, ys, x)), SC.snoc(A, SC.append(A, t, ys), x), append_snoc(A, t, ys, x)) 183 184 def snoc_append_cons(-A: Data, +xs: List<&2, A>, +x: A, +acc: List<&2, A>) -> {SC.append(A, SC.snoc(A, xs, x), acc) == SC.append(A, xs, Con{x, acc}) : List<&2, A>}: 185 match xs: 186 case Nil{}: 187 {==} 188 case Con{+h, +t}: 189 cons_cong(A, h, SC.append(A, SC.snoc(A, t, x), acc), SC.append(A, t, Con{x, acc}), snoc_append_cons(A, t, x, acc)) 190 191 def rev_snoc(-A: Data, +xs: List<&2, A>, +x: A) -> {SC.reverse(A, SC.snoc(A, xs, x)) == Con{x, SC.reverse(A, xs)} : List<&2, A>}: 192 match xs: 193 case Nil{}: 194 {==} 195 case Con{+h, +t}: 196 Equal.cong(List<&2, A>, List<&2, A>, zs => SC.snoc(A, zs, h), SC.reverse(A, SC.snoc(A, t, x)), Con{x, SC.reverse(A, t)}, rev_snoc(A, t, x)) 197 198 def spec_rev_rev(-A: Data, +xs: List<&2, A>) -> {SC.reverse(A, SC.reverse(A, xs)) == xs : List<&2, A>}: 199 match xs: 200 case Nil{}: 201 {==} 202 case Con{+h, +t}: 203 Equal.trans(List<&2, A>, SC.reverse(A, SC.snoc(A, SC.reverse(A, t), h)), Con{h, SC.reverse(A, SC.reverse(A, t))}, Con{h, t}, 204 rev_snoc(A, SC.reverse(A, t), h), cons_cong(A, h, SC.reverse(A, SC.reverse(A, t)), t, spec_rev_rev(A, t))) 205 206 def rev_append(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>) -> {SC.reverse(A, SC.append(A, xs, ys)) == SC.append(A, SC.reverse(A, ys), SC.reverse(A, xs)) : List<&2, A>}: 207 match xs: 208 case Nil{}: 209 Equal.sym(List<&2, A>, SC.append(A, SC.reverse(A, ys), Nil{}), SC.reverse(A, ys), append_nil(A, SC.reverse(A, ys))) 210 case Con{+h, +t}: 211 Equal.trans(List<&2, A>, SC.snoc(A, SC.reverse(A, SC.append(A, t, ys)), h), SC.snoc(A, SC.append(A, SC.reverse(A, ys), SC.reverse(A, t)), h), SC.append(A, SC.reverse(A, ys), SC.snoc(A, SC.reverse(A, t), h)), 212 Equal.cong(List<&2, A>, List<&2, A>, zs => SC.snoc(A, zs, h), SC.reverse(A, SC.append(A, t, ys)), SC.append(A, SC.reverse(A, ys), SC.reverse(A, t)), rev_append(A, t, ys)), 213 Equal.sym(List<&2, A>, SC.append(A, SC.reverse(A, ys), SC.snoc(A, SC.reverse(A, t), h)), SC.snoc(A, SC.append(A, SC.reverse(A, ys), SC.reverse(A, t)), h), append_snoc(A, SC.reverse(A, ys), SC.reverse(A, t), h))) 214 215 def length_rev(-A: Data, +xs: List<&2, A>) -> {SC.length(A, SC.reverse(A, xs)) == SC.length(A, xs) : Nat}: 216 match xs: 217 case Nil{}: 218 {==} 219 case Con{+h, +t}: 220 Equal.trans(Nat, SC.length(A, SC.snoc(A, SC.reverse(A, t), h)), 1n+SC.length(A, SC.reverse(A, t)), 1n+SC.length(A, t), length_snoc(A, SC.reverse(A, t), h), N.succ_cong(SC.length(A, SC.reverse(A, t)), SC.length(A, t), length_rev(A, t))) 221 222 def base_rev_go(-A: Data, +xs: List<&2, A>, +acc: List<&2, A>) -> {List.reverse.go(&2, A, xs, acc) == SC.append(A, SC.reverse(A, xs), acc) : List<&2, A>}: 223 match xs: 224 case Nil{}: 225 {==} 226 case Con{+h, +t}: 227 Equal.trans(List<&2, A>, List.reverse.go(&2, A, t, Con{h, acc}), SC.append(A, SC.reverse(A, t), Con{h, acc}), SC.append(A, SC.snoc(A, SC.reverse(A, t), h), acc), 228 base_rev_go(A, t, Con{h, acc}), Equal.sym(List<&2, A>, SC.append(A, SC.snoc(A, SC.reverse(A, t), h), acc), SC.append(A, SC.reverse(A, t), Con{h, acc}), snoc_append_cons(A, SC.reverse(A, t), h, acc))) 229 230 def base_rev(-A: Data, +xs: List<&2, A>) -> {List.reverse(&2, A, xs) == SC.reverse(A, xs) : List<&2, A>}: 231 Equal.trans(List<&2, A>, List.reverse.go(&2, A, xs, Nil{}), SC.append(A, SC.reverse(A, xs), Nil{}), SC.reverse(A, xs), base_rev_go(A, xs, Nil{}), append_nil(A, SC.reverse(A, xs))) 232 233 # ---- Base take / drop ---- 234 235 def base_take_drop(-A: Data, +xs: List<&2, A>, +k: Nat) -> {SC.append(A, List.take(&2, A, xs, k), List.drop(&2, A, xs, k)) == xs : List<&2, A>}: 236 match xs k: 237 case Nil{} _: 238 {==} 239 case Con{h, t} 0n: 240 {==} 241 case Con{+h, +t} 1n+p: 242 cons_cong(A, h, SC.append(A, List.take(&2, A, t, p), List.drop(&2, A, t, p)), t, base_take_drop(A, t, p)) 243 244 def length_take(-A: Data, +xs: List<&2, A>, +k: Nat, +h: {Nat.is_le(k, SC.length(A, xs)) == True{} : Bool}) -> {SC.length(A, List.take(&2, A, xs, k)) == k : Nat}: 245 match xs k: 246 case Nil{} 0n: 247 {==} 248 case Nil{} 1n+p: 249 Empty.absurd({0n == 1n+p : Nat}, L.false_true(h)) 250 case Con{x, t} 0n: 251 {==} 252 case Con{x, +t} 1n+p: 253 N.succ_cong(SC.length(A, List.take(&2, A, t, p)), p, length_take(A, t, p, h)) 254 255 def length_drop(-A: Data, +xs: List<&2, A>, +k: Nat) -> {SC.length(A, List.drop(&2, A, xs, k)) == Nat.sub(SC.length(A, xs), k) : Nat}: 256 match xs k: 257 case Nil{} 0n: 258 {==} 259 case Nil{} 1n+p: 260 {==} 261 case Con{x, t} 0n: 262 {==} 263 case Con{x, +t} 1n+p: 264 length_drop(A, t, p) 265 266 # ---- last / init ---- 267 268 def last_snoc(-A: Data, +xs: List<&2, A>, +x: A) -> {SC.last(A, SC.snoc(A, xs, x)) == Some{x} : Maybe<&2, A>}: 269 match xs: 270 case Nil{}: 271 {==} 272 case Con{h, Nil{}}: 273 {==} 274 case Con{h, Con{+h2, +t2}}: 275 last_snoc(A, Con{h2, t2}, x) 276 277 def init_snoc(-A: Data, +xs: List<&2, A>, +x: A) -> {SC.init(A, SC.snoc(A, xs, x)) == xs : List<&2, A>}: 278 match xs: 279 case Nil{}: 280 {==} 281 case Con{h, Nil{}}: 282 {==} 283 case Con{+h, Con{+h2, +t2}}: 284 cons_cong(A, h, SC.init(A, SC.snoc(A, Con{h2, t2}, x)), Con{h2, t2}, init_snoc(A, Con{h2, t2}, x)) 285 286 # ---- take / drop over spec/common (generic) ---- 287 288 def sc_length_take(-A: Data, +xs: List<&2, A>, +n: Nat, +h: {Nat.is_le(n, SC.length(A, xs)) == True{} : Bool}) -> {SC.length(A, SC.take(A, xs, n)) == n : Nat}: 289 match xs n: 290 case Nil{} 0n: 291 {==} 292 case Nil{} 1n+m: 293 Empty.absurd({SC.length(A, SC.take(A, Nil{}, 1n+m)) == 1n+m : Nat}, L.false_true(h)) 294 case Con{a, t} 0n: 295 {==} 296 case Con{a, t} 1n+m: 297 N.succ_cong(SC.length(A, SC.take(A, t, m)), m, sc_length_take(A, t, m, h)) 298 299 def sc_nth_take(-A: Data, +xs: List<&2, A>, +n: Nat, +i: Nat, +h: {Nat.is_lt(i, n) == True{} : Bool}) -> {SC.nth(A, SC.take(A, xs, n), i) == SC.nth(A, xs, i) : Maybe<&2, A>}: 300 match xs n i: 301 case Nil{} _ _: 302 {==} 303 case Con{a, t} 0n _: 304 Empty.absurd({SC.nth(A, SC.take(A, Con{a, t}, 0n), i) == SC.nth(A, Con{a, t}, i) : Maybe<&2, A>}, N.lt_zero_absurd(i, h)) 305 case Con{a, t} 1n+m 0n: 306 {==} 307 case Con{a, t} 1n+m 1n+j: 308 sc_nth_take(A, t, m, j, h) 309 310 def sc_take_take(-A: Data, +xs: List<&2, A>, +n: Nat, +e: Nat, +h: {Nat.is_le(e, n) == True{} : Bool}) -> {SC.take(A, SC.take(A, xs, n), e) == SC.take(A, xs, e) : List<&2, A>}: 311 match xs n e: 312 case Nil{} _ _: 313 {==} 314 case Con{a, t} 0n 0n: 315 {==} 316 case Con{a, t} 1n+m 0n: 317 {==} 318 case Con{a, t} 0n 1n+f: 319 Empty.absurd({SC.take(A, SC.take(A, Con{a, t}, 0n), 1n+f) == SC.take(A, Con{a, t}, 1n+f) : List<&2, A>}, L.false_true(h)) 320 case Con{a, t} 1n+m 1n+f: 321 cons_cong(A, a, SC.take(A, SC.take(A, t, m), f), SC.take(A, t, f), sc_take_take(A, t, m, f, h)) 322 323 def sc_take_zero(-A: Data, +xs: List<&2, A>) -> {SC.take(A, xs, 0n) == Nil{} : List<&2, A>}: 324 match xs: 325 case Nil{}: 326 {==} 327 case Con{a, t}: 328 {==} 329 330 def sc_take_append_left(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>, +i: Nat, +h: {Nat.is_le(i, SC.length(A, xs)) == True{} : Bool}) -> {SC.take(A, SC.append(A, xs, ys), i) == SC.take(A, xs, i) : List<&2, A>}: 331 match xs i: 332 case Nil{} 0n: 333 sc_take_zero(A, ys) 334 case Nil{} 1n+j: 335 Empty.absurd({SC.take(A, ys, 1n+j) == Nil{} : List<&2, A>}, L.false_true(h)) 336 case Con{a, t} 0n: 337 {==} 338 case Con{a, t} 1n+j: 339 cons_cong(A, a, SC.take(A, SC.append(A, t, ys), j), SC.take(A, t, j), sc_take_append_left(A, t, ys, j, h)) 340 341 def sc_take_append_right(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>, +i: Nat, +h: {Nat.is_le(SC.length(A, xs), i) == True{} : Bool}) -> {SC.take(A, SC.append(A, xs, ys), i) == SC.append(A, xs, SC.take(A, ys, Nat.sub(i, SC.length(A, xs)))) : List<&2, A>}: 342 match xs i: 343 case Nil{} 0n: 344 {==} 345 case Nil{} 1n+j: 346 {==} 347 case Con{a, t} 0n: 348 Empty.absurd({SC.take(A, SC.append(A, Con{a, t}, ys), 0n) == SC.append(A, Con{a, t}, SC.take(A, ys, Nat.sub(0n, 1n+SC.length(A, t)))) : List<&2, A>}, L.false_true(h)) 349 case Con{a, t} 1n+j: 350 cons_cong(A, a, SC.take(A, SC.append(A, t, ys), j), SC.append(A, t, SC.take(A, ys, Nat.sub(j, SC.length(A, t)))), sc_take_append_right(A, t, ys, j, h)) 351 352 # take r == take l ++ (next r - l after l), for l <= r 353 def sub_zero_eq(+r: Nat) -> {Nat.sub(r, 0n) == r : Nat}: 354 N.sub_zero(r) 355 356 def sc_take_split(-A: Data, +xs: List<&2, A>, +l: Nat, +r: Nat, +h: {Nat.is_le(l, r) == True{} : Bool}) -> {SC.take(A, xs, r) == SC.append(A, SC.take(A, xs, l), SC.take(A, SC.drop(A, xs, l), Nat.sub(r, l))) : List<&2, A>}: 357 match xs l r: 358 case Nil{} _ _: 359 {==} 360 case Con{a, t} 0n r: 361 %Equal.sym(Nat, Nat.sub(r, 0n), r, sub_zero_eq(r)) : {SC.take(A, Con{a, t}, r) == SC.take(A, Con{a, t}, _) : List<&2, A>} 362 {==} 363 case Con{a, t} 1n+k 0n: 364 Empty.absurd({SC.take(A, Con{a, t}, 0n) == SC.append(A, SC.take(A, Con{a, t}, 1n+k), SC.take(A, SC.drop(A, Con{a, t}, 1n+k), Nat.sub(0n, 1n+k))) : List<&2, A>}, L.false_true(h)) 365 case Con{a, t} 1n+k 1n+s: 366 cons_cong(A, a, SC.take(A, t, s), SC.append(A, SC.take(A, t, k), SC.take(A, SC.drop(A, t, k), Nat.sub(s, k))), sc_take_split(A, t, k, s, h)) 367 368 # drop l (take n xs) == take (n - l) (drop l xs) 369 def sc_drop_take(-A: Data, +xs: List<&2, A>, +n: Nat, +l: Nat) -> {SC.drop(A, SC.take(A, xs, n), l) == SC.take(A, SC.drop(A, xs, l), Nat.sub(n, l)) : List<&2, A>}: 370 match xs n l: 371 case Nil{} _ _: 372 {==} 373 case Con{a, t} 0n 0n: 374 {==} 375 case Con{a, t} 0n 1n+k: 376 Equal.sym(List<&2, A>, SC.take(A, SC.drop(A, t, k), 0n), Nil{}, sc_take_zero(A, SC.drop(A, t, k))) 377 case Con{a, t} 1n+m 0n: 378 {==} 379 case Con{a, t} 1n+m 1n+k: 380 sc_drop_take(A, t, m, k) 381 382 def sc_take_update(-A: Data, +xs: List<&2, A>, +i: Nat, +v: A, +n: Nat) -> {SC.take(A, SC.update(A, xs, i, v), n) == SC.update(A, SC.take(A, xs, n), i, v) : List<&2, A>}: 383 match xs i n: 384 case Nil{} _ _: 385 {==} 386 case Con{a, t} 0n 0n: 387 {==} 388 case Con{a, t} 1n+j 0n: 389 {==} 390 case Con{a, t} 0n 1n+m: 391 {==} 392 case Con{a, t} 1n+j 1n+m: 393 cons_cong(A, a, SC.take(A, SC.update(A, t, j, v), m), SC.update(A, SC.take(A, t, m), j, v), sc_take_update(A, t, j, v, m)) 394 395 def sc_take_rep(-A: Data, +m: Nat, +x: A, +n: Nat, +h: {Nat.is_le(n, m) == True{} : Bool}) -> {SC.take(A, SC.replicate(A, m, x), n) == SC.replicate(A, n, x) : List<&2, A>}: 396 match m n: 397 case 0n 0n: 398 {==} 399 case 0n 1n+k: 400 Empty.absurd({SC.take(A, Nil{}, 1n+k) == SC.replicate(A, 1n+k, x) : List<&2, A>}, L.false_true(h)) 401 case 1n+j 0n: 402 {==} 403 case 1n+j 1n+k: 404 cons_cong(A, x, SC.take(A, SC.replicate(A, j, x), k), SC.replicate(A, k, x), sc_take_rep(A, j, x, k, h)) 405 406 # nth below the length is not None 407 def sc_nth_some(-A: Data, +xs: List<&2, A>, +i: Nat, +h: {Nat.is_lt(i, SC.length(A, xs)) == True{} : Bool}, +e: {SC.nth(A, xs, i) == None{} : Maybe<&2, A>}) -> Empty: 408 match xs i: 409 case Nil{} _: 410 N.lt_zero_absurd(i, h) 411 case Con{a, t} 0n: 412 L.none_some(A, a, Equal.sym(Maybe<&2, A>, Some{a}, None{}, e)) 413 case Con{a, t} 1n+j: 414 sc_nth_some(A, t, j, h, e)