sbv-10.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Documentation.SBV.Examples.Misc.FirstOrderLogic

Contents

- Pushing negation over quantifiers
- Interchanging quantifiers
- Merging quantifiers
- Scoping over quantifiers
- A non-identity
- Exists unique
- Skolemization
- Special relations
  - Partial orders
  - Linear orders
  - Tree orders
  - Piecewise linear orders
  - Transitive closures

Description

Proves various first-order logic properties using SBV. The properties we prove all come from https://en.wikipedia.org/wiki/First-order_logic

Synopsis

- data U
- type SU = SBV U
- data V
- type SV = SBV V
- data E
  - = A
  - | B
  - | C
- type SE = SBV E
- sC :: SBV E
- sB :: SBV E
- sA :: SBV E
- qe :: QuantifiedBool a => a -> SBool
- skolemEx1 :: Forall "x" Word8 -> Exists "y" Word8 -> SBool
- skolemEx2 :: Forall "a" Word8 -> Exists "b" Word8 -> Forall "c" Word8 -> Exists "d" Word8 -> SBool
- skolemEx3 :: Exists "x" Word8 -> Forall "y" Word8 -> SBool
- skolemEx4 :: IO SatResult
- poExample :: IO ThmResult
- tcExample1 :: IO ThmResult
- tcExample2 :: IO ThmResult
- tcExample3 :: IO ThmResult

# Documentation

    >>> -- For doctest purposes only, ignore.
    >>> import Data.SBV
    >>> :set -XDataKinds

data U Source #

An uninterpreted sort for demo purposes, named `U`

#### Instances

Instances details

Data U Source # |

Instance details

Defined in Documentation.SBV.Examples.Misc.FirstOrderLogic

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> U -> c U Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c U Source #

toConstr :: U -> Constr Source #

dataTypeOf :: U -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c U) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c U) Source #

gmapT :: (forall b. Data b => b -> b) -> U -> U Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> U -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> U -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> U -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> U -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> U -> m U Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> U -> m U Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> U -> m U Source #

Read U Source # |
Instance details Defined in Documentation.SBV.Examples.Misc.FirstOrderLogic Methods readsPrec :: Int -> ReadS U Source # readList :: ReadS [U] Source # readPrec :: ReadPrec U Source # readListPrec :: ReadPrec [U] Source #
Show U Source # |
Instance details Defined in Documentation.SBV.Examples.Misc.FirstOrderLogic Methods showsPrec :: Int -> U -> ShowS Source # show :: U -> String Source # showList :: [U] -> ShowS Source #
SymVal U Source # |

Instance details

Defined in Documentation.SBV.Examples.Misc.FirstOrderLogic

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV U) Source #

literal :: U -> SBV U Source #

fromCV :: CV -> U Source #

isConcretely :: SBV U -> (U -> Bool) -> Bool Source #

free :: MonadSymbolic m => String -> m (SBV U) Source #

free_ :: MonadSymbolic m => m (SBV U) Source #

mkFreeVars :: MonadSymbolic m => Int -> m [SBV U] Source #

symbolic :: MonadSymbolic m => String -> m (SBV U) Source #

symbolics :: MonadSymbolic m => [String] -> m [SBV U] Source #

unliteral :: SBV U -> Maybe U Source #

isConcrete :: SBV U -> Bool Source #

isSymbolic :: SBV U -> Bool Source #

HasKind U Source # |

Instance details

Defined in Documentation.SBV.Examples.Misc.FirstOrderLogic

Methods

kindOf :: U -> Kind Source #

hasSign :: U -> Bool Source #

intSizeOf :: U -> Int Source #

isBoolean :: U -> Bool Source #

isBounded :: U -> Bool Source #

isReal :: U -> Bool Source #

isFloat :: U -> Bool Source #

isDouble :: U -> Bool Source #

isRational :: U -> Bool Source #

isFP :: U -> Bool Source #

isUnbounded :: U -> Bool Source #

isUserSort :: U -> Bool Source #

isChar :: U -> Bool Source #

isString :: U -> Bool Source #

isList :: U -> Bool Source #

