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

Hout.Prover.Proofs

Description

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

Synopsis

runProof :: Theorem a -> a
data Theorem a = 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
admitted :: Axiom a
noncomputable :: Axiom a -> a

Documentation

runProof :: Theorem a -> a Source #

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 Source #

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 Source #

type Corollary a = Theorem a Source #

type Example a = Theorem a Source #

type Definition a = Theorem a Source #

data Axiom a Source #

An unprovable axiom.

admitted :: Axiom a Source #

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 Source #

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.