Hout.Prover.Proofs

This module contains some helpers for declaring proofs, and running them as code.

Documentation

runProof :: Theorem a -> a

Run a theorem to its Haskell term. If the proof of the theorem uses only terminating values, then the resulting Haskell term can be run as usual without errors.

data Theorem a

A proven theorem.

As described in Hout.Prover.Tactics, proof of a is equivalent to reducing the proof goal a to the trival proof goal ().

Constructors

Proof (Tactic a () ())

type Lemma a = Theorem a

type Corollary a = Theorem a

type Example a = Theorem a

type Definition a = Theorem a

data Axiom a

An unprovable axiom.

admitted :: Axiom a

Admit an axiom, without proof. Note that this is not a terminating term, so using it will not yield computable Haskell.

noncomputable :: Axiom a -> a

Use an axiom, with the understood caveat that the result will not be a computable term. It is impossible to construct an Axiom, so using one cannot give runnable Haskell.