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
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
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
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.
 :: 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!
 :: (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!
 :: 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.
 :: 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
 :: (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
 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