We’re now prepared to define what a proof is and what it means for a proof to be valid. We’ll be using a basic natural deduction style of proof. In this style, proofs are rose trees of judgements, where each node is annotated with evidence. Evidence takes the form of inference rules. Each production rule for the judgement grammar gets one or more introduction rules that serve as evidence for statements that include a new instance of the production, as well as one or more elimination rules that serve as evidence for decomposing a judgement. Here’s an example of an inference rule.

\[\begin{array}{ccc} P & & Q \\ \hline & P \wedge Q & \end{array}\]

The symbols above the line are called premises and the one below is the conclusion. This rule says “if we have evidence for \(P\), and also evidence for \(Q\), then we have evidence for \(P \wedge Q\)”. The \(P\) and \(Q\) here are judgement variables. Natural deduction proofs are trees of statements like this, with each “node” in the tree supported by an inference rule.

As usual we start with some module imports.

{-# LANGUAGE LambdaCase #-}
module Proof where

import Control.Monad
  ( ap, foldM )
import Control.Monad.Loops
  ( concatM )
import Data.List
  ( groupBy, sortBy, nub )
import qualified Data.Map as M
import qualified Data.Set as S
import Test.QuickCheck

import Var
import Sub
import Expr
import Type
import Infer
import Jud


An inference rule consists of a conclusion and zero or more premises, where the conclusion and premises are judgements.

data Rule
  = Rule Jud [Jud]
  deriving (Eq, Show)

We can make an Arbitrary instance for rules. The vast majority of rules it generates will be nonsense.

instance Arbitrary Rule where
  arbitrary = Rule <$> arbitrary <*> arbitrary

  shrink (Rule q ps) =
    [ Rule q' ps' | q' <- shrink q, ps' <- shrink ps ] ++
    [ Rule q ps' | ps' <- shrink ps ] ++
    [ Rule q' ps | q' <- shrink q ]
captureJudSubRule :: Sub Jud -> Rule -> Rule
captureJudSubRule t (Rule q ps) =
  Rule (captureJudSub t q) (map (captureJudSub t) ps)

The most important operation on rules is matching. Inference rules are proof schemas, representing many concrete proofs. A rule can be applied to a particular conclusion and list of premises if there is a substitution from the rule to the candidate judgements.

matchRule :: Rule -> Jud -> [Jud] -> Maybe (Sub Jud, Sub Expr)
matchRule (Rule a as) b bs = matchList (a:as, b:bs)
    matchList :: ([Jud],[Jud]) -> Maybe (Sub Jud, Sub Expr)
    matchList = \case
      ([],[]) ->
        return (emptySub, emptySub)
      (u:us,v:vs) -> do
        (js1,es1) <- matchJud u v
        (js2,es2) <- matchList (us,vs)
        js <- unionSub js1 js2
        es <- unionSub es1 es2
        return (js, es)
      _ -> Nothing

Note that matching rules imposes an order on the premises. Most authors on natural deduction say that the order of premises for an inference rule doesn’t matter, but allowing rearrangements of the premises would make matching much more complicated – so we just won’t do that :).

We can test matchRule a couple of different ways. The most obvious one is that if a rule matches a given list of judgements, then the substitution should carry the rule to the judgements.

  :: Rule -> Jud -> [Jud] -> Bool
