{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE TypeFamilies #-}
-- | First order logic with equality.
--
-- Copyright (co) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)

{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, OverloadedStrings, RankNTypes, ScopedTypeVariables, TypeSynonymInstances #-}
{-# OPTIONS_GHC -Wall #-}

module Data.Logic.ATP.Equal
    ( function_congruence
    , equalitize
    -- * Tests
    , wishnu
    , testEqual
    ) where

import Data.Logic.ATP.Apply (functions, HasApply(TermOf, PredOf, applyPredicate), pApp)
import Data.Logic.ATP.Equate ((.=.), HasEquate(foldEquate))
import Data.Logic.ATP.Formulas (IsFormula(AtomOf, atomic), atom_union)
import Data.Logic.ATP.Lib ((∅), Depth(Depth), Failing (Success, Failure), timeMessage)
import Data.Logic.ATP.Meson (meson)
import Data.Logic.ATP.Pretty (assertEqual')
import Data.Logic.ATP.Prop ((.&.), (.=>.), (∧), (⇒))
import Data.Logic.ATP.Quantified ((∃), (∀), IsQuantified(..))
import Data.Logic.ATP.Parser (fof)
import Data.Logic.ATP.Skolem (runSkolem, Formula)
import Data.Logic.ATP.Term (IsTerm(..))
import Data.List as List (foldr, map)
import Data.Set as Set
import Data.String (IsString(fromString))
import Prelude hiding ((*))
import Test.HUnit

-- is_eq :: (IsQuantified fof atom v, IsAtomWithEquate atom p term) => fof -> Bool
-- is_eq = foldFirstOrder (\ _ _ _ -> False) (\ _ -> False) (\ _ -> False) (foldAtomEq (\ _ _ -> False) (\ _ -> False) (\ _ _ -> True))
--
-- mk_eq :: (IsQuantified fof atom v, IsAtomWithEquate atom p term) => term -> term -> fof
-- mk_eq = (.=.)
--
-- dest_eq :: (IsQuantified fof atom v, IsAtomWithEquate atom p term) => fof -> Failing (term, term)
-- dest_eq fm =
--     foldFirstOrder (\ _ _ _ -> err) (\ _ -> err) (\ _ -> err) at fm
--     where
--       at = foldAtomEq (\ _ _ -> err) (\ _ -> err) (\ s t -> Success (s, t))
--       err = Failure ["dest_eq: not an equation"]
--
-- lhs :: (IsQuantified fof atom v, IsAtomWithEquate atom p term) => fof -> Failing term
-- lhs eq = dest_eq eq >>= return . fst
-- rhs :: (IsQuantified fof atom v, IsAtomWithEquate atom p term) => fof -> Failing term
-- rhs eq = dest_eq eq >>= return . snd

-- | The set of predicates in a formula.
-- predicates :: (IsQuantified formula atom v, IsAtomWithEquate atom p term, Ord atom, Ord p) => formula -> Set atom
predicates :: IsFormula formula => formula -> Set (AtomOf formula)
predicates :: forall formula.
IsFormula formula =>
formula -> Set (AtomOf formula)
predicates formula
fm = (AtomOf formula -> Set (AtomOf formula))
-> formula -> Set (AtomOf formula)
forall formula r.
(IsFormula formula, Ord r) =>
(AtomOf formula -> Set r) -> formula -> Set r
atom_union AtomOf formula -> Set (AtomOf formula)
forall a. a -> Set a
Set.singleton formula
fm

-- | Code to generate equate axioms for functions.
function_congruence :: forall fof atom term v p function.
                       (atom ~ AtomOf fof, term ~ TermOf atom, p ~ PredOf atom, v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term,
                        IsQuantified fof, HasEquate atom, IsTerm term, Ord fof) =>
                       (function, Int) -> Set fof
function_congruence :: forall fof atom term v p function.
(atom ~ AtomOf fof, term ~ TermOf atom, p ~ PredOf atom,
 v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term,
 IsQuantified fof, HasEquate atom, IsTerm term, Ord fof) =>
(function, Int) -> Set fof
function_congruence (function
_,Int
0) = Set fof
forall (c :: * -> *) a. (Monoid (c a), SetLike c) => c a
(∅)
function_congruence (function
f,Int
n) =
    fof -> Set fof
forall a. a -> Set a
Set.singleton ((v -> fof -> fof) -> fof -> [v] -> fof
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
List.foldr v -> fof -> fof
VarOf fof -> fof -> fof
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) (fof
ant fof -> fof -> fof
forall formula.
IsPropositional formula =>
formula -> formula -> formula
⇒ fof
con) ([v]
[VarOf fof]
argnames_x [v] -> [v] -> [v]
forall a. [a] -> [a] -> [a]
++ [v]
[VarOf fof]
argnames_y))
    where
      argnames_x :: [VarOf fof]
      argnames_x :: [VarOf fof]
argnames_x = (Int -> v) -> [Int] -> [v]
forall a b. (a -> b) -> [a] -> [b]
List.map (\ Int
m -> String -> v
forall a. IsString a => String -> a
fromString (String
"x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
m)) [Int
1..Int
n]
      argnames_y :: [VarOf fof]
      argnames_y :: [VarOf fof]
argnames_y = (Int -> v) -> [Int] -> [v]
forall a b. (a -> b) -> [a] -> [b]
List.map (\ Int
m -> String -> v
forall a. IsString a => String -> a
fromString (String
"y" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
m)) [Int
1..Int
n]
      args_x :: [term]
args_x = (TVarOf term -> term) -> [TVarOf term] -> [term]
forall a b. (a -> b) -> [a] -> [b]
List.map TVarOf term -> term
forall term. IsTerm term => TVarOf term -> term
vt [TVarOf term]
[VarOf fof]
argnames_x
      args_y :: [term]
args_y = (TVarOf term -> term) -> [TVarOf term] -> [term]
forall a b. (a -> b) -> [a] -> [b]
List.map TVarOf term -> term
forall term. IsTerm term => TVarOf term -> term
vt [TVarOf term]
[VarOf fof]
argnames_y
      ant :: fof
ant = (fof -> fof -> fof) -> [fof] -> fof
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 fof -> fof -> fof
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(∧) (((term, term) -> fof) -> [(term, term)] -> [fof]
forall a b. (a -> b) -> [a] -> [b]
List.map ((term -> term -> fof) -> (term, term) -> fof
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry term -> term -> fof
TermOf atom -> TermOf atom -> fof
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
(.=.)) ([term] -> [term] -> [(term, term)]
forall a b. [a] -> [b] -> [(a, b)]
zip [term]
args_x [term]
args_y))
      con :: fof
con = FunOf term -> [term] -> term
forall term. IsTerm term => FunOf term -> [term] -> term
fApp function
FunOf term
f [term]
args_x TermOf atom -> TermOf atom -> fof
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FunOf term -> [term] -> term
forall term. IsTerm term => FunOf term -> [term] -> term
fApp function
FunOf term
f [term]
args_y

-- | And for predicates.
predicate_congruence :: (atom ~ AtomOf fof, predicate ~ PredOf atom, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term,
                         IsQuantified fof, HasEquate atom, IsTerm term, Ord predicate) =>
                        AtomOf fof -> Set fof
predicate_congruence :: forall atom fof predicate term v.
(atom ~ AtomOf fof, predicate ~ PredOf atom, term ~ TermOf atom,
 v ~ VarOf fof, v ~ TVarOf term, IsQuantified fof, HasEquate atom,
 IsTerm term, Ord predicate) =>
AtomOf fof -> Set fof
predicate_congruence =
    (TermOf atom -> TermOf atom -> Set fof)
-> (PredOf atom -> [TermOf atom] -> Set fof) -> atom -> Set fof
forall atom r.
HasEquate atom =>
(TermOf atom -> TermOf atom -> r)
-> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
forall r.
(TermOf atom -> TermOf atom -> r)
-> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
foldEquate (\TermOf atom
_ TermOf atom
_ -> Set fof
forall a. Set a
Set.empty) (\PredOf atom
p [TermOf atom]
ts -> PredOf (AtomOf fof) -> Int -> Set fof
forall {a} {a}.
(VarOf a ~ TVarOf (TermOf (AtomOf a)), Num a, Enum a,
 HasEquate (AtomOf a), IsQuantified a, Eq a, Show a) =>
PredOf (AtomOf a) -> a -> Set a
ap PredOf atom
PredOf (AtomOf fof)
p ([term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [term]
[TermOf atom]
ts))
    where
      ap :: PredOf (AtomOf a) -> a -> Set a
ap PredOf (AtomOf a)
_ a
0 = Set a
forall a. Set a
Set.empty
      ap PredOf (AtomOf a)
p a
n = a -> Set a
forall a. a -> Set a
Set.singleton ((TVarOf (TermOf (AtomOf a)) -> a -> a)
-> a -> [TVarOf (TermOf (AtomOf a))] -> a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
List.foldr TVarOf (TermOf (AtomOf a)) -> a -> a
VarOf a -> a -> a
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) (a
ant a -> a -> a
forall formula.
IsPropositional formula =>
formula -> formula -> formula
⇒ a
con) ([TVarOf (TermOf (AtomOf a))]
argnames_x [TVarOf (TermOf (AtomOf a))]
-> [TVarOf (TermOf (AtomOf a))] -> [TVarOf (TermOf (AtomOf a))]
forall a. [a] -> [a] -> [a]
++ [TVarOf (TermOf (AtomOf a))]
argnames_y))
          where
            argnames_x :: [TVarOf (TermOf (AtomOf a))]
argnames_x = (a -> TVarOf (TermOf (AtomOf a)))
-> [a] -> [TVarOf (TermOf (AtomOf a))]
forall a b. (a -> b) -> [a] -> [b]
List.map (\ a
m -> String -> TVarOf (TermOf (AtomOf a))
forall a. IsString a => String -> a
fromString (String
"x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
m)) [a
1..a
n]
            argnames_y :: [TVarOf (TermOf (AtomOf a))]
argnames_y = (a -> TVarOf (TermOf (AtomOf a)))
-> [a] -> [TVarOf (TermOf (AtomOf a))]
forall a b. (a -> b) -> [a] -> [b]
List.map (\ a
m -> String -> TVarOf (TermOf (AtomOf a))
forall a. IsString a => String -> a
fromString (String
"y" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
m)) [a
1..a
n]
            args_x :: [TermOf (AtomOf a)]
args_x = (TVarOf (TermOf (AtomOf a)) -> TermOf (AtomOf a))
-> [TVarOf (TermOf (AtomOf a))] -> [TermOf (AtomOf a)]
forall a b. (a -> b) -> [a] -> [b]
List.map TVarOf (TermOf (AtomOf a)) -> TermOf (AtomOf a)
forall term. IsTerm term => TVarOf term -> term
vt [TVarOf (TermOf (AtomOf a))]
argnames_x
            args_y :: [TermOf (AtomOf a)]
args_y = (TVarOf (TermOf (AtomOf a)) -> TermOf (AtomOf a))
-> [TVarOf (TermOf (AtomOf a))] -> [TermOf (AtomOf a)]
forall a b. (a -> b) -> [a] -> [b]
List.map TVarOf (TermOf (AtomOf a)) -> TermOf (AtomOf a)
forall term. IsTerm term => TVarOf term -> term
vt [TVarOf (TermOf (AtomOf a))]
argnames_y
            ant :: a
ant = (a -> a -> a) -> [a] -> a
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 a -> a -> a
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(∧) (((TermOf (AtomOf a), TermOf (AtomOf a)) -> a)
-> [(TermOf (AtomOf a), TermOf (AtomOf a))] -> [a]
forall a b. (a -> b) -> [a] -> [b]
List.map ((TermOf (AtomOf a) -> TermOf (AtomOf a) -> a)
-> (TermOf (AtomOf a), TermOf (AtomOf a)) -> a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry TermOf (AtomOf a) -> TermOf (AtomOf a) -> a
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
(.=.)) ([TermOf (AtomOf a)]
-> [TermOf (AtomOf a)] -> [(TermOf (AtomOf a), TermOf (AtomOf a))]
forall a b. [a] -> [b] -> [(a, b)]
zip [TermOf (AtomOf a)]
args_x [TermOf (AtomOf a)]
args_y))
            con :: a
con = AtomOf a -> a
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (PredOf (AtomOf a) -> [TermOf (AtomOf a)] -> AtomOf a
forall atom. HasApply atom => PredOf atom -> [TermOf atom] -> atom
applyPredicate PredOf (AtomOf a)
p [TermOf (AtomOf a)]
args_x) a -> a -> a
forall formula.
IsPropositional formula =>
formula -> formula -> formula
⇒ AtomOf a -> a
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (PredOf (AtomOf a) -> [TermOf (AtomOf a)] -> AtomOf a
forall atom. HasApply atom => PredOf atom -> [TermOf atom] -> atom
applyPredicate PredOf (AtomOf a)
p [TermOf (AtomOf a)]
args_y)

-- | Hence implement logic with equate just by adding equate "axioms".
equivalence_axioms :: forall fof atom term v.
                      (atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof,
                       IsQuantified fof, HasEquate atom, IsTerm term, Ord fof) => Set fof
equivalence_axioms :: forall fof atom term v.
(atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof,
 IsQuantified fof, HasEquate atom, IsTerm term, Ord fof) =>
Set fof
equivalence_axioms =
    [fof] -> Set fof
forall a. Ord a => [a] -> Set a
Set.fromList
    [VarOf fof -> fof -> fof
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) v
VarOf fof
"x" (term
TermOf atom
x TermOf atom -> TermOf atom -> fof
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. term
TermOf atom
x),
     VarOf fof -> fof -> fof
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) v
VarOf fof
"x" (VarOf fof -> fof -> fof
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) v
VarOf fof
"y" (VarOf fof -> fof -> fof
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) v
VarOf fof
"z" (term
TermOf atom
x TermOf atom -> TermOf atom -> fof
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. term
TermOf atom
y fof -> fof -> fof
forall formula.
IsPropositional formula =>
formula -> formula -> formula
∧ term
TermOf atom
x TermOf atom -> TermOf atom -> fof
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. term
TermOf atom
z fof -> fof -> fof
forall formula.
IsPropositional formula =>
formula -> formula -> formula
⇒ term
TermOf atom
y TermOf atom -> TermOf atom -> fof
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. term
TermOf atom
z)))]
    where
      x :: term
      x :: term
