~/bend-docscommunity

LAWS.bend open laws/TODOs

raw source on the hub · import 0x36850d3ea56845a044f30fd80ec1da6c/LAWS.bend as LAWS

2 imports
import Base
import ./lib.bend as P

Laws

law empty_is_p_nil provedin PROOF.bendsource · line 5 · raw

{0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.empty == 0x36850d3ea56845a044f30fd80ec1da6c/lib.P{[]} : 0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio}

empty is P{Nil}.

law to_list_empty provedin PROOF.bendsource · line 9 · raw

{0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.to_list(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.empty) == [] : List<&2, U32>}

to_list(empty) is Nil.

law to_list_p provedin PROOF.bendsource · line 13 · raw

@xs:List<&2, U32> -> {0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.to_list(0x36850d3ea56845a044f30fd80ec1da6c/lib.P{xs}) == xs : List<&2, U32>}

to_list(P{xs}) exposes the list.

law to_list_push_empty provedin PROOF.bendsource · line 18 · raw

@x:U32 -> {0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.to_list(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.push(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.empty, x)) == [x] : List<&2, U32>}

push(empty, x) stores the singleton list.

law peek_empty provedin PROOF.bendsource · line 23 · raw

{0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.peek_min(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.empty) == None{} : Maybe<&2, U32>}

peek_min(empty) is None.

law peek_push_empty provedin PROOF.bendsource · line 27 · raw

@x:U32 -> {0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.peek_min(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.push(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.empty, x)) == Some{x} : Maybe<&2, U32>}

peek_min(push(empty, x)) is x.

law peek_p_cons provedin PROOF.bendsource · line 32 · raw

@h:U32 -> @t:List<&2, U32> -> {0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.peek_min(0x36850d3ea56845a044f30fd80ec1da6c/lib.P{h <> t}) == Some{h} : Maybe<&2, U32>}

peek_min on a concrete Cons recovers the head (min when sorted).

law pop_empty provedin PROOF.bendsource · line 38 · raw

{0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.pop_min(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.empty) == None{} : Maybe<&2, 0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.Pop>}

pop_min(empty) is None.

law pop_push_empty provedin PROOF.bendsource · line 42 · raw

@x:U32 -> {0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.pop_min(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.push(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.empty, x)) == Some{0x36850d3ea56845a044f30fd80ec1da6c/lib.PP{x, 0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.empty}} : Maybe<&2, 0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.Pop>}

pop_min(push(empty, x)) returns x and empty.

law pop_p_cons provedin PROOF.bendsource · line 51 · raw

@h:U32 -> @t:List<&2, U32> -> {0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.pop_min(0x36850d3ea56845a044f30fd80ec1da6c/lib.P{h <> t}) == Some{0x36850d3ea56845a044f30fd80ec1da6c/lib.PP{h, 0x36850d3ea56845a044f30fd80ec1da6c/lib.P{t}}} : Maybe<&2, 0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.Pop>}

pop_min on Cons recovers head/rest.

law size_empty provedin PROOF.bendsource · line 57 · raw

{0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.size(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.empty) == 0n : Nat}

size(empty) is 0.

law size_p provedin PROOF.bendsource · line 61 · raw

@xs:List<&2, U32> -> {0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.size(0x36850d3ea56845a044f30fd80ec1da6c/lib.P{xs}) == List.length(&2, U32, xs) : Nat}

size(P{xs}) is List.length(xs).

law size_push_empty provedin PROOF.bendsource · line 66 · raw

@x:U32 -> {0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.size(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.push(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.empty, x)) == 1n : Nat}

size(push(empty, x)) is 1.

law is_empty_empty provedin PROOF.bendsource · line 71 · raw

{0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.is_empty(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.empty) == True{} : Bool}

is_empty(empty) is True.

law is_empty_p_nil provedin PROOF.bendsource · line 74 · raw

{0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.is_empty(0x36850d3ea56845a044f30fd80ec1da6c/lib.P{[]}) == True{} : Bool}

law is_empty_p_cons provedin PROOF.bendsource · line 77 · raw

@h:U32 -> @t:List<&2, U32> -> {0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.is_empty(0x36850d3ea56845a044f30fd80ec1da6c/lib.P{h <> t}) == False{} : Bool}

law is_empty_push provedin PROOF.bendsource · line 82 · raw

@x:U32 -> {0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.is_empty(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.push(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.empty, x)) == False{} : Bool}

law from_list_empty provedin PROOF.bendsource · line 87 · raw

{0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.from_list([]) == 0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.empty : 0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio}

from_list(Nil) is empty.

law from_list_singleton provedin PROOF.bendsource · line 91 · raw

@x:U32 -> {0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.from_list([x]) == 0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.push(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.empty, x) : 0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio}

from_list(singleton) is the singleton bag.

law insert_nil provedin PROOF.bendsource · line 96 · raw

@x:U32 -> {0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.insert([], x) == [x] : List<&2, U32>}

insert into Nil yields singleton.

law push_two_ordered provedin PROOF.bendsource · line 101 · raw

{0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.to_list(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.push(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.push(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.empty, 2), 1)) == [1, 2] : List<&2, U32>}

Concrete ordering: push 2 then 1 sorts ascending.

law push_two_same_order provedin PROOF.bendsource · line 109 · raw

{0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.to_list(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.push(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.push(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.empty, 1), 2)) == [1, 2] : List<&2, U32>}

Concrete ordering: push 1 then 2 stays ascending.

law peek_two_min provedin PROOF.bendsource · line 117 · raw

{0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.peek_min(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.push(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.push(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.empty, 5), 3)) == Some{3} : Maybe<&2, U32>}

peek_min of two pushed values is the smaller.

law size_two provedin PROOF.bendsource · line 125 · raw

{0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.size(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.push(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.push(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.empty, 1), 2)) == 2n : Nat}

size after two pushes is 2.

law from_list_two provedin PROOF.bendsource · line 133 · raw

{0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.to_list(0x36850d3ea56845a044f30fd80ec1da6c/lib.Prio.from_list([2, 1])) == [1, 2] : List<&2, U32>}

from_list sorts into nondecreasing order (concrete).