isSet :: U -> Bool Source #

isTuple :: U -> Bool Source #

isMaybe :: U -> Bool Source #

isEither :: U -> Bool Source #

showType :: U -> String Source #

SatModel U Source # |
Instance details Defined in Documentation.SBV.Examples.Misc.FirstOrderLogic Methods parseCVs :: [CV] -> Maybe (U, [CV]) Source # cvtModel :: (U -> Maybe b) -> Maybe (U, [CV]) -> Maybe (b, [CV]) Source #

type SU = SBV U Source #

Symbolic version of the type `U`.

data V Source #

An uninterpreted sort for demo purposes, named `V`

#### Instances

Instances details

Data V Source # |

Instance details

Defined in Documentation.SBV.Examples.Misc.FirstOrderLogic

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> V -> c V Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c V Source #

toConstr :: V -> Constr Source #

dataTypeOf :: V -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c V) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c V) Source #

gmapT :: (forall b. Data b => b -> b) -> V -> V Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> V -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> V -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> V -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> V -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> V -> m V Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> V -> m V Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> V -> m V Source #

Read V Source # |
Instance details Defined in Documentation.SBV.Examples.Misc.FirstOrderLogic Methods readsPrec :: Int -> ReadS V Source # readList :: ReadS [V] Source # readPrec :: ReadPrec V Source # readListPrec :: ReadPrec [V] Source #
Show V Source # |
Instance details Defined in Documentation.SBV.Examples.Misc.FirstOrderLogic Methods showsPrec :: Int -> V -> ShowS Source # show :: V -> String Source # showList :: [V] -> ShowS Source #
SymVal V Source # |

Instance details

Defined in Documentation.SBV.Examples.Misc.FirstOrderLogic

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV V) Source #

literal :: V -> SBV V Source #

fromCV :: CV -> V Source #

isConcretely :: SBV V -> (V -> Bool) -> Bool Source #

free :: MonadSymbolic m => String -> m (SBV V) Source #

free_ :: MonadSymbolic m => m (SBV V) Source #

mkFreeVars :: MonadSymbolic m => Int -> m [SBV V] Source #

symbolic :: MonadSymbolic m => String -> m (SBV V) Source #

symbolics :: MonadSymbolic m => [String] -> m [SBV V] Source #

unliteral :: SBV V -> Maybe V Source #

isConcrete :: SBV V -> Bool Source #

isSymbolic :: SBV V -> Bool Source #

HasKind V Source # |

Instance details

Defined in Documentation.SBV.Examples.Misc.FirstOrderLogic

Methods

kindOf :: V -> Kind Source #

hasSign :: V -> Bool Source #

intSizeOf :: V -> Int Source #

isBoolean :: V -> Bool Source #

isBounded :: V -> Bool Source #

isReal :: V -> Bool Source #

isFloat :: V -> Bool Source #

isDouble :: V -> Bool Source #

isRational :: V -> Bool Source #

isFP :: V -> Bool Source #

isUnbounded :: V -> Bool Source #

isUserSort :: V -> Bool Source #

isChar :: V -> Bool Source #

isString :: V -> Bool Source #

isList :: V -> Bool Source #

isSet :: V -> Bool Source #

isTuple :: V -> Bool Source #

isMaybe :: V -> Bool Source #

isEither :: V -> Bool Source #

showType :: V -> String Source #

SatModel V Source # |
Instance details Defined in Documentation.SBV.Examples.Misc.FirstOrderLogic Methods parseCVs :: [CV] -> Maybe (V, [CV]) Source # cvtModel :: (V -> Maybe b) -> Maybe (V, [CV]) -> Maybe (b, [CV]) Source #

type SV = SBV V Source #

Symbolic version of the type `V`.

data E Source #

An enumerated type for demo purposes, named `E`

Constructors

A |
B |
C |

#### Instances

Instances details

Data E Source # |

Instance details

Defined in Documentation.SBV.Examples.Misc.FirstOrderLogic

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> E -> c E Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c E Source #

toConstr :: E -> Constr Source #

dataTypeOf :: E -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c E) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c E) Source #