x = TVarOf term -> term
forall term. IsTerm term => TVarOf term -> term
vt (String -> TVarOf term
forall a. IsString a => String -> a
fromString String
"x")
      y :: term
      y :: term
y = TVarOf term -> term
forall term. IsTerm term => TVarOf term -> term
vt (String -> TVarOf term
forall a. IsString a => String -> a
fromString String
"y")
      z :: term
      z :: term
z = TVarOf term -> term
forall term. IsTerm term => TVarOf term -> term
vt (String -> TVarOf term
forall a. IsString a => String -> a
fromString String
"z")

equalitize :: forall formula atom term v function.
              (atom ~ AtomOf formula, term ~ TermOf atom, v ~ VarOf formula, v ~ TVarOf term, function ~ FunOf term,
               IsQuantified formula, HasEquate atom,
               IsTerm term, Ord formula, Ord atom) =>
              formula -> formula
equalitize :: forall formula atom term v function.
(atom ~ AtomOf formula, term ~ TermOf atom, v ~ VarOf formula,
 v ~ TVarOf term, function ~ FunOf term, IsQuantified formula,
 HasEquate atom, IsTerm term, Ord formula, Ord atom) =>
formula -> formula
equalitize formula
fm =
    if Set atom -> Bool
forall a. Set a -> Bool
Set.null Set atom
eqPreds then formula
fm else (formula -> formula -> formula) -> Set formula -> formula
forall a. (a -> a -> a) -> Set a -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(∧) Set formula
axioms formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
⇒ formula
fm
    where
      axioms :: Set formula
