~/bend-docscommunity

LAWS.bend open laws/TODOs

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

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

Laws

law empty_is_d_nil provedin PROOF.bendsource · line 5 · raw

@-a:Quant -> @-A:Kind(a) -> {0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.empty(a, A) == 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.D{[], []} : 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque<a, A>}

empty is D{Nil, Nil}.

law peek_front_empty provedin PROOF.bendsource · line 11 · raw

@-a:Quant -> @-A:Kind(a) -> {0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.peek_front(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.empty(a, A)) == None{} : Maybe<a, A>}

Empty has no front element.

law peek_back_empty provedin PROOF.bendsource · line 17 · raw

@-a:Quant -> @-A:Kind(a) -> {0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.peek_back(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.empty(a, A)) == None{} : Maybe<a, A>}

Empty has no back element.

law pop_front_empty provedin PROOF.bendsource · line 23 · raw

@-a:Quant -> @-A:Kind(a) -> {0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.pop_front(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.empty(a, A)) == None{} : Maybe<a, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.Pop<a, A>>}

Empty pops from either end to None.

law pop_back_empty provedin PROOF.bendsource · line 28 · raw

@-a:Quant -> @-A:Kind(a) -> {0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.pop_back(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.empty(a, A)) == None{} : Maybe<a, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.Pop<a, A>>}

law to_list_empty provedin PROOF.bendsource · line 33 · raw

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

law length_empty provedin PROOF.bendsource · line 38 · raw

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

law is_empty_empty provedin PROOF.bendsource · line 43 · raw

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

law to_list_d provedin PROOF.bendsource · line 49 · raw

@-a:Quant -> @-A:Kind(a) -> @f:List<a, A> -> @r:List<a, A> -> {0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.to_list(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.D{f, r}) == List.append(a, A, f, List.reverse(a, A, r)) : List<a, A>}

Definitional characterization of the two-list order.

law length_d provedin PROOF.bendsource · line 56 · raw

@-a:Quant -> @-A:Kind(a) -> @f:List<a, A> -> @r:List<a, A> -> {0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.length(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.D{f, r}) == Nat.add(List.length(a, A, f), List.length(a, A, r)) : Nat}

law from_list_d provedin PROOF.bendsource · line 67 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> {0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.from_list(a, A, xs) == 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.D{xs, []} : 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque<a, A>}

law from_list_empty provedin PROOF.bendsource · line 73 · raw

@-a:Quant -> @-A:Kind(a) -> {0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.from_list(a, A, []) == 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.empty(a, A) : 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque<a, A>}

law from_list_singleton_roundtrip provedin PROOF.bendsource · line 78 · raw

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

law push_front_d provedin PROOF.bendsource · line 84 · raw

@-a:Quant -> @-A:Kind(a) -> @f:List<a, A> -> @r:List<a, A> -> @x:A -> {0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.push_front(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.D{f, r}, x) == 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.D{x <> f, r} : 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque<a, A>}

law push_back_d provedin PROOF.bendsource · line 92 · raw

@-a:Quant -> @-A:Kind(a) -> @f:List<a, A> -> @r:List<a, A> -> @x:A -> {0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.push_back(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.D{f, r}, x) == 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.D{f, x <> r} : 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque<a, A>}

law push_front_singleton provedin PROOF.bendsource · line 101 · raw

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

Pushing at either end produces the same singleton order.

law push_back_singleton provedin PROOF.bendsource · line 107 · raw

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

law length_push_front_empty provedin PROOF.bendsource · line 113 · raw

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

law length_push_back_empty provedin PROOF.bendsource · line 119 · raw

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

law is_empty_push_front provedin PROOF.bendsource · line 125 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.is_empty(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.push_front(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.empty(a, A), x)) == False{} : Bool}

law is_empty_push_back provedin PROOF.bendsource · line 131 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.is_empty(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.push_back(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.empty(a, A), x)) == False{} : Bool}

law peek_front_push_front provedin PROOF.bendsource · line 137 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.peek_front(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.push_front(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.empty(a, A), x)) == Some{x} : Maybe<a, A>}

law peek_back_push_back provedin PROOF.bendsource · line 143 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.peek_back(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.push_back(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.empty(a, A), x)) == Some{x} : Maybe<a, A>}

law peek_front_push_back provedin PROOF.bendsource · line 149 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.peek_front(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.push_back(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.empty(a, A), x)) == Some{x} : Maybe<a, A>}

law peek_back_push_front provedin PROOF.bendsource · line 155 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.peek_back(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.push_front(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.empty(a, A), x)) == Some{x} : Maybe<a, A>}

law pop_front_push_front_empty provedin PROOF.bendsource · line 162 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.pop_front(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.push_front(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.empty(a, A), x)) == Some{0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.P{x, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.empty(a, A)}} : Maybe<a, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.Pop<a, A>>}

Singleton pops recover the value and an empty deque.

law pop_front_push_back_empty provedin PROOF.bendsource · line 168 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.pop_front(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.push_back(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.empty(a, A), x)) == Some{0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.P{x, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.empty(a, A)}} : Maybe<a, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.Pop<a, A>>}

law pop_back_push_back_empty provedin PROOF.bendsource · line 174 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.pop_back(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.push_back(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.empty(a, A), x)) == Some{0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.P{x, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.empty(a, A)}} : Maybe<a, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.Pop<a, A>>}

law pop_back_push_front_empty provedin PROOF.bendsource · line 180 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.pop_back(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.push_front(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.empty(a, A), x)) == Some{0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.P{x, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.empty(a, A)}} : Maybe<a, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.Pop<a, A>>}

law pop_front_cons provedin PROOF.bendsource · line 186 · raw

@-a:Quant -> @-A:Kind(a) -> @h:A -> @t:List<a, A> -> @r:List<a, A> -> {0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.pop_front(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.D{h <> t, r}) == Some{0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.P{h, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.D{t, r}}} : Maybe<a, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.Pop<a, A>>}

law pop_back_cons provedin PROOF.bendsource · line 198 · raw

@-a:Quant -> @-A:Kind(a) -> @f:List<a, A> -> @h:A -> @t:List<a, A> -> {0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.pop_back(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.D{f, h <> t}) == Some{0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.P{h, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.D{f, t}}} : Maybe<a, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.Pop<a, A>>}

law norm_front_cons provedin PROOF.bendsource · line 210 · raw

@-a:Quant -> @-A:Kind(a) -> @h:A -> @t:List<a, A> -> @r:List<a, A> -> {0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.norm_front(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.D{h <> t, r}) == 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.D{h <> t, r} : 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque<a, A>}

law norm_back_cons provedin PROOF.bendsource · line 218 · raw

@-a:Quant -> @-A:Kind(a) -> @f:List<a, A> -> @h:A -> @t:List<a, A> -> {0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.norm_back(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.D{f, h <> t}) == 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.D{f, h <> t} : 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque<a, A>}

law norm_front_rear_one provedin PROOF.bendsource · line 226 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.norm_front(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.D{[], [x]}) == 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.D{[x], []} : 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque<a, A>}

law norm_back_front_one provedin PROOF.bendsource · line 232 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.norm_back(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.D{[x], []}) == 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.D{[], [x]} : 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque<a, A>}

law to_list_front_then_back provedin PROOF.bendsource · line 239 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> @y:A -> {0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.to_list(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.push_back(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.push_front(a, A, 0xfeda1cb3f8c4b9576ff8c9fdc7be7891/lib.Deque.empty(a, A), x), y)) == [x, y] : List<a, A>}

push_front then push_back order.