logic-classes-1.7.1: Tests/Harrison/Equal.hs
{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, OverloadedStrings, RankNTypes, ScopedTypeVariables, TypeSynonymInstances #-}
{-# OPTIONS_GHC -Wall #-}
module Harrison.Equal where
-- =========================================================================
-- First order logic with equality.
--
-- Copyright (co) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)
-- =========================================================================
import Common (render)
import Control.Applicative.Error (Failing(..))
import Data.List as List
import Data.Map as Map
import Data.Set as Set
import Data.String (IsString(fromString))
import Equal (equalitize, function_congruence)
import FOL ((.=.), (∃), (∀), IsTerm(..), pApp, Predicate, V)
import Formulas (IsCombinable(..), (∧), (⇒))
import Meson (meson)
import Prelude hiding ((*))
import Skolem (HasSkolem(..), MyTerm, MyFormula, runSkolem)
import Tableaux (Depth(Depth))
import Test.HUnit
-- type TF = TestFormula (Formula FOL) FOL MyTerm String String Function
-- type TFE = TestFormulaEq (MyFormula) FOLEQ MyTerm String String Function
tests :: Test
tests = TestLabel "Data.Logic.Tests.Harrison.Equal" $ TestList [test01, test02, test03, test04]
-- -------------------------------------------------------------------------
-- Example.
-- -------------------------------------------------------------------------
test01 :: Test
test01 = TestCase $ assertEqual "function_congruence" expected input
where input = List.map function_congruence [(fromString "f", 3 :: Int), (fromString "+",2)]
expected :: [Set.Set (MyFormula)]
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
test label expected input = TestLabel label $ TestCase $ assertEqual label expected input
test02 :: Test
test02 = TestCase $ assertEqual "equalitize 1 (p. 241)" (expected, expectedProof) input
where input = (render ewd, runSkolem (meson (Just (Depth 10)) ewd))
ewd = equalitize fm :: MyFormula
fm :: MyFormula
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) [] :: MyTerm)],0,1),1),
Success ((Map.fromList [("_0",fApp (Skolem 2) [] :: MyTerm)],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),Depth 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 -> [MyTerm] -> MyFormula
pApp' s ts = pApp (fromString s :: Predicate) ts
--vt' :: String -> MyTerm
--vt' s = vt (fromString s)
-- -------------------------------------------------------------------------
-- Wishnu Prasetya's example (even nicer with an "exists unique" primitive).
-- -------------------------------------------------------------------------
wishnu :: MyFormula
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
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 (Depth 16)) wishnu))
x = vt "x" :: MyTerm
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 :: MyFormula
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 ["Not sure what we git here if this finishes"]]
{-
Set.fromList [Success ((Map.fromList [("_0",vt "_1")],0,2 :: Map.Map String MyTerm),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
test04 = TestCase $ assertEqual "equalitize 3 (p. 248)" (render expected, expectedProof) input
where
input = (render (equalitize fm), runSkolem (meson (Just (Depth 20)) . equalitize $ fm))
fm :: MyFormula
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" :: MyTerm
y' = vt "y" :: MyTerm
z' = vt "z" :: MyTerm
(*) = fApp (fromString "*")
i = fApp (fromString "i")
one = fApp (fromString "1") []
expected :: MyFormula
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 V MyTerm, Int, Int), Depth))
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),Depth 13)]
vt' = vt . fromString