gmapT :: (forall b. Data b => b -> b) -> E -> E Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> E -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> E -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> E -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> E -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> E -> m E Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> E -> m E Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> E -> m E Source #

Read E Source # |
Instance details Defined in Documentation.SBV.Examples.Misc.FirstOrderLogic Methods readsPrec :: Int -> ReadS E Source # readList :: ReadS [E] Source # readPrec :: ReadPrec E Source # readListPrec :: ReadPrec [E] Source #
Show E Source # |
Instance details Defined in Documentation.SBV.Examples.Misc.FirstOrderLogic Methods showsPrec :: Int -> E -> ShowS Source # show :: E -> String Source # showList :: [E] -> ShowS Source #
Eq E Source # |
Instance details Defined in Documentation.SBV.Examples.Misc.FirstOrderLogic Methods (==) :: E -> E -> Bool Source # (/=) :: E -> E -> Bool Source #
Ord E Source # |
Instance details Defined in Documentation.SBV.Examples.Misc.FirstOrderLogic Methods compare :: E -> E -> Ordering Source # (<) :: E -> E -> Bool Source # (<=) :: E -> E -> Bool Source # (>) :: E -> E -> Bool Source # (>=) :: E -> E -> Bool Source # max :: E -> E -> E Source # min :: E -> E -> E Source #
SymVal E Source # |

Instance details

Defined in Documentation.SBV.Examples.Misc.FirstOrderLogic

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV E) Source #

literal :: E -> SBV E Source #

fromCV :: CV -> E Source #

isConcretely :: SBV E -> (E -> Bool) -> Bool Source #

free :: MonadSymbolic m => String -> m (SBV E) Source #

free_ :: MonadSymbolic m => m (SBV E) Source #

mkFreeVars :: MonadSymbolic m => Int -> m [SBV E] Source #

symbolic :: MonadSymbolic m => String -> m (SBV E) Source #

symbolics :: MonadSymbolic m => [String] -> m [SBV E] Source #

unliteral :: SBV E -> Maybe E Source #

isConcrete :: SBV E -> Bool Source #

isSymbolic :: SBV E -> Bool Source #

HasKind E Source # |

Instance details

Defined in Documentation.SBV.Examples.Misc.FirstOrderLogic

Methods

kindOf :: E -> Kind Source #

hasSign :: E -> Bool Source #

intSizeOf :: E -> Int Source #

isBoolean :: E -> Bool Source #

isBounded :: E -> Bool Source #

isReal :: E -> Bool Source #

isFloat :: E -> Bool Source #

isDouble :: E -> Bool Source #

isRational :: E -> Bool Source #

isFP :: E -> Bool Source #

isUnbounded :: E -> Bool Source #

isUserSort :: E -> Bool Source #

isChar :: E -> Bool Source #

isString :: E -> Bool Source #

isList :: E -> Bool Source #

isSet :: E -> Bool Source #

isTuple :: E -> Bool Source #

isMaybe :: E -> Bool Source #

isEither :: E -> Bool Source #

showType :: E -> String Source #

SatModel E Source # |
Instance details Defined in Documentation.SBV.Examples.Misc.FirstOrderLogic Methods parseCVs :: [CV] -> Maybe (E, [CV]) Source # cvtModel :: (E -> Maybe b) -> Maybe (E, [CV]) -> Maybe (b, [CV]) Source #

type SE = SBV E Source #

Symbolic version of the type `E`.

sC :: SBV E Source #

Symbolic version of the constructor `C`.

sB :: SBV E Source #

Symbolic version of the constructor `B`.

sA :: SBV E Source #

Symbolic version of the constructor `A`.

qe :: QuantifiedBool a => a -> SBool Source #

Helper to turn quantified formula to a regular boolean. We can think of this as quantifier elimination, hence the name `qe`.

# Pushing negation over quantifiers

\(\lnot \forall x\,P(x)\Leftrightarrow \exists x\,\lnot P(x)\)

    >>> let p = uninterpret "P" :: SU -> SBool
    >>> prove $ sNot (qe (\(Forall x) -> p x)) .<=> qe (\(Exists x) -> sNot (p x))
    Q.E.D.

