~/bend-docscommunity

proofs/lib/list.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/lib/list.bend as MList

4 imports
import Base
import ./logic.bend as L
import ./nat.bend as N
import ../../spec/lib/common.bend as SC

Definitions

def cons_cong source · line 8 · raw

@-A:Data -> @+h:A -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> @+e:{xs == ys : List<&2, A>} -> {h <> xs == h <> ys : List<&2, A>}

def append_nil source · line 11 · raw

@-A:Data -> @+xs:List<&2, A> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, xs, []) == xs : List<&2, A>}

def append_assoc source · line 18 · raw

@-A:Data -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> @+zs:List<&2, A> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, xs, ys), zs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, xs, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, ys, zs)) : List<&2, A>}

def length_append source · line 25 · raw

@-A:Data -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, xs, ys)) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, ys)) : Nat}

def snoc_append source · line 32 · raw

@-A:Data -> @+xs:List<&2, A> -> @+x:A -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.snoc(A, xs, x) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, xs, [x]) : List<&2, A>}

def length_snoc source · line 39 · raw

@-A:Data -> @+xs:List<&2, A> -> @+x:A -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.snoc(A, xs, x)) == 1n+0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs) : Nat}

def length_replicate source · line 46 · raw

@-A:Data -> @+n:Nat -> @+x:A -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.replicate(A, n, x)) == n : Nat}

def replicate_add source · line 53 · raw

@-A:Data -> @+m:Nat -> @+n:Nat -> @+x:A -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.replicate(A, m, x), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.replicate(A, n, x)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.replicate(A, Nat.add(m, n), x) : List<&2, A>}

def nth_append_left source · line 62 · raw

@-A:Data -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.nth(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, xs, ys), i) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.nth(A, xs, i) : Maybe<&2, A>}

def nth_append_right source · line 71 · raw

@-A:Data -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> @+i:Nat -> @+h:{Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs), i) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.nth(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, xs, ys), i) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.nth(A, ys, Nat.sub(i, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs))) : Maybe<&2, A>}

def update_append_left source · line 81 · raw

@-A:Data -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> @+i:Nat -> @+v:A -> @+h:{Nat.is_lt(i, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.update(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, xs, ys), i, v) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.update(A, xs, i, v), ys) : List<&2, A>}

def update_append_right source · line 90 · raw

@-A:Data -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> @+i:Nat -> @+v:A -> @+h:{Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs), i) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.update(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, xs, ys), i, v) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, xs, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.update(A, ys, Nat.sub(i, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs)), v)) : List<&2, A>}

def length_update source · line 100 · raw

@-A:Data -> @+xs:List<&2, A> -> @+i:Nat -> @+v:A -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.update(A, xs, i, v)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs) : Nat}

def nth_lt_length source · line 109 · raw

@-A:Data -> @+xs:List<&2, A> -> @+i:Nat -> @+x:A -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.nth(A, xs, i) == Some{x} : Maybe<&2, A>} -> {Nat.is_lt(i, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs)) == True{} : Bool}

def nth_update_same source · line 118 · raw

@-A:Data -> @+xs:List<&2, A> -> @+i:Nat -> @+v:A -> @+h:{Nat.is_lt(i, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.nth(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.update(A, xs, i, v), i) == Some{v} : Maybe<&2, A>}

def nth_none source · line 127 · raw

@-A:Data -> @+xs:List<&2, A> -> @+i:Nat -> @+h:{Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs), i) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.nth(A, xs, i) == None{} : Maybe<&2, A>}

def base_append source · line 137 · raw

@-A:Data -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> {List.append(&2, A, xs, ys) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, xs, ys) : List<&2, A>}

Base List.append agrees with the specification append.

def length_zero_nil source · line 144 · raw

@-A:Data -> @+xs:List<&2, A> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs) == 0n : Nat} -> {xs == [] : List<&2, A>}

def rev_go_twice source · line 152 · raw

@-A:Data -> @+xs:List<&2, A> -> @+a:List<&2, A> -> @+b:List<&2, A> -> {List.reverse.go(&2, A, List.reverse.go(&2, A, xs, a), b) == List.reverse.go(&2, A, a, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, xs, b)) : List<&2, A>}

reverse.go(reverse.go(xs, a), b) == reverse.go(a, xs ++ b)

def rev_rev source · line 159 · raw

@-A:Data -> @+xs:List<&2, A> -> {List.reverse(&2, A, List.reverse.go(&2, A, xs, [])) == xs : List<&2, A>}

def nth_update_other source · line 162 · raw

@-A:Data -> @+xs:List<&2, A> -> @+i:Nat -> @+j:Nat -> @+v:A -> @+ne:{Nat.is_eq(i, j) == False{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.nth(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.update(A, xs, i, v), j) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.nth(A, xs, j) : Maybe<&2, A>}

def append_snoc source · line 177 · raw

@-A:Data -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> @+x:A -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, xs, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.snoc(A, ys, x)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.snoc(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, xs, ys), x) : List<&2, A>}

def snoc_append_cons source · line 184 · raw

@-A:Data -> @+xs:List<&2, A> -> @+x:A -> @+acc:List<&2, A> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.snoc(A, xs, x), acc) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, xs, x <> acc) : List<&2, A>}

