# luqui/dana

Woo, first proof completed!

1 parent 1b4d766 commit 733ab02ac4f61e73986b1d24c30d2e2b35324264 committed Jun 11, 2009
Showing with 80 additions and 21 deletions.
1. +1 −1 ixi/IXi/Helpers.hs
2. +13 −13 ixi/IXi/Sequent.hs
3. +12 −7 ixi/IXi/Tactic.hs
4. +54 −0 ixi/IXi/Tactics.hs
2 ixi/IXi/Helpers.hs
 @@ -55,4 +55,4 @@ convExpandK y = mconcat [ convExpandConst y, convInAppL convExpandLambda ] -convReduceK = mconcat [convBetaReduce, convBetaReduce] +convReduceK = mconcat [convInAppL convBetaReduce, convBetaReduce]
26 ixi/IXi/Sequent.hs
 @@ -23,50 +23,50 @@ hypotheses (h :|- g) = h type Err = Either String valid = Right -invalid = Left +invalid g x = Left (x ++ "\n|- " ++ show g) hypothesis :: Int -> Sequent -> Err () hypothesis z (hyps :|- goal) | not (0 <= z && z < length hyps) - = invalid "Index out of range" + = invalid goal "Index out of range" | not (hyps !! z == goal) - = invalid "Hypothesis does not match goal" + = invalid goal \$ "Hypothesis (" ++ show (hyps !! z) ++ ") does not match goal" | otherwise = valid () conversion :: Conversion -> Sequent -> Err Sequent conversion c (hyps :|- goal) = case convert c goal of - Nothing -> invalid "Goal conversion failed" + Nothing -> invalid goal "Goal conversion failed" Just goal' -> valid (hyps :|- goal') implRule :: Term -> Sequent -> Err (Sequent, Sequent) implRule p (hyps :|- q :% x) = valid (hyps :|- p :% x, hyps :|- Xi :% p :% q) -implRule _ _ = invalid "Goal is not an application" +implRule _ (hyps :|- goal) = invalid goal "Goal is not an application" xiRule :: Name -> Sequent -> Err (Sequent, Sequent) -xiRule name (hyps :|- Xi :% a :% b) +xiRule name (hyps :|- goal@(Xi :% a :% b)) | nameFree name a || nameFree name b || any (nameFree name) hyps - = invalid "Name must not be free in environment" + = invalid goal "Name must not be free in environment" | otherwise = valid (hyps :|- H :% (a :% n), (a :% n):hyps :|- b :% n) where n = NameVar name -xiRule _ _ = invalid "Goal is not a Xi-form" +xiRule _ (hyps :|- goal) = invalid goal "Goal is not a Xi-form" hxiRule :: Name -> Sequent -> Err (Sequent, Sequent) -hxiRule name (hyps :|- H :% (Xi :% a :% b)) +hxiRule name (hyps :|- goal@(H :% (Xi :% a :% b))) | nameFree name a || nameFree name b || any (nameFree name) hyps - = invalid "Name must not be free in environment" + = invalid goal "Name must not be free in environment" | otherwise = valid (hyps :|- H :% (a :% n), (a :% n):hyps :|- H :% (b :% n)) where n = NameVar name -hxiRule _ _ = invalid "Goal is not an H-Xi-form" +hxiRule _ (hyps :|- goal) = invalid goal "Goal is not an H-Xi-form" hhRule :: Sequent -> Err () hhRule (hyps :|- H :% (H :% x)) = valid () -hhRule _ = invalid "Goal is not an H-H-form" +hhRule (hyps :|- goal) = invalid goal "Goal is not an H-H-form" newName :: Sequent -> Name newName seq = safeName' (goal seq : hypotheses seq) @@ -76,4 +76,4 @@ xihRule :: Sequent -> Err Sequent xihRule (hyps :|- goal) = case goal of H :% x -> valid (hyps :|- x) - _ -> invalid "Goal is not an H-form" + _ -> invalid goal "Goal is not an H-form"