\(\lnot \exists x\,P(x)\Leftrightarrow \forall x\,\lnot P(x)\)

    >>> let p = uninterpret "P" :: SU -> SBool
    >>> prove $ sNot (qe (\(Exists x) -> p x)) .<=> qe (\(Forall x) -> sNot (p x))
    Q.E.D.

# Interchanging quantifiers

\(\forall x\,\forall y\,P(x,y)\Leftrightarrow \forall y\,\forall x\,P(x,y)\)

    >>> let p = uninterpret "P" :: (SU, SV) -> SBool
    >>> prove $ qe (\(Forall x) (Forall y) -> p (x, y)) .<=> qe (\(Forall y) (Forall x) -> p (x, y))
    Q.E.D.

\(\exists x\,\exists y\,P(x,y)\Leftrightarrow \exists y\,\exists x\,P(x,y)\)

    >>> let p = uninterpret "P" :: (SU, SV) -> SBool
    >>> prove $ qe (\(Exists x) (Exists y) -> p (x, y)) .<=> qe (\(Exists y) (Exists x) -> p (x, y))
    Q.E.D.

# Merging quantifiers

\(\forall x\,P(x)\land \forall x\,Q(x)\Leftrightarrow \forall x\,(P(x)\land Q(x))\)

    >>> let p = uninterpret "P" :: SU -> SBool
    >>> let q = uninterpret "Q" :: SU -> SBool
    >>> prove $ (qe (\(Forall x) -> p x) .&& qe (\(Forall x) -> q x)) .<=> qe (\(Forall x) -> p x .&& q x)
    Q.E.D.

\(\exists x\,P(x)\lor \exists x\,Q(x)\Leftrightarrow \exists x\,(P(x)\lor Q(x))\)

    >>> let p = uninterpret "P" :: SU -> SBool
    >>> let q = uninterpret "Q" :: SU -> SBool
    >>> prove $ (qe (\(Exists x) -> p x) .|| qe (\(Exists x) -> q x)) .<=> qe (\(Exists x) -> p x .|| q x)
    Q.E.D.

# Scoping over quantifiers

Provided \(x\) is not free in \(P\): \(P\land \exists x\,Q(x)\Leftrightarrow \exists x\,(P\land Q(x))\)

    >>> let p = uninterpret "P" :: SBool
    >>> let q = uninterpret "Q" :: SU -> SBool
    >>> prove $ (p .&& qe (\(Exists x) -> q x)) .<=> qe (\(Exists x) -> p .&& q x)
    Q.E.D.

Provided \(x\) is not free in \(P\): \(P\lor \forall x\,Q(x)\Leftrightarrow \forall x\,(P\lor Q(x))\)

    >>> let p = uninterpret "P" :: SBool
    >>> let q = uninterpret "Q" :: SU -> SBool
    >>> prove $ (p .|| qe (\(Forall x) -> q x)) .<=> qe (\(Forall x) -> p .|| q x)
    Q.E.D.

# A non-identity

It's instructive to look at an example where the proof actually fails. Consider, for instance, an example of a merging quantifiers like we did above, except when the equality doesn't hold. That is, we try to prove the "correct" sounding, but incorrect conjecture:

\(\forall x\,P(x)\lor \forall x\,Q(x)\Leftrightarrow \forall x\,(P(x)\lor Q(x))\)

We have:

    >>> let p = uninterpret "P" :: SU -> SBool
    >>> let q = uninterpret "Q" :: SU -> SBool
    >>> prove $ (qe (\(Forall x) -> p x) .|| qe (\(Forall x) -> q x)) .<=> qe (\(Forall x) -> p x .|| q x)
    Falsifiable. Counter-example:
      P :: U -> Bool
      P U!val!2 = True
      P U!val!0 = True
      P _       = False

      Q :: U -> Bool
      Q U!val!2 = False
      Q U!val!0 = False
      Q _       = True

The solver found us a falsifying instance: Pick a domain with at least three elements. We'll call the first element `U!val!2`, and the second element `U!val!0`, without naming the others. (Unfortunately the solver picks nonintuitive names, but you can substitute better names if you like. They're just names of two distinct objects that belong to the domain \(U\) with no other meaning.)

