Tactic Metaprogramming in Haskell
Tactic Metaprogramming as a library! This project aims to bring the proof automation capabilities of Coq and others to Haskell.
Here's some examples:
tactic "pair" [t| forall a b. a -> b -> (a,b)|] $ do
forall
intros_
split
assumption
tactic "&" [t| forall a b. a -> (a -> b) -> b |] $ do
forall
intro "x"
intro "f"
apply "f"
exact "x"
tactic "foo" [t| forall a b c. a -> (a -> b) -> (b -> c) -> (a,c)|] $ do
auto 5
tactic "either" [t| forall a b c. (a -> c) -> (b -> c) -> Either a b -> c |] $ auto 5
tactic "myFold" [t| forall a b. (a -> b -> b) -> b -> [a] -> b |] $ auto 5
data Nat = Z | S Nat deriving (Show)
tactic "plus" [t| Nat -> Nat -> Nat |] $ do
intros ["n", "m"]
induction "n" <@>
[ exact "m"
, do
apply 'S
exact "ind"
]
For more examples, see the samples/
directory.
auto
to use at top-level bindings/imported functions.induction
This is very much a work in progress! tactic-haskell
makes
no promises about anything at this stage. It could work perfectly, or it could decide to burn down your house.
Also, even though auto
is good at it's job, it isn't perfect, make sure to check the output by
using debugTactic
.