logic-classes-1.4: Data/Logic/Tests/Harrison/Equal.hs
{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, OverloadedStrings, RankNTypes, ScopedTypeVariables, TypeSynonymInstances #-}
{-# OPTIONS_GHC -Wall #-}
module Data.Logic.Tests.Harrison.Equal where
-- =========================================================================
-- First order logic with equality.
--
-- Copyright (co) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)
-- =========================================================================
import Control.Applicative.Error (Failing(..))
import Data.Logic.Classes.Combine (Combinable(..), (∧), (⇒))
--import Data.Logic.Classes.Constants (true)
import Data.Logic.Classes.Equals ((.=.), pApp)
import Data.Logic.Classes.FirstOrder ((∃), (∀))
--import Data.Logic.Classes.Pretty (Pretty(pretty))
import Data.Logic.Classes.Skolem (Skolem(..))
import Data.Logic.Classes.Term (Term(..))
import Data.Logic.Harrison.Equal (equalitize, function_congruence)
import Data.Logic.Harrison.Meson (meson)
import Data.Logic.Harrison.Skolem (runSkolem)
import Data.Logic.Tests.Common (render)
import Data.Logic.Types.Harrison.FOL (TermType(..))
import Data.Logic.Types.Harrison.Formulas.FirstOrder (Formula(..))
import Data.Logic.Types.Harrison.Equal (FOLEQ(..), PredName)
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.String (IsString(fromString))
import Data.Logic.Tests.HUnit
-- type TF = TestFormula (Formula FOL) FOL TermType String String Function
-- type TFE = TestFormulaEq (Formula FOLEQ) FOLEQ TermType String String Function
tests :: Test (Formula FOLEQ)
tests = TestLabel "Data.Logic.Tests.Harrison.Equal" $ TestList [test01, test02, test03, test04]
-- -------------------------------------------------------------------------
-- Example.
-- -------------------------------------------------------------------------
test01 :: Test (Formula FOLEQ)
test01 = TestCase $ assertEqual "function_congruence" expected input
where input = map function_congruence [(fromString "f", 3 :: Int), (fromString "+",2)]
expected :: [Set.Set (Formula FOLEQ)]
expected = [Set.fromList
[(∀) x1
((∀) x2
((∀) x3
((∀) y1
((∀) y2
((∀) y3 ((((vt x1) .=. (vt y1)) ∧ (((vt x2) .=. (vt y2)) ∧ ((vt x3) .=. (vt y3)))) ⇒
((fApp (fromString "f") [vt x1,vt x2,vt x3]) .=. (fApp (fromString "f") [vt y1,vt y2,vt y3]))))))))],
Set.fromList
[(∀) x1
((∀) x2
((∀) y1
((∀) y2 ((((vt x1) .=. (vt y1)) ∧ ((vt x2) .=. (vt y2))) ⇒
((fApp (fromString "+") [vt x1,vt x2]) .=. (fApp (fromString "+") [vt y1,vt y2]))))))]]
x1 = fromString "x1"
x2 = fromString "x2"
x3 = fromString "x3"
y1 = fromString "y1"
y2 = fromString "y2"
y3 = fromString "y3"
-- -------------------------------------------------------------------------
-- A simple example (see EWD1266a and the application to Morley's theorem).
-- -------------------------------------------------------------------------
test :: (Show a, Eq a) => String -> a -> a -> Test (Formula FOLEQ)
test label expected input = TestLabel label $ TestCase $ assertEqual label expected input
test02 :: Test (Formula FOLEQ)
test02 = test "equalitize 1 (p. 241)" (expected, expectedProof) input
where input = (render ewd, runSkolem (meson (Just 10) ewd))
ewd = equalitize fm :: Formula FOLEQ
fm :: Formula FOLEQ
fm = ((∀) "x" (fx ⇒ gx)) ∧
((∃) "x" fx) ∧
((∀) "x" ((∀) "y" (gx ∧ gy ⇒ x .=. y))) ⇒
((∀) "y" (gy ⇒ fy))
fx = pApp' "f" [x]
gx = pApp' "g" [x]
fy = pApp' "f" [y]
gy = pApp' "g" [y]
x = vt "x"
y = vt "y"
z = vt "z"
x1 = vt "x1"
y1 = vt "y1"
fx1 = pApp' "f" [x1]
gx1 = pApp' "g" [x1]
fy1 = pApp' "f" [y1]
gy1 = pApp' "g" [y1]
-- y1 = fromString "y1"
-- z = fromString "z"
expected = render $
((∀) "x" (x .=. x)) .&.
((∀) "x" ((∀) "y" ((∀) "z" (x .=. y .&. x .=. z .=>. y .=. z)))) .&.
((∀) "x1" ((∀) "y1" (x1 .=. y1 .=>. fx1 .=>. fy1))) .&.
((∀) "x1" ((∀) "y1" (x1 .=. y1 .=>. gx1 .=>. gy1))) .=>.
((∀) "x" (fx .=>. gx)) .&.
((∃) "x" (fx)) .&.
((∀) "x" ((∀) "y" (gx .&. gy .=>. x .=. y))) .=>.
((∀) "y" (gy .=>. fy))
{-
-- I don't yet know if this is right. Almost certainly not.
expectedProof = Set.fromList [Success ((Map.fromList [("_0",vt "_1")],0,2),1),
Success ((Map.fromList [("_0",vt "_2"),("_1",vt "_2")],0,3),1),
Success ((Map.fromList [("_0",fApp (Skolem 1) [] :: TermType)],0,1),1),
Success ((Map.fromList [("_0",fApp (Skolem 2) [] :: TermType)],0,1),1)]
expected = ("<<(forall x. x = x) /\ " ++
" (forall x y z. x = y /\ x = z ==> y = z) /\ " ++
" (forall x1 y1. x1 = y1 ==> f(x1) ==> f(y1)) /\ " ++
" (forall x1 y1. x1 = y1 ==> g(x1) ==> g(y1)) ==> " ++
" (forall x. f(x) ==> g(x)) /\ " ++
" (exists x. f(x)) /\ (forall x y. g(x) /\ g(y) ==> x = y) ==> " ++
" (forall y. g(y) ==> f(y))>> ")
-}
expectedProof =
Set.fromList [Success ((Map.fromList [(fromString "_0",vt "_2"),
(fromString "_1",fApp (toSkolem "y") []),
(fromString "_2",vt "_4"),
(fromString "_3",fApp (toSkolem "y") []),
(fromString "_4",fApp (toSkolem "x") [])],0,5),6)]
{-
expectedProof =
Set.singleton (Success ((Map.fromList [(fromString "_0",vt' "_2"),
(fromString "_1",fApp (toSkolem "x") []),
(fromString "_2",vt' "_4"),
(fromString "_3",fApp (toSkolem "x") []),
(fromString "_4",fApp (toSkolem "x") []),
(fromString "_5",fApp (toSkolem "x") [])], 0, 6), 5))
fApp' :: String -> [term] -> term
fApp' s ts = fApp (fromString s) ts
for_all' s = for_all (fromString s)
exists' s = exists (fromString s)
-}
pApp' :: String -> [TermType] -> Formula FOLEQ
pApp' s ts = pApp (fromString s :: PredName) ts
--vt' :: String -> TermType
--vt' s = vt (fromString s)
-- -------------------------------------------------------------------------
-- Wishnu Prasetya's example (even nicer with an "exists unique" primitive).
-- -------------------------------------------------------------------------
wishnu :: Formula FOLEQ
wishnu = ((∃) ("x") ((x .=. f[g[x]]) ∧ (∀) ("x'") ((x' .=. f[g[x']]) ⇒ (x .=. x')))) .<=>.
((∃) ("y") ((y .=. g[f[y]]) ∧ (∀) ("y'") ((y' .=. g[f[y']]) ⇒ (y .=. y'))))
where
x = vt "x"
y = vt "y"
x' = vt "x'"
y' = vt "y"
f terms = fApp (fromString "f") terms
g terms = fApp (fromString "g") terms
test03 :: Test (Formula FOLEQ)
test03 = TestLabel "equalitize 2" $ TestCase $ assertEqual "equalitize 2 (p. 241)" (render expected, expectedProof) input
where -- This depth is not sufficient to finish. It shoudl work with 16, but that takes a long time.
input = (render (equalitize wishnu), runSkolem (meson (Just 50) wishnu))
x = vt "x" :: TermType
x1 = vt "x1"
y = vt "y"
y1 = vt "y1"
z = vt "z"
x' = vt "x'"
y' = vt "y"
f terms = fApp (fromString "f") terms
g terms = fApp (fromString "g") terms
expected :: Formula FOLEQ
expected =
((∀) "x" (x .=. x)) .&.
((∀) "x" . (∀) "y" . (∀) "z" $ (x .=. y .&. x .=. z .=>. y .=. z)) .&.
((∀) "x1" . (∀) "y1" $ (x1 .=. y1 .=>. f[x1] .=. f[y1])) .&.
((∀) "x1" . (∀) "y1" $ (x1 .=. y1 .=>. g[x1] .=. g[y1])) .=>.
(((∃) "x" $ x .=. f[g[x]] .&. ((∀) "x'" $ (x' .=. f[g[x']] .=>. x .=. x'))) .<=>.
((∃) "y" $ y .=. g[f[y]] .&. ((∀) "y'" $ (y' .=. g[f[y']] .=>. y .=. y'))))
expectedProof =
Set.fromList [Failure ["Exceeded maximum depth limit"]]
{-
Set.fromList [Success ((Map.fromList [("_0",vt "_1")],0,2 :: Map.Map String TermType),1),
Success ((Map.fromList [("_0",vt "_1"),("_1",fApp "f" [fApp "g" [vt "_0"]])],0,2),1),
Success ((Map.fromList [("_0",vt "_1"),("_1",fApp "g" [fApp "f" [vt "_0"]])],0,2),1),
Success ((Map.fromList [("_0",vt "_1"),("_2",fApp (fromSkolem 2) [vt "_0"])],0,3),1),
Success ((Map.fromList [("_0",vt "_2"),("_1",vt "_2")],0,3),1)] -}
-- -------------------------------------------------------------------------
-- More challenging equational problems. (Size 18, 61814 seconds.)
-- -------------------------------------------------------------------------
test04 :: Test (Formula FOLEQ)
test04 = test "equalitize 3 (p. 248)" (render expected, expectedProof) input
where
input = (render (equalitize fm), runSkolem (meson (Just 20) . equalitize $ fm))
fm :: Formula FOLEQ
fm = ((∀) "x" . (∀) "y" . (∀) "z") ((*) [x', (*) [y', z']] .=. (*) [((*) [x', y']), z']) ∧
(∀) "x" ((*) [one, x'] .=. x') ∧
(∀) "x" ((*) [i [x'], x'] .=. one) ⇒
(∀) "x" ((*) [x', i [x']] .=. one)
x' = vt "x" :: TermType
y' = vt "y" :: TermType
z' = vt "z" :: TermType
(*) = fApp (fromString "*")
i = fApp (fromString "i")
one = fApp (fromString "1") []
expected :: Formula FOLEQ
expected =
((∀) "x" ((vt "x") .=. (vt "x")) .&.
((∀) "x" ((∀) "y" ((∀) "z" ((((vt "x") .=. (vt "y")) .&. ((vt "x") .=. (vt "z"))) .=>. ((vt "y") .=. (vt "z"))))) .&.
((∀) "x1" ((∀) "x2" ((∀) "y1" ((∀) "y2" ((((vt "x1") .=. (vt "y1")) .&. ((vt "x2") .=. (vt "y2"))) .=>.
((fApp "*" [vt "x1",vt "x2"]) .=. (fApp "*" [vt "y1",vt "y2"])))))) .&.
(∀) "x1" ((∀) "y1" (((vt "x1") .=. (vt "y1")) .=>. ((fApp "i" [vt "x1"]) .=. (fApp "i" [vt "y1"]))))))) .=>.
((((∀) "x" ((∀) "y" ((∀) "z" ((fApp "*" [vt "x",fApp "*" [vt "y",vt "z"]]) .=. (fApp "*" [fApp "*" [vt "x",vt "y"],vt "z"])))) .&.
(∀) "x" ((fApp "*" [fApp "1" [],vt "x"]) .=. (vt "x"))) .&.
(∀) "x" ((fApp "*" [fApp "i" [vt "x"],vt "x"]) .=. (fApp "1" []))) .=>.
(∀) "x" ((fApp "*" [vt "x",fApp "i" [vt "x"]]) .=. (fApp "1" [])))
expectedProof :: Set.Set (Failing ((Map.Map String TermType, Int, Int), Int))
expectedProof =
Set.fromList
[Success ((Map.fromList
[( "_0", (*) [one, vt' "_3"]),
( "_1", (*) [fApp (toSkolem "x") [],i [fApp (toSkolem "x") []]]),
( "_2", one),
( "_3", (*) [fApp (toSkolem "x") [],i [fApp (toSkolem "x") []]]),
( "_4", vt' "_8"),
( "_5", (*) [one, vt' "_3"]),
( "_6", one),
( "_7", vt' "_11"),
( "_8", vt' "_12"),
( "_9", (*) [one, vt' "_3"]),
("_10", (*) [vt' "_13",(*) [vt' "_14", vt' "_15"]]),
("_11", (*) [(*) [vt' "_13", vt' "_14"], vt' "_15"]),
("_12", (*) [vt' "_19", vt' "_18"]),
("_13", vt' "_16"),
("_14", vt' "_21"),
("_15", (*) [vt' "_22", vt' "_23"]),
("_16", vt' "_20"),
("_17", (*) [vt' "_14", vt' "_15"]),
("_18", (*) [(*) [vt' "_21", vt' "_22"], vt' "_23"]),
("_19", vt' "_20"),
("_20", i [vt' "_28"]),
("_21", vt' "_28"),
("_22", fApp (toSkolem "x") []),
("_23", i [fApp (toSkolem "x") []]),
("_24", (*) [vt' "_13", vt' "_14"]),
("_25", (*) [vt' "_22", vt' "_23"]),
("_26", (*) [fApp (toSkolem "x") [],i [fApp (toSkolem "x") []]]),
("_27", one),
("_28", vt' "_30"),
("_29", (*) [vt' "_22", vt' "_23"]),
("_30", (*) [(*) [vt' "_21", vt' "_22"], vt' "_23"])],
0,31),13)]
vt' = vt . fromString