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.
-
tamarin-prover
Main source code repository of the Tamarin prover for security protocol verification. -
-
-
-
-
haskhol-core
The core logical system of the HaskHOL theorem prover. See haskhol.org for more details.
InfluxDB - Purpose built for real-time analytics at any scale.
* 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?
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 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.