test_match_rule r@(Rule cr hrs) ct hts =
  case matchRule r ct hts of
    Nothing -> True
    Just (js,es) ->
        ok a b = a == js $~ (es $> b)
      in and
        [ ok ct cr
        , length hrs == length hts
        , and $ zipWith ok hts hrs

This test doesn’t carry a lot of confidence, because the vast majority of generated test cases are useless.

Another check is that rules should match themselves.

  :: Rule -> Bool
test_match_rule_self r@(Rule c hs) =
  case matchRule r c hs of
    Nothing -> False
    Just (_,es) -> trivialExprSub es

And if we apply a substitution to a rule, it should match the result.

  :: Rule -> Sub Jud -> Sub Expr -> Bool
test_match_rule_sub r@(Rule c hs) js es =
  let s x = js $~ (es $> x) in
  case matchRule r (s c) (map s hs) of
    Nothing -> False
    Just _ -> True

In one sense a Rule is just a list of judgements, which makes it easy to define HasExprVars and TypeCheck instances.

instance HasExprVars Rule where
  freeExprVars (Rule c hs) =
    mconcat $ map freeExprVars (c:hs)
  renameBoundExpr avoid (Rule c hs) =
    Rule (renameBoundExpr avoid c) (map (renameBoundExpr avoid) hs)
  renameFreeExpr (u,v) (Rule c hs) =
    Rule (renameFreeExpr (u,v) c) (map (renameFreeExpr (u,v)) hs)

instance TypeCheck Rule where
  typeCheck (Rule c hs) env = concatM (map typeCheck (c:hs)) env

For funsies, let’s see an example. From the rule

\[\begin{array}{ccc} \\ \hline xy = z \end{array}\]

we infer that \(y\) has type \(a\), \(z\) has type \(b\), and \(x\) has type \(a \rightarrow b\).

test_cases_rule_typecheck :: Bool
test_cases_rule_typecheck = and
  [ _typecheck_and_unify

      (JEq Q
        (EApp Q (EVar Q (Var "x")) (EVar Q (Var "y")))
        (EVar Q (Var "z")))

    (TypeEnv $ M.fromList
      [ (Right $ Var "x", ForAll S.empty
          (TArr Q (TVar Q (Var "a")) (TVar Q (Var "b"))))
      , (Right $ Var "y", ForAll S.empty
          (TVar Q (Var "a")))
      , (Right $ Var "z", ForAll S.empty
          (TVar Q (Var "b")))

Inference rules will end up playing a role similar to axioms and theorems. We’ll have a bunch of them we consider “valid” for some reason and are allowed to match them against proofs. With this in mind, we define a rule environment to be a set of named rules.

data RuleEnv = RuleEnv
  { theRuleEnv :: M.Map RuleName Rule
  } deriving (Eq, Show)

data RuleName = RuleName String
  deriving (Eq, Ord, Show)

instance Arbitrary RuleName where
  arbitrary = RuleName <$> (listOf1 $ elements _rulename_chars)

_rulename_chars = concat
  [ "abcdefghijklmnopqrstuvwxyz"
  , "0123456789-_"


A natural deduction style proof is essentially a labeled rose tree of judgements; the nodes in the tree are supported judgements, and each node is labeled with a justification. We can define this with a type; the full details are a little more complicated than ‘labeled rose tree’ because certain labels are special forms that need to be dealt with differently.

data Proof
  = Use Loc RuleName Jud [Proof]
  | Invoke Loc RuleName Jud [Proof] (Sub Jud)

We will eventually need to have introduction and elimination rules for each judgement constructor. But many of these can be expressed in essentially the same way that we would express a theorem at the user level. For instance, the introduction rule for \(\wedge\). These are collectively handled by Use. Other rules will require special syntactic support, and these have to be built into the definition of proof. For example!

  | Hyp Loc HypName Jud
  | Dis Loc HypName Jud Proof

The Hypothesis and Discharge proofs together comprise the introduction rule for \(\Rightarrow\), and have to be dealt with outside of the usual rule-matching strategy because they involve state. Typically discharging is explained something like this:

\[\begin{array}{ccc} P \\ \vdots \\ Q \\ \hline P \Rightarrow Q \end{array}\]

The elipses are doing a lot of work here. The idea is that \(P\) is introduced as a named hypothesis somewhere above \(Q\), and this is discharged as \(P \Rightarrow Q\) but not before. The “but not before” part is the state; when validating a proof from the leaves to the root, we have to keep track of which hypotheses have been introduced and which have already been discharged.

  | ElimEq Loc Jud (Var Expr) Jud Proof Proof
  | IntroEq Loc Jud

The ElimEq rule is what justifies substituting equals for equals in a judgement. Schematically it looks like this:

\[\begin{array}{ccc} s = t & & \Phi[x \mapsto s] \\ \hline & \Phi[x \mapsto t] & \end{array}\]

Where [square brackets] denote a substitution; \(\Phi[x \mapsto s]\) is obtained by replacing all free occurrences of the expression variable \(x\) in \(\Phi\) by the expression \(s\). This substitution is not part of the judgement syntax itself, but rather a kind of metasyntax; that’s why this rule needs to be dealt with separately. IntroEq is the introduction rule for equality; it can be defined with Use (it doesn’t require any syntactic support) but it will be handy to build this into the syntax.

  | IntroU Loc Jud (Var Expr) (Var Expr) Proof
  | ElimU Loc Jud (Var Expr) Expr Proof

IntroU and ElimU are the introduction and elimination rules for universal quantifiers; these also need a special syntax because they come with side conditions on correctness. The introduction rule is schematically

\[\begin{array}{c} \Phi \\ \hline \forall x . \Phi[u \mapsto x] \end{array}\]

with the side condition that \(x\) is not free in \(\Phi\) and \(u\) is not free in any assumptions or undischarged hypotheses. The elimination rule is

\[\begin{array}{c} \forall x . \Phi \\ \hline \Phi[x \mapsto u] \end{array}\]

These side conditions are another kind of contextual state, which is why these need to be handled separately.

  | IntroE Loc Jud (Var Expr) Expr Proof
  | ElimE Loc Jud (Var Expr) (Var Expr) Proof Proof

IntroE and ElimE are the introduction and elimination rules for existential quantifiers. Schematically, IntroE is

\[\begin{array}{c} \Phi[u \mapsto e] \\ \hline \exists u . \Phi \end{array}\]

while ElimE is

\[\begin{array}{c} \exists x. \Phi & & \Phi[x \mapsto u] \Rightarrow \Psi \\ \hline & \Psi & \end{array}\]

with the side conditions that \(u\) does not occur in \(\exists x . \Phi\), in \(\Psi\), or in any undischarged hypotheses or assumptions in the proof of \(\Phi[x \mapsto u] \Rightarrow \Psi\).

  | Assume Loc Int Jud
  deriving (Show)

The final proof type is the assumption. Assumptions are similar to hypotheses in that they let us introduce a judgement with no explicit support. However, hypotheses must eventually be discharged, while assumptions are never discharged. To see the difference, suppose we were trying to prove a rule like the following.

\[\begin{array}{ccc} R & & Q \\ \hline & P \Rightarrow Q & \end{array}\]

(This is nonsense, just go with it.) In the proof tree for this rule, \(Q\) is an assumption; it’s one of the premises of the rule being proved. \(P\) appears as the antecedent of an implies judgement in the conclusion. Somewhere in the proof tree, \(P\) is introduced as a hypothesis and then discharged to support \(P \Rightarrow Q\), but \(P\) is not one of the premises of the rule.

And that’s it; every step in a proof has one of these forms. It looks a little puny. What about the other logical connectives? Everything we need to say about them can be expressed as an atomic inference rule, and does not need to be baked in to our definition of proof. This means our proof checker can be pretty flexible – we can, for example, decide later whether or not to allow some rules, like the law of the excluded middle.

For testing, we’ll need an Eq instance for Proof that ignores Loc parameters.

instance Eq Proof where
  p1 == p2 = case (p1,p2) of
    (Assume _ k1 p1, Assume _ k2 p2) ->
      (k1 == k2) && (p1 == p2)
    (Hyp _ n1 p1, Hyp _ n2 p2) ->
      (n1 == n2) && (p1 == p2)
    (Dis _ n1 q1 p1, Dis _ n2 q2 p2) ->
      (n1 == n2) && (p1 == p2) && (q1 == q2)
    (IntroEq _ e1, IntroEq _ e2) ->
      (e1 == e2)
    (ElimEq _ q1 x1 e1 p1 u1, ElimEq _ q2 x2 e2 p2 u2) ->
      (q1 == q2) && (x1 == x2) && (e1 == e2) && (p1 == p2) && (u1 == u2)
    (IntroU _ q1 x1 y1 p1, IntroU _ q2 x2 y2 p2) ->
      (q1 == q2) && (x1 == x2) && (y1 == y2) && (p1 == p2)
    (ElimU _ q1 x1 e1 p1, ElimU _ q2 x2 e2 p2) ->
      (q1 == q2) && (x1 == x2) && (e1 == e2) && (p1 == p2)
    (IntroE _ q1 x1 e1 p1, IntroE _ q2 x2 e2 p2) ->
      (q1 == q2) && (x1 == x2) && (e1 == e2) && (p1 == p2)
    (ElimE _ q1 x1 y1 u1 v1, ElimE _ q2 x2 y2 u2 v2) ->
      (q1 == q2) && (x1 == x2) && (y1 == y2) && (u1 == u2) && (v1 == v2)
    (Use _ n1 q1 p1, Use _ n2 q2 p2) ->
      (n1 == n2) && (q1 == q2) && (p1 == p2)
    (Invoke _ n1 q1 p1 t1, Invoke _ n2 q2 p2 t2) ->
      (n1 == n2) && (q1 == q2) && (p1 == p2) && (t1 == t2)
    _ -> False

And here’s an Arbitrary instance.

instance Arbitrary Proof where
  arbitrary = getSize >>= genDepth
      genDepth k
        | k <= 0 = oneof
            [ Assume <$> arbitrary <*> (abs <$> arbitrary) <*> arbitrary
            , Hyp <$> arbitrary <*> arbitrary <*> arbitrary
        | otherwise = do
            let recur = genDepth =<< elements [0..(div k 2)]
              [ Dis <$> arbitrary <*> arbitrary <*> arbitrary
                  <*> recur
              , IntroEq <$> arbitrary <*> arbitrary
              , ElimEq <$> arbitrary <*> arbitrary <*> arbitrary
                  <*> arbitrary <*> recur <*> recur
              , IntroU <$> arbitrary <*> arbitrary <*> arbitrary
                  <*> arbitrary <*> recur
              , ElimU <$> arbitrary <*> arbitrary <*> arbitrary
                  <*> arbitrary <*> recur
              , IntroE <$> arbitrary <*> arbitrary <*> arbitrary
                  <*> arbitrary <*> recur
              , ElimE <$> arbitrary <*> arbitrary <*> arbitrary
                  <*> arbitrary <*> recur <*> recur
              , Use <$> arbitrary <*> arbitrary <*> arbitrary
                  <*> listOf recur
              , Invoke <$> arbitrary <*> arbitrary <*> arbitrary
                  <*> listOf recur <*> (return emptySub)

  shrink = \case
    Assume loc k q -> map (Assume loc k) $ shrink q
    Hyp loc n q -> map (Hyp loc n) $ shrink q
    Dis loc n q p ->
      [ p ] ++
      [ Dis loc n q' p' | q' <- shrink q, p' <- shrink p ] ++
      [ Dis loc n q p' | p' <- shrink p ] ++
      [ Dis loc n q' p | q' <- shrink q ]
    IntroEq loc j ->
      [ IntroEq loc q | q <- shrink j ]
    ElimEq loc u x v p q ->
      [ p, q ] ++
      [ ElimEq loc u' x v' p' q' |
        u' <- shrink u, v' <- shrink v, p' <- shrink p, q' <- shrink q ]
    IntroU loc q x y p ->
      [ p ] ++
      [ IntroU loc q' x y p' |
        q' <- shrink q, p' <- shrink p ]
    ElimU loc q x e p ->
      [ p ] ++
      [ ElimU loc q' x e' p' |
        q' <- shrink q, e' <- shrink e, p' <- shrink p ]
    IntroE loc q x y p ->
      [ p ] ++
      [ IntroE loc q' x y p' |
        q' <- shrink q, p' <- shrink p ]
    ElimE loc q x e p u ->
      [ p ] ++
      [ ElimE loc q' x e' p' u' |
        q' <- shrink q, e' <- shrink e, p' <- shrink p, u' <- shrink u ]
    Use loc name p ps ->
      ps ++
      [ Use loc name p' ps' |
        p' <- shrink p, ps' <- shrink ps ]
    Invoke loc name p ps t ->
      ps ++
      [ Invoke loc name p' ps' t' |
        p' <- shrink p, ps' <- shrink ps, t' <- shrink t ]


We’ve defined what a proof is; now let’s tackle what it means for a proof to be valid.

Proof checking requires dealing with effects of a few kinds.

This is a job for monads.

First we introduce types for the hypothesis environment; this will help us keep track of which hypotheses have been introduced but not discharged.

data HypEnv = HypEnv
  { theHypEnv :: M.Map HypName Jud
  } deriving (Eq, Show)

data HypName = HypName String
  deriving (Eq, Ord, Show)

instance Arbitrary HypName where
  arbitrary = HypName <$> (listOf1 $ elements _hypname_chars)

_hypname_chars = concat
  [ "abcdefghijklmnopqrstuvwxyz"
  , "0123456789-_"

instance HasExprVars HypEnv where
  freeExprVars (HypEnv hs) =
    S.unions $ map freeExprVars $ M.elems hs
  renameFreeExpr (u,v) (HypEnv hs) =
    HypEnv $ (renameFreeExpr (u,v)) hs
  renameBoundExpr avoid (HypEnv hs) =
    HypEnv $ (renameBoundExpr avoid) hs

instance Arbitrary HypEnv where
  arbitrary = HypEnv <$> arbitrary

  shrink (HypEnv hs) = map HypEnv $ shrink hs

We also need a structure to keep track of what assumptions have been made. This will be the log type for a writer monad. It’s important that we also keep track of whether the same number has been used to encode two different assumptions.

data Assumptions
  = Assumptions (M.Map Int Jud) (S.Set Int)
  deriving (Eq, Show)

instance HasExprVars Assumptions where
  freeExprVars (Assumptions as _) =
    S.unions $ map freeExprVars $ M.elems as
  renameFreeExpr (u,v) (Assumptions as ws) =
    Assumptions ( (renameFreeExpr (u,v)) as) ws
  renameBoundExpr avoid (Assumptions as ws) =
    Assumptions ( (renameBoundExpr avoid) as) ws

instance Arbitrary Assumptions where
  arbitrary = Assumptions <$> arbitrary <*> arbitrary

  shrink (Assumptions m ks) =
    [ Assumptions n ls | n <- shrink m, ls <- shrink ks ] ++
    [ Assumptions m ls | ls <- shrink ks ] ++
    [ Assumptions n ks | n <- shrink m ]

Assumptions need to be a Monoid as well.

instance Semigroup Assumptions where
  (Assumptions m1 k1) <> (Assumptions m2 k2) =
    Assumptions (M.union m1 m2) $
        [ k1, k2
        , S.filter (\k -> M.lookup k m1 /= M.lookup k m2) $
          S.intersection (M.keysSet m1) (M.keysSet m2)

instance Monoid Assumptions where
  mempty = Assumptions mempty mempty

Now Check is a hand rolled stack of reader, writer, error, and state monads.

data Check a = Check
  { runCheck
      :: (RuleEnv, HypEnv)
      -> Either VerifyError (a, (HypEnv, Assumptions))

The monad instance for Check is standard stuff.

instance Monad Check where
  return a = Check $ \(_,hs) ->
    Right (a, (hs, mempty))

  x >>= f = Check $ \(rs,hs) ->
    case runCheck x (rs,hs) of
      Left err -> Left err
      Right (a, (hs', w1)) ->
        case runCheck (f a) (rs,hs') of
          Left err -> Left err
          Right (b, (hs'', w2)) ->
            Right (b, (hs'', w1 <> w2))

instance Applicative Check where
  pure = return
  (<*>) = ap

instance Functor Check where
  fmap f x = x >>= (return . f)

So Check a represents a computation that can read from a rule environment, can alter a hypothesis environment, and will return either an a with an assumption log or a verification error.

We need a few helpers. First one that throws a verification error:

checkError :: VerifyError -> Check a
checkError err = Check $ \_ -> Left err

We also have a rogues gallery of things that can go wrong with a proof.

data VerifyError
  = HypAlreadyDefined HypName Jud
  | HypNotFound HypName
  | HypNotDischarged [HypName]
  | MalformedDischarge Loc Jud Jud
  | BadSubstitution (Sub Expr)
  | RuleNotFound RuleName
  | MalformedSubstitution Loc
  | RuleDoesNotMatch Loc RuleName Rule [Jud]
  | InvokeDoesNotMatch Loc RuleName Rule Rule [Jud]
  | ReusedAssumptions (S.Set Int)
  | ProofDoesNotMatch Rule Jud [Jud]
  | RuleAlreadyDefined RuleName
  | TypeAlreadyDefined PolyType
  | FreeVariableInPremise Loc (Var Expr)
  | BindingFreeVar Loc (Var Expr) Jud
  | EqExpected Loc
  | NotEqual Loc
  | BadEqSubstitutionRHS Loc
  | BadEqSubstitutionLHS Loc
  | MalformedIntroU Loc
  | MalformedElimU Loc
  | MalformedIntroE Loc
  | SomeVarMismatch Loc
  | SomeSubMismatch Loc
  | AllExpected Loc
  | MalformedElimE Loc
  | ElimEBindVar Loc
  | AllVarMismatch Loc (Var Expr) (Var Expr) Jud Proof
  | TypeUnificationError Loc UnificationError
  | InferenceError Loc TypeError
  deriving (Eq, Show)

A helper for adding a new hypothesis to the environment, making sure its name is unique:

introHyp :: HypName -> Jud -> Check ()
introHyp name p = Check $ \(_, HypEnv hs) ->
  case M.lookup name hs of
    Nothing ->
      Right ((), (HypEnv $ M.insert name p hs, mempty))
    Just q ->
      if q == p
        then Right ((), (HypEnv hs, mempty))
        else Left $ HypAlreadyDefined name p

A helper for logging an assumption:

assume :: Int -> Jud -> Check ()
assume k p = Check $ \(_,hs) ->
  Right ((), (hs, Assumptions (M.fromList [(k,p)]) mempty))

A helper for discharging a hypothesis:

dischargeHyp :: HypName -> Check Jud
dischargeHyp name = Check $ \(_, HypEnv hs) ->
  case M.lookup name hs of
    Nothing ->
      Left $ HypNotFound name
    Just j ->
      Right (j, (HypEnv $ M.delete name hs, mempty))

A helper for looking up a rule in the environment.

lookupRule :: RuleName -> Check Rule
lookupRule name = Check $ \(RuleEnv rs, hs) ->
  case M.lookup name rs of
    Nothing -> Left $ RuleNotFound name
    Just r -> Right (r, (hs, mempty))

And a helper for checking that a variable is unused in the undischarged premises of a proof.

unusedInHyp :: Loc -> Var Expr -> Check a -> Check a
unusedInHyp loc x m = Check $ \(rs, hs) ->
  case runCheck m (rs,hs) of
    Left err -> Left err
    Right (a, (hs, as)) ->
      if (S.member x (freeExprVars hs))
           || (S.member x (freeExprVars as))
        then Left $ FreeVariableInPremise loc x
        else Right (a, (hs, as))

We’re finally prepared to check a proof. The result of checking the proof will be the conclusion of the theorem statement.

checkProof :: Proof -> Check Jud
checkProof = \case
  Assume _ k p -> do
    assume k p
    return p

Assumptions are valid evidence of themselves. Note that we also add the assumption to the environment.

  Hyp _ name p -> do
    introHyp name p
    return p

Hypotheses are also valid evidence of themselves; but note that we add the name and judgement to the current hypothesis environment.

  Dis loc name w pf -> do
    q <- checkProof pf
    p <- dischargeHyp name
    if w == (JImpl Q p q)
      then return (JImpl Q p q)
      else checkError $ MalformedDischarge loc w (JImpl Q p q)

To check a discharge proof, we recursively check its child proof and look up and discharge the corresponding hypothesis before returning an implication judgement.

  ElimEq loc w x p pe pf -> do
    eq <- checkProof pe
    case eq of
      JEq _ lhs rhs -> do
        q <- checkProof pf
        if q == (x --> lhs) $> p
          then if w == (x --> rhs) $> p
            then return $ (x --> rhs) $> p
            else checkError $ BadEqSubstitutionRHS loc
          else checkError $ BadEqSubstitutionLHS loc
      _ -> checkError $ EqExpected loc

  IntroEq loc q -> do
    case q of
      JEq loc' e1 e2 -> if e1 == e2
        then return $ JEq loc' e1 e2
        else checkError $ NotEqual loc
      _ -> checkError $ EqExpected loc

The equality elimination and introduction rules need to ensure we’ve given proofs of the correct form.

  IntroU loc w x y pf -> do
    q <- unusedInHyp loc x $ checkProof pf
    if S.member y (freeExprVars q)
      then checkError $ BindingFreeVar loc y q
      else if w == JAll loc y ((x --> EVar loc y) $> q)
        then return $ JAll loc y ((x --> EVar loc y) $> q)
        else checkError $ MalformedIntroU loc

  ElimU loc w x e pf -> do
    q <- checkProof pf
    case q of
      JAll _ z p ->
        if z == z
          then if w == (z --> e) $> p
            then return $ (z --> e) $> p
            else checkError $ MalformedElimU loc
          else checkError $ AllVarMismatch loc x z w pf
      _ -> checkError $ AllExpected loc

The universal introduction and elimination rules need to check their respective side conditions.

  IntroE loc w x e pf -> do
    q <- checkProof pf
    case w of
      JSome _ y p -> do
        if x == y
          then if q == (x --> e) $> p
            then return w
            else checkError $ SomeSubMismatch loc
          else checkError $ SomeVarMismatch loc
      _ -> checkError $ MalformedIntroE loc

  ElimE loc w u x pe pi -> do
    qe <- checkProof pe
    qi <- unusedInHyp loc u $ checkProof pi
    case (qe, qi) of
      (JSome _ y pe, JImpl _ pi m) ->
        if y == x
          then if pi == (x --> (EVar Q u)) $> pe
            then if (S.member u (freeExprVars pe))
                   || (S.member u (freeExprVars m))
              then checkError $ ElimEBindVar loc
              else if w == m
                then return w
                else checkError $ MalformedElimE loc
            else checkError $ MalformedElimE loc
          else checkError $ SomeVarMismatch loc
      _ -> checkError $ MalformedElimE loc

The existential introduction and elimination rules need to check their respective side conditions.

  Use loc name c ps -> do
    hs <- mapM checkProof ps
    r <- lookupRule name
    case matchRule r c hs of
      Nothing -> checkError $ RuleDoesNotMatch loc name r (c:hs)
      Just _ -> return c
  Invoke loc name c ps t -> do
    hs <- mapM checkProof ps
    r <- lookupRule name
    case matchRule (captureJudSubRule t r) c hs of
      Nothing -> checkError $ InvokeDoesNotMatch loc name r (captureJudSubRule t r) (c:hs)
      Just _ -> return c

Finally we have Use; these proofs are checked by recursively checking the child proofs and then verifying that the named rule matches.

And with that, we can express and check proofs. The check function

  1. recursively checks all nodes in the proof;
  2. ensures that all hypotheses are discharged;
  3. and verifies that the assumptions are numbered consistently

before returning the conclusion and premises of the proof.

check :: RuleEnv -> Proof -> Either VerifyError (Jud, [Jud])
check rules proof =
  case runCheck (checkProof proof) (rules, HypEnv M.empty) of
    Left err -> Left err
    Right (j, (HypEnv hs, Assumptions as ks)) -> if not $ M.null hs
      then Left $ HypNotDischarged $ M.keys hs
      else if not $ S.null ks
        then Left $ ReusedAssumptions ks
        else Right (j, M.elems as)

validate takes the proof check one step further, comparing the conclusion and premises of a proof to some rule.

validate :: RuleEnv -> Rule -> Proof -> Either VerifyError ()
validate env (Rule cr ars) pf = do
  (ct, ats) <- check env pf
  if (ct == cr) && (ats == ars)
    then return ()
    else Left $ ProofDoesNotMatch (Rule cr ars) ct ats


We can also type check proofs.

checkTypes :: Proof -> TypeEnv -> Infer TypeEnv
checkTypes proof env = case proof of
  Assume _ _ q -> typeCheck q env
  Hyp _ _ q -> typeCheck q env

  Dis _ _ w pf -> concatM
    [ typeCheck w
    , checkTypes pf
    ] env
  IntroEq _ p -> typeCheck p env
  ElimEq _ w x q pe pf -> concatM
    [ typeCheck w
    , typeCheck q
    , checkTypes pe
    , checkTypes pf
    ] env
  IntroU _ w x y pf -> concatM
    [ typeCheck w
    , checkTypes pf
    ] env
  ElimU _ w x e pf -> concatM
    [ typeCheck w
    , checkTypes pf
    ] env
  IntroE _ w x e pf -> concatM
    [ typeCheck w
    , checkTypes pf
    ] env
  ElimE _ w u x pe pi -> concatM
    [ typeCheck w
    , checkTypes pe
    , checkTypes pi
    ] env
  Use _ n q pfs -> concatM
    ( typeCheck q : map checkTypes pfs ) env
  Invoke _ n q pfs s -> concatM
    ( typeCheck q : map checkTypes pfs ) env

We just need a utility for lifting inference errors to verification errors.

liftInfer :: Loc -> Infer a -> Either VerifyError a
liftInfer loc x = case execInfer x of
  Left (Left err) -> Left $ TypeUnificationError loc err
  Left (Right err) -> Left $ InferenceError loc err
  Right a -> return a


An axiom is a rule we accept without proof, while a theorem is a rule we accept only with a valid proof. Collectively axioms and theorems are called claims.

data Claim
  = Axiom RuleType RuleName Rule
  | Theorem RuleName Rule Proof
  | TypeDecl (Con Expr) MonoType
  deriving (Eq, Show)

data RuleType
  = InferenceRule
  | Definition
  deriving (Eq, Show)

instance Arbitrary Claim where
  arbitrary = do
    k <- arbitrary :: Gen Int
    case k`mod`3 of
      0 -> Axiom <$> arbitrary <*> arbitrary <*> arbitrary
      1 -> Theorem <$> arbitrary <*> arbitrary <*> arbitrary
      _ -> TypeDecl <$> arbitrary <*> arbitrary

instance Arbitrary RuleType where
  arbitrary = do
    p <- arbitrary
    if p
      then return InferenceRule
      else return Definition

A theory is a list of claims with the property that proofs only refer to named claims appearing earlier in the list. If the proof of a rule is valid, it can be added to the rule environment.

addRule :: RuleName -> Rule -> RuleEnv -> Either VerifyError RuleEnv
addRule name rule (RuleEnv m) =
  case M.lookup name m of
    Nothing -> Right $ RuleEnv $ M.insert name rule m
    Just _ -> Left $ RuleAlreadyDefined name

  :: Con Expr -> MonoType -> TypeEnv -> Either VerifyError TypeEnv
addType x t env@(TypeEnv m) =
  case M.lookup (Left x) m of
    Nothing -> Right $ TypeEnv $ M.insert (Left x) (generalize env t) m
    Just _ -> Left $ TypeAlreadyDefined (generalize env t)

  :: (TypeEnv, RuleEnv) -> (Loc, Claim)
  -> Either VerifyError (TypeEnv, RuleEnv)
checkClaim (typeEnv, ruleEnv) (loc, claim) = case claim of
  Axiom _ name rule -> do
    ruleEnv' <- addRule name rule ruleEnv
    liftInfer loc $ typeCheck rule typeEnv
    return (typeEnv, ruleEnv')
  Theorem name rule proof -> do
    validate ruleEnv rule proof
    liftInfer loc $ checkTypes proof typeEnv
    ruleEnv' <- addRule name rule ruleEnv
    return (typeEnv, ruleEnv')
  TypeDecl x t -> do
    typeEnv' <- addType x t typeEnv
    return (typeEnv', ruleEnv)

We can also check an entire list of claims, adding each to the rule environment as it is checked.

  :: (TypeEnv, RuleEnv) -> [(Loc, Claim)]
  -> Either VerifyError (TypeEnv, RuleEnv)
checkClaims env cs = case cs of
  [] -> return env
  a:as -> do
    env' <- checkClaim env a
    checkClaims env' as