array

ArrayTree

data ArrayTree (A : Type)

A binary trie of a fixed depth: vacant is a whole subtree without values, single one cell.

ArrayTree.left

def ArrayTree.left {A : Type} (t : ArrayTree A) : ArrayTree A

The left subtree (a vacant tree has vacant subtrees).

ArrayTree.right

def ArrayTree.right {A : Type} (t : ArrayTree A) : ArrayTree A

The right subtree (a vacant tree has vacant subtrees).

ArrayTree.value

def ArrayTree.value {A : Type} (t : ArrayTree A) : Option A

The value of a one-cell tree (none for a vacant one).

ArrayTree.cells

def ArrayTree.cells {A : Type} (d : Nat) (t : ArrayTree A) : List (Option A)

The cells of a trie of depth d, left to right (2^d of them): the specification of reads and writes.

ArrayTree.get

def ArrayTree.get {A : Type} (d : Nat) (t : ArrayTree A) (i : Nat) : Option A

Reads cell i of a trie of depth d: the high bit picks the subtree.

ArrayTree.getAt

def ArrayTree.getAt {A : Type} (k : Nat) (t : ArrayTree A) (i : Nat) (b : Bool) : Option A

Reads below a branch: the left half when b, else the right half.

ArrayTree.set

def ArrayTree.set {A : Type} (d : Nat) (t : ArrayTree A) (i : Nat) (x : Option A) : ArrayTree A

Writes cell i of a trie of depth d.

ArrayTree.setAt

def ArrayTree.setAt {A : Type} (k : Nat) (t : ArrayTree A) (i : Nat) (x : Option A) (b : Bool) : ArrayTree A

Writes below a branch: the left half when b, else the right half.

ArrayTree.lengthCells

def ArrayTree.lengthCells {A : Type} (d : Nat) (t : ArrayTree A) : length (ArrayTree.cells d t) = Nat.pow 2 d

A trie of depth d has 2^d cells.

ArrayTree.getSpec

def ArrayTree.getSpec {A : Type} (d : Nat) (t : ArrayTree A) (i : Nat) : Nat.blt i (Nat.pow 2 d) = true -> List.nthOption (ArrayTree.cells d t) i = some (ArrayTree.get d t i)

Reading cell i of the cell list gives the trie read, for i below 2^d.

ArrayTree.getSpecAt

def ArrayTree.getSpecAt {A : Type} (k : Nat) (t : ArrayTree A) (i : Nat) (b : Bool) : Nat.blt i (Nat.pow 2 k) = b -> Nat.blt i (Nat.pow 2 (succ k)) = true -> List.nthOption (ArrayTree.cells (succ k) t) i = some (ArrayTree.getAt k t i b)

The read specification below a branch, with the half decided by b.

ArrayTree.setSpec

def ArrayTree.setSpec {A : Type} (d : Nat) (t : ArrayTree A) (i : Nat) (x : Option A) : Nat.blt i (Nat.pow 2 d) = true -> ArrayTree.cells d (ArrayTree.set d t i x) = List.setNth (ArrayTree.cells d t) i x

Writing cell i replaces cell i of the cell list, for i below 2^d.

ArrayTree.setSpecAt

def ArrayTree.setSpecAt {A : Type} (k : Nat) (t : ArrayTree A) (i : Nat) (x : Option A) (b : Bool) : Nat.blt i (Nat.pow 2 k) = b -> Nat.blt i (Nat.pow 2 (succ k)) = true -> ArrayTree.cells (succ k) (ArrayTree.setAt k t i x b) = List.setNth (ArrayTree.cells (succ k) t) i x

The write specification below a branch, with the half decided by b.

ArrayTree.getFast

def ArrayTree.getFast {A : Type} (d : Nat) (width : Nat) (t : ArrayTree A) (i : Nat) : Option A

The read that runs: each level halves the previous half instead of recomputing 2^k (equal to get, see getFastSpec).

ArrayTree.getFastAt

