ivor-0.1.8: Theorem proving library based on dependent type theory Source code Contents Index

Ivor.TT Portability non-portable Stability experimental Maintainer eb@dcs.st-and.ac.uk

Contents System state Exported view of terms Definitions and Theorems Pattern matching definitions Manipulating Proof State Examining the Context Goals, tactic types Primitive Tactics Basics Proof navigation Introductions Eliminations Conversions Equality Computations Staging Tactic combinators

Description

Public interface for theorem proving gadgets.

Synopsis

emptyContext :: Context data Context fastCheck :: Context -> ViewTerm -> Term checkCtxt :: (IsTerm a, Monad m) => Context -> Goal -> a -> m Term converts :: (Monad m, IsTerm a, IsTerm b) => Context -> Goal -> a -> b -> m Bool compile :: Context -> String -> IO () class IsTerm a where check :: Monad m => Context -> a -> m Term class IsData a where addData :: Monad m => Context -> a -> m Context addDataNoElim :: Monad m => Context -> a -> m Context addDef :: (IsTerm a, Monad m) => Context -> Name -> a -> m Context addTypedDef :: (IsTerm term, IsTerm ty, Monad m) => Context -> Name -> term -> ty -> m Context addAxiom :: (IsTerm a, Monad m) => Context -> Name -> a -> m Context declare :: (IsTerm a, Monad m) => Context -> Name -> a -> m Context declareData :: (IsTerm a, Monad m) => Context -> Name -> a -> m Context theorem :: (IsTerm a, Monad m) => Context -> Name -> a -> m Context interactive :: (IsTerm a, Monad m) => Context -> Name -> a -> m Context addPrimitive :: Monad m => Context -> Name -> m Context addBinOp :: (ViewConst a, ViewConst b, ViewConst c, IsTerm ty, Monad m) => Context -> Name -> (a -> b -> c) -> ty -> m Context addBinFn :: (ViewConst a, ViewConst b, IsTerm ty, Monad m) => Context -> Name -> (a -> b -> ViewTerm) -> ty -> m Context addPrimFn :: (ViewConst a, IsTerm ty, Monad m) => Context -> Name -> (a -> ViewTerm) -> ty -> m Context addExternalFn :: (IsTerm ty, Monad m) => Context -> Name -> Int -> ([ViewTerm] -> Maybe ViewTerm) -> ty -> m Context addEquality :: Monad m => Context -> Name -> Name -> m Context forgetDef :: Monad m => Context -> Name -> m Context addGenRec :: Monad m => Context -> Name -> m Context addImplicit :: Context -> ViewTerm -> (Int, ViewTerm) data PClause = PClause { arguments :: [ViewTerm] returnval :: ViewTerm } data Patterns = Patterns [PClause] data PattOpt = Partial | GenRec | Holey addPatternDef :: (IsTerm ty, Monad m) => Context -> Name -> ty -> Patterns -> [PattOpt] -> m (Context, [(Name, ViewTerm)]) toPattern :: Context -> ViewTerm -> ViewTerm proving :: Context -> Bool numUnsolved :: Context -> Int suspend :: Context -> Context resume :: Monad m => Context -> Name -> m Context save :: Context -> Context restore :: Monad m => Context -> m Context clearSaved :: Context -> Context proofterm :: Monad m => Context -> m Term getGoals :: Context -> [Goal] getGoal :: Monad m => Context -> Goal -> m ([(Name, Term)], Term) uniqueName :: Monad m => Context -> Name -> m Name allSolved :: Context -> Bool qed :: Monad m => Context -> m Context eval :: Context -> Term -> Term whnf :: Context -> Term -> Term evalnew :: Context -> Term -> Term evalCtxt :: (IsTerm a, Monad m) => Context -> Goal -> a -> m Term getDef :: Monad m => Context -> Name -> m Term defined :: Context -> Name -> Bool getPatternDef :: Monad m => Context -> Name -> m (ViewTerm, Patterns) getAllTypes :: Context -> [(Name, Term)] getAllDefs :: Context -> [(Name, Term)] getAllPatternDefs :: Context -> [(Name, (ViewTerm, Patterns))] getConstructors :: Monad m => Context -> Name -> m [Name] getInductive :: Monad m => Context -> Name -> m Inductive getAllInductives :: Context -> [(Name, Inductive)] getType :: Monad m => Context -> Name -> m Term data Rule = Case | Elim getElimRule :: Monad m => Context -> Name -> Rule -> m Patterns nameType :: Monad m => Context -> Name -> m NameType getConstructorTag :: Monad m => Context -> Name -> m Int getConstructorArity :: Monad m => Context -> Name -> m Int freeze :: Monad m => Context -> Name -> m Context thaw :: Monad m => Context -> Name -> m Context data Goal goal :: String -> Goal defaultGoal :: Goal type Tactic = forall m. Monad m => Goal -> Context -> m Context data GoalData bindings :: GoalData -> [(Name, Term)] goalName :: GoalData -> Goal goalType :: GoalData -> Term goalData :: Monad m => Context -> Bool -> Goal -> m GoalData subGoals :: Monad m => Context -> m [(Name, Term)] intro :: Tactic introName :: Name -> Tactic intros :: Tactic intros1 :: Tactic introsNames :: [Name] -> Tactic addArg :: IsTerm a => Name -> a -> Tactic generalise :: IsTerm a => a -> Tactic dependentGeneralise :: IsTerm a => a -> Tactic claim :: IsTerm a => Name -> a -> Tactic focus :: Tactic rename :: Name -> Tactic attack :: Tactic attackWith :: Name -> Tactic solve :: Tactic trySolve :: Tactic keepSolving :: Tactic abandon :: Tactic hide :: Tactic fill :: IsTerm a => a -> Tactic refine :: IsTerm a => a -> Tactic basicRefine :: IsTerm a => a -> Tactic refineWith :: IsTerm a => a -> [a] -> Tactic trivial :: Tactic axiomatise :: Name -> [Name] -> Tactic by :: IsTerm a => a -> Tactic induction :: IsTerm a => a -> Tactic cases :: IsTerm a => a -> Tactic equiv :: IsTerm a => a -> Tactic compute :: Tactic beta :: Tactic unfold :: Name -> Tactic replace :: (IsTerm a, IsTerm b, IsTerm c, IsTerm d) => a -> b -> c -> d -> Bool -> Tactic call :: IsTerm a => a -> Tactic returnComputation :: Tactic quoteVal :: Tactic idTac :: Tactic tacs :: Monad m => [Goal -> Context -> m Context] -> Goal -> Context -> m Context (>->) :: Tactic -> Tactic -> Tactic (>=>) :: Tactic -> Tactic -> Tactic (>+>) :: Tactic -> Tactic -> Tactic (>|>) :: Tactic -> Tactic -> Tactic try :: Tactic -> Tactic -> Tactic -> Tactic traceTac :: Tactic

