Copyright	(c) Isaac van Bakel 2020
License	BSD-3
Maintainer	ivb@vanbakel.io
Stability	experimental
Portability	POSIX
Safe Haskell	Safe
Language	Haskell2010

Hout.Prover.Tactics

Description

The module forms the basis of hout as a non-interactive proof assistant. It contains the definition of Tactic, the monad which allows for proof-goal manipulations in do-notation, and defines some useful Tactic functions to mimic the syntax of actual proof assistants.

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.

Constructors

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

Instances

IxMonad Tactic Source #
Instance details Defined in Hout.Prover.Tactics Methods ibind :: (a -> Tactic j k1 b) -> Tactic i j a -> Tactic i k1 b #
IxApplicative Tactic Source #
Instance details Defined in Hout.Prover.Tactics Methods iap :: Tactic i j (a -> b) -> Tactic j k1 a -> Tactic i k1 b #
IxPointed Tactic Source #
Instance details Defined in Hout.Prover.Tactics Methods ireturn :: a -> Tactic i i a #
IxFunctor Tactic Source #
Instance details Defined in Hout.Prover.Tactics Methods imap :: (a -> b) -> Tactic j k2 a -> Tactic j k2 b #

name :: a -> Tactic b b a Source #

Bind a term as a hypothesis name.

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.

left :: Tactic (a \/ b) a () Source #

Transform a disjunction goal into the goal of the left side.

right :: Tactic (a \/ b) b () Source #

Transform a disjunction goal into the goal of the right side.

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

Give a name to the hypothesis of an ->.

exact :: a -> Tactic a () () Source #

Solve a goal by giving its exact proof.

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.

symmetry :: Tactic (Equal a b) (Equal b a) () Source #

Transform an equality goal by symmetry.

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

Split an equality goal into two subgoals, by transitivity.

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

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

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

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

qed :: Tactic () () () Source #

A helper for the end of proofs. Assert to the type system that the proof is complete, and act as an ending statement if the final Tactic otherwise introduces a hypothesis.