|
Ivor.TT | Portability | non-portable | Stability | experimental | Maintainer | eb@dcs.st-and.ac.uk |
|
|
|
|
|
Description |
Public interface for theorem proving gadgets.
|
|
Synopsis |
|
emptyContext :: Context | | data Context | | fastCheck :: Context -> ViewTerm -> Term | | checkCtxt :: IsTerm a => Context -> Goal -> a -> TTM Term | | converts :: (IsTerm a, IsTerm b) => Context -> Goal -> a -> b -> TTM Bool | | compile :: Context -> String -> IO () | | class IsTerm a where | | | class IsData a where | | | | | ttfail :: String -> TTM a | | getError :: IError -> TTError | | type TTM = Either TTError | | addDef :: IsTerm a => Context -> Name -> a -> TTM Context | | addTypedDef :: (IsTerm term, IsTerm ty) => Context -> Name -> term -> ty -> TTM Context | | addAxiom :: IsTerm a => Context -> Name -> a -> TTM Context | | declare :: IsTerm a => Context -> Name -> a -> TTM Context | | declareData :: IsTerm a => Context -> Name -> a -> TTM Context | | theorem :: IsTerm a => Context -> Name -> a -> TTM Context | | interactive :: IsTerm a => Context -> Name -> a -> TTM Context | | addPrimitive :: Context -> Name -> TTM Context | | addBinOp :: (ViewConst a, ViewConst b, ViewConst c, IsTerm ty) => Context -> Name -> (a -> b -> c) -> ty -> TTM Context | | addBinFn :: (ViewConst a, ViewConst b, IsTerm ty) => Context -> Name -> (a -> b -> ViewTerm) -> ty -> TTM Context | | addPrimFn :: (ViewConst a, IsTerm ty) => Context -> Name -> (a -> ViewTerm) -> ty -> TTM Context | | addExternalFn :: IsTerm ty => Context -> Name -> Int -> ([ViewTerm] -> Maybe ViewTerm) -> ty -> TTM Context | | addEquality :: Context -> Name -> Name -> TTM Context | | forgetDef :: Context -> Name -> TTM Context | | addGenRec :: Context -> Name -> TTM Context | | addImplicit :: Context -> ViewTerm -> (Int, ViewTerm) | | | | data Patterns = Patterns [PClause] | | | | addPatternDef :: IsTerm ty => Context -> Name -> ty -> Patterns -> [PattOpt] -> TTM (Context, [(Name, ViewTerm)]) | | toPattern :: Context -> ViewTerm -> ViewTerm | | proving :: Context -> Bool | | numUnsolved :: Context -> Int | | suspend :: Context -> Context | | resume :: Context -> Name -> TTM Context | | save :: Context -> Context | | restore :: Context -> TTM Context | | clearSaved :: Context -> Context | | proofterm :: Context -> TTM Term | | getGoals :: Context -> [Goal] | | getGoal :: Context -> Goal -> TTM ([(Name, Term)], Term) | | uniqueName :: Context -> Name -> TTM Name | | allSolved :: Context -> Bool | | qed :: Context -> TTM Context | | eval :: Context -> Term -> Term | | whnf :: Context -> Term -> Term | | evalnew :: Context -> Term -> Term | | evalnewWithout :: Context -> Term -> [Name] -> Term | | evalnewLimit :: Context -> Term -> [(Name, Int)] -> Term | | evalCtxt :: IsTerm a => Context -> Goal -> a -> TTM Term | | getDef :: Context -> Name -> TTM Term | | defined :: Context -> Name -> Bool | | getPatternDef :: Context -> Name -> TTM (ViewTerm, Patterns) | | getAllTypes :: Context -> [(Name, Term)] | | getAllDefs :: Context -> [(Name, Term)] | | getAllPatternDefs :: Context -> [(Name, (ViewTerm, Patterns))] | | isAuxPattern :: Context -> Name -> Bool | | getConstructors :: Context -> Name -> TTM [Name] | | getInductive :: Context -> Name -> TTM Inductive | | getAllInductives :: Context -> [(Name, Inductive)] | | getType :: Context -> Name -> TTM Term | | | | getElimRule :: Context -> Name -> Rule -> TTM Patterns | | nameType :: Context -> Name -> TTM NameType | | getConstructorTag :: Context -> Name -> TTM Int | | getConstructorArity :: Context -> Name -> TTM Int | | freeze :: Context -> Name -> TTM Context | | thaw :: Context -> Name -> TTM Context | | data Goal | | goal :: String -> Goal | | defaultGoal :: Goal | | type Tactic = Goal -> Context -> TTM Context | | data GoalData | | bindings :: GoalData -> [(Name, Term)] | | goalName :: GoalData -> Goal | | goalType :: GoalData -> Term | | goalData :: Context -> Bool -> Goal -> TTM GoalData | | subGoals :: Context -> TTM [(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 :: [Goal -> Context -> TTM Context] -> Goal -> Context -> TTM Context | | (>->) :: Tactic -> Tactic -> Tactic | | (>=>) :: Tactic -> Tactic -> Tactic | | (>+>) :: Tactic -> Tactic -> Tactic | | (>|>) :: Tactic -> Tactic -> Tactic | | try :: Tactic -> Tactic -> Tactic -> Tactic | | traceTac :: Tactic |
|
|
|
System state
|
|
|
Initialise a context, with no data or definitions and an
empty proof state.
|
|
|
Abstract type representing state of the system.
|
|
|
|
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.
|
|
|
Check a term in the context of the given goal
|
|
|
Check whether the conversion relation holds between two terms, in the
context of the given goal
|
|
|
:: 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
|
|
|
| Methods | | | Instances | |
|
|
|
| Methods | | | Instances | |
|
|
Errors
|
|
|
Constructors | | Instances | |
|
|
|
|
|
|
|
|
Definitions and Theorems
|
|
|
Add a new definition to the global state.
|
|
|
Add a new definition, with its type to the global state.
These definitions can be recursive, so use with care.
|
|
|
Add a new axiom to the global state.
|
|
|
Declare a name which is to be defined later
|
|
|
Declare a type constructor which is to be defined later
|
|
|
Begin a new proof.
|
|
|
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.
|
|
|
:: Context | | -> Name | Type name
| -> TTM 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.
|
|
|
|
Add a new binary operator on constants. Warning: The type you give
is not checked!
|
|
|
Add a new binary function on constants. Warning: The type you give
is not checked!
|
|
|
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!
|
|
|
|
|
|
:: Context | | -> Name | Name to give equality type
| -> Name | Name to give constructor
| -> TTM Context | | Add the heterogenous ("John Major") equality rule and its reduction
|
|
|
|
Forget a definition and all following definitions.
|
|
|
:: Context | | -> Name | Name to give recursion rule
| -> TTM Context | | Add the general recursion elimination rule, thus making all further
definitions untrustworthy :).
|
|
|
|
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
|
|
|
Constructors | | Instances | |
|
|
|
Constructors | | Instances | |
|
|
|
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 | |
|
|
|
:: IsTerm ty | | => Context | | -> Name | Type
| -> ty | Definition
| -> Patterns | Options to set which definitions will be accepted
| -> [PattOpt] | | -> TTM (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.
|
|
|
|
|
Manipulating Proof State
|
|
|
Return whether we are in the middle of proving something.
|
|
|
Get the number of unsolved goals
|
|
|
Suspend the current proof. Clears the current proof state; use resume
to continue the proof.
|
|
|
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 the state (e.g. for Undo)
|
|
|
Restore a saved state; fails if none have been saved.
|
|
|
Clears the saved state (e.g. if undo no longer makes sense, like when
a proof has been completed)
|
|
|
Get the current proof term, if we are in the middle of a proof.
|
|
|
Get the goals still to be solved.
|
|
|
Get the type and context of the given goal, if it exists
|
|
|
:: Context | | -> Name | Suggested name
| -> TTM Name | Unique name based on suggested name
| Create a name unique in the proof state
|
|
|
|
Return whether all goals have been solved.
|
|
|
Lift a finished proof into the context
|
|
Examining the Context
|
|
|
Normalise a term and its type (using old evaluator_
|
|
|
Reduce a term and its type to Weak Head Normal Form
|
|
|
Reduce a term and its type to Normal Form (using new evaluator)
|
|
|
Reduce a term and its type to Normal Form (using new evaluator, not
reducing given names)
|
|
|
Reduce a term and its type to Normal Form (using new evaluator, reducing
given names a maximum number of times)
|
|
|
Evaluate a term in the context of the given goal
|
|
|
Lookup a definition in the context.
|
|
|
Check whether a name is defined
|
|
|
Lookup a pattern matching definition in the context. Return the
type and the pattern definition.
|
|
|
Get all the names and types in the context
|
|
|
|
|
Get all the pattern matching definitions in the context.
Also returns CAFs (i.e. 0 argument functions)
|
|
|
Is the name an auxiliary function of a pattern definition (e.g. generated by a with
clause?
|
|
|
Get the names of all of the constructors of an inductive family
|
|
|
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.
|
|
|
Get all the inductive type definitions in the context.
|
|
|
Get the type of a definition in the context.
|
|
|
Types of elimination rule
| Constructors | |
|
|
|
:: Context | | -> Name | Type
| -> Rule | Which rule to get patterns for (case or elim)
| -> TTM Patterns | | Get the pattern matching elimination rule for a type
|
|
|
|
Find out what type of variable the given name is
|
|
|
Get an integer tag for a constructor. Each constructor has a tag
unique within the data type, which could be used by a compiler.
|
|
|
Get the arity of the given constructor.
|
|
|
Freeze a name (i.e., set it so that it does not reduce)
Fails if the name does not exist.
|
|
|
Unfreeze a name (i.e., allow it to reduce).
Fails if the name does not exist.
|
|
Goals, tactic types
|
|
|
Abstract type representing goal or subgoal names.
| Instances | |
|
|
|
|
|
|
|
A tactic is any function which manipulates a term at the given goal
binding. Tactics may fail, hence the monad.
|
|
|
Environment and goal type for a given subgoal
|
|
|
|
Get the premises of the goal
|
|
|
Get the name of the goal
|
|
|
Get the type of the goal
|
|
|
|
|
|
Get the names and types of all goals
|
|
Primitive Tactics
|
|
Basics
|
|
|
Introduce an assumption (i.e. a lambda binding)
|
|
|
:: Name | Name for the assumption
| -> Tactic | | Introduce an assumption (i.e. a lambda binding)
|
|
|
|
Keep introducing things until there's nothing left to introduce.
|
|
|
Keep introducing things until there's nothing left to introduce,
Must introduce at least one thing.
|
|
|
As intros, but with names, and stop when we've run out of names.
Fails if too many names are given.
|
|
|
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.
|
|
|
Abstract over the given term in the goal.
|
|
|
Abstract over the given term in the goal, and also all variables
appearing in the goal whose types depend on it.
|
|
|
Make a local claim
|
|
Proof navigation
|
|
|
Focus on a different hole, i.e. set the default goal.
|
|
|
Rename the outermost binder in the given goal
|
|
|
Prepare a goal for introduction.
|
|
|
:: Name | Name for new goal
| -> Tactic | | Prepare a goal for introduction.
|
|
|
|
Finalise a goal's solution.
|
|
|
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.
|
|
|
Finalise as many solutions of as many goals as possible.
|
|
|
Remove a solution from a goal.
|
|
|
Hide a premise
|
|
Introductions
|
|
|
Attach a solution to a goal.
|
|
|
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.
|
|
|
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).
|
|
|
Solve a goal by applying a function with some arguments filled in.
See refine for details.
|
|
|
Find a trivial solution to the goal by searching through the context
for a premise which solves it immediately by refinement
|
|
|
:: 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
|
|
|
|
|
|
:: IsTerm a | | => a | | -> Tactic | | Apply the appropriate induction rule to the term.
|
|
|
|
:: IsTerm a | | => a | | -> Tactic | | Apply the appropriate case analysis rule to the term.
Like induction, but no induction hypotheses generated.
|
|
|
Conversions
|
|
|
Check that the goal is definitionally equal to the given term,
and rewrite the goal accordingly.
|
|
|
Normalise the goal
|
|
|
Beta reduce in the goal
|
|
|
Beta reduce the goal, unfolding the given function
|
|
Equality
|
|
|
:: (IsTerm a, IsTerm b, IsTerm c, IsTerm d) | | => a | replacement lemma (e.g. repl : (A:*)(a:A)(b:A)(q:Eq _ a b)(P:(a:A)*)(p:P a)(P b))
| -> b | symmetry lemma (e.g. sym : (A:*)(a:A)(b:A)(p:Eq _ a b)(Eq _ b a))
| -> c | equality premise
| -> d | apply premise backwards (i.e. apply symmetry)
| -> Bool | | -> 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
|
|
|
Make a recursive call of a computation. The term must be an
allowed recursive call, identified in the context by having a
labelled type.
|
|
|
Prepare to return a value in a computation
|
|
Staging
|
|
|
Prepare to return a quoted value
|
|
Tactic combinators
|
|
|
The Identity tactic, does nothing.
|
|
|
Apply a sequence of tactics to the default goal. Read the type
as [Tactic] -> Tactic
|
|
|
Sequence two tactics; applies two tactics sequentially to the same goal
|
|
|
Apply a tactic, then apply another to each subgoal generated.
|
|
|
Apply a tactic, then apply the next tactic to the next default subgoal.
|
|
|
Tries the left tactic, if that fails try the right one. Shorthand for
try x idTac y.
|
|
|
:: Tactic | Tactic to apply
| -> Tactic | Apply if first tactic succeeds
| -> Tactic | Apply if first tactic fails.
| -> Tactic | | Try a tactic.
|
|
|
|
The Tracing tactic; does nothing, but uses trace to dump the
current proof state
|
|
Produced by Haddock version 2.6.0 |