System state

emptyContext :: Context Source

Initialise a context, with no data or definitions and an empty proof state.

data Context Source

Abstract type representing state of the system.

fastCheck :: Context -> ViewTerm -> Term Source

Quickly convert a ViewTerm into a real Term. This is dangerous; you must know that typechecking will succeed, and the resulting term won't have a valid type, but you will be able to run it. This is useful if you simply want to do a substitution into a ViewTerm.

checkCtxt :: (IsTerm a, Monad m) => Context -> Goal -> a -> m Term Source

Check a term in the context of the given goal

converts :: (Monad m, IsTerm a, IsTerm b) => Context -> Goal -> a -> b -> m Bool Source

Check whether the conversion relation holds between two terms, in the context of the given goal

compile Source

:: Context context to compile -> String root of filenames to generate -> IO () Create a .hs file containing (unreadable) Haskell code implementing all of the definitions. (TODO: Generate a more readable, usable interface)

Exported view of terms

class IsTerm a where Source

Methods check :: Monad m => Context -> a -> m Term Source Typecheck a term Instances IsTerm String IsTerm Raw IsTerm ViewTerm IsTerm Term

class IsData a where Source

Methods addData :: Monad m => Context -> a -> m Context Source addDataNoElim :: Monad m => Context -> a -> m Context Source Instances IsData String IsData Inductive

Definitions and Theorems

addDef :: (IsTerm a, Monad m) => Context -> Name -> a -> m Context Source

Add a new definition to the global state.

addTypedDef :: (IsTerm term, IsTerm ty, Monad m) => Context -> Name -> term -> ty -> m Context Source

Add a new definition, with its type to the global state. These definitions can be recursive, so use with care.

addAxiom :: (IsTerm a, Monad m) => Context -> Name -> a -> m Context Source

Add a new axiom to the global state.

declare :: (IsTerm a, Monad m) => Context -> Name -> a -> m Context Source

Declare a name which is to be defined later

declareData :: (IsTerm a, Monad m) => Context -> Name -> a -> m Context Source

Declare a type constructor which is to be defined later

theorem :: (IsTerm a, Monad m) => Context -> Name -> a -> m Context Source

Begin a new proof.

