proofs/lib/lemmas/proofs/map_delete_common.bend checks

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

7 imports

import Base
import ./map_bridge.bend as MB
import ./string_compare.bend as N
import ./map_insert.bend as I
import ./map_routing.bend as R
import ./invariants.bend as Inv
import ./map_delete_prefix.bend as P

Laws

law conjunction proved
Also proved in bend-mathlib as bool.and_eq_true: `import bend-mathlib@0.7.2.0/bool.bend as MBool`, then `MBool.and_eq_true`.
source · line 11 · raw

@a:Bool -> @b:Bool -> @left:{a == True{} : Bool} -> @right:{b == True{} : Bool} -> {Bool.and(a, b) == True{} : Bool}

Deletion preserves every existing all-pairs row constraint. This law unfolds native pop, including collapsing an empty child.

law low provedsource · line 21 · raw

@-V:Data -> @p:Nat -> @+hi:Map<&2, V> -> @r:Pair(Map<&2, V>, Maybe<&2, V>) -> @+whole:Map<&2, V> -> @+limit:Nat -> @left:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.common_prefix(V, Map.del.fin(&2, V, r), whole, limit) == True{} : Bool} -> @right:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.common_prefix(V, hi, whole, limit) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.common_prefix(V, Map.del.fin(&2, V, Map.pop.lo(&2, V, p, hi, r)), whole, limit) == True{} : Bool}

law high provedsource · line 42 · raw

@-V:Data -> @p:Nat -> @+lo:Map<&2, V> -> @r:Pair(Map<&2, V>, Maybe<&2, V>) -> @+whole:Map<&2, V> -> @+limit:Nat -> @left:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.common_prefix(V, lo, whole, limit) == True{} : Bool} -> @right:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.common_prefix(V, Map.del.fin(&2, V, r), whole, limit) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.common_prefix(V, Map.del.fin(&2, V, Map.pop.hi(&2, V, p, lo, r)), whole, limit) == True{} : Bool}

law leaf provedsource · line 63 · raw

@-V:Data -> @value:V -> @key:String -> @stored:String -> @c:Cmp -> @whole:Map<&2, V> -> @limit:Nat -> @route:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.prefix_against(V, stored, whole, limit) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.common_prefix(V, Map.del.fin(&2, V, Map.pop.leaf(&2, V, value, ((key, stored), c))), whole, limit) == True{} : Bool}

law branch provedsource · line 82 · raw

@-V:Data -> @+lo:Map<&2, V> -> @+hi:Map<&2, V> -> @+p:Nat -> @+key:String -> @bit:Bool -> @e:{Map.bit(key, p) == (key, bit) : Pair(String, Bool)} -> @+whole:Map<&2, V> -> @+limit:Nat -> @left:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.common_prefix(V, lo, whole, limit) == True{} : Bool} -> @right:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.common_prefix(V, hi, whole, limit) == True{} : Bool} -> @lp:(@_:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.common_prefix(V, lo, whole, limit) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.common_prefix(V, Map.del(&2, V, lo, key), whole, limit) == True{} : Bool}) -> @hp:(@_:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.common_prefix(V, hi, whole, limit) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.common_prefix(V, Map.del(&2, V, hi, key), whole, limit) == True{} : Bool}) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.common_prefix(V, Map.del(&2, V, MNode{p, lo, hi}, key), whole, limit) == True{} : Bool}

law preserves_rows provedsource · line 108 · raw

@-V:Data -> @tree:Map<&2, V> -> @+key:String -> @+whole:Map<&2, V> -> @+limit:Nat -> @+routes:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.common_prefix(V, tree, whole, limit) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.common_prefix(V, Map.del(&2, V, tree, key), whole, limit) == True{} : Bool}

law preserves_columns provedsource · line 129 · raw

@-V:Data -> @tree:Map<&2, V> -> @+whole:Map<&2, V> -> @+key:String -> @+limit:Nat -> @+proof:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.common_prefix(V, tree, whole, limit) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.common_prefix(V, tree, Map.del(&2, V, whole, key), limit) == True{} : Bool}

law preserves_common_prefix provedsource · line 147 · raw

@-V:Data -> @+tree:Map<&2, V> -> @+whole:Map<&2, V> -> @+key:String -> @+limit:Nat -> @proof:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.common_prefix(V, tree, whole, limit) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.common_prefix(V, Map.del(&2, V, tree, key), Map.del(&2, V, whole, key), limit) == True{} : Bool}

Both quantified leaf domains shrink under actual Base.pop/del. No relation between the two input trees, and no validity premise, is needed for this fact.