root/logic
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

laws: (==) iff they are relabellings of each other

Browse source
This commit is contained in:
hi 2025-08-16 08:58:22 +00:00
parent b0e98b0e51
commit 550e589bc8
2 changed files with 12 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

9
lib/Logic/Statement.hs
View file

@ -28,3 +28,12 @@ substatements s@(And s1 s2) = (s:) $ substatements s1 ++ substatements s2
substatements s@(Or s1 s2) = (s:) $ substatements s1 ++ substatements s2 substatements s@(Or s1 s2) = (s:) $ substatements s1 ++ substatements s2
substatements s@(Implies s1 s2) = (s:) $ substatements s1 ++ substatements s2 substatements s@(Implies s1 s2) = (s:) $ substatements s1 ++ substatements s2
substatements s@(Iff s1 s2) = (s:) $ substatements s1 ++ substatements s2 substatements s@(Iff s1 s2) = (s:) $ substatements s1 ++ substatements s2
relabellings :: Statement -> Statement -> Bool
relabellings (Atom _) (Atom _) = True
relabellings (Not s1) (Not r1) = relabellings s1 r1
relabellings (And s1 s2) (And r1 r2) = relabellings s1 r1 && relabellings s2 r2
relabellings (Or s1 s2) (Or r1 r2) = relabellings s1 r1 && relabellings s2 r2
relabellings (Implies s1 s2) (Implies r1 r2) = relabellings s1 r1 && relabellings s2 r2
relabellings (Iff s1 s2) (Iff r1 r2) = relabellings s1 r1 && relabellings s2 r2
relabellings _ _ = False

6
lib/Logic/Statement/Laws.hs
View file

@ -1,7 +1,7 @@
module Logic.Statement.Laws where module Logic.Statement.Laws where
import Logic.Parse (eof, mkInput) import Logic.Parse (eof, mkInput)
import Logic.Statement (Statement(..)) import Logic.Statement (Statement(..), relabellings)
import Logic.Statement.Parse (stmt) import Logic.Statement.Parse (stmt)
import Logic.Statement.Serialize (serialize, SerializeFormat(Plain)) import Logic.Statement.Serialize (serialize, SerializeFormat(Plain))
import Logic.Graph (bfs, verifyPath, VerifyPathError) import Logic.Graph (bfs, verifyPath, VerifyPathError)
@ -20,8 +20,8 @@ data Law = Law
instance Eq Law where instance Eq Law where
law1 == law2 = law1 == law2 =
lawLhs law1 == lawLhs law2 relabellings (lawLhs law1) (lawLhs law2)
&& lawRhs law1 == lawRhs law2 && relabellings (lawRhs law1) (lawRhs law2)
instance Show Law where instance Show Law where
show law = show law =