interactive :: (IsTerm a, Monad m) => Context -> Name -> a -> m Context Source

Begin a new interactive definition. Actually, just the same as theorem but this version allows you to make recursive calls, which should of course be done with care.

addPrimitive Source

:: Monad m => Context -> Name Type name -> m Context Add a new primitive type. This should be done in assocation with creating an instance of ViewConst for the type, and creating appropriate primitive functions.

addBinOp :: (ViewConst a, ViewConst b, ViewConst c, IsTerm ty, Monad m) => Context -> Name -> (a -> b -> c) -> ty -> m Context Source

Add a new binary operator on constants. Warning: The type you give is not checked!

addBinFn :: (ViewConst a, ViewConst b, IsTerm ty, Monad m) => Context -> Name -> (a -> b -> ViewTerm) -> ty -> m Context Source

Add a new binary function on constants. Warning: The type you give is not checked!

addPrimFn :: (ViewConst a, IsTerm ty, Monad m) => Context -> Name -> (a -> ViewTerm) -> ty -> m Context Source

Add a new primitive function on constants, usually used for converting to some form which can be examined in the type theory itself. Warning: The type you give is not checked!

addExternalFn Source

:: (IsTerm ty, Monad m) => Context -> Name -> Int arity -> [ViewTerm] -> Maybe ViewTerm The function, which must accept a list of the right length given by arity. -> ty -> m Context Add a new externally defined function. Warning: The type you give is not checked!

addEquality Source

:: Monad m => Context -> Name Name to give equality type -> Name Name to give constructor -> m Context Add the heterogenous ("John Major") equality rule and its reduction

forgetDef :: Monad m => Context -> Name -> m Context Source

Forget a definition and all following definitions.

addGenRec Source

:: Monad m => Context -> Name Name to give recursion rule -> m Context Add the general recursion elimination rule, thus making all further definitions untrustworthy :).

addImplicit :: Context -> ViewTerm -> (Int, ViewTerm) Source

Add implicit binders for names used in a type, but not declared. |Returns the new type and the number of implicit names bound.

Pattern matching definitions

data PClause Source

Constructors PClause arguments :: [ViewTerm] returnval :: ViewTerm Instances Show PClause

data Patterns Source

Constructors Patterns [PClause] Instances Show Patterns

data PattOpt Source

Constructors Partial No need to cover all cases GenRec No termination checking Holey Allow metavariables in the definition, which will become theorems which need to be proved. Instances Eq PattOpt

addPatternDef Source

:: (IsTerm ty, Monad m) => Context -> Name -> ty Type -> Patterns Definition -> [PattOpt] Options to set which definitions will be accepted -> m (Context, [(Name, ViewTerm)]) Add a new definition to the global state. By default, these definitions must cover all cases and be well-founded, but can be optionally partial or general recursive. Returns the new context, and a list of names which need to be defined to complete the definition.

toPattern :: Context -> ViewTerm -> ViewTerm Source

Manipulating Proof State

proving :: Context -> Bool Source

Return whether we are in the middle of proving something.

numUnsolved :: Context -> Int Source

Get the number of unsolved goals

suspend :: Context -> Context Source

Suspend the current proof. Clears the current proof state; use resume to continue the proof.

resume :: Monad m => Context -> Name -> m Context Source

Resume an unfinished proof, suspending the current one if necessary. Fails if there is no such name. Can also be used to begin a proof of an identifier previously claimed as an axiom. Remember that you will need to attack the goal if you are resuming an axiom.

save :: Context -> Context Source

Save the state (e.g. for Undo)

restore :: Monad m => Context -> m Context Source

Restore a saved state; fails if none have been saved.

clearSaved :: Context -> Context Source

Clears the saved state (e.g. if undo no longer makes sense, like when a proof has been completed)

proofterm :: Monad m => Context -> m Term Source

Get the current proof term, if we are in the middle of a proof.

getGoals :: Context -> [Goal] Source

Get the goals still to be solved.

getGoal :: Monad m => Context -> Goal -> m ([(Name, Term)], Term) Source

Get the type and context of the given goal, if it exists

uniqueName Source

:: Monad m => Context -> Name Suggested name -> m Name Unique name based on suggested name Create a name unique in the proof state

allSolved :: Context -> Bool Source

Return whether all goals have been solved.

qed :: Monad m => Context -> m Context Source

Lift a finished proof into the context

Examining the Context

eval :: Context -> Term -> Term Source

