Data.ProofDelay

The contents of this module are based on the paper
Deferring the Details and Deriving Programs
by Liam O'Connor
https://doi.org/10.1145/3331554.3342605

Definitions

record PDelay : Type -> Type

  A type `x` which can only be computed once some, delayed, proof obligations
  have been fulfilled.

Totality: total
Visibility: public export
Constructor: 

Prf : (goals : List Type) -> (HList goals -> x) -> PDelay x

Projections:

.goals : PDelay x -> List Type

  List of propositions we need to prove.

.prove : ({rec:0} : PDelay x) -> HList (goals {rec:0}) -> x

  Given the proofs required (i.e. the goals), actually compute the value x.

.goals : PDelay x -> List Type

  List of propositions we need to prove.

Totality: total
Visibility: public export

goals : PDelay x -> List Type

  List of propositions we need to prove.

Totality: total
Visibility: public export

.prove : ({rec:0} : PDelay x) -> HList (goals {rec:0}) -> x

  Given the proofs required (i.e. the goals), actually compute the value x.

Totality: total
Visibility: public export

prove : ({rec:0} : PDelay x) -> HList (goals {rec:0}) -> x

  Given the proofs required (i.e. the goals), actually compute the value x.

Totality: total
Visibility: public export

pure : tx -> PDelay tx

  A value which can immediately be constructed (i.e. no delayed proofs).

Totality: total
Visibility: public export

later : PDelay tx

  Delay the full computation of `x` until `later`.

Totality: total
Visibility: public export

(<*>) : PDelay (a -> b) -> PDelay a -> PDelay b

  We can compose `PDelay` computations.

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 3

data OList : Nat -> Nat -> Type

  An ordered list type.
  
  [27](https://dl.acm.org/doi/10.1145/2503778.2503786)

Totality: total
Visibility: public export
Constructors:

Nil : LTE m n -> OList m n

Cons : (x : Nat) -> LTE m x -> OList x n -> OList m n

data BST : Nat -> Nat -> Type

  A binary search tree carrying proofs of the ordering in the leaves.
  
  [31](https://dl.acm.org/doi/10.1145/2628136.2628163)

Totality: total
Visibility: public export
Constructors:

Leaf : LTE m n -> BST m n

Branch : (x : Nat) -> BST m x -> BST x n -> BST m n

nil : PDelay (OList m n)

  OList `Nil`, but delaying the proof obligation.

Totality: total
Visibility: public export

cons : (x : Nat) -> PDelay (OList x n) -> PDelay (OList m n)

  OList `Cons`, but delaying the proof obligations.

Totality: total
Visibility: public export

example : OList 1 5

  Extracting an actual `OList` from the delayed version requires providing the
  unergonomic proofs.

Totality: total
Visibility: public export

leaf : PDelay (BST m n)

  BST `Leaf`, but delaying the proof obligation.

Totality: total
Visibility: public export

branch : (x : Nat) -> PDelay (BST m x) -> PDelay (BST x n) -> PDelay (BST m n)

  BST `Branch`, but delaying the proof obligations.

Totality: total
Visibility: public export

example2 : BST 2 10

  Once again, extracting the actual `BST` requires providing the uninteresting
  proofs.

Totality: total
Visibility: public export