proofs/containers/hash_table/ring.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/ring.bend as Ring

10 imports

import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../../spec/lib/common.bend as SC
import ./buckets.bend as B
import ./modn.bend as M
import ./inv.bend as IV
import ./insm.bend as IM
import ./insert.bend as IS

Definitions

def mod_n source · line 15 · raw

@+bp:Nat -> @+r:Nat -> {Nat.mod(Nat.add(1n+bp, r), 1n+bp) == Nat.mod(r, 1n+bp) : Nat}

def pos_add source · line 19 · raw

@+bp:Nat -> @+a:Nat -> @+x:Nat -> @+y:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, a, x), y) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, a, Nat.add(x, y)) : Nat}

walking x then y steps is walking x + y steps

def pos_wrap source · line 26 · raw

@+bp:Nat -> @+a:Nat -> @+t:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, a, Nat.add(1n+bp, t)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, a, t) : Nat}

walking n more steps comes back

def dist_self source · line 29 · raw

@+bp:Nat -> @+a:Nat -> @+ha:{Nat.is_lt(a, 1n+bp) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, a, a) == 0n : Nat}

def eq_of_dist0 source · line 32 · raw

@+bp:Nat -> @+a:Nat -> @+j:Nat -> @+ha:{Nat.is_lt(a, 1n+bp) == True{} : Bool} -> @+hj:{Nat.is_lt(j, 1n+bp) == True{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, a, j) == 0n : Nat} -> {a == j : Nat}

def pn_c source · line 35 · raw

@+bp:Nat -> @+a:Nat -> @+t:Nat -> @+h:Nat -> @+ha:{Nat.is_lt(a, 1n+bp) == True{} : Bool} -> @+ht:{Nat.is_lt(t, 1n+bp) == True{} : Bool} -> @+hne:{Nat.is_eq(t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, a, h)) == False{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, a, t), h) == c : Bool} -> {c == False{} : Bool}

def pos_ne source · line 44 · raw

@+bp:Nat -> @+a:Nat -> @+t:Nat -> @+h:Nat -> @+ha:{Nat.is_lt(a, 1n+bp) == True{} : Bool} -> @+ht:{Nat.is_lt(t, 1n+bp) == True{} : Bool} -> @+hne:{Nat.is_eq(t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, a, h)) == False{} : Bool} -> {Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, a, t), h) == False{} : Bool}

the step t < n of a path is at h only when t = dist(a, h)

def zy_lt source · line 48 · raw

@+x:Nat -> @+y:Nat -> @+z:Nat -> @+h:{Nat.is_lt(Nat.add(x, z), Nat.add(x, y)) == True{} : Bool} -> {Nat.is_lt(z, y) == True{} : Bool}

x + z < x + y: z < y

def ds_c source · line 55 · raw

@+bp:Nat -> @+a:Nat -> @+h:Nat -> @+j:Nat -> @+ha:{Nat.is_lt(a, 1n+bp) == True{} : Bool} -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+hj:{Nat.is_lt(j, 1n+bp) == True{} : Bool} -> @+hle:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, j), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, a, j)) == True{} : Bool} -> @+pj:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, a, Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, a, h), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, j))) == j : Nat} -> @+c:Bool -> @+hc:{Nat.is_lt(Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, a, h), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, j)), 1n+bp) == c : Bool} -> {Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, a, h), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, j)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, a, j) : Nat}

def dist_split source · line 70 · raw

@+bp:Nat -> @+a:Nat -> @+h:Nat -> @+j:Nat -> @+ha:{Nat.is_lt(a, 1n+bp) == True{} : Bool} -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+hj:{Nat.is_lt(j, 1n+bp) == True{} : Bool} -> @+hle:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, j), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, a, j)) == True{} : Bool} -> {Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, a, h), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, j)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, a, j) : Nat}

THEOREM: when h lies no further from j than a does, the path a -> j goes through h

def bupd_over source · line 78 · raw

@+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+a:Nat -> @+u:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+v:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(xs, a, u), a, v) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(xs, a, v) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk>}

def bupd_comm source · line 87 · raw

@+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+a:Nat -> @+b:Nat -> @+u:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+v:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hne:{Nat.is_eq(a, b) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(xs, a, u), b, v) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(xs, b, v), a, u) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk>}

def len_bupd source · line 100 · raw

@+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+a:Nat -> @+u:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(xs, a, u)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, xs) : Nat}