def ArrayTree.getFastAt {A : Type} (k : Nat) (half : Nat) (t : ArrayTree A) (i : Nat) (b : Bool) : Option A

The fast read below a branch: matches the subtree directly.

ArrayTree.setFast

def ArrayTree.setFast {A : Type} (d : Nat) (width : Nat) (t : ArrayTree A) (i : Nat) (x : Option A) : ArrayTree A

The write that runs: each level halves the previous half (equal to set, see setFastSpec).

ArrayTree.setFastAt

def ArrayTree.setFastAt {A : Type} (k : Nat) (half : Nat) (t : ArrayTree A) (i : Nat) (x : Option A) (b : Bool) : ArrayTree A

The fast write below a branch: matches the subtree directly.

ArrayTree.getFastSpec

def ArrayTree.getFastSpec {A : Type} (d : Nat) (t : ArrayTree A) (i : Nat) : ArrayTree.getFast d (Nat.pow 2 d) t i = ArrayTree.get d t i

The fast read equals the specified read.

ArrayTree.getFastSpecAt

def ArrayTree.getFastSpecAt {A : Type} (k : Nat) (t : ArrayTree A) (i : Nat) (b : Bool) : ArrayTree.getFastAt k (Nat.pow 2 k) t i b = ArrayTree.getAt k t i b

The fast read below a branch equals the specified one.

ArrayTree.setFastSpec

def ArrayTree.setFastSpec {A : Type} (d : Nat) (t : ArrayTree A) (i : Nat) (x : Option A) : ArrayTree.setFast d (Nat.pow 2 d) t i x = ArrayTree.set d t i x

The fast write equals the specified write.

ArrayTree.setFastSpecAt

def ArrayTree.setFastSpecAt {A : Type} (k : Nat) (t : ArrayTree A) (i : Nat) (x : Option A) (b : Bool) : ArrayTree.setFastAt k (Nat.pow 2 k) t i x b = ArrayTree.setAt k t i x b

The fast write below a branch equals the specified one.

Array.firstCells

def Array.firstCells {A : Type} (n : Nat) (d : Nat) (t : ArrayTree A) : List (Option A)

The first n cells of a trie of depth d.

ArrayTree.store

def ArrayTree.store {A : Type} (d : Nat) (t : ArrayTree A) (i : Nat) (x : Option A) : ArrayTree A

Writes cell i with the fast write at the trie’s full width.

Array.isFilled

def Array.isFilled {A : Type} (depth : Nat) (size : Nat) (tree : ArrayTree A) : Bool

Whether a trie of the given depth holds an array of the given size: the size fits and every cell below it holds a value.

Array

record Array (A : Type)

A persistent array: reads and writes take time logarithmic in the size, writing gives a new array.

Array.cells

def Array.cells {A : Type} (a : Array A) : List (Option A)

The cells below the size (each holds a value).

Array.writtenTree

def Array.writtenTree {A : Type} (a : Array A) (i : Nat) (x : A) : ArrayTree A

The trie after writing x at index i.

Array.toList

def Array.toList {A : Type} (a : Array A) : List A

The elements in order: the specification every operation is stated against.

Array.empty

def Array.empty {A : Type} : Array A

The array with no elements.

Array.sizeFits

def Array.sizeFits {A : Type} (a : Array A) : Nat.ble a.size (Nat.pow 2 a.depth) = true

The size fits the depth.

Array.cellsFull

def Array.cellsFull {A : Type} (a : Array A) : List.allSome (Array.cells a) = true

Every cell below the size holds a value.

Array.lengthCells

def Array.lengthCells {A : Type} (a : Array A) : length (Array.cells a) = a.size

There are as many cells below the size as the size.

Array.lengthToList

def Array.lengthToList {A : Type} (a : Array A) : length (Array.toList a) = a.size

The array has as many elements as its size.

Array.get

def Array.get {A : Type} (a : Array A) (i : Nat) : Option A

