structural-induction alternatives and similar packages
Based on the "Logic" category.
Alternatively, view structural-induction alternatives based on common mentions on social networks and blogs.
Main source code repository of the Tamarin prover for security protocol verification.
Convert from Haskell to Tip
Haskell version of the code from "Handbook of Practical Logic and Automated Reasoning"
Framework for propositional and first order logic, theorem proving
* 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 structural-induction or a related project?
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 (
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
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
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
but you need to remove them, using for instance
unTag. If you want to sync
it with your own name supply, use
An example invocation:
*Mini> natInd ["X"]  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
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
A bigger example is in
example/Example.hs in the distribution.