def rev_snoc source · line 191 · raw

@-A:Data -> @+xs:List<&2, A> -> @+x:A -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.reverse(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.snoc(A, xs, x)) == x <> 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.reverse(A, xs) : List<&2, A>}

def spec_rev_rev source · line 198 · raw

@-A:Data -> @+xs:List<&2, A> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.reverse(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.reverse(A, xs)) == xs : List<&2, A>}

def rev_append source · line 206 · raw

@-A:Data -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.reverse(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, xs, ys)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.reverse(A, ys), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.reverse(A, xs)) : List<&2, A>}

def length_rev source · line 215 · raw

@-A:Data -> @+xs:List<&2, A> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.reverse(A, xs)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs) : Nat}

def base_rev_go source · line 222 · raw

@-A:Data -> @+xs:List<&2, A> -> @+acc:List<&2, A> -> {List.reverse.go(&2, A, xs, acc) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.reverse(A, xs), acc) : List<&2, A>}

def base_rev source · line 230 · raw

@-A:Data -> @+xs:List<&2, A> -> {List.reverse(&2, A, xs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.reverse(A, xs) : List<&2, A>}

def base_take_drop source · line 235 · raw

@-A:Data -> @+xs:List<&2, A> -> @+k:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, List.take(&2, A, xs, k), List.drop(&2, A, xs, k)) == xs : List<&2, A>}

def length_take source · line 244 · raw

@-A:Data -> @+xs:List<&2, A> -> @+k:Nat -> @+h:{Nat.is_le(k, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, List.take(&2, A, xs, k)) == k : Nat}

def length_drop source · line 255 · raw

@-A:Data -> @+xs:List<&2, A> -> @+k:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, List.drop(&2, A, xs, k)) == Nat.sub(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs), k) : Nat}

def last_snoc source · line 268 · raw

@-A:Data -> @+xs:List<&2, A> -> @+x:A -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.last(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.snoc(A, xs, x)) == Some{x} : Maybe<&2, A>}

def init_snoc source · line 277 · raw

@-A:Data -> @+xs:List<&2, A> -> @+x:A -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.init(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.snoc(A, xs, x)) == xs : List<&2, A>}

def sc_length_take source · line 288 · raw

@-A:Data -> @+xs:List<&2, A> -> @+n:Nat -> @+h:{Nat.is_le(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(A, xs, n)) == n : Nat}

def sc_nth_take source · line 299 · raw

@-A:Data -> @+xs:List<&2, A> -> @+n:Nat -> @+i:Nat -> @+h:{Nat.is_lt(i, n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.nth(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(A, xs, n), i) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.nth(A, xs, i) : Maybe<&2, A>}

def sc_take_take source · line 310 · raw

@-A:Data -> @+xs:List<&2, A> -> @+n:Nat -> @+e:Nat -> @+h:{Nat.is_le(e, n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(A, xs, n), e) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(A, xs, e) : List<&2, A>}

def sc_take_zero source · line 323 · raw

@-A:Data -> @+xs:List<&2, A> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(A, xs, 0n) == [] : List<&2, A>}

def sc_take_append_left source · line 330 · raw

@-A:Data -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> @+i:Nat -> @+h:{Nat.is_le(i, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, xs, ys), i) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(A, xs, i) : List<&2, A>}

def sc_take_append_right source · line 341 · raw

@-A:Data -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> @+i:Nat -> @+h:{Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs), i) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, xs, ys), i) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, xs, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(A, ys, Nat.sub(i, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs)))) : List<&2, A>}

def sub_zero_eq source · line 353 · raw

@+r:Nat -> {Nat.sub(r, 0n) == r : Nat}

take r == take l ++ (next r - l after l), for l <= r

def sc_take_split source · line 356 · raw

@-A:Data -> @+xs:List<&2, A> -> @+l:Nat -> @+r:Nat -> @+h:{Nat.is_le(l, r) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(A, xs, r) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(A, xs, l), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.drop(A, xs, l), Nat.sub(r, l))) : List<&2, A>}

def sc_drop_take source · line 369 · raw

@-A:Data -> @+xs:List<&2, A> -> @+n:Nat -> @+l:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.drop(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(A, xs, n), l) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.drop(A, xs, l), Nat.sub(n, l)) : List<&2, A>}

drop l (take n xs) == take (n - l) (drop l xs)

def sc_take_update source · line 382 · raw

@-A:Data -> @+xs:List<&2, A> -> @+i:Nat -> @+v:A -> @+n:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.update(A, xs, i, v), n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.update(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(A, xs, n), i, v) : List<&2, A>}

def sc_take_rep source · line 395 · raw

@-A:Data -> @+m:Nat -> @+x:A -> @+n:Nat -> @+h:{Nat.is_le(n, m) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.replicate(A, m, x), n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.replicate(A, n, x) : List<&2, A>}

def sc_nth_some source · line 407 · raw

@-A:Data -> @+xs:List<&2, A> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs)) == True{} : Bool} -> @+e:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.nth(A, xs, i) == None{} : Maybe<&2, A>} -> Empty

nth below the length is not None