~/bend-docscommunity

LAWS.bend open laws/TODOs

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

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

Laws

law to_list_empty provedin PROOF.bendsource · line 5 · raw

@-a:Quant -> @-A:Kind(a) -> {0xcc241f125bd10140bf0de054c2512463/lib.Stack.to_list(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.Stack.empty(a, A)) == [] : List<a, A>}

to_list(empty) is Nil.

law empty_is_s_nil provedin PROOF.bendsource · line 11 · raw

@-a:Quant -> @-A:Kind(a) -> {0xcc241f125bd10140bf0de054c2512463/lib.Stack.empty(a, A) == 0xcc241f125bd10140bf0de054c2512463/lib.S{[]} : 0xcc241f125bd10140bf0de054c2512463/lib.Stack<a, A>}

empty is S{Nil}.

law to_list_s provedin PROOF.bendsource · line 17 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> {0xcc241f125bd10140bf0de054c2512463/lib.Stack.to_list(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.S{xs}) == xs : List<a, A>}

to_list(S{xs}) exposes the underlying list.

law to_list_push provedin PROOF.bendsource · line 24 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> @x:A -> {0xcc241f125bd10140bf0de054c2512463/lib.Stack.to_list(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.Stack.push(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.S{xs}, x)) == x <> xs : List<a, A>}

push places the new value at the list head.

law push_empty provedin PROOF.bendsource · line 32 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0xcc241f125bd10140bf0de054c2512463/lib.Stack.push(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.Stack.empty(a, A), x) == 0xcc241f125bd10140bf0de054c2512463/lib.S{[x]} : 0xcc241f125bd10140bf0de054c2512463/lib.Stack<a, A>}

push(empty, x) is S{x <> Nil}.

law pop_push_empty provedin PROOF.bendsource · line 39 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0xcc241f125bd10140bf0de054c2512463/lib.Stack.pop(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.Stack.push(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.Stack.empty(a, A), x)) == Some{0xcc241f125bd10140bf0de054c2512463/lib.HD{x, 0xcc241f125bd10140bf0de054c2512463/lib.Stack.empty(a, A)}} : Maybe<a, 0xcc241f125bd10140bf0de054c2512463/lib.Stack.Pop<a, A>>}

pop(push(empty, x)) recovers x and an empty rest.

law pop_push provedin PROOF.bendsource · line 50 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> @x:A -> {0xcc241f125bd10140bf0de054c2512463/lib.Stack.pop(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.Stack.push(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.S{xs}, x)) == Some{0xcc241f125bd10140bf0de054c2512463/lib.HD{x, 0xcc241f125bd10140bf0de054c2512463/lib.S{xs}}} : Maybe<a, 0xcc241f125bd10140bf0de054c2512463/lib.Stack.Pop<a, A>>}

pop(push(s, x)) recovers x and s.

law pop_s_cons provedin PROOF.bendsource · line 62 · raw

@-a:Quant -> @-A:Kind(a) -> @h:A -> @t:List<a, A> -> {0xcc241f125bd10140bf0de054c2512463/lib.Stack.pop(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.S{h <> t}) == Some{0xcc241f125bd10140bf0de054c2512463/lib.HD{h, 0xcc241f125bd10140bf0de054c2512463/lib.S{t}}} : Maybe<a, 0xcc241f125bd10140bf0de054c2512463/lib.Stack.Pop<a, A>>}

pop on a concrete Cons recovers head/rest.

law peek_push provedin PROOF.bendsource · line 70 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> @x:A -> {0xcc241f125bd10140bf0de054c2512463/lib.Stack.peek(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.Stack.push(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.S{xs}, x)) == Some{x} : Maybe<a, A>}

peek(push(s, x)) recovers x.

law peek_push_empty provedin PROOF.bendsource · line 78 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0xcc241f125bd10140bf0de054c2512463/lib.Stack.peek(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.Stack.push(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.Stack.empty(a, A), x)) == Some{x} : Maybe<a, A>}

peek(push(empty, x)) recovers x.

law peek_s_cons provedin PROOF.bendsource · line 85 · raw

@-a:Quant -> @-A:Kind(a) -> @h:A -> @t:List<a, A> -> {0xcc241f125bd10140bf0de054c2512463/lib.Stack.peek(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.S{h <> t}) == Some{h} : Maybe<a, A>}

peek on Cons recovers head.