Reads element i; none past the end.

Array.getInside

def Array.getInside {A : Type} (a : Array A) (i : Nat) (h : Nat.blt i a.size = true) : ArrayTree.get a.depth a.tree i = List.nthOption (Array.toList a) i

Reading the trie inside the size reads the elements.

Array.getSpecAt

def Array.getSpecAt {A : Type} (a : Array A) (i : Nat) (b : Bool) (e : Nat.blt i a.size = b) : (match b with | true => ArrayTree.getFast a.depth (Nat.pow 2 a.depth) a.tree i | false => none) = List.nthOption (Array.toList a) i

Reading by the outcome of the bounds check: the read specification in each case.

Array.getSpec

def Array.getSpec {A : Type} (a : Array A) (i : Nat) : Array.get a i = List.nthOption (Array.toList a) i

Reading an element reads the list of elements.

Array.cellsAfterSet

def Array.cellsAfterSet {A : Type} (d : Nat) (t : ArrayTree A) (i : Nat) (x : Option A) (h : Nat.blt i (Nat.pow 2 d) = true) : ArrayTree.cells d (ArrayTree.store d t i x) = List.setNth (ArrayTree.cells d t) i x

The cells of a trie after a write inside its width.

Array.cellsSet

def Array.cellsSet {A : Type} (a : Array A) (i : Nat) (x : A) (h : Nat.blt i a.size = true) : Array.firstCells a.size a.depth (Array.writtenTree a i x) = List.setNth (Array.cells a) i (some x)

The cells below the size after writing a value inside the size.

Array.filledSet

def Array.filledSet {A : Type} (a : Array A) (i : Nat) (x : A) (h : Nat.blt i a.size = true) : Array.isFilled a.depth a.size (Array.writtenTree a i x) = true

Writing a value inside the size keeps the array well formed. Irreducible, as the other proofs of the invariant (Array.filledPush, Array.filledPop): evaluating an array never computes its filled field (the proof walks the cells, so computing it made each write linear and n writes quadratic).

Array.setAt

def Array.setAt {A : Type} (a : Array A) (i : Nat) (x : A) (b : Bool) (e : Nat.blt i a.size = b) : Array A

Writing by the outcome of the bounds check.

Array.set

def Array.set {A : Type} (a : Array A) (i : Nat) (x : A) : Array A

Writes element i; an index past the end leaves the array unchanged.

Array.setSpecAt

def Array.setSpecAt {A : Type} (a : Array A) (i : Nat) (x : A) (b : Bool) (e : Nat.blt i a.size = b) : Array.toList (Array.setAt a i x b e) = List.setNth (Array.toList a) i x

The write specification in each case of the bounds check.

Array.setSpec

def Array.setSpec {A : Type} (a : Array A) (i : Nat) (x : A) : Array.toList (Array.set a i x) = List.setNth (Array.toList a) i x

Writing an element writes the list of elements.

Array.cellsPush

def Array.cellsPush {A : Type} (d : Nat) (t : ArrayTree A) (n : Nat) (x : A) (h : Nat.blt n (Nat.pow 2 d) = true) : Array.firstCells (succ n) d (ArrayTree.store d t n (some x)) = List.snoc (Array.firstCells n d t) (some x)

The cells up to a newly written last index: the old prefix followed by the value.

Array.filledPush

def Array.filledPush {A : Type} (d : Nat) (t : ArrayTree A) (n : Nat) (x : A) (h : Nat.blt n (Nat.pow 2 d) = true) (base : List.allSome (Array.firstCells n d t) = true) : Array.isFilled d (succ n) (ArrayTree.store d t n (some x)) = true

Appending a value at index n (below the width) of a trie whose first n cells hold values keeps it well formed. Irreducible (see Array.filledSet).

Array.pushInto

def Array.pushInto {A : Type} (d : Nat) (t : ArrayTree A) (n : Nat) (x : A) (h : Nat.blt n (Nat.pow 2 d) = true) (base : List.allSome (Array.firstCells n d t) = true) : Array A

