Copyright | (c) Isaac van Bakel 2020 |
---|---|

License | BSD-3 |

Maintainer | ivb@vanbakel.io |

Stability | experimental |

Portability | POSIX |

Safe Haskell | Safe |

Language | Haskell2010 |

## Synopsis

- data Tactic from to a = Tactic ((a -> to) -> from)
- name :: a -> Tactic b b a
- applyH :: (a -> b) -> Tactic m n a -> Tactic m n b
- combineH :: Tactic m n (a -> b) -> Tactic n o a -> Tactic m o b
- bindH :: (a -> Tactic n o b) -> Tactic m n a -> Tactic m o b
- apply :: (a -> b) -> Tactic b a ()
- applyF :: Forall k p -> Tactic (p a) () ()
- left :: Tactic (a \/ b) a ()
- right :: Tactic (a \/ b) b ()
- intro :: Tactic (a -> b) b a
- exact :: a -> Tactic a () ()
- split :: Tactic a () () -> Tactic b () () -> Tactic (a /\ b) () ()
- assert :: Tactic a () () -> Tactic m m a
- enough :: (a -> Tactic b () ()) -> Tactic b a ()
- exists :: Witness (a :: k) -> Tactic (Exists k p) (p a) ()
- generalize :: Tactic (p a) (Forall k p) ()
- reflexivity :: Tactic (Equal a a) () ()
- symmetry :: Tactic (Equal a b) (Equal b a) ()
- transitivity :: Tactic (Equal a b) () () -> Tactic (Equal b c) () () -> Tactic (Equal a c) () ()
- rewrite :: Equal a b -> Tactic (p a) (p b) ()
- rewriteRev :: Equal a b -> Tactic (p b) (p a) ()
- qed :: Tactic () () ()

# Documentation

data Tactic from to a Source #

The proof-transformation monad. `Tactic`

is an indexed monad for which
the type state is the current proof goal.

The aim of most `Tactic`

uses is to produce a term with type
`Tactic a () ()`

for the proof goal `a`

- this represents a proof of `a`

,
since it involves reducing the proof goal `a`

to the trivial proof goal `()`

.

A `Tactic`

term is a valid manipulation which takes a proof of `a -> to`

and gives a proof of `from`

- allowing for the proof-goal to be transformed
from `from`

into `to`

, giving the additional hypothesis `a`

.

Tactic ((a -> to) -> from) |

applyH :: (a -> b) -> Tactic m n a -> Tactic m n b Source #

Apply a proof transformation to the hypothesis.

combineH :: Tactic m n (a -> b) -> Tactic n o a -> Tactic m o b Source #

Combine two hypotheses together.

bindH :: (a -> Tactic n o b) -> Tactic m n a -> Tactic m o b Source #

Apply an intermediate proof to the hypothesis.

apply :: (a -> b) -> Tactic b a () Source #

Apply a proof transformation to the goal. This simplifies the goal of `b`

to a goal of `a`

.

applyF :: Forall k p -> Tactic (p a) () () Source #

Apply a forall to the goal. This solves the goal immediately.

split :: Tactic a () () -> Tactic b () () -> Tactic (a /\ b) () () Source #

Split a conjuction goal into two subgoals.

assert :: Tactic a () () -> Tactic m m a Source #

Assert a statement, giving a proof of it. The statement can then be bound as a hypothesis

enough :: (a -> Tactic b () ()) -> Tactic b a () Source #

Assert a statement, giving a proof that it solves the goal. The goal then becomes proving the statement.

exists :: Witness (a :: k) -> Tactic (Exists k p) (p a) () Source #

Give the witness for an existential goal. The goal then becomes proving the statement for that witness.

generalize :: Tactic (p a) (Forall k p) () Source #

Transform a goal for a specific value to a general `Forall`

goal

reflexivity :: Tactic (Equal a a) () () Source #

Solve a reflexive goal.

transitivity :: Tactic (Equal a b) () () -> Tactic (Equal b c) () () -> Tactic (Equal a c) () () Source #

Split an equality goal into two subgoals, by transitivity.

rewriteRev :: Equal a b -> Tactic (p b) (p a) () Source #

Rewrite a goal by equality, right-to-left.