hout-0.1.0.0: Non-interactive proof assistant monad for first-order logic.

Copyright (c) Isaac van Bakel 2020 BSD-3 ivb@vanbakel.io experimental POSIX Safe 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

# 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
 Source # Instance detailsDefined in Hout.Prover.Tactics Methodsibind :: (a -> Tactic j k1 b) -> Tactic i j a -> Tactic i k1 b # Source # Instance detailsDefined in Hout.Prover.Tactics Methodsiap :: Tactic i j (a -> b) -> Tactic j k1 a -> Tactic i k1 b # Source # Instance detailsDefined in Hout.Prover.Tactics Methodsireturn :: a -> Tactic i i a # Source # Instance detailsDefined in Hout.Prover.Tactics Methodsimap :: (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.