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 JudAn inference rule consists of a conclusion and zero or more premises, where the conclusion and premises are judgements.
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)
where
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)
_ -> NothingNote 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.
test_match_rule
:: Rule -> Jud -> [Jud] -> Bool
test_match_rule r@(Rule cr hrs) ct hts =
case matchRule r ct hts of
Nothing -> True
Just (js,es) ->
let
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.
test_match_rule_self
:: Rule -> Bool
test_match_rule_self r@(Rule c hs) =
case matchRule r c hs of
Nothing -> False
Just (_,es) -> trivialExprSub esAnd if we apply a substitution to a rule, it should match the result.
test_match_rule_sub
:: 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 _ -> TrueIn 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)) envFor 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
(Rule
(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"
, "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.
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!
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.
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 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 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\).
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)
_ -> FalseAnd here’s an Arbitrary instance.
instance Arbitrary Proof where
arbitrary = getSize >>= genDepth
where
genDepth k
| k <= 0 = oneof
[ Assume <$> arbitrary <*> (abs <$> arbitrary) <*> arbitrary
, Hyp <$> arbitrary <*> arbitrary <*> arbitrary
]
| otherwise = do
let recur = genDepth =<< elements [0..(div k 2)]
oneof
[ 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"
, "ABCDEFGHIJKLMNOPQRSTUVWXYZ"
, "0123456789-_"
]
instance HasExprVars HypEnv where
freeExprVars (HypEnv hs) =
S.unions $ map freeExprVars $ M.elems hs
renameFreeExpr (u,v) (HypEnv hs) =
HypEnv $ M.map (renameFreeExpr (u,v)) hs
renameBoundExpr avoid (HypEnv hs) =
HypEnv $ M.map (renameBoundExpr avoid) hs
instance Arbitrary HypEnv where
arbitrary = HypEnv <$> arbitrary
shrink (HypEnv hs) = map HypEnv $ shrink hsWe 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 (M.map (renameFreeExpr (u,v)) as) ws
renameBoundExpr avoid (Assumptions as ws) =
Assumptions (M.map (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) $
S.unions
[ 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 memptyNow 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:
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 pA 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.
Assumptions are valid evidence of themselves. Note that we also add the assumption to the environment.
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 locThe 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 locThe 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 locThe 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 cFinally 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
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 atsWe 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 ) envWe 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 aAn 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 DefinitionA 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
addType
:: 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)
checkClaim
:: (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.