structural-induction-0.2.0.1: Instantiate structural induction schemas for algebraic data types

Induction.Structural

Description

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 Terms from the proof Obligations 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"] 
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.

Synopsis

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).

Constructors

 Obligation Fieldsimplicit :: [(v, t)]Implicitly quantified variables (skolemised)hypotheses :: [Hypothesis c v t]Hypotheses, with explicitly quantified variablesconclusion :: Predicate c vThe induction conclusion

type TaggedObligation c v t = Obligation c (Tagged v) t Source

Obligations with tagged variables (see Tagged and unTag)

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

data Term c v Source

The simple term language only includes variables, constructors and functions.

Constructors

 Var v Con c [Term c v] Fun v [Term c v] Induction on exponential data types yield assumptions with functions

Instances

 (Eq c, Eq v) => Eq (Term c v) (Ord c, Ord v) => Ord (Term c v)

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

data Arg t Source

An argument to a constructor can be recursive (Rec) or non-recursive (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.

Constructors

 Rec t NonRec t Exp t [t]

Tagged (fresh) variables

data Tagged v Source

Cheap way of introducing fresh variables. The Eq and Ord instances only uses the Integer tag.

Constructors

 v :~ Integer

Instances

 Eq (Tagged v) Ord (Tagged v)

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 (pretty-printing) obligations and terms

linObligations :: Style c v t -> [Obligation c v t] -> Doc Source

Linearises a list of Obligation, using a given Style.

linObligation :: Style c v t -> Obligation c v t -> Doc Source

Linearises an Obligation using a given Style. The output format is inspired by TPTP, but with typed quantifiers.

linTerm :: Style c v t -> Term c v -> Doc Source

Linearises a Term using a given Style.

data Style c v t Source

Functions for linearising constructors (linc), variables (linv) and types (lint).

Constructors

 Style Fieldslinc :: c -> Doc linv :: v -> Doc lint :: t -> Doc

An example style where constructors, variables and types are represented as String.

Convenience re-export

render :: Doc -> String

Render the Doc to a String using the default Style.

text :: String -> Doc

A document of height 1 containing a literal string. text satisfies the following laws:

The side condition on the last law is necessary because text "" has height 1, while empty has no height.