content: {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE PolyKinds      #-}
  
  {-|
    Module      :  Logic.Proof
    Copyright   :  (c) Matt Noonan 2018
    License     :  BSD-style
    Maintainer  :  matt.noonan@gmail.com
    Portability :  portable
  -}
  
  module Logic.Proof
    ( -- * The `Proof` type
      Proof
    , axiom, sorry
    ) where
  
  {--------------------------------------------------
    The `Proof` type
  --------------------------------------------------}
  
  {-| 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)
  @
  -}
  data Proof (pf :: k) = QED
  
  -- | @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@!_
  sorry :: Proof p
  sorry = QED
  {-# WARNING sorry "Completed proofs should never use sorry!" #-}
  
  {-| @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
  @
  -}
  axiom :: Proof p
  axiom = QED
  