Skip to content

danr/structural-induction

Repository files navigation

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.

About

SII: Structural Induction Instantiator over any strictly-positive algebraic data type.

Resources

License

Stars

Watchers

Forks

Packages

No packages published