proofs/lib/lemmas/proofs/size_length.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/size_length.bend as Size_length

13 imports

import Base
import ../src/cache.bend as C
import ../src/codec.bend as Codec
import ../types/model.bend as T
import ./invariants.bend as Inv
import ./map_routing.bend as R
import ./recency_unique.bend as Unique
import ./recency_head_removal.bend as Head
import ./map_key_membership.bend as Keys
import ./map_delete_common.bend as Common
import ./native_map.bend as Native
import ./canonical_native.bend as CN
import ./representation_parts.bend as Parts

Definitions

def without_present source · line 18 · raw

@+h:String -> @+t:List<&2, String> -> @+key:String -> @eq:Bool -> @+decision:{String.eq(h, key) == eq : Bool} -> @present:{Bool.or(eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.member(t, key)) == True{} : Bool} -> @+unique:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.unique(h <> t) == True{} : Bool} -> @ih:(@p:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.member(t, key) == True{} : Bool} -> {Nat.add(1n, List.length(&2, String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.without(t, key))) == List.length(&2, String, t) : Nat}) -> {Nat.add(1n, List.length(&2, String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.without_keep(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.without(t, key), eq))) == 1n+List.length(&2, String, t) : Nat}

def without_length source · line 28 · raw

@xs:List<&2, String> -> @+key:String -> @present:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.member(xs, key) == True{} : Bool} -> @+unique:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.unique(xs) == True{} : Bool} -> {Nat.add(1n, List.length(&2, String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.without(xs, key))) == List.length(&2, String, xs) : Nat}

Removing a code present exactly once shortens the list by exactly one.

def member_without_step source · line 33 · raw

@+h:String -> @+t:List<&2, String> -> @+key:String -> @+x:String -> @drop:Bool -> @+decision:{String.eq(h, key) == drop : Bool} -> @hx:Bool -> @+ehx:{String.eq(h, x) == hx : Bool} -> @present:{Bool.or(hx, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.member(t, x)) == True{} : Bool} -> @+diff:{String.eq(key, x) == False{} : Bool} -> @ih:(@p:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.member(t, x) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.member(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.without(t, key), x) == True{} : Bool}) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.member(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.without_keep(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.without(t, key), drop), x) == True{} : Bool}

def member_without source · line 53 · raw

@xs:List<&2, String> -> @+key:String -> @+x:String -> @present:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.member(xs, x) == True{} : Bool} -> @+diff:{String.eq(key, x) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.member(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.without(xs, key), x) == True{} : Bool}

A code different from the removed one survives the filter.

def included_without source · line 59 · raw

@xs:List<&2, String> -> @+ys:List<&2, String> -> @+key:String -> @+incl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.included(xs, ys) == True{} : Bool} -> @+absent:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.member(xs, key) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.included(xs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.without(ys, key)) == True{} : Bool}

Inclusion into a list survives removing a code absent from the included list.

def or_right_true source · line 66 · raw

@a:Bool -> @b:Bool -> @e:{Bool.or(a, b) == True{} : Bool} -> @no:{a == False{} : Bool} -> {b == True{} : Bool}

def without_included_step source · line 71 · raw

@+y:String -> @+r:List<&2, String> -> @+h:String -> @+t:List<&2, String> -> @drop:Bool -> @+decision:{String.eq(y, h) == drop : Bool} -> @present:{Bool.or(String.eq(h, y), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.member(t, y)) == True{} : Bool} -> @ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.included(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.without(r, h), t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.included(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.without_keep(y, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.without(r, h), drop), t) == True{} : Bool}

def without_included source · line 77 · raw

@ys:List<&2, String> -> @+h:String -> @+t:List<&2, String> -> @+incl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.included(ys, h <> t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.included(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.without(ys, h), t) == True{} : Bool}

Codes of a list included in h::t, other than h, are included in t.

def same_length source · line 83 · raw

@xs:List<&2, String> -> @+ys:List<&2, String> -> @+uxs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.unique(xs) == True{} : Bool} -> @+uys:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.unique(ys) == True{} : Bool} -> @+i1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.included(xs, ys) == True{} : Bool} -> @+i2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.included(ys, xs) == True{} : Bool} -> {List.length(&2, String, xs) == List.length(&2, String, ys) : Nat}

Duplicate-free, mutually included code lists have equal length.

def list_keys_length source · line 96 · raw

@-V:Data -> @xs:List<&2, Sigma<&2, &2, String, _ => Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<String, V>>>> -> {List.length(&2, String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/canonical_native.list_keys(V, xs)) == List.length(&2, Sigma<&2, &2, String, _ => Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<String, V>>>, xs) : Nat}

def size_parts source · line 101 · raw

@-V:Data -> @+table:Map<&2, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<String, V>>> -> @+order:List<&2, String> -> @facts:Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.unique(order) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.unique(Map.keys(&2, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<String, V>>, table)) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.included(order, Map.keys(&2, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<String, V>>, table)) == True{} : Bool}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.included(Map.keys(&2, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<String, V>>, table), order) == True{} : Bool}))) -> {Map.size(&2, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<String, V>>, table) == List.length(&2, String, order) : Nat}

def size_components source · line 105 · raw

@-V:Data -> @+table:Map<&2, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<String, V>>> -> @+order:List<&2, String> -> @+cap:Nat -> @facts:Pair({Nat.is_gt(cap, 0n) == True{} : Bool}, Pair({Nat.is_le(List.length(&2, String, order), cap) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.unique(order) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.unique(Map.keys(&2, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<String, V>>, table)) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.included(order, Map.keys(&2, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<String, V>>, table)) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.included(Map.keys(&2, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<String, V>>, table), order) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.critbit(Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<String, V>>, table) == True{} : Bool}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.identities(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/codec.string_encode, V, Map.to_list(&2, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<String, V>>, table)) == True{} : Bool}))))))) -> {Map.size(&2, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<String, V>>, table) == List.length(&2, String, order) : Nat}

def native_size source · line 110 · raw

@-V:Data -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<String, V> -> @+valid:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.representation(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/codec.string_encode, V, c) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.map_size(String, V, c) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.len(String, V, c) : Nat}

The native leaf count equals the recency length for represented caches.