~/bend-docscommunity

proofs/lib/two_list.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/lib/two_list.bend as Two_list

5 imports
import Base
import ./nat.bend as N
import ./list.bend as LL
import ../../spec/lib/common.bend as SC
import ../../src/containers/deque.bend as D

Definitions

def zero_sub source · line 10 · raw

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

def take_drop source · line 17 · raw

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

def len_drop source · line 26 · raw

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

def half_le source · line 48 · raw

@+n:Nat -> {Nat.is_le(Nat.div(1n+n, 2n), n) == True{} : Bool}

half of a nonempty length is below it

def len_take source · line 58 · raw

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

def len_rev source · line 61 · raw

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

Templates

template split_eq source · line 36 · raw

@-T:Data -> @+n:Nat -> @+xs:List<&2, T> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.split(T, n, xs) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(T, xs, n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.reverse(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(T, xs, n))) : Pair(List<&2, T>, List<&2, T>)}

the deque's split keeps the first n and reverses the rest