proofs/lib/lemmas/proofs/recency_move_inclusion.bend
bend-collections-laws-containers@1.0.0.0 · 55 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/cache.bend as C
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/invariants.bend as Inv
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/recency_membership.bend as Filter
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/recency_update_membership.bend as Move
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_routing.bend as R
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_delete_prefix.bend as And
8import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_key_membership.bend as Keys
9
10def moved(+xs: List<&2, String>, +key: String) -> List<&2, String>:
11 List.append(&2, String, C.without(xs, key), Con{key, Nil{}})
12
13law append_included:
14 for xs: List<&2, String>
15 for +ys: List<&2, String>
16 for +key: String
17 for +included: {Inv.included(xs, ys) == True{} : Bool}
18 for +present: {Inv.member(ys, key) == True{} : Bool}
19 {Inv.included(List.append(&2, String, xs, Con{key, Nil{}}), ys) == True{} : Bool}
20def append_included(xs, ys, key, included, present):
21 match xs:
22 case Nil{}: And.conjunction(Inv.member(ys, key), True{}, present, {==})
23 case Con{+head, +tail}:
24 And.conjunction(Inv.member(ys, head), Inv.included(List.append(&2, String, tail, Con{key, Nil{}}), ys), R.and_left(Inv.member(ys, head), Inv.included(tail, ys), included), append_included(tail, ys, key, R.and_right(Inv.member(ys, head), Inv.included(tail, ys), included), present))
25
26law forward:
27 for +xs: List<&2, String>
28 for +ys: List<&2, String>
29 for +key: String
30 for +included: {Inv.included(xs, ys) == True{} : Bool}
31 for present: {Inv.member(ys, key) == True{} : Bool}
32 {Inv.included(moved(xs, key), ys) == True{} : Bool}
33def forward(xs, ys, key, included, present):
34 append_included(C.without(xs, key), ys, key, Filter.filter_included_left(xs, ys, key, included), present)
35
36law retained:
37 for +xs: List<&2, String>
38 for +key: String
39 for +query: String
40 for present: {Inv.member(xs, query) == True{} : Bool}
41 {Inv.member(moved(xs, key), query) == True{} : Bool}
42def retained(xs, key, query, present):
43 Equal.trans(Bool, Inv.member(moved(xs, key), query), String.eq(query, key) || Inv.member(xs, query), True{}, Move.move(xs, key, query), %Equal.sym(Bool, Inv.member(xs, query), True{}, present) : {String.eq(query, key) || _ == True{} : Bool} Keys.or_true(String.eq(query, key)))
44
45law backward:
46 for xs: List<&2, String>
47 for +ys: List<&2, String>
48 for +key: String
49 for +included: {Inv.included(xs, ys) == True{} : Bool}
50 {Inv.included(xs, moved(ys, key)) == True{} : Bool}
51def backward(xs, ys, key, included):
52 match xs:
53 case Nil{}: {==}
54 case Con{+head, +tail}:
55 And.conjunction(Inv.member(moved(ys, key), head), Inv.included(tail, moved(ys, key)), retained(ys, key, head, R.and_left(Inv.member(ys, head), Inv.included(tail, ys), included)), backward(tail, ys, key, R.and_right(Inv.member(ys, head), Inv.included(tail, ys), included)))