{- |
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.
-}
module Induction.Structural (
module Induction.Structural.Subterms,
module Induction.Structural.Types,
module Induction.Structural.Linearise
) where
import Induction.Structural.Subterms
import Induction.Structural.Types
import Induction.Structural.Linearise
{-# ANN module "HLint: ignore Use import/export shortcut" #-}