axioms = ((function, Int) -> Set formula -> Set formula)
-> Set formula -> Set (function, Int) -> Set formula
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Set formula -> Set formula -> Set formula
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Set formula -> Set formula -> Set formula)
-> ((function, Int) -> Set formula)
-> (function, Int)
-> Set formula
-> Set formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (function, Int) -> Set formula
forall fof atom term v p function.
(atom ~ AtomOf fof, term ~ TermOf atom, p ~ PredOf atom,
 v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term,
 IsQuantified fof, HasEquate atom, IsTerm term, Ord fof) =>
(function, Int) -> Set fof
function_congruence)
                        ((atom -> Set formula -> Set formula)
-> Set formula -> Set atom -> Set formula
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Set formula -> Set formula -> Set formula
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Set formula -> Set formula -> Set formula)
-> (atom -> Set formula) -> atom -> Set formula -> Set formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. atom -> Set formula
AtomOf formula -> Set formula
forall atom fof predicate term v.
(atom ~ AtomOf fof, predicate ~ PredOf atom, term ~ TermOf atom,
 v ~ VarOf fof, v ~ TVarOf term, IsQuantified fof, HasEquate atom,
 IsTerm term, Ord predicate) =>
AtomOf fof -> Set fof
predicate_congruence) Set formula
forall fof atom term v.
(atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof,
 IsQuantified fof, HasEquate atom, IsTerm term, Ord fof) =>
Set fof
equivalence_axioms Set atom
otherPreds)
                        (formula -> Set (function, Int)
forall formula atom function term.
(IsFormula formula, HasApply atom, Ord function,
 atom ~ AtomOf formula, term ~ TermOf atom,
 function ~ FunOf term) =>
formula -> Set (function, Int)
functions formula
fm)
      (Set atom
eqPreds, Set atom
otherPreds) = (atom -> Bool) -> Set atom -> (Set atom, Set atom)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition ((TermOf atom -> TermOf atom -> Bool)
-> (PredOf atom -> [TermOf atom] -> Bool) -> atom -> Bool
forall atom r.
HasEquate atom =>
(TermOf atom -> TermOf atom -> r)
-> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
forall r.
(TermOf atom -> TermOf atom -> r)
-> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
foldEquate (\TermOf atom
_ TermOf atom
_ -> Bool
True) (\PredOf atom
_ [TermOf atom]
_ -> Bool
False)) (formula -> Set (AtomOf formula)
forall formula.
IsFormula formula =>
formula -> Set (AtomOf formula)
predicates formula
fm)

-- -------------------------------------------------------------------------
-- Example.
-- -------------------------------------------------------------------------

testEqual01 :: Test
testEqual01 :: Test
testEqual01 = String -> Test -> Test
TestLabel String
"function_congruence" (Test -> Test) -> Test -> Test
forall a b. (a -> b) -> a -> b
$ Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> [Set Formula] -> [Set Formula] -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"function_congruence" [Set Formula]
expected [Set Formula]
input
    where input :: [Set Formula]
