Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP

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

branch: master

Fetching latest commit…

Octocat-spinner-32-eaf2f5

Cannot retrieve the latest commit at this time

Octocat-spinner-32 Induction
Octocat-spinner-32 example
Octocat-spinner-32 test
Octocat-spinner-32 .gitignore
Octocat-spinner-32 .travis.yml
Octocat-spinner-32 LICENSE
Octocat-spinner-32 README.md
Octocat-spinner-32 Setup.hs
Octocat-spinner-32 structural-induction.cabal
README.md

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.

Something went wrong with that request. Please try again.