19 ixi/IXi/Tactic.hs
 @@ -1,8 +1,8 @@ module IXi.Tactic - ( Tactic + ( Tactic, Hypothesis , conversion, implRule, xiRule, hxiRule, hhRule, xihRule, theorem , inspect, (>|<) - , newName + , newName, failure , prove ) where @@ -15,11 +15,13 @@ import Control.Applicative import Control.Monad (ap, MonadPlus(..)) newtype Tactic = Tactic { unTactic :: Seq.Sequent -> Seq.Err P.Proof } +type Hypothesis = Tactic topHyp :: Seq.Sequent -> Tactic topHyp seq = Tactic \$ \seq' -> do - () <- Seq.hypothesis ix seq' - return (P.hypothesis ix) + let ix' = length (Seq.hypotheses seq') - ix - 1 + () <- Seq.hypothesis ix' seq' + return (P.hypothesis ix') where ix = length (Seq.hypotheses seq) - 1 @@ -36,14 +38,14 @@ implRule p pxTac xpqTac = Tactic \$ \seq -> do xpqPf <- unTactic xpqTac xpqSeq return (P.implRule p pxPf xpqPf) -xiRule :: Name -> Tactic -> (Tactic -> Tactic) -> Tactic +xiRule :: Name -> Tactic -> (Hypothesis -> Tactic) -> Tactic xiRule name hTac implTac = Tactic \$ \seq -> do (hSeq, implSeq) <- Seq.xiRule name seq hPf <- unTactic hTac hSeq implPf <- unTactic (implTac (topHyp implSeq)) implSeq return (P.xiRule name hPf implPf) -hxiRule :: Name -> Tactic -> (Tactic -> Tactic) -> Tactic +hxiRule :: Name -> Tactic -> (Hypothesis -> Tactic) -> Tactic hxiRule name hTac implTac = Tactic \$ \seq -> do (hSeq, implSeq) <- Seq.hxiRule name seq hPf <- unTactic hTac hSeq @@ -55,7 +57,7 @@ hhRule = Tactic \$ \seq -> do () <- Seq.hhRule seq return P.hhRule -xihRule :: Tactic -> Tactic +xihRule :: Hypothesis -> Tactic xihRule tac = Tactic \$ \seq -> do seq' <- Seq.xihRule seq pf <- unTactic tac seq' @@ -73,6 +75,9 @@ inspect f = Tactic \$ \seq -> unTactic (f seq) seq newName :: (Name -> Tactic) -> Tactic newName f = Tactic \$ \seq -> unTactic (f (Seq.newName seq)) seq +failure :: Tactic +failure = Tactic \$ \seq -> mzero + infixr 1 >|< (>|<) :: Tactic -> Tactic -> Tactic t >|< u = Tactic \$ liftA2 mplus (unTactic t) (unTactic u)
54 ixi/IXi/Tactics.hs
 @@ -0,0 +1,54 @@ +module IXi.Tactics where + +import IXi.Tactic +import IXi.HOAS +import IXi.Term +import IXi.Helpers +import IXi.Conversion + +_K = fun (\x -> fun (\y -> x)) +_I = fun (\x -> x) + +p ==> q = _Xi % (_K % p) % (_K % q) + +-- |- Q +-- |- KQI +-- |- Ξ(KP)(KQ) +-- |- P ==> Q +-- |- KPI +-- |- P +modusPonens :: Exp -> Tactic -> Tactic -> Tactic +modusPonens p pqPf pPf = + conversion (convExpandK (hoas _I)) \$ + implRule (hoas (_K % p % _I)) (conversion convReduceK pPf) pqPf + +-- |- P ==> Q +-- |- Ξ(KP)(KQ) +-- |- H(KPx) +-- |- HP +-- KPx |- KQx +-- P |- Q +implAbstract :: Tactic -> (Hypothesis -> Tactic) -> Tactic +implAbstract hpPf pqPf = + newName \$ \name -> + xiRule name (conversion (convInAppR convReduceK) hpPf) + (\kpx -> conversion convReduceK (pqPf (conversion (convExpandK (NameVar name)) kpx))) + + +-- |- ΞA(\x. B) +-- |- H(Ax) +-- Ax |- (\x. B)x +-- Ax |- B +lambdaXiRule :: Name -> Tactic -> (Hypothesis -> Tactic) -> Tactic +lambdaXiRule x haPf abPf = + xiRule x haPf (\ax -> conversion convBetaReduce (abPf ax)) + +-- |- ΞH(\P. P ==> P) +-- |- H(Hx) +-- HP |- P ==> P +-- HP |- HP +-- HP, P |- P +impl_refl = prove (hoas (_Xi % _H % fun (\p -> p ==> p))) \$ + newName \$ \pvar -> + lambdaXiRule pvar hhRule \$ \hp -> + implAbstract hp (\p -> p)