input = ((FunOf (TermOf (AtomOf Formula)), Int) -> Set Formula)
-> [(FunOf (TermOf (AtomOf Formula)), Int)] -> [Set Formula]
forall a b. (a -> b) -> [a] -> [b]
List.map (FunOf (TermOf (AtomOf Formula)), Int) -> Set Formula
forall fof atom term v p function.
(atom ~ AtomOf fof, term ~ TermOf atom, p ~ PredOf atom,
 v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term,
 IsQuantified fof, HasEquate atom, IsTerm term, Ord fof) =>
(function, Int) -> Set fof
function_congruence [(String -> FunOf (TermOf (AtomOf Formula))
forall a. IsString a => String -> a
fromString String
"f", Int
3 :: Int), (String -> FunOf (TermOf (AtomOf Formula))
forall a. IsString a => String -> a
fromString String
"+",Int
2)]
          expected :: [Set.Set Formula]
          expected :: [Set Formula]
expected = [[Formula] -> Set Formula
forall a. Ord a => [a] -> Set a
Set.fromList
                      [VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) V
VarOf Formula
"x1"
                       (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) V
VarOf Formula
"x2"
                        (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) V
VarOf Formula
"x3"
                         (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) V
VarOf Formula
"y1"
                          (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) V
VarOf Formula
"y2"
                           (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) V
VarOf Formula
"y3" (((SkTerm
TermOf (FOL Predicate SkTerm)
"x1" TermOf (FOL Predicate SkTerm)
-> TermOf (FOL Predicate SkTerm) -> Formula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. SkTerm
TermOf (FOL Predicate SkTerm)
"y1") Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
∧ ((SkTerm
TermOf (FOL Predicate SkTerm)
"x2" TermOf (FOL Predicate SkTerm)
-> TermOf (FOL Predicate SkTerm) -> Formula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. SkTerm
TermOf (FOL Predicate SkTerm)
"y2") Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
∧ (SkTerm
TermOf (FOL Predicate SkTerm)
"x3" TermOf (FOL Predicate SkTerm)
-> TermOf (FOL Predicate SkTerm) -> Formula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. SkTerm
TermOf (FOL Predicate SkTerm)
"y3"))) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
⇒
                                          ((FunOf SkTerm -> [SkTerm] -> SkTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp (String -> Function
forall a. IsString a => String -> a
fromString String
"f") [SkTerm
"x1",SkTerm
"x2",SkTerm
"x3"]) TermOf (FOL Predicate SkTerm)
-> TermOf (FOL Predicate SkTerm) -> Formula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. (FunOf SkTerm -> [SkTerm] -> SkTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp (String -> Function
forall a. IsString a => String -> a
fromString String
"f") [SkTerm
"y1",SkTerm
"y2",SkTerm
"y3"]))))))))],
                      [Formula] -> Set Formula
forall a. Ord a => [a] -> Set a
Set.fromList
                      [VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) V
VarOf Formula
"x1"
                       (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) V
VarOf Formula
"x2"
                        (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) V
VarOf Formula
"y1"
                         (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) V
VarOf Formula
"y2" (((SkTerm
TermOf (FOL Predicate SkTerm)
"x1" TermOf (FOL Predicate SkTerm)
-> TermOf (FOL Predicate SkTerm) -> Formula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. SkTerm
TermOf (FOL Predicate SkTerm)
"y1") Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
∧ (SkTerm
TermOf (FOL Predicate SkTerm)
"x2" TermOf (FOL Predicate SkTerm)
-> TermOf (FOL Predicate SkTerm) -> Formula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. SkTerm
TermOf (FOL Predicate SkTerm)
"y2")) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
⇒
                                        ((FunOf SkTerm -> [SkTerm] -> SkTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp (String -> Function
forall a. IsString a => String -> a
fromString String
"+") [SkTerm
"x1",SkTerm
"x2"]) TermOf (FOL Predicate SkTerm)
-> TermOf (FOL Predicate SkTerm) -> Formula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. (FunOf SkTerm -> [SkTerm] -> SkTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp (String -> Function
forall a. IsString a => String -> a
fromString String
"+") [SkTerm
"y1",SkTerm
"y2"]))))))]]

-- -------------------------------------------------------------------------
-- A simple example (see EWD1266a and the application to Morley's theorem).
-- -------------------------------------------------------------------------

ewd :: Formula
ewd :: Formula
ewd = Formula -> Formula
forall formula atom term v function.
(atom ~ AtomOf formula, term ~ TermOf atom, v ~ VarOf formula,
 v ~ TVarOf term, function ~ FunOf term, IsQuantified formula,
 HasEquate atom, IsTerm term, Ord formula, Ord atom) =>
formula -> formula
equalitize Formula
fm
    where
      fm :: Formula
fm = (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) V
VarOf Formula
"x" (Formula
fx Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
⇒ Formula
gx)) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
∧
           (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∃) V
VarOf Formula
"x" Formula
fx) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
∧
           (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) V
VarOf Formula
"x" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) V
VarOf Formula
"y" (Formula
gx Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
∧ Formula
gy Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
⇒ SkTerm
TermOf (FOL Predicate SkTerm)
x TermOf (FOL Predicate SkTerm)
-> TermOf (FOL Predicate SkTerm) -> Formula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. SkTerm
TermOf (FOL Predicate SkTerm)
y))) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
⇒
           (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) V
VarOf Formula
"y" (Formula
gy Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
⇒ Formula
fy))
      fx :: Formula
fx = PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"f" [SkTerm
TermOf (FOL Predicate SkTerm)
x]
      gx :: Formula
gx = PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"g" [SkTerm
TermOf (FOL Predicate SkTerm)
x]
      fy :: Formula
fy = PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"f" [SkTerm
TermOf (FOL Predicate SkTerm)
y]
      gy :: Formula
gy = PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"g" [SkTerm
TermOf (FOL Predicate SkTerm)
y]
      x :: SkTerm
x = TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
"x"
      y :: SkTerm
y = TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
"y"

