module Proof.Exp.Prop(
Prop(..), sym, tautology, simplifyProp, (==>)
) where
import Proof.Exp.Core
import Proof.Util
import Data.Data
import Data.Maybe
import Data.List.Extra
import Control.DeepSeq
data Prop = Prop [Var] Exp Exp deriving (Eq,Data,Typeable)
instance NFData Prop where
rnf (Prop a b c) = rnf3 a b c
sym :: Prop -> Prop
sym (Prop vs a b) = Prop vs b a
instance Show Prop where
show (Prop vs a b) = unwords (map fromVar vs ++ ["=>"]) ++ "\n" ++ f a ++ "=" ++ drop 1 (f b)
where f = unlines . map (" "++) . lines . show
instance Read Prop where
readsPrec = simpleReadsPrec $ \x -> case () of
_ | (quant, x) <- fromMaybe ("",x) $ stripInfix " => " x
, Just (a,b) <- stripInfix " = " x
-> Prop (map V $ words quant) (read a) (read b)
simplifyProp :: Prop -> Prop
simplifyProp = label . simple . unlam . simple
where
simple (Prop vs a b) = Prop vs (simplifyExp a) (simplifyExp b)
unlam (Prop vs (Lam a1 a2) (Lam b1 b2))
| v:_ <- fresh $ a1:b1:vs ++ vars a2 ++ vars b2
= unlam $ Prop (v:vs) (subst [(a1,Var v)] a2) (subst [(b1,Var v)] b2)
unlam x = x
label (Prop vs a b) = Prop new (subst sub $ relabelAvoid (free a ++ new) a) (subst sub $ relabelAvoid (free b ++ new) b)
where fv = nubOrd $ free a ++ free b
vs2 = fv `intersect` vs
new = take (length vs2) $ fresh $ fv \\ vs
sub = zip vs2 $ map Var new
(==>) :: Prop -> Prop -> Bool
(==>) a b = simplifyProp a == simplifyProp b || simplifyProp (sym a) == simplifyProp b
tautology :: Prop -> Bool
tautology (Prop vs a b) = a == b