Induction.Structural

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"] [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.

Induction with subterms as hypotheses

subtermInduction :: Ord c => TyEnv c t -> [(v, t)] -> [Int] -> [TaggedObligation c v t]

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]

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

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

Fields

implicit :: [(v, t)]

Implicitly quantified variables (skolemised)

hypotheses :: [Hypothesis c v t]

Hypotheses, with explicitly quantified variables

conclusion :: Predicate c v

The induction conclusion

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

Obligations with tagged variables (see Tagged and unTag)

type Predicate c v = [Term c v]

A list of terms.

Example: [tm1,tm2] corresponds to the formula P(tm1,tm2)

type Hypothesis c v t = ([(v, t)], Predicate c v)

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

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

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

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

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)

tag :: Tagged v -> Integer

The Integer tag

Removing tagged variables

unTag :: (Tagged v -> v') -> [TaggedObligation c v t] -> [Obligation c v' t]

Removing tagged (fresh) variables

unTagM :: Applicative m => (Tagged v -> m v') -> [TaggedObligation c v t] -> m [Obligation c v' t]

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

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

Linearises a list of Obligation, using a given Style.

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

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

Linearises a Term using a given Style.

data Style c v t

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

Constructors

Style

Fields

linc :: c -> Doc

linv :: v -> Doc

lint :: t -> Doc

strStyle :: Style String String String

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:

• text s <> text t = text (s++t)

• text "" <> x = x, if x non-empty

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