ideas-math-1.0: src/Domain/Logic/Proofs.hs
{-# LANGUAGE RankNTypes #-}
-----------------------------------------------------------------------------
-- Copyright 2013, Open Universiteit Nederland. This file is distributed
-- under the terms of the GNU General Public License. For more information,
-- see the file "LICENSE.txt", which is included in the distribution.
-----------------------------------------------------------------------------
-- |
-- Maintainer : bastiaan.heeren@ou.nl
-- Stability : provisional
-- Portability : portable (depends on ghc)
--
-- Exercise for the logic domain: to prove two propositions equivalent
--
-----------------------------------------------------------------------------
module Domain.Logic.Proofs
( proofExercise, proofUnicodeExercise
) where
import Control.Arrow
import Control.Monad
import Data.Foldable (toList)
import Data.Function (on)
import Data.List
import Data.Maybe
import Domain.Logic.BuggyRules
import Domain.Logic.Examples
import Domain.Logic.Formula
import Domain.Logic.GeneralizedRules
import Domain.Logic.Generator (equalLogicA)
import Domain.Logic.Parser
import Domain.Logic.Rules
import Domain.Logic.Strategies (somewhereOr)
import Domain.Math.Expr ()
import Ideas.Common.Algebra.Boolean
import Ideas.Common.Library
import Ideas.Common.Rewriting.AC
import Ideas.Common.Traversal.Navigator
import Ideas.Common.Traversal.Utils
import Ideas.Common.Utils
{-
see :: Int -> IO ()
see n = do
let a = snd (examples proofExercise !! n)
der = defaultDerivation proofExercise a
printDerivation proofExercise a
putStrLn $ ">> " ++ show (derivationLength der) ++ " steps\n"
-}
-- Currently, we use the DWA strategy
proofExercise :: Exercise Proof
proofExercise = makeExercise
{ exerciseId = describe "Prove two propositions equivalent" $
newId "logic.proof"
, status = Experimental
, parser = mapSecond makeProof . parseLogicProof False
, prettyPrinter = showProof
, equivalence = withoutContext equivalentProofs
, similarity = withoutContext similarProofs
, suitable = predicate $ all (uncurry eqLogic) . subProofs
, ready = predicate $ all (uncurry equalLogicA) . subProofs
, strategy = proofStrategy
, extraRules = map use extraLogicRules ++ inverseRules ++ map use buggyRules
, navigation = termNavigator
, examples = map (second makeProof) exampleProofs
}
proofUnicodeExercise :: Exercise Proof
proofUnicodeExercise = proofExercise
{ exerciseId = describe "Prove two propositions equivalent (unicode support)" $
newId "logic.propositional.proof.unicode"
, parser = mapSecond makeProof . parseLogicProof True
, prettyPrinter = showProofUnicode
}
type Proof = Logic (SLogic, SLogic)
subProofs :: Proof -> [(SLogic, SLogic)]
subProofs = toList
makeProof :: (SLogic, SLogic) -> Proof
makeProof = Var
proofPair :: Proof -> (SLogic, SLogic)
proofPair x = (catLogic (fmap fst x), catLogic (fmap snd x))
showProof :: Proof -> String
showProof = uncurry f . proofPair
where
f p q = ppLogicPars p ++ " == " ++ ppLogicPars q
showProofUnicode :: Proof -> String
showProofUnicode = uncurry f . proofPair
where
f p q = ppLogicUnicodePars p ++ " == " ++ ppLogicUnicodePars q
equivalentProofs :: Proof -> Proof -> Bool
equivalentProofs proof1 proof2 =
let (p1, q1) = proofPair proof1
(p2, q2) = proofPair proof2
in eqLogic p1 p2 && eqLogic q1 q2
similarProofs :: Proof -> Proof -> Bool
similarProofs proof1 proof2 =
let (p1, q1) = proofPair proof1
(p2, q2) = proofPair proof2
in equalLogicA p1 p2 && equalLogicA q1 q2
proofStrategy :: LabeledStrategy (Context Proof)
proofStrategy = label "proof equivalent" $
repeatS (
somewhere splitTop
-- somewhere (useC commonExprAtom) -- (tijdelijk uitgezet)
|> useC dnfStrategyDWA
)
<*> use checkDNF <*> normStrategy
where
splitTop = use topIsNot <|> use topIsImpl
-- only use commutativity if not already in desired order
<|> (use topIsAnd |> use topIsAndCom)
<|> (use topIsOr |> use topIsOrCom)
<|> use topIsEquiv
checkDNF :: Rule Proof
checkDNF = minor $ makeRule "is-dnf" $ \proof -> do
guard $ and [ isDNF p && isDNF q | (p, q) <- subProofs proof ]
Just proof
normStrategy :: Strategy (Context Proof)
normStrategy = repeatS $
somewhere (use ruleFalseZeroAnd <|> use ruleTrueZeroOr)
|> somewhere (use ruleComplAnd)
|> somewhere (
use ruleIdempOr <|>
use ruleIdempAnd <|>
use ruleAndOverOr <|>
use ruleFalseZeroOr
)
|> oncetd (use sortRuleAnd)
|> oncetd (use sortRuleOr)
|> somewhereDisjunct introduceVar
sortRuleBy :: (b -> b -> Ordering) -> View a [b] -> Transformation a
sortRuleBy cmp v = makeTrans $ \p -> do
xs <- match v p
guard (not (sortedBy cmp xs))
let ys = sortBy cmp xs
return (build v ys)
sortRuleOr :: Rule SLogic
sortRuleOr = ruleTrans "CommOr.sort" $
sortRuleBy compareVar $ disjunctions <-> ors
sortRuleAnd :: Rule SLogic
sortRuleAnd = ruleTrans "CommAnd.sort" $
sortRuleBy compareVar $ conjunctions <-> ands
compareVar :: Ord a => Logic a -> Logic a -> Ordering
compareVar = compare `on` (\x -> (varsLogic x, x))
sortedBy :: (a -> a -> Ordering) -> [a] -> Bool
sortedBy cmp = rec
where
rec (x:y:zs) = cmp x y /= GT && rec (y:zs)
rec _ = True
-----------------------------------------------------------------------------
-- To DNF, with priorities (the "DWA" approach)
dnfStrategyDWA :: Strategy (Context SLogic)
dnfStrategyDWA =
toplevel <|> somewhereOr
( label "Simplify" simpler
|> label "Sort and simplify" (sortAndSimplify |> deMorganAndSimplify)
|> label "Eliminate implications/equivalences" eliminateImplEquiv
|> label "Eliminate nots" eliminateNots
|> label "Move ors to top" orToTop
)
where
toplevel = useRules
[ ruleFalseZeroOr, ruleTrueZeroOr, ruleIdempOr
, ruleAbsorpOr, ruleComplOr
]
simpler = somewhere $ useRules
[ ruleFalseZeroOr, ruleTrueZeroOr, ruleTrueZeroAnd
, ruleFalseZeroAnd, ruleNotTrue, ruleNotFalse
, ruleNotNot, ruleIdempOr, ruleIdempAnd, ruleAbsorpOr, ruleAbsorpAnd
, ruleComplOr, ruleComplAnd
]
sortAndSimplify = somewhere $
use ruleAbsorpOrNot
<|> (use sortForIdempOr <*> try (use ruleIdempOr))
<|> (use sortForIdempAnd <*> try (use ruleIdempAnd))
<|> (use sortForComplOr <*> try (use ruleComplOr))
<|> (use sortForComplAnd <*> try (use ruleComplAnd))
deMorganAndSimplify = somewhere $
(use ruleDeMorganOrNot <*> try (oncetd (use ruleNotNot)))
<|> (use ruleDeMorganAndNot <*> try (oncetd (use ruleNotNot)))
eliminateImplEquiv =
oncetd (use ruleDefImpl)
|> oncebu (use ruleDefEquiv)
eliminateNots = somewhere $ useRules
[ generalRuleDeMorganAnd, generalRuleDeMorganOr
, ruleDeMorganAnd, ruleDeMorganOr
]
orToTop = somewhere $ useRules
[ generalRuleAndOverOr, ruleAndOverOr ]
useRules :: [Rule SLogic] -> Strategy (Context SLogic)
useRules = alternatives . map liftToContext
{-
normLogicRule :: Rule (SLogic, SLogic)
normLogicRule = ruleMaybe "Normalize" $ \tuple@(p, q) -> do
guard (p /= q)
let xs = sort (varsLogic p `union` varsLogic q)
new = (normLogicWith xs p, normLogicWith xs q)
guard (tuple /= new)
return new -}
-- disabled for now
-- Find a common subexpression that can be treated as a box
{-
commonExprAtom :: Rule (Context (SLogic, SLogic))
commonExprAtom = minor $ ruleTrans "commonExprAtom" $ makeTransLiftContext $ \(p, q) -> do
let xs = filter (same <&&> complement isAtomic) (largestCommonSubExpr p q)
same cse = eqLogic (sub cse p) (sub cse q)
new = head (logicVars \\ (varsLogic p `union` varsLogic q))
sub a this
| a == this = Var new
| otherwise = descend (sub a) this
case xs of
hd:_ -> do
xs <- substRef :? []
substRef := (show new, show hd):xs
return (sub hd p, sub hd q)
_ -> fail "not applicable"
largestCommonSubExpr :: (Uniplate a, Ord a) => a -> a -> [a]
largestCommonSubExpr x = rec
where
uniX = S.fromList (universe x)
rec y | y `S.member` uniX = [y]
| otherwise = concatMap rec (children y)
substRef :: Ref [(String, String)]
substRef = makeRef "subst"
logicVars :: [ShowString]
logicVars = [ ShowString [c] | c <- ['a'..] ]
-}
{-
normLogic :: Ord a => Logic a -> Logic a
normLogic p = normLogicWith (sort (varsLogic p)) p
normLogicWith :: Eq a => [a] -> Logic a -> Logic a
normLogicWith xs p = make (filter keep (subsets xs))
where
keep ys = evalLogic (`elem` ys) p
make = ors . map atoms
atoms ys = ands [ f (x `elem` ys) (Var x) | x <- xs ]
f b = if b then id else Not
-}
-- p \/ q \/ ~p ~> reorder p and ~p
sortForComplOr :: Rule SLogic
sortForComplOr = ruleMaybe "ComplOr.sort" $ \p -> do
let xs = disjunctions p
ys = sortBy compareVar xs
guard (xs /= ys && any (\x -> Not x `elem` xs) xs)
return (ors ys)
-- p /\ q /\ ~p ~> reorder p and ~p
sortForComplAnd :: Rule SLogic
sortForComplAnd = ruleMaybe "ComplAnd.sort" $ \p -> do
let xs = conjunctions p
ys = sortBy compareVar xs
guard (xs /= ys && any (\x -> Not x `elem` xs) xs)
return (ands ys)
-- p \/ q \/ p ~> reorder p's
sortForIdempOr :: Rule SLogic
sortForIdempOr = ruleMaybe "IdempOr.sort" $ \p -> do
let xs = disjunctions p
ys = sortBy compareVar xs
guard (xs /= ys && not (distinct xs))
return (ors ys)
-- p /\ q /\ p ~> reorder p's
sortForIdempAnd :: Rule SLogic
sortForIdempAnd = ruleMaybe "IdempAnd.sort" $ \p -> do
let xs = conjunctions p
ys = sortBy compareVar xs
guard (xs /= ys && not (distinct xs))
return (ands ys)
{-
-- (p /\ q) \/ ... \/ (p /\ q /\ r) ~> (p /\ q) \/ ...
-- (subset relatie tussen rijtjes: bijzonder geval is gelijke rijtjes)
absorptionSubset :: Rule SLogic
absorptionSubset = ruleList "absorptionSubset" $ \p -> do
let xss = map conjunctions (disjunctions p)
yss = nub $ filter (\xs -> all (ok xs) xss) xss
ok xs ys = not (ys `isSubsetOf` xs) || xs == ys
guard (length yss < length xss)
return $ ors (map ands yss)
-- p \/ ... \/ (~p /\ q /\ r) ~> p \/ ... \/ (q /\ r)
-- (p is hier een losse variabele)
fakeAbsorption :: Rule SLogic
fakeAbsorption = makeRule "fakeAbsorption" $ \p -> do
let xs = disjunctions p
v <- [ a | a@(Var _) <- xs ]
let ys = map (ands . filter (/= Not v) . conjunctions) xs
new = ors ys
guard (p /= new)
return new
-- ~p \/ ... \/ (p /\ q /\ r) ~> ~p \/ ... \/ (q /\ r)
-- (p is hier een losse variabele)
fakeAbsorptionNot :: Rule SLogic
fakeAbsorptionNot = makeRule "fakeAbsorptionNot" $ \p -> do
let xs = disjunctions p
v <- [ a | Not a@(Var _) <- xs ]
let ys = map (ands . filter (/= v) . conjunctions) xs
new = ors ys
guard (p /= new)
return new -}
acTopRuleFor :: Bool -> (forall a . Isomorphism (Logic a) [Logic a])
-> Transformation Proof
acTopRuleFor com ep = makeTrans $ \proof -> do
pair <- maybeToList (getSingleton proof)
let pairings = if com then pairingsAC else pairingsA
ep2 = ep *** ep
(xs, ys) = from ep2 pair
guard (length xs > 1 && length ys > 1)
xs <- liftM (map (to ep2)) (pairings False xs ys)
guard (all (uncurry eqLogic) xs)
return (to ep (map Var xs))
collect :: View a (a, a) -> Isomorphism a [a]
collect v = f <-> g
where
f x = maybe [x] (\(y, z) -> f y ++ f z) (match v x)
g = foldr1 (curry (build v))
andView, orView, eqView :: View (Logic a) (Logic a, Logic a)
andView = makeView isAnd (uncurry (<&&>))
orView = makeView isOr (uncurry (<||>))
eqView = makeView isEq (uncurry equivalent)
where
isEq (p :<->: q) = Just (p, q)
isEq _ = Nothing
topIsAnd :: Rule Proof
topIsAnd = minor $ ruleTrans "top-is-and" $ acTopRuleFor False (collect andView)
topIsOr :: Rule Proof
topIsOr = minor $ ruleTrans "top-is-or" $ acTopRuleFor False (collect orView)
topIsEquiv :: Rule Proof
topIsEquiv = minor $ ruleTrans "top-is-equiv" $ acTopRuleFor False (collect eqView)
topIsAndCom :: Rule Proof
topIsAndCom = ruleTrans "top-is-and.com" $ acTopRuleFor True (collect andView)
topIsOrCom :: Rule Proof
topIsOrCom = ruleTrans "top-is-or.com" $ acTopRuleFor True (collect orView)
--topIsEquivCom :: Rule Proof
--topIsEquivCom = ruleTrans "top-is-equiv.com" $ acTopRuleFor True (collect eqView)
topIsImpl :: Rule Proof
topIsImpl = minorRule "top-is-impl" f
where
f (Var (p :->: q, r :->: s)) = do
guard (eqLogic p r && eqLogic q s)
return (Var (p, r) :->: Var (q, s))
f _ = Nothing
topIsNot :: Rule Proof
topIsNot = minorRule "top-is-not" f
where
f (Var (Not p, Not q)) = Just (Not (Var (p, q)))
f _ = Nothing
{- Strategie voor sterke(?) normalisatie
(prioritering)
1. p \/ q \/ ~p ~> T (propageren)
p /\ q /\ p ~> p /\ q
p /\ q /\ ~p ~> F (propageren)
2. (p /\ q) \/ ... \/ (p /\ q /\ r) ~> (p /\ q) \/ ...
(subset relatie tussen rijtjes: bijzonder geval is gelijke rijtjes)
p \/ ... \/ (~p /\ q /\ r) ~> p \/ ... \/ (q /\ r)
(p is hier een losse variabele)
~p \/ ... \/ (p /\ q /\ r) ~> ~p \/ ... \/ (q /\ r)
(p is hier een losse variabele)
3. a) elimineren wat aan een kant helemaal niet voorkomt (zie regel hieronder)
b) rijtjes sorteren
c) rijtjes aanvullen
Twijfelachtige regel bij stap 3: samennemen in plaats van aanvullen:
(p /\ q /\ r) \/ ... \/ (~p /\ q /\ r) ~> q /\ r
(p is hier een losse variable)
-}
-----------------------------------------------
-- Introduction of var
introduceVar :: Strategy (Context Proof)
introduceVar = check missing
<*> use introTrueLeft
<*> layer [] introCompl
missing :: Context Proof -> Bool
missing = isJust . missingVar
localEqVars :: Context Proof -> [ShowString]
localEqVars cp =
case currentTerm cp >>= fromTerm of
Just (p, q) -> varsLogic p `union` varsLogic q
Nothing -> maybe [] localEqVars (up cp)
missingVar :: Context Proof -> Maybe ShowString
missingVar cp =
case currentTerm cp >>= fromTerm of
Just p -> listToMaybe (localEqVars cp \\ varsLogic p)
Nothing -> Nothing
introTrueLeft :: Rule SLogic
introTrueLeft = rewriteRule "IntroTrueLeft" $
\x -> x :~> T :&&: x
introCompl :: Rule (Context Proof)
introCompl = makeRule "IntroCompl" $ \cp -> do
a <- missingVar (safe up cp)
let f = fromTerm >=> fmap toTerm . introTautology a
changeTerm f cp
where
introTautology :: a -> Logic a -> Maybe (Logic a)
introTautology a T = Just (Var a :||: Not (Var a))
introTautology _ _ = Nothing
{-
go = applyAll (somewhereDisjunct introduceVar) $ inContext proofExercise $
makeProof (p :||: (Not p :&&: q), p :||: q)
where
p = Var (ShowString "p")
q = Var (ShowString "q")
somewhereEq :: IsStrategy f => f (Context Proof) -> Strategy (Context Proof)
somewhereEq s = traverse [once, topdown]
(check isEq <*> layer [] s)
where
isEq :: Context Proof -> Bool
isEq cp = fromMaybe False $ do
t <- currentTerm cp
case fromTerm t :: Maybe (SLogic, SLogic) of
Just (p, q) -> return True
_ -> return False -}
somewhereDisjunct :: IsStrategy f => f (Context Proof) -> Strategy (Context Proof)
somewhereDisjunct s = oncetd (check isEq <*> layer [] (somewhereOrG s))
where
isEq :: Context Proof -> Bool
isEq cp = (isJust :: Maybe (SLogic, SLogic) -> Bool)
(currentTerm cp >>= fromTerm :: Maybe (SLogic, SLogic))
somewhereOrG :: IsStrategy g => g (Context a) -> Strategy (Context a)
somewhereOrG s =
let isOr a = case currentTerm a >>= (fromTerm :: Term -> Maybe SLogic) of
Just (_ :||: _) -> True
_ -> False
in fix $ \this -> check (Prelude.not . isOr) <*> s
<|> check isOr <*> layer [] this
----------------------
ruleAbsorpOrNot :: Rule SLogic
ruleAbsorpOrNot = rewriteRules "DistrOrNot"
[ -- not inside
\x y -> x :||: (Not x :&&: y) :~> (x :||: Not x) :&&: (x :||: y)
, \x y -> x :||: (y :&&: Not x) :~> (x :||: y) :&&: (x :||: Not x)
, \x y -> (Not x :&&: y) :||: x :~> (Not x :||: x) :&&: (y :||: x)
, \x y -> (y :&&: Not x) :||: x :~> (y :||: x) :&&: (Not x :||: x)
-- not outside
, \x y -> Not x :||: (x :&&: y) :~> (Not x :||: x) :&&: (Not x :||: y)
, \x y -> Not x :||: (y :&&: x) :~> (Not x :||: y) :&&: (Not x :||: x)
, \x y -> (x :&&: y) :||: Not x :~> (x :||: Not x) :&&: (y :||: Not x)
, \x y -> (y :&&: x) :||: Not x :~> (y :||: Not x) :&&: (x :||: Not x)
]
-- specialization of De Morgan rules with a not inside (gives higher priority)
ruleDeMorganOrNot :: Rule SLogic
ruleDeMorganOrNot = rewriteRules "DeMorganOrNot"
[ \x y -> Not (Not x :||: y) :~> Not (Not x) :&&: Not y
, \x y -> Not (x :||: Not y) :~> Not x :&&: Not (Not y)
]
ruleDeMorganAndNot :: Rule SLogic
ruleDeMorganAndNot = rewriteRules "DeMorganAndNot"
[ \x y -> Not (Not x :&&: y) :~> Not (Not x) :||: Not y
, \x y -> Not (x :&&: Not y) :~> Not x :||: Not (Not y)
]
{-
ruleAbsorpAndNot :: Rule SLogic
ruleAbsorpAndNot = rewriteRules "AbsorpAndNot.distr"
[ -- not inside
\x y -> x :&&: (Not x :||: y) :~> (x :&&: Not x) :||: (x :&&: y)
, \x y -> x :&&: (y :||: Not x) :~> (x :&&: y) :||: (x :&&: Not x)
, \x y -> (Not x :||: y) :&&: x :~> (Not x :&&: x) :||: (y :&&: x)
, \x y -> (y :||: Not x) :&&: x :~> (y :&&: x) :||: (Not x :&&: x)
-- not outside
, \x y -> Not x :&&: (x :||: y) :~> (Not x :||: x) :&&: (Not x :||: y)
, \x y -> Not x :&&: (y :||: x) :~> (Not x :||: y) :&&: (Not x :||: x)
, \x y -> (x :||: y) :&&: Not x :~> (x :||: Not x) :&&: (y :||: Not x)
, \x y -> (y :||: x) :&&: Not x :~> (y :||: Not x) :&&: (x :||: Not x)
] -}
-----------------------------------------------------------------------------
-- Inverse rules
inverseRules :: [Rule (Context Proof)]
inverseRules = map use [invDefImpl, invDefEquiv, invNotNot, invIdempOr, invIdempAnd,
invTrueZeroAnd, invNotTrue, invFalseZeroOr, invNotFalse] ++
[invAbsorpOr, invAbsorpAnd, invTrueZeroOr, invComplOr, invFalseZeroAnd, invComplAnd]
invDefImpl :: Rule SLogic
invDefImpl = rewriteRule "DefImpl.inv" $
\x y -> Not x :||: y :~> x :->: y
invDefEquiv :: Rule SLogic
invDefEquiv = rewriteRule "DefEquiv.inv" $
\x y -> (x :&&: y) :||: (Not x :&&: Not y) :~> x :<->: y
invNotNot :: Rule SLogic
invNotNot = rewriteRule "NotNot.inv" $
\x -> x :~> Not (Not x)
invIdempOr :: Rule SLogic
invIdempOr = rewriteRule "IdempOr.inv" $
\x -> x :~> x :||: x
invIdempAnd :: Rule SLogic
invIdempAnd = rewriteRule "IdempAnd.inv" $
\x -> x :&&: x :~> x
invTrueZeroAnd :: Rule SLogic
invTrueZeroAnd = rewriteRules "TrueZeroAnd.inv"
[ \x -> x :~> T :&&: x
, \x -> x :~> x :&&: T
]
invNotTrue :: Rule SLogic
invNotTrue = rewriteRule "NotTrue.inv" $
F :~> Not T
invFalseZeroOr :: Rule SLogic
invFalseZeroOr = rewriteRules "FalseZeroOr.inv"
[ \x -> x :~> F :||: x
, \x -> x :~> x :||: F
]
invNotFalse :: Rule SLogic
invNotFalse = rewriteRule "NotFalse.inv" $
T :~> Not F
makeInvRule :: String -> Rule SLogic -> Rule (Context Proof)
makeInvRule name r = addRecognizerBool eq $ makeRule name (const Nothing)
where
eq :: Context Proof -> Context Proof -> Bool
eq a b = or [ True
| c <- applyAll (somewhere (use r)) b
, similarity ex a c
]
ex = proofExercise
invAbsorpOr, invAbsorpAnd, invTrueZeroOr, invComplOr, invFalseZeroAnd, invComplAnd :: Rule (Context Proof)
invAbsorpOr = makeInvRule "AbsorpOr.inv" ruleAbsorpOr
invAbsorpAnd = makeInvRule "AbsorpAnd.inv" ruleAbsorpAnd
invTrueZeroOr = makeInvRule "TrueZeroOr.inv" ruleTrueZeroOr
invComplOr = makeInvRule "ComplOr.inv" ruleComplOr
invFalseZeroAnd = makeInvRule "FalseZeroAnd.inv" ruleFalseZeroAnd
invComplAnd = makeInvRule "ComplAnd.inv" ruleComplAnd