ideas-math-1.1: src/Domain/Logic/Proofs.hs
{-# LANGUAGE RankNTypes #-}
-----------------------------------------------------------------------------
-- Copyright 2014, 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
--
-----------------------------------------------------------------------------
-- $Id: Proofs.hs 6548 2014-05-16 10:34:18Z bastiaan $
module Domain.Logic.Proofs
( proofExercise, proofUnicodeExercise
, sortRuleOr, sortRuleAnd -- fix me
) 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.Exercises
import Domain.Logic.Formula
import Domain.Logic.GeneralizedRules
import Domain.Logic.Generator (equalLogicA)
import Domain.Logic.InverseRules
import Domain.Logic.Parser
import Domain.Logic.Rules
import Domain.Logic.Strategies (somewhereOr)
import Domain.Logic.Utils
import Domain.Math.Expr ()
import Ideas.Common.Library
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" $
propositionalId # "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)" $
propositionalId # "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
-- disabled: first investigate how the common subexpressions should be
-- communicated to the client
-- |> somewhere commonExprAtom
|> useC dnfStrategyDWA
|> commonLiteralSpecial
|> useC orToTop
|> (use checkDNF <*> commonLiteral)
)
<*> 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
commonLiteralSpecial :: Strategy (Context Proof)
commonLiteralSpecial =
repeat1 (somewhere (use ruleCommonLiteralSpecialInFront))
<*>
repeat1 (somewhere (use ruleInvDistrCommonLiteral))
<*>
repeatS (somewhere (use topIsAnd))
ruleCommonLiteralSpecialInFront :: Rule Proof
ruleCommonLiteralSpecialInFront = makeRule "command.common-literal-special" f
where
f (Var eq) =
[ Var x | x <- maybeToList (findInFrontLeft eq) ] ++
[ Var (swap x) | x <- maybeToList (findInFrontLeft (swap eq)) ]
f _ = []
findInFrontLeft eq@(p1 :&&: p2, q)
| isAtomic p1 && isDNF p2 && all (`notElem` varsLogic p2) (varsLogic p1) && isDNF q = do
lit <- listToMaybe (findCommonLiteral (p1, q))
res <- inFrontLeft lit (swap eq)
return (swap res)
findInFrontLeft _ = Nothing
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
)
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
<|> use sortForIdempAnd
<|> use sortForComplOr
<|> use sortForComplAnd
deMorganAndSimplify = somewhere $
deMorganOrNot <|> deMorganAndNot
eliminateImplEquiv =
somewhere (use ruleDefImpl) -- preference: top-down!
|> somewhere (use ruleDefEquiv) -- preference: bottom-up!
eliminateNots = somewhere $ useRules
[ generalRuleDeMorganAnd, generalRuleDeMorganOr
, ruleDeMorganAnd, ruleDeMorganOr
]
orToTop :: LabeledStrategy (Context SLogic)
orToTop = label "Move ors to top" $ somewhere $ useRules
[ generalRuleAndOverOr, ruleAndOverOr ]
useRules :: [Rule SLogic] -> Strategy (Context SLogic)
useRules = alternatives . map liftToContext
-- disabled for now
-- Find a common subexpression that can be treated as a box
{-
commonExprAtom :: Rule (Context Proof)
commonExprAtom = minor $ ruleTrans "commonExprAtom" $ makeTransLiftContext $ \proof ->
case proof of
Var (p, q) -> do
sub <- substRef :? []
let xs = filter (same <&&> complement isAtomic) (largestCommonSubExpr p q)
same cse = eqLogic (substitute cse p) (substitute cse q)
used = varsLogic p `union` varsLogic q `union` map (ShowString . fst) sub
new = head (logicVars \\ used)
substitute a this
| a == this = Var new
| otherwise = descend (substitute a) this
case xs of
hd:_ -> do
substRef := (show new, show hd):sub
return (Var (substitute hd p, substitute hd q))
_ -> fail "not applicable"
_ -> 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'..] ]
-}
--------------------------------------------------------------------
-- 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)
acTopRuleFor :: Bool -> (forall a . Isomorphism (Logic a) [Logic a])
-> Transformation Proof
acTopRuleFor com iso = makeTrans $ \proof -> do
(lhs, rhs) <- maybeToList (getSingleton proof)
let as = from iso lhs
bs = from iso rhs
splitter = if com then divide else split
(as1, as2, bs1, bs2) <- splitTwoLists splitter as bs
let eqList xs ys = eqLogic (to iso xs) (to iso ys)
guard (eqList as1 bs1 && eqList as2 bs2)
return $ to iso
[ Var (to iso as1, to iso bs1)
, Var (to iso as2, to iso bs2)
]
splitTwoLists :: (forall t . [t] -> [([t], [t])])
-> [a] -> [b] -> [([a], [a], [b], [b])]
splitTwoLists f as bs =
[ (as1, as2, bs1, bs2)
| (as1, as2) <- f as
, not (null as1 || null as2)
, (bs1, bs2) <- f bs
, not (null bs1 || null bs2)
]
split :: [a] -> [([a], [a])] -- associative
split as = [ splitAt i as | i <- [1..length as-1] ]
divide :: [a] -> [([a], [a])] -- associative + commutative
divide = foldr op [([], [])]
where
op a xs = map addLeft xs ++ map addRight xs
where
addLeft (ys, zs) = (a:ys, zs)
addRight (ys, zs) = (ys, a:zs)
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 curIsOr a = case currentTerm a >>= (fromTerm :: Term -> Maybe SLogic) of
Just (_ :||: _) -> True
_ -> False
in fix $ \this -> check (Prelude.not . curIsOr) <*> s
<|> check curIsOr <*> 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)
deMorganOrNot :: Strategy (Context SLogic)
deMorganOrNot = check p <*> (use ruleDeMorganOr <|> use generalRuleDeMorganOr)
where
p :: Context SLogic -> Bool
p ctx = case currentInContext ctx of
Just (Not x) ->
let ys = disjunctions x
in length ys > 1 && any isNot ys
_ -> False
deMorganAndNot :: Strategy (Context SLogic)
deMorganAndNot = check p <*> (use ruleDeMorganAnd <|> use generalRuleDeMorganAnd)
where
p :: Context SLogic -> Bool
p ctx = case currentInContext ctx of
Just (Not x) ->
let ys = conjunctions x
in length ys > 1 && any isNot ys
_ -> False
{-
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, invAndOverOr, invOrOverAnd]
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
proofInvRule :: String -> Rule SLogic -> Rule (Context Proof)
proofInvRule = makeInvRuleWithUse (similarity proofExercise)
invAbsorpOr, invAbsorpAnd, invTrueZeroOr, invComplOr, invFalseZeroAnd,
invComplAnd, invAndOverOr, invOrOverAnd :: Rule (Context Proof)
invAbsorpOr = proofInvRule "AbsorpOr.inv" ruleAbsorpOr
invAbsorpAnd = proofInvRule "AbsorpAnd.inv" ruleAbsorpAnd
invTrueZeroOr = proofInvRule "TrueZeroOr.inv" ruleTrueZeroOr
invComplOr = proofInvRule "ComplOr.inv" ruleComplOr
invFalseZeroAnd = proofInvRule "FalseZeroAnd.inv" ruleFalseZeroAnd
invComplAnd = proofInvRule "ComplAnd.inv" ruleComplAnd
invAndOverOr = proofInvRule "AndOverOr.inv" ruleAndOverOr -- see GeneralizedRules
invOrOverAnd = proofInvRule "OrOverAnd.inv" ruleOrOverAnd -- see GeneralizedRules
-----------------------------------------------------------------------------
-- Heuristic
{-
vb :: Proof
vb = makeProof
( (p :&&: Not q :&&: Not r) :||: (Not p :&&: Not q)
, (Not p :&&: Not q :&&: r) :||: (Not q :&&: Not r)
)
where
(p, q, r) = (Var $ ShowString "p", Var $ ShowString "q", Var $ ShowString "r")
-}
-- Special case: all conjunctions, on both sides, have a common literal.
-- Move this literal to the front (on both sides). Then use inverse distribution
-- (and top-is-and if possible).
commonLiteral :: Strategy (Context Proof)
commonLiteral =
repeatS (somewhere (use ruleCommonLiteralInFront))
<*>
repeat1 (somewhere (use ruleInvDistrCommonLiteral))
<*>
repeatS (somewhere (use topIsAnd))
findCommonLiteral :: Ord a => (Logic a, Logic a) -> [Logic a]
findCommonLiteral (p, q) = sort $
intersectList (map conjunctions (disjunctions p ++ disjunctions q))
ruleCommonLiteralInFront :: Rule Proof
ruleCommonLiteralInFront = makeRule "command.common-literal" f
where
f (Var eq) =
[ Var x | x <- maybeToList (findInFrontLeft eq) ] ++
[ Var (swap x) | x <- maybeToList (findInFrontLeft (swap eq)) ]
f _ = []
findInFrontLeft eq = do
lit <- listToMaybe (findCommonLiteral eq)
inFrontLeft lit eq
inFrontLeft :: SLogic -> (SLogic, SLogic) -> Maybe (SLogic, SLogic)
inFrontLeft lit (p, q) = do
let pss = map (toFront . conjunctions) (disjunctions p)
toFront = uncurry (++) . partition (==lit)
new = ors (map ands pss)
guard (new /= p)
Just (new, q)
ruleInvDistrCommonLiteral :: Rule Proof
ruleInvDistrCommonLiteral = makeRule "andoveror.inv.common-literal" f
where
f (Var eq) = [ Var x | x <- invDistr eq ] ++
[ Var (swap x) | x <- invDistr (swap eq) ]
f _ = []
invDistr eq@(p, q) = do
guard (not (null (findCommonLiteral eq)))
new <- applyAll inverseAndOverOr p
return (new, q)
intersectList :: Eq a => [[a]] -> [a]
intersectList [] = []
intersectList xs = foldr1 intersect xs
swap :: (a, b) -> (b, a)
swap (x, y) = (y, x)