structuralinduction alternatives and similar packages
Based on the "Logic" category.
Alternatively, view structuralinduction alternatives based on common mentions on social networks and blogs.

tamarinprover
Main source code repository of the Tamarin prover for security protocol verification. 
tiphaskellfrontend
Convert from Haskell to Tip 
atphaskell
Haskell version of the code from "Handbook of Practical Logic and Automated Reasoning" 
logicclasses
Framework for propositional and first order logic, theorem proving 
hout
A noninteractive proof assistant using the Haskell type system 
obdd
pure Haskell implementation of reduced ordered binary decision diagrams 
g4ipprover
Theorem prover for intuitionistic propositional logic, fork of github.com/cacay/G4ip 
tpdb
parser and prettyprinter for TPDB syntax (termination problem data base) 
haskholcore
The core logical system of the HaskHOL theorem prover. See haskhol.org for more details.
* Code Quality Rankings and insights are calculated and provided by Lumnify.
They vary from L1 to L5 with "L5" being the highest.
Do you think we are missing an alternative of structuralinduction or a related project?
README
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.