From 550e589bc89305cadfd263aaf6c60c78f87b3f32 Mon Sep 17 00:00:00 2001 From: hi Date: Sat, 16 Aug 2025 08:58:22 +0000 Subject: [PATCH] laws: (==) iff they are relabellings of each other --- lib/Logic/Statement.hs | 9 +++++++++ lib/Logic/Statement/Laws.hs | 6 +++--- 2 files changed, 12 insertions(+), 3 deletions(-) diff --git a/lib/Logic/Statement.hs b/lib/Logic/Statement.hs index 6d7268b..953827f 100644 --- a/lib/Logic/Statement.hs +++ b/lib/Logic/Statement.hs @@ -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@(Implies 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 diff --git a/lib/Logic/Statement/Laws.hs b/lib/Logic/Statement/Laws.hs index 407b661..4cc09c2 100644 --- a/lib/Logic/Statement/Laws.hs +++ b/lib/Logic/Statement/Laws.hs @@ -1,7 +1,7 @@ module Logic.Statement.Laws where import Logic.Parse (eof, mkInput) -import Logic.Statement (Statement(..)) +import Logic.Statement (Statement(..), relabellings) import Logic.Statement.Parse (stmt) import Logic.Statement.Serialize (serialize, SerializeFormat(Plain)) import Logic.Graph (bfs, verifyPath, VerifyPathError) @@ -20,8 +20,8 @@ data Law = Law instance Eq Law where law1 == law2 = - lawLhs law1 == lawLhs law2 - && lawRhs law1 == lawRhs law2 + relabellings (lawLhs law1) (lawLhs law2) + && relabellings (lawRhs law1) (lawRhs law2) instance Show Law where show law =