testEqual02 :: Test
testEqual02 :: Test
testEqual02 = String -> Test -> Test
TestLabel String
"equalitize 1 (p. 241)" (Test -> Test) -> Test -> Test
forall a b. (a -> b) -> a -> b
$ Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String
-> (Formula, Set (Failing Depth))
-> (Formula, Set (Failing Depth))
-> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"equalitize 1 (p. 241)" (Formula
expected, Set (Failing Depth)
expectedProof) (Formula, Set (Failing Depth))
input
    where input :: (Formula, Set (Failing Depth))
input = (Formula
ewd, SkolemT Identity Function (Set (Failing Depth))
-> Set (Failing Depth)
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem (Maybe Depth
-> Formula -> SkolemT Identity Function (Set (Failing Depth))
forall fof atom term function (m :: * -> *) v.
(IsFirstOrder fof, Unify Failing (atom, atom),
 term ~ UTermOf (atom, atom), HasSkolem function, Monad m, Ord fof,
 atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term,
 v ~ VarOf fof, v ~ SVarOf function) =>
Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))
meson (Depth -> Maybe Depth
forall a. a -> Maybe a
Just (Int -> Depth
Depth Int
17)) Formula
ewd))
          fx :: Formula
fx = PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"f" [SkTerm
TermOf (FOL Predicate SkTerm)
x]
          gx :: Formula
gx = PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"g" [SkTerm
TermOf (FOL Predicate SkTerm)
x]
          fy :: Formula
fy = PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"f" [SkTerm
TermOf (FOL Predicate SkTerm)
y]
          gy :: Formula
gy = PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"g" [SkTerm
TermOf (FOL Predicate SkTerm)
y]
          x :: SkTerm
x = TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
"x"
          y :: SkTerm
y = TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
"y"
          z :: SkTerm
z = TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
"z"
          x1 :: SkTerm
x1 = TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
"x1"
          y1 :: SkTerm
y1 = TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
"y1"
          fx1 :: Formula
fx1 = PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"f" [SkTerm
TermOf (FOL Predicate SkTerm)
x1]
          gx1 :: Formula
gx1 = PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"g" [SkTerm
TermOf (FOL Predicate SkTerm)
x1]
          fy1 :: Formula
fy1 = PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"f" [SkTerm
TermOf (FOL Predicate SkTerm)
y1]
          gy1 :: Formula
gy1 = PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"g" [SkTerm
TermOf (FOL Predicate SkTerm)
y1]
          -- y1 = fromString "y1"
          -- z = fromString "z"
          expected :: Formula
expected =
              (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) V
VarOf Formula
"x" (SkTerm
TermOf (FOL Predicate SkTerm)
x TermOf (FOL Predicate SkTerm)
-> TermOf (FOL Predicate SkTerm) -> Formula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. SkTerm
TermOf (FOL Predicate SkTerm)
x) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
               ((VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) V
VarOf Formula
"x" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) V
VarOf Formula
"y" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) V
VarOf Formula
"z" (SkTerm
TermOf (FOL Predicate SkTerm)
x TermOf (FOL Predicate SkTerm)
-> TermOf (FOL Predicate SkTerm) -> Formula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. SkTerm
TermOf (FOL Predicate SkTerm)
y Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. SkTerm
TermOf (FOL Predicate SkTerm)
x TermOf (FOL Predicate SkTerm)
-> TermOf (FOL Predicate SkTerm) -> Formula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. SkTerm
TermOf (FOL Predicate SkTerm)
z Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. SkTerm
TermOf (FOL Predicate SkTerm)
y TermOf (FOL Predicate SkTerm)
-> TermOf (FOL Predicate SkTerm) -> Formula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. SkTerm
TermOf (FOL Predicate SkTerm)
z)))) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
                ((VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) V
VarOf Formula
"x1" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) V
VarOf Formula
"y1" (SkTerm
TermOf (FOL Predicate SkTerm)
x1 TermOf (FOL Predicate SkTerm)
-> TermOf (FOL Predicate SkTerm) -> Formula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. SkTerm
TermOf (FOL Predicate SkTerm)
y1 Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. Formula
fx1 Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. Formula
fy1))) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
                 (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) V
VarOf Formula
"x1" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) V
VarOf Formula
"y1" (SkTerm
TermOf (FOL Predicate SkTerm)
x1 TermOf (FOL Predicate SkTerm)
-> TermOf (FOL Predicate SkTerm) -> Formula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. SkTerm
TermOf (FOL Predicate SkTerm)
y1 Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. Formula
gx1 Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. Formula
gy1)))))) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>.
              (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) V
VarOf Formula
"x" (Formula
fx Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. Formula
gx)) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
              (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∃) V
VarOf Formula
"x" (Formula
fx)) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
              (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) V
VarOf Formula
"x" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) V
VarOf Formula
"y" (Formula
gx Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. Formula
gy Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. SkTerm
TermOf (FOL Predicate SkTerm)
x TermOf (FOL Predicate SkTerm)
-> TermOf (FOL Predicate SkTerm) -> Formula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. SkTerm
TermOf (FOL Predicate SkTerm)
y))) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>.
              (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) V
VarOf Formula
"y" (Formula
gy Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. Formula
fy))
          expectedProof :: Set (Failing Depth)
expectedProof =
              [Failing Depth] -> Set (Failing Depth)
forall a. Ord a => [a] -> Set a
Set.fromList [Depth -> Failing Depth
forall a. a -> Failing a
Success (Int -> Depth
Depth Int
6)]

-- | Wishnu Prasetya's example (even nicer with an "exists unique" primitive).

--instance IsString ([MyTerm] -> MyTerm) where
--    fromString = fApp . fromString

