Safe Haskell  None 

This package aims to perform the fiddly details of instantiating induction
schemas for algebraic data types. The library is parameterised over
the type of variables (v
), constructors (c
) and types (t
).
Let's see how it looks if you instantiate all these three with String and want
to do induction over natural numbers. First, one needs to create a type
environment, a TyEnv
. For every type (we only have one), we need to list its
constructors. For each constructor, we need to list its arguments and whether
they are recursive or not.
testEnv :: TyEnv String String testEnv "Nat" = Just [ ("zero",[]) , ("succ",[Rec "Nat"]) ] testEnv _ = Nothing
Now, we can use the subtermInduction
to get induction hypotheses which are
just subterms of the conclusion. Normally, you would translate the Term
s from
the proof Obligation
s to some other representation, but there is also
linearisation functions included (linObligations
, for instance.)
natInd :: [String] > [Int] > IO () natInd vars coords = putStrLn $ render $ linObligations strStyle $ unTag (\(x :~ i) > x ++ show i) $ subtermInduction testEnv typed_vars coords where typed_vars = zip vars (repeat "Nat")
The library will create fresh variables for you (called Tagged
variables),
but you need to remove them, using for instance unTag
. If you want to sync
it with your own name supply, use unTagM
or unTagMapM
.
An example invocation:
*Mini> natInd ["X"] [0] P(zero). ! [X1 : Nat] : (P(X1) => P(succ(X1))).
This means to do induction on the zeroth coord (hence the 0
), and the variable
is called X. When using the library, it is up to you to translate the
abstract P
predicate to something meaningful.
We can also do induction on several variables:
*Mini> natInd ["X","Y"] [0,1] P(zero,zero). ! [Y3 : Nat] : (P(zero,Y3) => P(zero,succ(Y3))). ! [X1 : Nat] : (P(X1,zero) => P(succ(X1),zero)). ! [X1 : Nat,Y3 : Nat] : (P(X1,Y3) & P(X1,succ(Y3)) & P(succ(X1),Y3) => P(succ(X1),succ(Y3))).
In the last step case, all proper subterms of succ(X1),succ(Y3)
are used as
hypotheses.
A bigger example is in example/Example.hs
in the distribution.
 subtermInduction :: Ord c => TyEnv c t > [(v, t)] > [Int] > [TaggedObligation c v t]
 caseAnalysis :: TyEnv c t > [(v, t)] > [Int] > [TaggedObligation c v t]
 data Obligation c v t = Obligation {
 implicit :: [(v, t)]
 hypotheses :: [Hypothesis c v t]
 conclusion :: Predicate c v
 type TaggedObligation c v t = Obligation c (Tagged v) t
 type Predicate c v = [Term c v]
 type Hypothesis c v t = ([(v, t)], Predicate c v)
 data Term c v
 type TyEnv c t = t > Maybe [(c, [Arg t])]
 data Arg t
 data Tagged v = v :~ Integer
 tag :: Tagged v > Integer
 unTag :: (Tagged v > v') > [TaggedObligation c v t] > [Obligation c v' t]
 unTagM :: Applicative m => (Tagged v > m v') > [TaggedObligation c v t] > m [Obligation c v' t]
 unTagMapM :: (Functor m, Monad m) => (Tagged v > m v') > [TaggedObligation c v t] > m ([Obligation c v' t], Map (Tagged v) v')
 linObligations :: Style c v t > [Obligation c v t] > Doc
 linObligation :: Style c v t > Obligation c v t > Doc
 linTerm :: Style c v t > Term c v > Doc
 data Style c v t = Style {}
 strStyle :: Style String String String
 render :: Doc > String
 text :: String > Doc
Induction with subterms as hypotheses
subtermInduction :: Ord c => TyEnv c t > [(v, t)] > [Int] > [TaggedObligation c v t]Source
Subterm induction: the induction hypotheses will contain the proper subterms of the conclusion.
Case analysis (no induction hypotheses)
caseAnalysis :: TyEnv c t > [(v, t)] > [Int] > [TaggedObligation c v t]Source
Does case analysis on a list of typed variables. This function is equal
to removing all the hypotheses from subtermInduction
.
Obligations
data Obligation c v t Source
Quantifier lists are represented as tuples of variables and their type.
Example:
Obligation { implicit = [(x,t1),(y,t2)] , hypotheses = [([],[htm1,htm2]) ,([(z,t3)],[htm3,htm4]) ] , conclusion = [tm1,tm2] }
Corresponds to the formula:
forall (x : t1) (y : t2) . (P(htm1,htm2) & (forall (z : t3) . P(htm3,htm4)) => P(tm1,tm2))
The implicit variables (x and y) can be viewed as skolemised, and use these three formulae instead:
P(htm1,htm2).
forall (z : t3) . P(htm3,htm4).
~ P(tm1,tm2).
Obligation  

type TaggedObligation c v t = Obligation c (Tagged v) tSource
type Predicate c v = [Term c v]Source
A list of terms.
Example: [tm1,tm2]
corresponds to the formula P(tm1,tm2)
type Hypothesis c v t = ([(v, t)], Predicate c v)Source
Quantifier lists are represented as tuples of variables and their type.
Example:
([(x,t1),(y,t2)],[tm1,tm2])
corresponds to the formula
forall (x : t1) (y : t2) . P(tm1,tm2)
Terms
The simple term language only includes variables, constructors and functions.
Typing environment
type TyEnv c t = t > Maybe [(c, [Arg t])]Source
Given a type, return either that you cannot do induction on is type
(Nothing
), or Just
the constructors and a description of their arguments
(see Arg
).
The function should instantiate type variables. For instance, if you look
up the type [Nat]
, you should return the cons constructor with arguments
Nat
and [Nat]
(see Arg
).
Examples of types not possible to do induction on are function spaces and
type variables. For these, return Nothing
.
Arguments
An argument to a constructor can be recursive (Rec
) or nonrecursive
(NonRec
). Induction hypotheses will be asserted for Rec
arguments.
For instance, when doing induction on [a]
, then (:)
has two arguments,
NonRec a
and Rec [a]
. On the other hand, if doing induction on [Nat]
,
then (:)
has NonRec Nat
and Rec [Nat]
.
Data types can also be exponential. Consider
data Ord = Zero  Succ Ord  Lim (Nat > Ord)
Here, the Lim
constructor is exponential. If we describe types and
constructors with strings, the constructors for this data type is:
[ ("Zero",[]) , ("Succ",[Rec "Ord"]) , ("Lim",[Exp ("Nat > Ord") ["Nat"]) ]
The first argument to Exp
is the type of the function, and the second
argument are the arguments to the function.
Tagged (fresh) variables
Removing tagged variables
unTag :: (Tagged v > v') > [TaggedObligation c v t] > [Obligation c v' t]Source
Removing tagged (fresh) variables
unTagM :: Applicative m => (Tagged v > m v') > [TaggedObligation c v t] > m [Obligation c v' t]Source
Removing tagged (fresh) variables in a monad. The remove function is exectued at every occurence of a tagged variable. This is useful if you want to sync it with your own name supply monad.
unTagMapM :: (Functor m, Monad m) => (Tagged v > m v') > [TaggedObligation c v t] > m ([Obligation c v' t], Map (Tagged v) v')Source
Remove tagged (fresh) variables in a monad.
The remove function is exectued only once for each tagged variable,
and a Map
of renamings is returned.
This is useful if you want to sync it with your own name supply monad.
Linearising (prettyprinting) obligations and terms
linObligations :: Style c v t > [Obligation c v t] > DocSource
Linearises a list of Obligation
, using a given Style
.
linObligation :: Style c v t > Obligation c v t > DocSource
Linearises an Obligation
using a given Style
. The output format is
inspired by TPTP, but with typed quantifiers.
strStyle :: Style String String StringSource
An example style where constructors, variables and types are represented as String
.