Arrange so that \(P\) is true on `U!val!2` and `U!val!0`, but false for everything else. Also arrange so that \(Q\) is false on these two elements, but true for everything else.

With this assignment, the right hand side of our conjecture is true no matter which element you pick, because either \(P\) or \(Q\) is true on any given element. (Actually, only one will be true on any element, but that is tangential.) But left-hand-side is not a tautology: Clearly neither \(P\) nor \(Q\) are true for all elements, and hence both disjuncts are false. Thus, the alleged conjecture is not an equivalence in first order logic.

# Exists unique

We can use the `ExistsUnique` constructor to indicate a value must exists uniquely. For instance, we can prove that there is an element in `E` that's less than `C`, but it's not unique. However, there's a unique element that's less than all the elements in `E`:

    >>> prove $ \(Exists       (me :: SE)) -> me .<= sC
    Q.E.D.
    >>> prove $ \(ExistsUnique (me :: SE)) -> me .<= sC
    Falsifiable
    >>> prove $ \(ExistsUnique (me :: SE)) (Forall e) -> me .<= e
    Q.E.D.

# Skolemization

Given a formula, skolemization produces an equisatisfiable formula that has no existential quantifiers. Instead, the existentials are replaced by uninterpreted functions. Skolemization is useful when we want to see the instantiation of nested existential variables. Interpretation for such variables will be functions of the enclosing universals.

skolemEx1 :: Forall "x" Word8 -> Exists "y" Word8 -> SBool Source #

Consider the formula \(\forall x\,\exists y\, x \ge y\), over bit-vectors of size 8. We can ask SBV to satisfy it:

    >>> sat skolemEx1
    Satisfiable

But this isn't really illimunating. We can first skolemize, and then ask to satisfy:

    >>> sat $ skolemize skolemEx1
    Satisfiable. Model:
      y :: Word8 -> Word8
      y x = x

which is much better We are told that we can have the witness as the value given for each choice of `x`.

skolemEx2 :: Forall "a" Word8 -> Exists "b" Word8 -> Forall "c" Word8 -> Exists "d" Word8 -> SBool Source #

Consider the formula \(\forall a\,\exists b\,\forall c\,\exists d\, a + b >= c + d\), over bit-vectors of size 8. We can ask SBV to satisfy it:

    >>> sat skolemEx2
    Satisfiable

Again, we're left in the dark as to why this is satisfiable. Let's skolemize first, and then call `sat` on it:

    >>> sat $ skolemize skolemEx2
    Satisfiable. Model:
      b :: Word8 -> Word8
      b _ = 0

      d :: Word8 -> Word8 -> Word8
      d a c = a + (255 * c)

Let's see what the solver said. It suggested we should use the value of `0` for `b`, regardless of the choice of `a`. (Note how `b` is a function of one variable, i.e., of `a`) And it suggested using `a + (255 * c)` for `d`, for whatever we choose for `a` and `c`. Why does this work? Well, given arbitrary `a` and `c`, we end up with:

        a + b >= c + d
        --> substitute b = 0 and d = a + 255c as suggested by the solver
        a + 0 >= c + a + 255c
        a >= 256c + a
        a >= a

showing the formula is satisfiable for whatever values you pick for `a` and `c`. Note that `256` is simply `0` when interpreted modulo `2^8`. Clever!

skolemEx3 :: Exists "x" Word8 -> Forall "y" Word8 -> SBool Source #

A common proof technique to show validity is to show that the negation is unsatisfiable. Note that if you want to skolemize during this process, you should first negate and then skolemize!

This example demonstrates the possible pitfall. The `skolemEx3` function encodes \(\exists x\, \forall y\, y \ge x\) for 8-bit bitvectors; which is a valid statement since `x = 0` acts as the witness. We can directly prove this in SBV:

    >>> prove skolemEx3
    Q.E.D.

Or, we can ask if the negation is unsatisfiable:

    >>> sat (qNot skolemEx3)
    Unsatisfiable