law is_empty_empty provedin PROOF.bendsource · line 93 · raw

@-a:Quant -> @-A:Kind(a) -> {0xcc241f125bd10140bf0de054c2512463/lib.Stack.is_empty(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.Stack.empty(a, A)) == True{} : Bool}

is_empty(empty) is true.

law is_empty_s_nil provedin PROOF.bendsource · line 99 · raw

@-a:Quant -> @-A:Kind(a) -> {0xcc241f125bd10140bf0de054c2512463/lib.Stack.is_empty(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.S{[]}) == True{} : Bool}

is_empty(S{Nil}) is true.

law is_empty_push provedin PROOF.bendsource · line 105 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> @x:A -> {0xcc241f125bd10140bf0de054c2512463/lib.Stack.is_empty(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.Stack.push(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.S{xs}, x)) == False{} : Bool}

is_empty after push is false.

law is_empty_s_cons provedin PROOF.bendsource · line 113 · raw

@-a:Quant -> @-A:Kind(a) -> @h:A -> @t:List<a, A> -> {0xcc241f125bd10140bf0de054c2512463/lib.Stack.is_empty(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.S{h <> t}) == False{} : Bool}

is_empty(S{h <> t}) is false.

law length_empty provedin PROOF.bendsource · line 121 · raw

@-a:Quant -> @-A:Kind(a) -> {0xcc241f125bd10140bf0de054c2512463/lib.Stack.length(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.Stack.empty(a, A)) == 0n : Nat}

length(empty) is 0.

law length_s provedin PROOF.bendsource · line 127 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> {0xcc241f125bd10140bf0de054c2512463/lib.Stack.length(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.S{xs}) == List.length(a, A, xs) : Nat}

length(S{xs}) is List.length(xs).

law length_push provedin PROOF.bendsource · line 134 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> @x:A -> {0xcc241f125bd10140bf0de054c2512463/lib.Stack.length(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.Stack.push(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.S{xs}, x)) == 1n+List.length(a, A, xs) : Nat}

length after push is one plus the prior list length.

law length_push_empty provedin PROOF.bendsource · line 146 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0xcc241f125bd10140bf0de054c2512463/lib.Stack.length(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.Stack.push(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.Stack.empty(a, A), x)) == 1n : Nat}

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

law from_list_s provedin PROOF.bendsource · line 153 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> {0xcc241f125bd10140bf0de054c2512463/lib.Stack.from_list(a, A, xs) == 0xcc241f125bd10140bf0de054c2512463/lib.S{xs} : 0xcc241f125bd10140bf0de054c2512463/lib.Stack<a, A>}

from_list puts the list directly in stack order.

law to_list_from_list provedin PROOF.bendsource · line 160 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> {0xcc241f125bd10140bf0de054c2512463/lib.Stack.to_list(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.Stack.from_list(a, A, xs)) == xs : List<a, A>}

to_list ∘ from_list is identity on lists.

law from_list_to_list provedin PROOF.bendsource · line 167 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> {0xcc241f125bd10140bf0de054c2512463/lib.Stack.from_list(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.Stack.to_list(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.S{xs})) == 0xcc241f125bd10140bf0de054c2512463/lib.S{xs} : 0xcc241f125bd10140bf0de054c2512463/lib.Stack<a, A>}

from_list ∘ to_list is identity on stacks.

law to_list_from_empty provedin PROOF.bendsource · line 174 · raw

@-a:Quant -> @-A:Kind(a) -> {0xcc241f125bd10140bf0de054c2512463/lib.Stack.to_list(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.Stack.from_list(a, A, [])) == [] : List<a, A>}

from_list(Nil) roundtrips to empty via to_list.

law pop_empty provedin PROOF.bendsource · line 180 · raw

@-a:Quant -> @-A:Kind(a) -> {0xcc241f125bd10140bf0de054c2512463/lib.Stack.pop(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.Stack.empty(a, A)) == None{} : Maybe<a, 0xcc241f125bd10140bf0de054c2512463/lib.Stack.Pop<a, A>>}

pop(empty) is None.

law peek_empty provedin PROOF.bendsource · line 186 · raw

@-a:Quant -> @-A:Kind(a) -> {0xcc241f125bd10140bf0de054c2512463/lib.Stack.peek(a, A, 0xcc241f125bd10140bf0de054c2512463/lib.Stack.empty(a, A)) == None{} : Maybe<a, A>}

peek(empty) is None.