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

Documentation.SBV.Examples.TP.Tao

Description

A question posed by Terrence Tao: https://mathstodon.xyz/@tao/110736805384878353. Essentially, for an arbitrary binary operation op, we prove that

   (x op x) op y == y op x

Implies op must be commutative.

Synopsis

data T
cv2T :: String -> [CV] -> T
_undefiner_T :: a
type ST = SBV T
tao :: SymVal a => (SBV a -> SBV a -> SBV a) -> IO (Proof SBool)

Documentation

data T Source #

Create an uninterpreted type to do the proofs over.

Instances

Instances details

Arbitrary T Source #
Instance details Defined in Documentation.SBV.Examples.TP.Tao Methods arbitrary :: Gen T # shrink :: T -> [T] #
SymVal T Source #
Instance details Defined in Documentation.SBV.Examples.TP.Tao Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV T) Source # mkSymValInit :: State -> SBV T -> IO () Source # literal :: T -> SBV T Source # fromCV :: CV -> T Source # isConcretely :: SBV T -> (T -> Bool) -> Bool Source # minMaxBound :: Maybe (T, T) Source # free :: MonadSymbolic m => String -> m (SBV T) Source # free_ :: MonadSymbolic m => m (SBV T) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV T] Source # symbolic :: MonadSymbolic m => String -> m (SBV T) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV T] Source # unliteral :: SBV T -> Maybe T Source # unlitCV :: SBV T -> Maybe (Kind, CVal) Source # isConcrete :: SBV T -> Bool Source # isSymbolic :: SBV T -> Bool Source #
HasKind T Source #
Instance details Defined in Documentation.SBV.Examples.TP.Tao Methods kindOf :: T -> Kind Source # hasSign :: T -> Bool Source # intSizeOf :: T -> Int Source # isBoolean :: T -> Bool Source # isBounded :: T -> Bool Source # isReal :: T -> Bool Source # isFloat :: T -> Bool Source # isDouble :: T -> Bool Source # isRational :: T -> Bool Source # isFP :: T -> Bool Source # isUnbounded :: T -> Bool Source # isADT :: T -> Bool Source # isChar :: T -> Bool Source # isString :: T -> Bool Source # isList :: T -> Bool Source # isSet :: T -> Bool Source # isTuple :: T -> Bool Source # isArray :: T -> Bool Source # isRoundingMode :: T -> Bool Source # isUninterpreted :: T -> Bool Source # showType :: T -> String Source #

cv2T :: String -> [CV] -> T Source #

Conversion from SMT values to T values.

_undefiner_T :: a Source #

Autogenerated definition to avoid unused-variable warnings from GHC.

type ST = SBV T Source #

Symbolic version of the type T.

tao :: SymVal a => (SBV a -> SBV a -> SBV a) -> IO (Proof SBool) Source #

Prove that:

   (x op x) op y == y op x

means that op is commutative.

We have:

>>> tao @T (uninterpret "op")
Lemma: tao                              Q.E.D.
[Proven] tao :: Bool