If we want, we can skolemize after the negation step:

    >>> sat (skolemize (qNot skolemEx3))
    Unsatisfiable

and get the same result. However, it would be unsound to skolemize first and then negate:

    >>> sat (qNot (skolemize skolemEx3))
    Satisfiable. Model:
      x = 1 :: Word8

And that would be the incorrect conclusion that our formula is invalid with a counter-example! You can see the same by doing:

    >>> prove (skolemize skolemEx3)
    Falsifiable. Counter-example:
      x = 1 :: Word8

So, if you want to check validity and want to also perform skolemization; you should negate your formula first and then skolemize, not the other way around!

skolemEx4 :: IO SatResult Source #

If you skolemize different formulas that share the same name for their existentials, then SBV will get confused and will think those represent the same skolem function. This is unfortunate, but it follows the requirement that uninterpreted function names should be unique. In this particular case, however, since SBV creates these functions, it is harder to control the internal names. In such cases, use the function `taggedSkolemize` to provide a name to prefix the skolem functions. As demonstrated by `skolemEx4`. We get:

    >>> skolemEx4
    Satisfiable. Model:
      c1_y :: Integer -> Integer
      c1_y x = x

      c2_y :: Integer -> Integer
      c2_y x = 1 + x

Note how the internal skolem functions are named according to the tag given. If you use regular `skolemize` this program will essentially do the wrong thing by assuming the skolem functions for both predicates are the same, and will return unsat. Beware! All skolem functions should be named differently in your program for your deductions to be sound.

# Special relations

## Partial orders

A partial order is a reflexive, antisymmetic, and a transitive relation. We can prove these properties for relations that are checked by the `isPartialOrder` predicate in SBV:

\(\forall x\,R(x,x)\)

\(\forall x\,\forall y\, R(x, y) \land R(y, x) \Rightarrow x = y\)

\(\forall x\,\forall y\, \forall z\, R(x, y) \land R(y, z) \Rightarrow R(x, z)\)

    >>> let r         = uninterpret "R" :: Relation U
    >>> let isPartial = isPartialOrder "poR" r
    >>> prove $ \(Forall x) -> isPartial .=> r (x, x)
    Q.E.D.
    >>> prove $ \(Forall x) (Forall y) -> isPartial .=> (r (x, y) .&& r (y, x) .=> x .== y)
    Q.E.D.
    >>> prove $ \(Forall x) (Forall y) (Forall z) -> isPartial .=> (r (x, y) .&& r (y, z) .=> r (x, z))
    Q.E.D.

poExample :: IO ThmResult Source #

Demonstrates creating a partial order. We have:

    >>> poExample
    Q.E.D.

## Linear orders

A linear order, ensured by the predicate `isLinearOrder`, satisfies the following axioms:

\(\forall x\,R(x,x)\)

\(\forall x\,\forall y\, R(x, y) \land R(y, x) \Rightarrow x = y\)

\(\forall x\,\forall y\, \forall z\, R(x, y) \land R(y, z) \Rightarrow R(x, z)\)

\(\forall x\,\forall y\, R(x, y) \lor R(y, x)\)

    >>> let r        = uninterpret "R" :: Relation U
    >>> let isLinear = isLinearOrder "loR" r
    >>> prove $ \(Forall x) -> isLinear .=> r (x, x)
    Q.E.D.
    >>> prove $ \(Forall x) (Forall y) -> isLinear .=> (r (x, y) .&& r (y, x) .=> x .== y)
    Q.E.D.
    >>> prove $ \(Forall x) (Forall y) (Forall z) -> isLinear .=> (r (x, y) .&& r (y, z) .=> r (x, z))
    Q.E.D.
    >>> prove $ \(Forall x) (Forall y) -> isLinear .=> (r (x, y) .|| r (y, x))
    Q.E.D.

## Tree orders

A tree order, ensured by the predicate `isTreeOrder`, satisfies the following axioms:

\(\forall x\,R(x,x)\)

\(\forall x\,\forall y\, R(x, y) \land R(y, x) \Rightarrow x = y\)

