~/bend-docscommunity

LAWS.bend open laws/TODOs

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

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

Laws

law to_list_empty provedin PROOF.bendsource · line 5 · raw

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

to_list(empty) is Nil.

law empty_is_q_nil provedin PROOF.bendsource · line 11 · raw

@-a:Quant -> @-A:Kind(a) -> {0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.empty(a, A) == 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Q{[], []} : 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue<a, A>}

empty is Q{Nil, Nil}.

law to_list_q provedin PROOF.bendsource · line 17 · raw

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

to_list unfolds to front ++ reverse(rear).

law to_list_enqueue_empty provedin PROOF.bendsource · line 25 · raw

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

Enqueue on empty yields a singleton list in FIFO order.

law enqueue_empty provedin PROOF.bendsource · line 32 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.enqueue(a, A, 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.empty(a, A), x) == 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Q{[], [x]} : 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue<a, A>}

enqueue(empty, x) puts x on the rear.

law enqueue_q provedin PROOF.bendsource · line 39 · raw

@-a:Quant -> @-A:Kind(a) -> @f:List<a, A> -> @r:List<a, A> -> @x:A -> {0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.enqueue(a, A, 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Q{f, r}, x) == 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Q{f, x <> r} : 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue<a, A>}

enqueue preserves front and conses onto rear.

law dequeue_enqueue_empty provedin PROOF.bendsource · line 48 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.dequeue(a, A, 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.enqueue(a, A, 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.empty(a, A), x)) == Some{0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.HD{x, 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.empty(a, A)}} : Maybe<a, 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.Deq<a, A>>}

dequeue(enqueue(empty, x)) recovers x and an empty rest.

law dequeue_front_cons provedin PROOF.bendsource · line 59 · raw

@-a:Quant -> @-A:Kind(a) -> @h:A -> @t:List<a, A> -> @r:List<a, A> -> {0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.dequeue(a, A, 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Q{h <> t, r}) == Some{0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.HD{h, 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Q{t, r}}} : Maybe<a, 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.Deq<a, A>>}

dequeue with nonempty front recovers head without rotating.

law dequeue_from_cons provedin PROOF.bendsource · line 72 · raw

@-a:Quant -> @-A:Kind(a) -> @h:A -> @t:List<a, A> -> {0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.dequeue(a, A, 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.from_list(a, A, h <> t)) == Some{0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.HD{h, 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Q{t, []}}} : Maybe<a, 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.Deq<a, A>>}

dequeue(from_list(h <> t)) recovers h.

law peek_empty provedin PROOF.bendsource · line 84 · raw

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

peek(empty) is None.

law peek_enqueue_empty provedin PROOF.bendsource · line 90 · raw

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

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

law peek_from_cons provedin PROOF.bendsource · line 97 · raw

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

peek(from_list(h <> t)) recovers h.

law length_empty provedin PROOF.bendsource · line 105 · raw

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

length(empty) is 0.

law length_q provedin PROOF.bendsource · line 111 · raw

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

length(Q{f,r}) is |f| + |r|.

law length_enqueue provedin PROOF.bendsource · line 123 · raw

@-a:Quant -> @-A:Kind(a) -> @f:List<a, A> -> @r:List<a, A> -> @x:A -> {0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.length(a, A, 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.enqueue(a, A, 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Q{f, r}, x)) == Nat.add(List.length(a, A, f), 1n+List.length(a, A, r)) : Nat}

length after enqueue on a concrete Q{f,r}: |f| + Succ(|r|).

law length_enqueue_empty provedin PROOF.bendsource · line 136 · raw

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

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

law length_from_list_def provedin PROOF.bendsource · line 143 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> {0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.length(a, A, 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.from_list(a, A, xs)) == Nat.add(List.length(a, A, xs), List.length(a, A, [])) : Nat}

Definitional characterization of length(from_list(xs)).

law from_list_q provedin PROOF.bendsource · line 154 · raw

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

from_list puts the whole list in front.

law to_list_from_list_def provedin PROOF.bendsource · line 161 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> {0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.to_list(a, A, 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.from_list(a, A, xs)) == List.append(a, A, xs, List.reverse(a, A, [])) : List<a, A>}

Definitional characterization of to_list(from_list(xs)).

law dequeue_empty provedin PROOF.bendsource · line 172 · raw

@-a:Quant -> @-A:Kind(a) -> {0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.dequeue(a, A, 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.empty(a, A)) == None{} : Maybe<a, 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.Deq<a, A>>}

dequeue(empty) is None.

law is_empty_empty provedin PROOF.bendsource · line 178 · raw

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

is_empty(empty) is true.

law is_empty_enqueue_empty provedin PROOF.bendsource · line 184 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.is_empty(a, A, 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.enqueue(a, A, 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.empty(a, A), x)) == False{} : Bool}

is_empty(enqueue(empty, x)) is false.

law is_empty_front_cons provedin PROOF.bendsource · line 191 · raw

@-a:Quant -> @-A:Kind(a) -> @h:A -> @t:List<a, A> -> @r:List<a, A> -> {0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.is_empty(a, A, 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Q{h <> t, r}) == False{} : Bool}

is_empty with nonempty front is false.

law is_empty_from_nil provedin PROOF.bendsource · line 200 · raw

@-a:Quant -> @-A:Kind(a) -> {0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.is_empty(a, A, 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.from_list(a, A, [])) == True{} : Bool}

is_empty(from_list(Nil)) is true.

law is_empty_from_cons provedin PROOF.bendsource · line 206 · raw

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

is_empty(from_list(h <> t)) is false.

law norm_empty provedin PROOF.bendsource · line 214 · raw

@-a:Quant -> @-A:Kind(a) -> {0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.norm(a, A, 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.empty(a, A)) == 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Q{[], []} : 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue<a, A>}

norm(empty) is empty.

law norm_front_cons provedin PROOF.bendsource · line 220 · raw

@-a:Quant -> @-A:Kind(a) -> @h:A -> @t:List<a, A> -> @r:List<a, A> -> {0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.norm(a, A, 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Q{h <> t, r}) == 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Q{h <> t, r} : 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue<a, A>}

norm with nonempty front is identity.

law norm_rear_singleton provedin PROOF.bendsource · line 229 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue.norm(a, A, 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Q{[], [x]}) == 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Q{[x], []} : 0x5af6678dfaeeeb1cd1ffcb22d02217bc/lib.Queue<a, A>}

norm rotates a singleton rear into front.