wishnu :: Formula
wishnu :: Formula
wishnu = [fof| (∃x. x=f (g (x))∧(∀x'. x'=f (g (x'))⇒x=x'))⇔(∃y. y=g (f (y))∧(∀y'. y'=g (f (y'))⇒y=y')) |]

-- This takes 0.7 seconds on my machine.
testEqual03 :: Test
testEqual03 :: Test
testEqual03 =
    (String -> Test -> Test
TestLabel String
"equalitize 2" (Test -> Test) -> (Assertion -> Test) -> Assertion -> Test
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Assertion -> Test
TestCase (Assertion -> Test)
-> (Assertion -> Assertion) -> Assertion -> Test
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (() -> NominalDiffTime -> String) -> Assertion -> Assertion
forall r. (r -> NominalDiffTime -> String) -> IO r -> IO r
timeMessage (\()
_ NominalDiffTime
t -> String
"\nEqualitize 2 compute time: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ NominalDiffTime -> String
forall a. Show a => a -> String
show NominalDiffTime
t))
       (String
-> (Formula, Set (Failing Depth))
-> (Formula, Set (Failing Depth))
-> Assertion
forall a.
(?loc::CallStack, Eq a, Pretty a) =>
String -> a -> a -> Assertion
assertEqual' String
"equalitize 2 (p. 241)" (Formula
expected, Set (Failing Depth)
expectedProof) (Formula, Set (Failing Depth))
input)
    where input :: (Formula, Set (Failing Depth))
input = (Formula -> Formula
forall formula atom term v function.
(atom ~ AtomOf formula, term ~ TermOf atom, v ~ VarOf formula,
 v ~ TVarOf term, function ~ FunOf term, IsQuantified formula,
 HasEquate atom, IsTerm term, Ord formula, Ord atom) =>
formula -> formula
equalitize Formula
wishnu, SkolemT Identity Function (Set (Failing Depth))
-> Set (Failing Depth)
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem (Maybe Depth
-> Formula -> SkolemT Identity Function (Set (Failing Depth))
forall fof atom term function (m :: * -> *) v.
(IsFirstOrder fof, Unify Failing (atom, atom),
 term ~ UTermOf (atom, atom), HasSkolem function, Monad m, Ord fof,
 atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term,
 v ~ VarOf fof, v ~ SVarOf function) =>
Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))
meson Maybe Depth
forall a. Maybe a
Nothing (Formula -> Formula
forall formula atom term v function.
(atom ~ AtomOf formula, term ~ TermOf atom, v ~ VarOf formula,
 v ~ TVarOf term, function ~ FunOf term, IsQuantified formula,
 HasEquate atom, IsTerm term, Ord formula, Ord atom) =>
formula -> formula
equalitize Formula
wishnu)))
          expected :: Formula
          expected :: Formula
expected = [fof| (∀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 (Failing Depth)
expectedProof = [Failing Depth] -> Set (Failing Depth)
forall a. Ord a => [a] -> Set a
Set.fromList [Depth -> Failing Depth
forall a. a -> Failing a
Success (Int -> Depth
Depth Int
16)]

-- -------------------------------------------------------------------------
-- More challenging equational problems. (Size 18, 61814 seconds.)
-- -------------------------------------------------------------------------

{-
(meson ** equalitize)
 <<(forall x y z. x * (y * z) = (x * y) * z) /\
   (forall x. 1 * x = x) /\
   (forall x. i(x) * x = 1)
   ==> forall x. x * i(x) = 1>>;;
-}

testEqual04 :: Test
testEqual04 :: Test
testEqual04 = String -> Test -> Test
TestLabel String
"equalitize 3 (p. 248)" (Test -> Test) -> Test -> Test
forall a b. (a -> b) -> a -> b
$ Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$
  (() -> NominalDiffTime -> String) -> Assertion -> Assertion
forall r. (r -> NominalDiffTime -> String) -> IO r -> IO r
timeMessage (\()
_ NominalDiffTime
t -> String
"\nCompute time: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ NominalDiffTime -> String
forall a. Show a => a -> String
show NominalDiffTime
t) (Assertion -> Assertion) -> Assertion -> Assertion
forall a b. (a -> b) -> a -> b
$
  String
-> (Formula, Set (Failing Depth))
-> (Formula, Set (Failing Depth))
-> Assertion
forall a.
(?loc::CallStack, Eq a, Pretty a) =>
String -> a -> a -> Assertion
assertEqual' String
"equalitize 3 (p. 248)" (Formula
expected, Set (Failing Depth)
expectedProof) (Formula, Set (Failing Depth))
input
    where
      input :: (Formula, Set (Failing Depth))
input = (Formula -> Formula
forall formula atom term v function.
(atom ~ AtomOf formula, term ~ TermOf atom, v ~ VarOf formula,
 v ~ TVarOf term, function ~ FunOf term, IsQuantified formula,
 HasEquate atom, IsTerm term, Ord formula, Ord atom) =>
formula -> formula
equalitize Formula
fm, SkolemT Identity Function (Set (Failing Depth))
-> Set (Failing Depth)
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem (Maybe Depth
-> Formula -> SkolemT Identity Function (Set (Failing Depth))
forall fof atom term function (m :: * -> *) v.
(IsFirstOrder fof, Unify Failing (atom, atom),
 term ~ UTermOf (atom, atom), HasSkolem function, Monad m, Ord fof,
 atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term,
 v ~ VarOf fof, v ~ SVarOf function) =>
Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))
meson (Depth -> Maybe Depth
forall a. a -> Maybe a
Just (Int -> Depth
Depth Int
20)) (Formula -> SkolemT Identity Function (Set (Failing Depth)))
-> (Formula -> Formula)
-> Formula
-> SkolemT Identity Function (Set (Failing Depth))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula -> Formula
forall formula atom term v function.
(atom ~ AtomOf formula, term ~ TermOf atom, v ~ VarOf formula,
 v ~ TVarOf term, function ~ FunOf term, IsQuantified formula,
 HasEquate atom, IsTerm term, Ord formula, Ord atom) =>
formula -> formula
equalitize (Formula -> SkolemT Identity Function (Set (Failing Depth)))
-> Formula -> SkolemT Identity Function (Set (Failing Depth))
forall a b. (a -> b) -> a -> b
$ Formula
fm))
      fm :: Formula
      fm :: Formula
fm = [fof| (forall x y z. x * (y * z) = (x * y) * z) .&.
                 (forall x. 1 * x = x) .&.
                 (forall x. i(x) * x = 1)
                 ==> (forall x. x * i(x) = 1) |]
{-
      fm = [fof| (∀x y z. ((*) ["x'", (*) ["y'", "z'"]] .=. (*) [((*) ["x'", "y'"]), "z'"]) ∧
           (∀) "x" ((*) [one, "x'"] .=. "x'") ∧
           (∀) "x" ((*) [i ["x'"], "x'"] .=. one) ⇒
           (∀) "x" ((*) ["x'", i ["x'"]] .=. one)
      fm = ((∀) "x" . (∀) "y" . (∀) "z") ((*) ["x'", (*) ["y'", "z'"]] .=. (*) [((*) ["x'", "y'"]), "z'"]) ∧
           (∀) "x" ((*) [one, "x'"] .=. "x'") ∧
           (∀) "x" ((*) [i ["x'"], "x'"] .=. one) ⇒
           (∀) "x" ((*) ["x'", i ["x'"]] .=. one)
      (*) = fApp (fromString "*")
      i = fApp (fromString "i")
      one = fApp (fromString "1") []
-}
      expected :: Formula
      expected :: Formula
expected =
          [fof| (∀x. x=x)∧
                (∀x y z. x=y∧x=z⇒y=z)∧
                (∀x' x'' y' y''. x'=y'∧x''=y''⇒(x' * x'')=(y' * y''))⇒
                (∀x y z. (x' * (y' * z'))=((x'* y') * z'))∧
                (∀x. (1 * x')=x')∧
                (∀x. (i(x') * x')=1)⇒
                (∀x. (x' * i(x'))=1) |]
{-
          ((∀) "x" ("x" .=. "x") .&.
           ((∀) "x" ((∀) "y" ((∀) "z" ((("x" .=. "y") .&. ("x" .=. "z")) .=>. ("y" .=. "z")))) .&.
            ((∀) "x1" ((∀) "x2" ((∀) "y1" ((∀) "y2" ((("x1" .=. "y1") .&. ("x2" .=. "y2")) .=>.
                                                                     ((fApp "*" ["x1","x2"]) .=. (fApp "*" ["y1","y2"])))))) .&.
             (∀) "x1" ((∀) "y1" (("x1" .=. "y1") .=>. ((fApp "i" ["x1"]) .=. (fApp "i" ["y1"]))))))) .=>.
          ((((∀) "x" ((∀) "y" ((∀) "z" ((fApp "*" ["x",fApp "*" ["y","z"]]) .=. (fApp "*" [fApp "*" ["x","y"],"z"])))) .&.
             (∀) "x" ((fApp "*" [fApp "1" [],"x"]) .=. "x")) .&.
            (∀) "x" ((fApp "*" [fApp "i" ["x"],"x"]) .=. (fApp "1" []))) .=>.
           (∀) "x" ((fApp "*" ["x",fApp "i" ["x"]]) .=. (fApp "1" []))) -}
      expectedProof :: Set.Set (Failing Depth)
      expectedProof :: Set (Failing Depth)
expectedProof = [Failing Depth] -> Set (Failing Depth)
forall a. Ord a => [a] -> Set a
Set.fromList [[String] -> Failing Depth
forall a. [String] -> Failing a
Failure [String
"Exceeded maximum depth limit"]]

testEqual :: Test
testEqual :: Test
testEqual = String -> Test -> Test
TestLabel String
"Equal" ([Test] -> Test
TestList [Test
testEqual01, Test
testEqual02, Test
testEqual03 {-, testEqual04-}])

-- -------------------------------------------------------------------------
-- Other variants not mentioned in book.
-- -------------------------------------------------------------------------

{-
{- ************

(meson ** equalitize)
 <<(forall x y z. x * (y * z) = (x * y) * z) /\
   (forall x. 1 * x = x) /\
   (forall x. x * 1 = x) /\
   (forall x. x * x = 1)
   ==> forall x y. x * y  = y * x>>;;

-- -------------------------------------------------------------------------
-- With symmetry at leaves and one-sided congruences (Size = 16, 54659 s).
-- -------------------------------------------------------------------------

let fm =
 <<(forall x. x = x) /\
   (forall x y z. x * (y * z) = (x * y) * z) /\
   (forall x y z. =((x * y) * z,x * (y * z))) /\
   (forall x. 1 * x = x) /\
   (forall x. x = 1 * x) /\
   (forall x. i(x) * x = 1) /\
   (forall x. 1 = i(x) * x) /\
   (forall x y. x = y ==> i(x) = i(y)) /\
   (forall x y z. x = y ==> x * z = y * z) /\
   (forall x y z. x = y ==> z * x = z * y) /\
   (forall x y z. x = y /\ y = z ==> x = z)
   ==> forall x. x * i(x) = 1>>;;

time meson fm;;

-- -------------------------------------------------------------------------
-- Newer version of stratified equalities.
-- -------------------------------------------------------------------------

let fm =
 <<(forall x y z. axiom(x * (y * z),(x * y) * z)) /\
   (forall x y z. axiom((x * y) * z,x * (y * z)) /\
   (forall x. axiom(1 * x,x)) /\
   (forall x. axiom(x,1 * x)) /\
   (forall x. axiom(i(x) * x,1)) /\
   (forall x. axiom(1,i(x) * x)) /\
   (forall x x'. x = x' ==> cchain(i(x),i(x'))) /\
   (forall x x' y y'. x = x' /\ y = y' ==> cchain(x * y,x' * y'))) /\
   (forall s t. axiom(s,t) ==> achain(s,t)) /\
   (forall s t u. axiom(s,t) /\ (t = u) ==> achain(s,u)) /\
   (forall x x' u. x = x' /\ achain(i(x'),u) ==> cchain(i(x),u)) /\
   (forall x x' y y' u.
        x = x' /\ y = y' /\ achain(x' * y',u) ==> cchain(x * y,u)) /\
   (forall s t. cchain(s,t) ==> s = t) /\
   (forall s t. achain(s,t) ==> s = t) /\
   (forall t. t = t)
   ==> forall x. x * i(x) = 1>>;;

time meson fm;;

let fm =
 <<(forall x y z. axiom(x * (y * z),(x * y) * z)) /\
   (forall x y z. axiom((x * y) * z,x * (y * z)) /\
   (forall x. axiom(1 * x,x)) /\
   (forall x. axiom(x,1 * x)) /\
   (forall x. axiom(i(x) * x,1)) /\
   (forall x. axiom(1,i(x) * x)) /\
   (forall x x'. x = x' ==> cong(i(x),i(x'))) /\
   (forall x x' y y'. x = x' /\ y = y' ==> cong(x * y,x' * y'))) /\
   (forall s t. axiom(s,t) ==> achain(s,t)) /\
   (forall s t. cong(s,t) ==> cchain(s,t)) /\
   (forall s t u. axiom(s,t) /\ (t = u) ==> achain(s,u)) /\
   (forall s t u. cong(s,t) /\ achain(t,u) ==> cchain(s,u)) /\
   (forall s t. cchain(s,t) ==> s = t) /\
   (forall s t. achain(s,t) ==> s = t) /\
   (forall t. t = t)
   ==> forall x. x * i(x) = 1>>;;

time meson fm;;

-- -------------------------------------------------------------------------
-- Showing congruence closure.
-- -------------------------------------------------------------------------

let fm = equalitize
 <<forall c. f(f(f(f(f(c))))) = c /\ f(f(f(c))) = c ==> f(c) = c>>;;

time meson fm;;

let fm =
 <<axiom(f(f(f(f(f(c))))),c) /\
   axiom(c,f(f(f(f(f(c)))))) /\
   axiom(f(f(f(c))),c) /\
   axiom(c,f(f(f(c)))) /\
   (forall s t. axiom(s,t) ==> achain(s,t)) /\
   (forall s t. cong(s,t) ==> cchain(s,t)) /\
   (forall s t u. axiom(s,t) /\ (t = u) ==> achain(s,u)) /\
   (forall s t u. cong(s,t) /\ achain(t,u) ==> cchain(s,u)) /\
   (forall s t. cchain(s,t) ==> s = t) /\
   (forall s t. achain(s,t) ==> s = t) /\
   (forall t. t = t) /\
   (forall x y. x = y ==> cong(f(x),f(y)))
   ==> f(c) = c>>;;

time meson fm;;

-- -------------------------------------------------------------------------
-- With stratified equalities.
-- -------------------------------------------------------------------------

let fm =
 <<(forall x y z. eqA (x * (y * z),(x * y) * z)) /\
   (forall x y z. eqA ((x * y) * z)) /\
   (forall x. eqA (1 * x,x)) /\
   (forall x. eqA (x,1 * x)) /\
   (forall x. eqA (i(x) * x,1)) /\
   (forall x. eqA (1,i(x) * x)) /\
   (forall x. eqA (x,x)) /\
   (forall x y. eqA (x,y) ==> eqC (i(x),i(y))) /\
   (forall x y. eqC (x,y) ==> eqC (i(x),i(y))) /\
   (forall x y. eqT (x,y) ==> eqC (i(x),i(y))) /\
   (forall w x y z. eqA (w,x) /\ eqA (y,z) ==> eqC (w * y,x * z)) /\
   (forall w x y z. eqA (w,x) /\ eqC (y,z) ==> eqC (w * y,x * z)) /\
   (forall w x y z. eqA (w,x) /\ eqT (y,z) ==> eqC (w * y,x * z)) /\
   (forall w x y z. eqC (w,x) /\ eqA (y,z) ==> eqC (w * y,x * z)) /\
   (forall w x y z. eqC (w,x) /\ eqC (y,z) ==> eqC (w * y,x * z)) /\
   (forall w x y z. eqC (w,x) /\ eqT (y,z) ==> eqC (w * y,x * z)) /\
   (forall w x y z. eqT (w,x) /\ eqA (y,z) ==> eqC (w * y,x * z)) /\
   (forall w x y z. eqT (w,x) /\ eqC (y,z) ==> eqC (w * y,x * z)) /\
   (forall w x y z. eqT (w,x) /\ eqT (y,z) ==> eqC (w * y,x * z)) /\
   (forall x y z. eqA (x,y) /\ eqA (y,z) ==> eqT (x,z)) /\
   (forall x y z. eqC (x,y) /\ eqA (y,z) ==> eqT (x,z)) /\
   (forall x y z. eqA (x,y) /\ eqC (y,z) ==> eqT (x,z)) /\
   (forall x y z. eqA (x,y) /\ eqT (y,z) ==> eqT (x,z)) /\
   (forall x y z. eqC (x,y) /\ eqT (y,z) ==> eqT (x,z))
   ==> forall x. eqT (x * i(x),1)>>;;

-- -------------------------------------------------------------------------
-- With transitivity chains...
-- -------------------------------------------------------------------------

let fm =
 <<(forall x y z. eqA (x * (y * z),(x * y) * z)) /\
   (forall x y z. eqA ((x * y) * z)) /\
   (forall x. eqA (1 * x,x)) /\
   (forall x. eqA (x,1 * x)) /\
   (forall x. eqA (i(x) * x,1)) /\
   (forall x. eqA (1,i(x) * x)) /\
   (forall x y. eqA (x,y) ==> eqC (i(x),i(y))) /\
   (forall x y. eqC (x,y) ==> eqC (i(x),i(y))) /\
   (forall w x y. eqA (w,x) ==> eqC (w * y,x * y)) /\
   (forall w x y. eqC (w,x) ==> eqC (w * y,x * y)) /\
   (forall x y z. eqA (y,z) ==> eqC (x * y,x * z)) /\
   (forall x y z. eqC (y,z) ==> eqC (x * y,x * z)) /\
   (forall x y z. eqA (x,y) /\ eqA (y,z) ==> eqT (x,z)) /\
   (forall x y z. eqC (x,y) /\ eqA (y,z) ==> eqT (x,z)) /\
   (forall x y z. eqA (x,y) /\ eqC (y,z) ==> eqT (x,z)) /\
   (forall x y z. eqC (x,y) /\ eqC (y,z) ==> eqT (x,z)) /\
   (forall x y z. eqA (x,y) /\ eqT (y,z) ==> eqT (x,z)) /\
   (forall x y z. eqC (x,y) /\ eqT (y,z) ==> eqT (x,z))
   ==> forall x. eqT (x * i(x),1) \/ eqC (x * i(x),1)>>;;

time meson fm;;

-- -------------------------------------------------------------------------
-- Enforce canonicity (proof size = 20).
-- -------------------------------------------------------------------------

let fm =
 <<(forall x y z. eq1(x * (y * z),(x * y) * z)) /\
   (forall x y z. eq1((x * y) * z,x * (y * z))) /\
   (forall x. eq1(1 * x,x)) /\
   (forall x. eq1(x,1 * x)) /\
   (forall x. eq1(i(x) * x,1)) /\
   (forall x. eq1(1,i(x) * x)) /\
   (forall x y z. eq1(x,y) ==> eq1(x * z,y * z)) /\
   (forall x y z. eq1(x,y) ==> eq1(z * x,z * y)) /\
   (forall x y z. eq1(x,y) /\ eq2(y,z) ==> eq2(x,z)) /\
   (forall x y. eq1(x,y) ==> eq2(x,y))
   ==> forall x. eq2(x,i(x))>>;;

time meson fm;;

***************** -}
END_INTERACTIVE;;
-}