proofs/containers/bitset/listx.bend
bend-collections-laws-containers@1.0.0.0 · 91 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6
7# List facts about take / drop / update at one position, used to describe the
8# effect of an indexed loop over an array on the list of its slots.
9
10def take_zero(-A: Data, xs: List<&2, A>) -> {SC.take(A, xs, 0n) == Nil{} : List<&2, A>}:
11 match xs:
12 case Nil{}:
13 {==}
14 case Con{h, t}:
15 {==}
16
17def drop_zero(-A: Data, xs: List<&2, A>) -> {SC.drop(A, xs, 0n) == xs : List<&2, A>}:
18 match xs:
19 case Nil{}:
20 {==}
21 case Con{h, t}:
22 {==}
23
24# The element at q, pulled out of the tail that starts there.
25def drop_cons(-A: Data, xs: List<&2, A>, q: Nat, +x: A, +hx: {SC.nth(A, xs, q) == Some{x} : Maybe<&2, A>}) -> {SC.drop(A, xs, q) == Con{x, SC.drop(A, xs, 1n+q)} : List<&2, A>}:
26 match xs q:
27 case Nil{} _:
28 Empty.absurd({Nil{} == Con{x, Nil{}} : List<&2, A>}, L.none_some(A, x, hx))
29 case Con{h, t} 0n:
30 %Equal.sym(List<&2, A>, SC.drop(A, t, 0n), t, drop_zero(A, t)) : {Con{h, t} == Con{x, _} : List<&2, A>}
31 %Equal.sym(A, h, x, L.some_inj(A, h, x, hx)) : {Con{_, t} == Con{x, t} : List<&2, A>}
32 {==}
33 case Con{h, t} 1n+p:
34 drop_cons(A, t, p, x, hx)
35
36# One more element taken is that element appended.
37def take_succ(-A: Data, xs: List<&2, A>, q: Nat, +x: A, +hx: {SC.nth(A, xs, q) == Some{x} : Maybe<&2, A>}) -> {SC.take(A, xs, 1n+q) == SC.snoc(A, SC.take(A, xs, q), x) : List<&2, A>}:
38 match xs q:
39 case Nil{} _:
40 Empty.absurd({Nil{} == Con{x, Nil{}} : List<&2, A>}, L.none_some(A, x, hx))
41 case Con{h, t} 0n:
42 %Equal.sym(List<&2, A>, SC.take(A, t, 0n), Nil{}, take_zero(A, t)) : {Con{h, _} == SC.snoc(A, Nil{}, x) : List<&2, A>}
43 %Equal.sym(A, h, x, L.some_inj(A, h, x, hx)) : {Con{_, Nil{}} == SC.snoc(A, Nil{}, x) : List<&2, A>}
44 {==}
45 case Con{h, t} 1n+p:
46 Equal.cong(List<&2, A>, List<&2, A>, z => Con{h, z}, SC.take(A, t, 1n+p), SC.snoc(A, SC.take(A, t, p), x), take_succ(A, t, p, x, hx))
47
48# Replacing position q does not disturb what follows it.
49def drop_update(-A: Data, xs: List<&2, A>, q: Nat, +v: A) -> {SC.drop(A, SC.update(A, xs, q, v), 1n+q) == SC.drop(A, xs, 1n+q) : List<&2, A>}:
50 match xs q:
51 case Nil{} _:
52 {==}
53 case Con{h, t} 0n:
54 {==}
55 case Con{h, t} 1n+p:
56 drop_update(A, t, p, v)
57
58# ... nor what precedes it.
59def take_update(-A: Data, xs: List<&2, A>, q: Nat, +v: A) -> {SC.take(A, SC.update(A, xs, q, v), q) == SC.take(A, xs, q) : List<&2, A>}:
60 match xs q:
61 case Nil{} _:
62 {==}
63 case Con{h, t} 0n:
64 {==}
65 case Con{h, t} 1n+p:
66 Equal.cong(List<&2, A>, List<&2, A>, z => Con{h, z}, SC.take(A, SC.update(A, t, p, v), p), SC.take(A, t, p), take_update(A, t, p, v))
67
68def take_update_succ(-A: Data, xs: List<&2, A>, q: Nat, +v: A, +h: {Nat.is_lt(q, SC.length(A, xs)) == True{} : Bool}) -> {SC.take(A, SC.update(A, xs, q, v), 1n+q) == SC.snoc(A, SC.take(A, xs, q), v) : List<&2, A>}:
69 match xs q:
70 case Nil{} _:
71 Empty.absurd({SC.take(A, Nil{}, 1n+q) == SC.snoc(A, Nil{}, v) : List<&2, A>}, N.lt_zero_absurd(q, h))
72 case Con{h2, t} 0n:
73 %Equal.sym(List<&2, A>, SC.take(A, t, 0n), Nil{}, take_zero(A, t)) : {Con{v, _} == SC.snoc(A, Nil{}, v) : List<&2, A>}
74 {==}
75 case Con{h2, t} 1n+p:
76 Equal.cong(List<&2, A>, List<&2, A>, z => Con{h2, z}, SC.take(A, SC.update(A, t, p, v), 1n+p), SC.snoc(A, SC.take(A, t, p), v), take_update_succ(A, t, p, v, h))
77
78def take_all(-A: Data, xs: List<&2, A>) -> {SC.take(A, xs, SC.length(A, xs)) == xs : List<&2, A>}:
79 match xs:
80 case Nil{}:
81 {==}
82 case Con{h, t}:
83 Equal.cong(List<&2, A>, List<&2, A>, z => Con{h, z}, SC.take(A, t, SC.length(A, t)), t, take_all(A, t))
84
85def drop_all(-A: Data, xs: List<&2, A>) -> {SC.drop(A, xs, SC.length(A, xs)) == Nil{} : List<&2, A>}:
86 match xs:
87 case Nil{}:
88 {==}
89 case Con{h, t}:
90 drop_all(A, t)
91