proofs/lib/links.bend
bend-collections-laws-containers@1.0.0.0 · 73 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32.bend as UW
4import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
8import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
9import bend-collections-laws-containers@1.0.0.0/proofs/lib/words32.bend as W32
10import bend-collections-laws-containers@1.0.0.0/proofs/lib/word.bend as WD
11
12# Ids linked through U32 words: lnk(s) is the link word of slot s, fst_or and
13# last_or the link of a list's first and last id (or a default), and how they
14# behave over appends and reversed appends.
15
16def lnk(+s: Nat) -> U32:
17 H.link(U32.from_nat(s))
18
19def fst_or(t: List<&2, Nat>, +q: U32) -> U32:
20 match t:
21 case Nil{}:
22 q
23 case Con{+s, t2}:
24 lnk(s)
25
26def last_or(t: List<&2, Nat>, +p: U32) -> U32:
27 match t:
28 case Nil{}:
29 p
30 case Con{+s, +t2}:
31 last_or(t2, lnk(s))
32
33def u_refl(+x: U32) -> {U32.is_eq(x, x) == True{} : Bool}:
34 UW.u32_eq_refl(x)
35
36def fst_app(+a: List<&2, Nat>, +b: List<&2, Nat>, +q: U32) -> {fst_or(SC.append(Nat, a, b), q) == fst_or(a, fst_or(b, q)) : U32}:
37 match a:
38 case Nil{}:
39 {==}
40 case Con{+h, +t}:
41 {==}
42
43def last_app(+a: List<&2, Nat>, +b: List<&2, Nat>, +p: U32) -> {last_or(SC.append(Nat, a, b), p) == last_or(b, last_or(a, p)) : U32}:
44 match a:
45 case Nil{}:
46 {==}
47 case Con{+h, +t}:
48 last_app(t, b, lnk(h))
49
50def last_lnk(+t: List<&2, Nat>, +a: Nat) -> {last_or(t, lnk(a)) == lnk(NL.lastn(t, a)) : U32}:
51 match t:
52 case Nil{}:
53 {==}
54 case Con{+b, +t2}:
55 last_lnk(t2, b)
56
57def fo_rapp(+l: List<&2, Nat>, +b: List<&2, Nat>, +d: U32) -> {fst_or(NL.rapp(l, b), d) == last_or(l, fst_or(b, d)) : U32}:
58 match l:
59 case Nil{}:
60 {==}
61 case Con{+x, +r}:
62 fo_rapp(r, Con{x, b}, d)
63
64def slot_link(+one: Nat, +h1: {one == 1n : Nat}, +s: U32, +hs: {Nat.is_lt(1n+UD.v(s), WD.sc(32n, one)) == True{} : Bool}) -> {UD.v(H.slot(H.link(s))) == UD.v(s) : Nat}:
65 +lv = W32.link_val(one, h1, s, hs)
66 +hle = L.subst(Nat, z => {Nat.is_le(1n, z) == True{} : Bool}, 1n+UD.v(s), UD.v(H.link(s)), Equal.sym(Nat, UD.v(H.link(s)), 1n+UD.v(s), lv), N.zero_le(UD.v(s)))
67 Equal.trans(Nat, UD.v(H.slot(H.link(s))), Nat.sub(UD.v(H.link(s)), 1n), UD.v(s), UW.sub_nat(H.link(s), 1, hle), Equal.trans(Nat, Nat.sub(UD.v(H.link(s)), 1n), Nat.sub(1n+UD.v(s), 1n), UD.v(s), Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), UD.v(H.link(s)), 1n+UD.v(s), lv), N.sub_zero(UD.v(s))))
68
69def slot_lnk(+one: Nat, +h1: {one == 1n : Nat}, +s: Nat, +sd: Nat, +hsd: {Nat.is_lt(1n+sd, 32n) == True{} : Bool}, +hs: {Nat.is_lt(s, SC.pow2(sd)) == True{} : Bool}) -> {UD.v(H.slot(lnk(s))) == s : Nat}:
70 +hk = N.lt_le(sd, 32n, N.lt_trans(sd, 1n+sd, 32n, N.lt_succ(sd), hsd))
71 +e1 = UW.to_nat_from_nat(s, sd, hk, hs)
72 +hs2 = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(sd)) == True{} : Bool}, s, UD.v(U32.from_nat(s)), Equal.sym(Nat, UD.v(U32.from_nat(s)), s, e1), hs)
73 Equal.trans(Nat, UD.v(H.slot(lnk(s))), UD.v(U32.from_nat(s)), s, slot_link(one, h1, U32.from_nat(s), W32.bound32(one, h1, UD.v(U32.from_nat(s)), sd, hsd, hs2)), e1)