Normalise a term and its type (using old evaluator_

whnf :: Context -> Term -> Term Source

Reduce a term and its type to Weak Head Normal Form

evalnew :: Context -> Term -> Term Source

Reduce a term and its type to Normal Form (using new evaluator)

evalCtxt :: (IsTerm a, Monad m) => Context -> Goal -> a -> m Term Source

Evaluate a term in the context of the given goal

getDef :: Monad m => Context -> Name -> m Term Source

Lookup a definition in the context.

defined :: Context -> Name -> Bool Source

Check whether a name is defined

getPatternDef :: Monad m => Context -> Name -> m (ViewTerm, Patterns) Source

Lookup a pattern matching definition in the context. Return the type and the pattern definition.

getAllTypes :: Context -> [(Name, Term)] Source

Get all the names and types in the context

getAllDefs :: Context -> [(Name, Term)] Source

getAllPatternDefs :: Context -> [(Name, (ViewTerm, Patterns))] Source

Get all the pattern matching definitions in the context. Also returns CAFs (i.e. 0 argument functions)

getConstructors :: Monad m => Context -> Name -> m [Name] Source

Get the names of all of the constructors of an inductive family

getInductive :: Monad m => Context -> Name -> m Inductive Source

Return the data type with the given name. Note that this knows nothing about the difference between parameters and indices; that information is discarded after the elimination rule is constructed.

getAllInductives :: Context -> [(Name, Inductive)] Source

Get all the inductive type definitions in the context.

getType :: Monad m => Context -> Name -> m Term Source

Get the type of a definition in the context.

data Rule Source

Types of elimination rule Constructors Case Elim

getElimRule Source

:: Monad m => Context -> Name Type -> Rule Which rule to get patterns for (case or elim) -> m Patterns Get the pattern matching elimination rule for a type

nameType :: Monad m => Context -> Name -> m NameType Source

Find out what type of variable the given name is

getConstructorTag :: Monad m => Context -> Name -> m Int Source

Get an integer tag for a constructor. Each constructor has a tag unique within the data type, which could be used by a compiler.

getConstructorArity :: Monad m => Context -> Name -> m Int Source

Get the arity of the given constructor.

freeze :: Monad m => Context -> Name -> m Context Source

Freeze a name (i.e., set it so that it does not reduce) Fails if the name does not exist.

thaw :: Monad m => Context -> Name -> m Context Source

Unfreeze a name (i.e., allow it to reduce). Fails if the name does not exist.

Goals, tactic types

data Goal Source

Abstract type representing goal or subgoal names. Instances Eq Goal Show Goal

goal :: String -> Goal Source

defaultGoal :: Goal Source

type Tactic = forall m. Monad m => Goal -> Context -> m Context Source

A tactic is any function which manipulates a term at the given goal binding. Tactics may fail, hence the monad.

data GoalData Source

Environment and goal type for a given subgoal

bindings :: GoalData -> [(Name, Term)] Source

Get the premises of the goal

goalName :: GoalData -> Goal Source

Get the name of the goal

goalType :: GoalData -> Term Source

Get the type of the goal

goalData Source

:: Monad m => Context -> Bool Get all bindings (True), or just lambda bindings (False) -> Goal -> m GoalData Get information about a subgoal.

subGoals :: Monad m => Context -> m [(Name, Term)] Source

Get the names and types of all goals

Primitive Tactics

Basics

intro :: Tactic Source

Introduce an assumption (i.e. a lambda binding)

introName Source

:: Name Name for the assumption -> Tactic Introduce an assumption (i.e. a lambda binding)

intros :: Tactic Source

Keep introducing things until there's nothing left to introduce.

intros1 :: Tactic Source

Keep introducing things until there's nothing left to introduce, Must introduce at least one thing.

introsNames :: [Name] -> Tactic Source

As intros, but with names, and stop when we've run out of names. Fails if too many names are given.

addArg :: IsTerm a => Name -> a -> Tactic Source

Add a new top level argument after the arguments its type depends on (changing the type of the theorem). This can be useful if, for example, you find you need an extra premise to prove a goal.

generalise :: IsTerm a => a -> Tactic Source

Abstract over the given term in the goal.

dependentGeneralise :: IsTerm a => a -> Tactic Source

Abstract over the given term in the goal, and also all variables appearing in the goal whose types depend on it.

claim :: IsTerm a => Name -> a -> Tactic Source

Make a local claim

Proof navigation

focus :: Tactic Source

Focus on a different hole, i.e. set the default goal.

rename :: Name -> Tactic Source

Rename the outermost binder in the given goal

attack :: Tactic Source

Prepare a goal for introduction.

attackWith Source

:: Name Name for new goal -> Tactic Prepare a goal for introduction.

solve :: Tactic Source

Finalise a goal's solution.

trySolve :: Tactic Source

If the goal has a solution, finalise it, otherwise prepare the goal (with attack). Typically, could be used on the subgoals generated by refinement, where some may have solutions attached already, and others will need to be prepared.

keepSolving :: Tactic Source

Finalise as many solutions of as many goals as possible.

abandon :: Tactic Source

Remove a solution from a goal.

hide :: Tactic Source

Hide a premise

Introductions

fill :: IsTerm a => a -> Tactic Source

Attach a solution to a goal.

refine :: IsTerm a => a -> Tactic Source

Solve a goal by applying a function. If the term given has arguments, attempts to fill in these arguments by unification and solves them (with solve). See refineWith and basicRefine for slight variations.

basicRefine :: IsTerm a => a -> Tactic Source

Solve a goal by applying a function. If the term given has arguments, this will create a subgoal for each. Some arguments may be solved by unification, in which case they will already have a guess attached after refinement, but the guess will not be solved (via solve).

refineWith :: IsTerm a => a -> [a] -> Tactic Source

Solve a goal by applying a function with some arguments filled in. See refine for details.

trivial :: Tactic Source

Find a trivial solution to the goal by searching through the context for a premise which solves it immediately by refinement

axiomatise Source

:: Name Name to give axiom -> [Name] Premises to pass to axiom -> Tactic Add an axiom to the global context which would solve the goal, and apply it. FIXME: This tactic doesn't pick up all dependencies on types, but is okay for simply typed axioms, e.g. equations on Nats.

Eliminations

by Source

:: IsTerm a => a An elimination rule applied to a target. -> Tactic Apply an eliminator.

induction Source

:: IsTerm a => a target of the elimination -> Tactic Apply the appropriate induction rule to the term.

cases Source

:: IsTerm a => a target of the case analysis -> Tactic Apply the appropriate case analysis rule to the term. Like induction, but no induction hypotheses generated.

Conversions

equiv :: IsTerm a => a -> Tactic Source

Check that the goal is definitionally equal to the given term, and rewrite the goal accordingly.

compute :: Tactic Source

Normalise the goal

beta :: Tactic Source

Beta reduce in the goal

unfold :: Name -> Tactic Source

Beta reduce the goal, unfolding the given function

Equality

replace Source

:: (IsTerm a, IsTerm b, IsTerm c, IsTerm d) => a Equality type (e.g. Eq : (A:*)(a:A)(b:A)*) -> b replacement lemma (e.g. repl : (A:*)(a:A)(b:A)(q:Eq _ a b)(P:(a:A)*)(p:P a)(P b)) -> c symmetry lemma (e.g. sym : (A:*)(a:A)(b:A)(p:Eq _ a b)(Eq _ b a)) -> d equality premise -> Bool apply premise backwards (i.e. apply symmetry) -> Tactic Replace a term in the goal according to an equality premise. Any equality type with three arguments is acceptable (i.e. the type, and the two values), provided there are suitable replacement and symmetry lemmas. Heterogeneous equality as provided by addEquality is acceptable (if you provide the lemmas!).

Computations

call :: IsTerm a => a -> Tactic Source

Make a recursive call of a computation. The term must be an allowed recursive call, identified in the context by having a labelled type.

returnComputation :: Tactic Source

Prepare to return a value in a computation

Staging

quoteVal :: Tactic Source

Prepare to return a quoted value

Tactic combinators

idTac :: Tactic Source

The Identity tactic, does nothing.

tacs :: Monad m => [Goal -> Context -> m Context] -> Goal -> Context -> m Context Source

Apply a sequence of tactics to the default goal. Read the type as [Tactic] -> Tactic

(>->) :: Tactic -> Tactic -> Tactic Source

Sequence two tactics; applies two tactics sequentially to the same goal

(>=>) :: Tactic -> Tactic -> Tactic Source

Apply a tactic, then apply another to each subgoal generated.

(>+>) :: Tactic -> Tactic -> Tactic Source

Apply a tactic, then apply the next tactic to the next default subgoal.

(>|>) :: Tactic -> Tactic -> Tactic Source

Tries the left tactic, if that fails try the right one. Shorthand for try x idTac y.

try Source

:: Tactic Tactic to apply -> Tactic Apply if first tactic succeeds -> Tactic Apply if first tactic fails. -> Tactic Try a tactic.

traceTac :: Tactic Source

The Tracing tactic; does nothing, but uses trace to dump the current proof state

Produced by Haddock version 2.4.2