\(\forall x\,\forall y\, \forall z\, R(x, y) \land R(y, z) \Rightarrow R(x, z)\)

\(\forall x\,\forall y\,\forall z\, (R(y, x) \land R(z, z)) \Rightarrow (R (y, z) \lor R (z, y))\)

    >>> let r      = uninterpret "R" :: Relation U
    >>> let isTree = isTreeOrder "toR" r
    >>> prove $ \(Forall x) -> isTree .=> r (x, x)
    Q.E.D.
    >>> prove $ \(Forall x) (Forall y) -> isTree .=> (r (x, y) .&& r (y, x) .=> x .== y)
    Q.E.D.
    >>> prove $ \(Forall x) (Forall y) (Forall z) -> isTree .=> (r (x, y) .&& r (y, z) .=> r (x, z))
    Q.E.D.
    >>> prove $ \(Forall x) (Forall y) (Forall z) -> isTree .=> ((r (y, x) .&& r (z, x)) .=> (r (y, z) .|| r (z, y)))
    Q.E.D.

## Piecewise linear orders

A piecewise linear order, ensured by the predicate `isPiecewiseLinearOrder`, satisfies the following axioms:

\(\forall x\,R(x,x)\)

\(\forall x\,\forall y\, R(x, y) \land R(y, x) \Rightarrow x = y\)

\(\forall x\,\forall y\, \forall z\, R(x, y) \land R(y, z) \Rightarrow R(x, z)\)

\(\forall x\,\forall y\,\forall z\, (R(x, y) \land R(x, z)) \Rightarrow (R (y, z) \lor R (z, y))\)

\(\forall x\,\forall y\,\forall z\, (R(y, x) \land R(z, x)) \Rightarrow (R (y, z) \lor R (z, y))\)

    >>> let r           = uninterpret "R" :: Relation U
    >>> let isPiecewise = isPiecewiseLinearOrder "plR" r
    >>> prove $ \(Forall x) -> isPiecewise .=> r (x, x)
    Q.E.D.
    >>> prove $ \(Forall x) (Forall y) -> isPiecewise .=> (r (x, y) .&& r (y, x) .=> x .== y)
    Q.E.D.
    >>> prove $ \(Forall x) (Forall y) (Forall z) -> isPiecewise .=> (r (x, y) .&& r (y, z) .=> r (x, z))
    Q.E.D.
    >>> prove $ \(Forall x) (Forall y) (Forall z) -> isPiecewise .=> ((r (x, y) .&& r (x, z)) .=> (r (y, z) .|| r (z, y)))
    Q.E.D.
    >>> prove $ \(Forall x) (Forall y) (Forall z) -> isPiecewise .=> ((r (y, x) .&& r (z, x)) .=> (r (y, z) .|| r (z, y)))
    Q.E.D.

## Transitive closures

The transitive closure of a relation can be created using `mkTransitiveClosure`. Transitive closures are not first-order axiomatizable. That is, we cannot write first-order formulas to uniquely describe them. However, we can check some of the expected properties:

    >>> let r   = uninterpret "R" :: Relation U
    >>> let tcR = mkTransitiveClosure "tcR" r
    >>> prove $ \(Forall x) (Forall y) -> r (x, y) .=> tcR (x, y)
    Q.E.D.
    >>> prove $ \(Forall x) (Forall y) (Forall z) -> r (x, y) .&& r (y, z) .=> tcR (x, z)
    Q.E.D.

What's missing here is the check that if the transitive closure relates two elements, then they are connected transitively in the original relation. This requirement is not axiomatizable in first order logic.

tcExample1 :: IO ThmResult Source #

Create a transitive relation of a simple relation and show that transitive connections are respected. We have:

    >>> tcExample1
    Q.E.D.

tcExample2 :: IO ThmResult Source #

Another transitive-closure example, this time we show the transitive closure is the smallest relation, i.e., doesn't have extra connections. We have:

    >>> tcExample2
    Q.E.D.

tcExample3 :: IO ThmResult Source #

Demonstrates computing the transitive closure of existing relations. We have:

    >>> tcExample3
    Q.E.D.