Appends x at index n of a trie whose first n cells hold values (n below the width).

Array.pushIntoSpec

def Array.pushIntoSpec {A : Type} (d : Nat) (t : ArrayTree A) (n : Nat) (x : A) (h : Nat.blt n (Nat.pow 2 d) = true) (base : List.allSome (Array.firstCells n d t) = true) : Array.toList (Array.pushInto d t n x h base) = List.snoc (List.somes (Array.firstCells n d t)) x

The elements after appending: the old prefix’s values followed by x.

Array.fitsGrown

def Array.fitsGrown {A : Type} (a : Array A) : Nat.blt a.size (Nat.pow 2 (succ a.depth)) = true

A full array fits below the next width: size <= 2^d < 2^(d+1).

Array.grownTree

def Array.grownTree {A : Type} (a : Array A) : ArrayTree A

The trie grown by a level: the old tree is the left half.

Array.cellsGrown

def Array.cellsGrown {A : Type} (a : Array A) : Array.firstCells a.size (succ a.depth) (Array.grownTree a) = Array.cells a

Growing a level keeps the cells below the size.

Array.fullGrown

def Array.fullGrown {A : Type} (a : Array A) : List.allSome (Array.firstCells a.size (succ a.depth) (Array.grownTree a)) = true

The grown tree’s first cells hold values.

Array.pushAt

def Array.pushAt {A : Type} (a : Array A) (x : A) (b : Bool) (e : Nat.blt a.size (Nat.pow 2 a.depth) = b) : Array A

Appending by the outcome of the room check: write in place, or grow a level first.

Array.push

def Array.push {A : Type} (a : Array A) (x : A) : Array A

Appends x at the end, growing a level when full.

Array.pushSpecAt

def Array.pushSpecAt {A : Type} (a : Array A) (x : A) (b : Bool) (e : Nat.blt a.size (Nat.pow 2 a.depth) = b) : Array.toList (Array.pushAt a x b e) = List.snoc (Array.toList a) x

The append specification in each case of the room check.

Array.pushSpec

def Array.pushSpec {A : Type} (a : Array A) (x : A) : Array.toList (Array.push a x) = List.snoc (Array.toList a) x

Appending an element appends to the list of elements.

Array.filledPop

def Array.filledPop {A : Type} (a : Array A) (m : Nat) (e : a.size = succ m) : Array.isFilled a.depth m a.tree = true

Dropping the last element (the size is succ m) keeps the array well formed. Irreducible (see Array.filledSet).

Array.popAt

def Array.popAt {A : Type} (a : Array A) (n : Nat) (e : a.size = n) : Array A

Dropping the last element by the size: unchanged when empty.

Array.pop

def Array.pop {A : Type} (a : Array A) : Array A

Removes the last element; the empty array stays empty.

Array.popSpecAt

def Array.popSpecAt {A : Type} (a : Array A) (n : Nat) (e : a.size = n) : Array.toList (Array.popAt a n e) = List.take (pred n) (Array.toList a)

The remove specification for each size.

Array.popSpec

def Array.popSpec {A : Type} (a : Array A) : Array.toList (Array.pop a) = List.take (pred a.size) (Array.toList a)

Removing the last element keeps all but the last of the elements.

Array.pushAll

def Array.pushAll {A : Type} (a : Array A) (xs : List A) : Array A

Appends every element of xs in order.

Array.ofList

def Array.ofList {A : Type} (xs : List A) : Array A

The array holding the elements of xs in order.

Array.pushAllSpec

def Array.pushAllSpec {A : Type} (a : Array A) (xs : List A) : Array.toList (Array.pushAll a xs) = append (Array.toList a) xs

Appending a list appends it to the elements.

Array.ofListSpec

def Array.ofListSpec {A : Type} (xs : List A) : Array.toList (Array.ofList xs) = xs

An array built from a list holds exactly that list.