Logic.Proof

The Proof type

data Proof (pf :: k)

The Proof type is used as a domain-specific language for constructing proofs. A value of type Proof p represents a proof of the proposition p.

A Proof as an argument to a function represents an assumption. For example, this function constructions a proof of "P or Q" from the assumption "P and Q":

and2or :: Proof (p && q) -> Proof (p || q)

and2or pq = introOrL $ elimAndL pq

If the body of the proof does not match the proposition you claim to be proving, the compiler will raise a type error. Here, we accidentally try to use or_introR instead of or_introL:

and2or :: Proof (p && q) -> Proof (p || q)

and2or pq = introOrR $ elimAndL pq

resulting in the error

    • Couldn't match type ‘p’ with ‘q’
      ‘p’ is a rigid type variable bound by
        the type signature for:
          and2or :: forall p q. Proof (p && q) -> Proof (p || q)

      ‘q’ is a rigid type variable bound by
        the type signature for:
          and2or :: forall p q. Proof (p && q) -> Proof (p || q)

      Expected type: Proof (p || q)
        Actual type: Proof (p || p)

axiom :: Proof p

axiom, like sorry, provides a "proof" of any proposition. Unlike sorry, which is used to indicate that a proof is still in progress, axiom is meant to be used by library authors to assert axioms about how their library works. For example:

data Reverse xs = Reverse Defn
data Length  xs = Length  Defn

revLengthLemma :: Proof (Length (Reverse xs) == Length xs)
revLengthLemma = axiom

sorry :: Proof p

Warning: Completed proofs should never use sorry!

sorry can be used to provide a "proof" of any proposition, by simply assering it as true. This is useful for stubbing out portions of a proof as you work on it, but subverts the entire proof system.

_Completed proofs should never use sorry!_