~/bend-docscommunity

LAWS.bend open laws/TODOs

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

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

Laws

law from_list_cons provedin PROOF.bendsource · line 5 · raw

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

When from_list succeeds on a Cons, the payload is that Cons as NE.

law from_list_nil provedin PROOF.bendsource · line 13 · raw

@-a:Quant -> @-A:Kind(a) -> {0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.from_list(a, A, []) == None{} : Maybe<a, 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty<a, A>>}

from_list on Nil is None.

law to_list_ne provedin PROOF.bendsource · line 19 · raw

@-a:Quant -> @-A:Kind(a) -> @h:A -> @t:List<a, A> -> {0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.to_list(a, A, 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NE{h, t}) == h <> t : List<a, A>}

to_list undoes the NE encoding: recovers head <> tail.

law to_list_one provedin PROOF.bendsource · line 27 · raw

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

to_list(one(x)) is the singleton list.

law from_to_list_ne provedin PROOF.bendsource · line 34 · raw

@-a:Quant -> @-A:Kind(a) -> @h:A -> @t:List<a, A> -> {0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.from_list(a, A, 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.to_list(a, A, 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NE{h, t})) == Some{0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NE{h, t}} : Maybe<a, 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty<a, A>>}

from_list ∘ to_list recovers Some{NE{h,t}}.

law length_succ_tail provedin PROOF.bendsource · line 46 · raw

@-a:Quant -> @-A:Kind(a) -> @h:A -> @t:List<a, A> -> {0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.length(a, A, 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NE{h, t}) == 1n+List.length(a, A, t) : Nat}

length(NE{h,t}) is always Succ of List.length(t) (hence ≥ 1).

law length_one provedin PROOF.bendsource · line 54 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.length(a, A, 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.one(a, A, x)) == 1n : Nat}

length(one(x)) is 1.

law head_one provedin PROOF.bendsource · line 61 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.head(a, A, 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.one(a, A, x)) == x : A}

head(one(x)) is x.

law head_ne provedin PROOF.bendsource · line 68 · raw

@-a:Quant -> @-A:Kind(a) -> @h:A -> @t:List<a, A> -> {0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.head(a, A, 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NE{h, t}) == h : A}

head/tail project the NE constructor.

law tail_ne provedin PROOF.bendsource · line 75 · raw

@-a:Quant -> @-A:Kind(a) -> @h:A -> @t:List<a, A> -> {0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.tail(a, A, 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NE{h, t}) == t : List<a, A>}

law tail_one provedin PROOF.bendsource · line 83 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.tail(a, A, 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.one(a, A, x)) == [] : List<a, A>}

tail(one(x)) is Nil.

law one_is_ne provedin PROOF.bendsource · line 90 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.one(a, A, x) == 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NE{x, []} : 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty<a, A>}

one(x) is NE{x, Nil}.

law cons_one provedin PROOF.bendsource · line 97 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> @y:A -> {0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.cons(a, A, x, 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.one(a, A, y)) == 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NE{x, [y]} : 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty<a, A>}

cons(x, one(y)) prepends x.

law head_cons_one provedin PROOF.bendsource · line 105 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> @y:A -> {0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.head(a, A, 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.cons(a, A, x, 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.one(a, A, y))) == x : A}

head(cons(x, one(y))) is x.

law to_list_cons_one provedin PROOF.bendsource · line 113 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> @y:A -> {0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.to_list(a, A, 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.cons(a, A, x, 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.one(a, A, y))) == [x, y] : List<a, A>}

to_list(cons(x, one(y))) is x <> y <> Nil.

law snoc_one provedin PROOF.bendsource · line 125 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> @y:A -> {0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.snoc(a, A, 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.one(a, A, x), y) == 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NE{x, [y]} : 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty<a, A>}

snoc(one(x), y) appends y.

law length_snoc_one provedin PROOF.bendsource · line 133 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> @y:A -> {0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.length(a, A, 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.snoc(a, A, 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.one(a, A, x), y)) == 2n : Nat}

length(snoc(one(x), y)) is 2.

law append_ones provedin PROOF.bendsource · line 141 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> @y:A -> {0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.append(a, A, 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.one(a, A, x), 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty.one(a, A, y)) == 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NE{x, [y]} : 0xcc99578c1df5dd4557ca2ffa56ffce5f/lib.NonEmpty<a, A>}

append(one(x), one(y)) is NE{x, y <> Nil}.