Search.Auto

(source)

The content of this module is based on the paper
Auto in Agda - Programming proof search using reflection
by Wen Kokke and Wouter Swierstra

Definitions

data RuleName : Type

Totality: total
Visibility: public export
Constructors:

Free : Name -> RuleName
Bound : Nat -> RuleName

Hint:

Show RuleName

toName : RuleName -> Name

Totality: total
Visibility: export

data TermName : Type

Totality: total
Visibility: public export
Constructors:

UName : Name -> TermName
Bound : Nat -> TermName
Arrow : TermName

Hint:

Eq TermName

data Tm : Nat -> Type

  Proof search terms

Totality: total
Visibility: public export
Constructors:

Var : Fin n -> Tm n
Con : TermName -> List (Tm n) -> Tm n

showTerm : (ns : SnocList Name) -> Tm (length ns) -> String

Totality: total
Visibility: export

Env : (Nat -> Type) -> Nat -> Nat -> Type

Totality: total
Visibility: public export

rename : Env Fin m n -> Tm m -> Tm n

Totality: total
Visibility: export

subst : Env Tm m n -> Tm m -> Tm n

Totality: total
Visibility: export

split : Tm m -> (List (Tm m), Tm m)

Totality: total
Visibility: export

thin : Fin (S n) -> Fin n -> Fin (S n)

Totality: total
Visibility: export

thinInjective : (x : Fin (S n)) -> (y : Fin n) -> (z : Fin n) -> thin x y = thin x z -> y = z

Totality: total
Visibility: export

thinnedApart : (x : Fin (S n)) -> (y : Fin n) -> Not (thin x y = x)

Totality: total
Visibility: export

thinApart : (x : Fin (S n)) -> (y : Fin (S n)) -> Not (x = y) -> (y' : Fin n ** thin x y' = y)

Totality: total
Visibility: export

data Thicken : Fin n -> Fin n -> Type

Totality: total
Visibility: public export
Constructors:

EQ : Thicken x x
NEQ : (y : Fin n) -> Thicken x (thin x y)

thicken : (x : Fin n) -> (y : Fin n) -> Thicken x y

Totality: total
Visibility: export

check : Fin (S n) -> Tm (S n) -> Maybe (Tm n)

Totality: total
Visibility: export

for : Tm n -> Fin (S n) -> Env Tm (S n) n

Totality: total
Visibility: export

data AList : Nat -> Nat -> Type

Totality: total
Visibility: public export
Constructors:

Lin : AList m m
(:<) : AList m n -> (Fin (S m), Tm m) -> AList (S m) n

(++) : AList m n -> AList l m -> AList l n

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 7

toSubst : AList m n -> Env Tm m n

Totality: total
Visibility: export

mgu : Tm m -> Tm m -> Maybe (Unifying m)

Totality: total
Visibility: export

record Rule : Type

Totality: total
Visibility: export
Constructor:

MkRule : (context : SnocList Name) -> RuleName -> Vect arity (Tm (length context)) -> Tm (length context) -> Rule

Projections:

.arity : Rule -> Nat
.conclusion : ({rec:0} : Rule) -> Tm (length (context {rec:0}))
.context : Rule -> SnocList Name
.premises : ({rec:0} : Rule) -> Vect (arity {rec:0}) (Tm (length (context {rec:0})))
.ruleName : Rule -> RuleName

Hint:

Show Rule

.scope : Rule -> Nat

Totality: total
Visibility: export

HintDB : Type

Totality: total
Visibility: public export

data Space : Type -> Type

  A search Space represents the space of possible solutions to a problem.
  It is a finitely branching, potentially infinitely deep, tree.
  E.g. we can prove `Nat` using:
  1. either Z or S                  (finitely branching)
  2. arbitrarily many S constructor (unbounded depth)

Totality: total
Visibility: public export
Constructors:

Solution : a -> Space a
Candidates : List (Inf (Space a)) -> Space a

data Proof : Type

  A proof is a completed tree where each node is the invocation of a rule
  together with proofs for its premises, or a lambda abstraction with a
  subproof.

Totality: total
Visibility: public export
Constructors:

Call : RuleName -> List Proof -> Proof
Lam : Nat -> Proof -> Proof

Hint:

Show Proof

record PartialProof : Nat -> Type

  A partial proof is a vector of goals and a continuation which, provided
  a proof for each of the goals, returns a completed proof

Totality: total
Visibility: public export
Constructor:

MkPartialProof : (leftovers : Nat) -> Vect leftovers (Tm m) -> (Vect leftovers Proof -> Proof) -> PartialProof m

Projections:

.continuation : ({rec:0} : PartialProof m) -> Vect (leftovers {rec:0}) Proof -> Proof
.goals : ({rec:0} : PartialProof m) -> Vect (leftovers {rec:0}) (Tm m)
.leftovers : PartialProof m -> Nat

.leftovers : PartialProof m -> Nat

Totality: total
Visibility: public export

leftovers : PartialProof m -> Nat

Totality: total
Visibility: public export

.goals : ({rec:0} : PartialProof m) -> Vect (leftovers {rec:0}) (Tm m)

Totality: total
Visibility: public export

goals : ({rec:0} : PartialProof m) -> Vect (leftovers {rec:0}) (Tm m)

Totality: total
Visibility: public export

.continuation : ({rec:0} : PartialProof m) -> Vect (leftovers {rec:0}) Proof -> Proof

Totality: total
Visibility: public export

continuation : ({rec:0} : PartialProof m) -> Vect (leftovers {rec:0}) Proof -> Proof

Totality: total
Visibility: public export

apply : (r : Rule) -> Vect (r .arity + k) Proof -> Vect (S k) Proof

  Helper function to manufacture a proof step

Totality: total
Visibility: export

solve : Nat -> HintDB -> Tm m -> Space Proof

  Solve takes a database of hints, a goal to prove and returns
  the full search space.

Totality: total
Visibility: export

dfs : Nat -> Space a -> List a

  Depth first search strategy to explore a search space.
  This is made total by preemptively limiting the depth the search
  is willing to explore.

Totality: total
Visibility: export

convert : (0 f : (SnocList Name -> Nat)) -> ((vars : SnocList Name) -> Name -> Tm (f vars)) -> (vars : SnocList Name) -> TTImp -> Either TTImp (Tm (f vars))

  Converts a type of the form (a -> (a -> b -> c) -> b -> c)
  to our internal representation

Totality: total
Visibility: export

parseType : (0 f : (SnocList Name -> Nat)) -> ((vars : SnocList Name) -> Name -> Tm (f vars)) -> TTImp -> Either TTImp (vars : SnocList Name ** Tm (f vars))

  Parse a type of the form
  forall a b c. a -> (a -> b -> c) -> b -> c to
  1. a scope [<a,b,c]
  2. a representation of the rest

Totality: total
Visibility: export

parseRule : TTImp -> Either TTImp (vars : SnocList Name ** Tm (length vars))

  Parse a type, where bound variables are flexible variables

Totality: total
Visibility: export

parseGoal : TTImp -> Either TTImp (SnocList Name, Tm 0)

  Parse a type, where bound variables are rigid variables

Totality: total
Visibility: export

mkRule : Name -> Elab Rule

Totality: total
Visibility: export

getGoal : Elab (HintDB, Tm 0)

Totality: total
Visibility: export

unquote : Proof -> TTImp

Totality: total
Visibility: export

intros : List a -> TTImp -> TTImp

Totality: total
Visibility: export

bySearch : Nat -> HintDB -> Elab a

Totality: total
Visibility: export