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.