Permalink
Browse files

Added the XIH rule, an obvious conservative extension.

  • Loading branch information...
luqui committed Jun 11, 2009
1 parent b72cdee commit f7ed462fb5268d4e97c568b6145b76a72cef2cf6
Showing with 28 additions and 4 deletions.
  1. +5 −2 ixi/IXi/Proof.hs
  2. +12 −1 ixi/IXi/Sequent.hs
  3. +11 −1 ixi/IXi/Tactic.hs
View
@@ -1,7 +1,7 @@
module IXi.Proof
( Proof
, hypothesis, conversion
- , implRule, xiRule, hxiRule, hhRule
+ , implRule, xiRule, hxiRule, hhRule, xihRule
, theorem
, Theorem, thmStatement, prove
)
@@ -20,6 +20,7 @@ data Proof
| XiRule Name Proof Proof
| HXiRule Name Proof Proof
| HHRule
+ | XIHRule Int
| Theorem Theorem
hypothesis = Hypothesis
@@ -28,6 +29,7 @@ implRule = ImplRule
xiRule = XiRule
hxiRule = HXiRule
hhRule = HHRule
+xihRule = XIHRule
theorem = Theorem
@@ -54,11 +56,12 @@ checkProof (HXiRule name hproof hxiproof) seq = do
checkProof HHRule seq = S.hhRule seq
+checkProof (XIHRule z) seq = S.xihRule z seq
+
checkProof (Theorem (MkTheorem t _)) (hyps S.:|- goal)
| goal == t = Right ()
| otherwise = Left "Goal does not match theorem"
-
data Theorem = MkTheorem Term Proof
instance Show Theorem where
View
@@ -3,7 +3,8 @@ module IXi.Sequent
, goal, hypotheses
, Err
, hypothesis, conversion, implRule
- , xiRule, hxiRule, hhRule
+ , xiRule, hxiRule, hhRule, xihRule
+ , newName
)
where
@@ -66,3 +67,13 @@ hxiRule _ _ = invalid "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"
+
+newName :: Sequent -> Name
+newName seq = safeName' (goal seq : hypotheses seq)
+
+-- conservative extension, Γ,x |- Hx
+xihRule :: Int -> Sequent -> Err ()
+xihRule z (hyps :|- goal)
+ | not (0 <= z && z <= length hyps) = invalid "Index out of range"
+ | not (H :% (hyps !! z) == goal) = invalid "Hypothesis does not match goal"
+ | otherwise = valid ()
View
@@ -1,7 +1,8 @@
module IXi.Tactic
( Tactic, Hypothesis
- , hypothesis, conversion, implRule, xiRule, hxiRule, hhRule
+ , hypothesis, conversion, implRule, xiRule, hxiRule, hhRule, xihRule
, inspect, (>|<)
+ , newName
)
where
@@ -56,9 +57,18 @@ hhRule = Tactic $ \seq -> do
() <- Seq.hhRule seq
return P.hhRule
+xihRule :: Hypothesis -> Tactic
+xihRule (Hypothesis z) = Tactic $ \seq -> do
+ let ix = length (Seq.hypotheses seq) - z - 1
+ () <- Seq.xihRule ix seq
+ return (P.xihRule ix)
+
inspect :: (Seq.Sequent -> Tactic) -> Tactic
inspect f = Tactic $ \seq -> unTactic (f seq) seq
+newName :: (Name -> Tactic) -> Tactic
+newName f = Tactic $ \seq -> unTactic (f (Seq.newName seq)) seq
+
infixr 1 >|<
(>|<) :: Tactic -> Tactic -> Tactic
t >|< u = Tactic $ liftA2 mplus (unTactic t) (unTactic u)

0 comments on commit f7ed462

Please sign in to comment.