# hout - a non-interactive proof assistant for first-order logic, in Haskell

hout is an in-Haskell non-interactive proof assistant for intuitionistic first-order logic.

Alternatively, hout provides a monad that allows you to write functions in the style of proof-assistant proofs, which are then computable Haskell terms.

This is possible thanks to the Curry-Howard isomorphism.

## Examples

Have a look at `examples/Hout/Examples.hs` for some examples.

## What?

If you know about the CHI and intuitionistic logic, skip this section.

### The Curry-Howard isomorphism

The Curry-Howard isomorphism (or correspondence) is a pattern between intuitionistic logic and type theory, which says that propositions correspond to types, and proofs correspond to terms.

The basis of this correspondence is that an *inhabitant* of a type is a proof that the type is inhabited. For example, the term `3 :: Int` is a proof that you can construct some terminating value of type `Int`.

What about types with no inhabitant? Taking some type known to have no inhabitants, like `Void`, you can show that a type `a` is uninhabited by producing a terminating term of type `a -> Void`. Why? Because `a -> Void` is inhabited only if `a` is uninhabited, and a term of type `a -> Void` is a *proof that `a -> Void` is inhabited*!

This also has implications for function types - a term with type `a -> b` is a function from terms of type `a` to terms of type `b`. You can equally consider it as a function from proofs of the proposition `a` to proofs of the proposition `b` - in other words, the function itself is a proof that `a` implies `b`, because if you have a proof that `a` is true, you can obtain a proof that `b` is true.

Other logical connectives also have equivalents in Haskell types. `False` is `Void`, because you can't construct a proof for it; `a /\ b` is the tuple (or product) `(a, b)`; `a \/ b` is (the sum) `Either a b`; and `Not a` - the claim that `a` is uninhabited - is precisely `a -> False`. `True` can be any inhabited type, but it's helpful to have a type with a canonical construction, so `True` is normally `()`, the empty tuple, which has the unique constructor `()`.

You can see the correspondence in these types - `(a, b)` is inhabited if and only if both `a` and `b` are inhabited. Similarly, `Either a b` is inhabited if and only if at least one of `a`, `b` is inhabited. Phrasing it in terms of proofs, if you have a proof of `a` and a proof of `b`, you can construct a proof of `a /\ b` (and vice-versa) - and with a proof of `a`, you can construct a proof of `a \/ b`. With a proof of `a \/ b`, you can *destruct* the proof to get either a proof for `a` (`Left a`) or a proof for `b` (`Right b`).

For notation's sake, we write `a <-> b` for the type `(a -> b) /\ (b -> a)`.

### Intuistionistic logic

Intuistionistic (or constructive) logic is a subset of classical logic (the kind of logic you normally learn in a CS or Maths course). It behaves exactly like classical logic, but with one caveat - *you can only _construct_ proofs of a proposition*.

To see what that means, consider the type of the law of the excluded middle - `forall a. a \/ Not a`. For every type `a`, one of these two terms must be constructable - either `a` is inhabited, so you can construct a value of type `a`, or `a` is uninhabited, so you can construct a function of type `a -> Void`.

But you can't write a terminating Haskell function with type `forall a. a \/ Not a` - because it would require you to somehow decide if `a` is inhabited, and then get a value of type `a` if it was. In other words, you have to construct either a `Left a` or a `Right (Not a)`, and you have no way to do either of those things.

There are lots of other consequences of this caveat: the following implications do *not* hold in intuitionistic logic - and similarly, you cannot write a terminating Haskell term for their type.

  * `Not (Not a) -> a`
  * `(a -> b) -> (Not a \/ b)`
  * `Not (Not a /\ Not b) -> a \/ b`

## Proofs and the Tactic monad

The `Tactic` monad is an indexed monad for which the monad state is the current proof goal, and the type argument is an additional hypothesis introduced at that proof step. Looking at its definition
```
data Tactic from to a = Tactic ((a -> to) -> from)
```
A `Tactic` term represents a valid goal transformation - you are allowed to change a proof of `from` into a proof of `to`, and introduce the additional hypothesis `a`, if you can use a proof of `a -> to` to prove `from`.

For example, the `apply` function has the signature
```
apply :: (a -> b) -> Tactic b a ()
```
Given a function `a -> b`, it allows you to transform the goal from proving `b` to proving `a` - because once you prove `a`, it will be possible to use the given function to produce a proof of `b`.

Some tactics introduce additional hypotheses - such as `intro`
```
intro :: Tactic (a -> b) b a
```
`intro` allows you to transform a goal of `a -> b` to a goal of `b`, giving you the hypothesis of type `a` to bind into a variable. If you can use the proof of `a` to construct a proof of `b`, then the resulting function term is indeed a proof of `a -> b`.

### Available tactics

hout provides some tactics based on those used in `Coq` - for example, you can `apply` hypotheses to a goal; you can `split` the proof a conjunction into proofs of its conjuncts; you can `intro` a variable; you can `exists` the witness of an existential goal; you can `rewrite` propositions with equality; you can even `assert` hypothesis and produce subgoals.

The full list of tactics is given in `Hout.Prover.Tactics`, and it is possible to write your own using the type signature of the `Tactic` monad.

### Proofs in do notation

Because `Tactic` is an indexed monad, you can use the `do-notation` package to write proofs in do notation, which end up looking quite similar to proofs in interactive proof assistants. Some advice for doing this is:

  * use pattern-matching in binds, particularly when working with existential types. GHC has some unfortunate behaviour when trying to use `let` in do notation when working with existential type arguments.
  * Enable block arguments, and use do notation for subgoals
  * If your final statement is a tactic that introduces a hypothesis, but the new goal is trivial `()`, use `qed` to end your proof.

### Limitations

The use of `Forall` is limited by Haskell's lack of support for impredicative polymorphism - the instantiation of type variables with higher-ranked types. This makes it basically impossible to prove a `Forall` using the `Tactic` monad, since under the hood `Forall` is just a Haskell type-level `forall`.

## Computations written in the proof style

hout also has the nice property of intuitionistic proof assistants that proofs are themselves terms, and can be run as Haskell code. This gives hout the alternative use of writing functions in a proof-y syntax using the `Tactic` monad. For example, the `identity` function can be written as
```
identity :: a -> a
identity :: runProof $ Proof do
  a <- intro
  exact a
```