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

Documentation.SBV.Examples.KnuckleDragger.Tao

Description

Proves a problem originating in algebra: https://mathoverflow.net/questions/450890/is-there-an-identity-between-the-commutative-identity-and-the-constant-identity/

Apparently this was 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 that op must be commutative.

Synopsis

data T
type ST = SBV T
tao :: IO Proof

Documentation

data T Source #

Create an uninterpreted type to do the proofs over.

Instances

Instances details

Data T Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Tao Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> T -> c T # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c T # toConstr :: T -> Constr # dataTypeOf :: T -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c T) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c T) # gmapT :: (forall b. Data b => b -> b) -> T -> T # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> T -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> T -> r # gmapQ :: (forall d. Data d => d -> u) -> T -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> T -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> T -> m T # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> T -> m T # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> T -> m T #
Read T Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Tao Methods readsPrec :: Int -> ReadS T # readList :: ReadS [T] # readPrec :: ReadPrec T # readListPrec :: ReadPrec [T] #
Show T Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Tao Methods showsPrec :: Int -> T -> ShowS # show :: T -> String # showList :: [T] -> ShowS #
SymVal T Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Tao Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV T) Source # literal :: T -> SBV T Source # fromCV :: CV -> T Source # isConcretely :: SBV T -> (T -> Bool) -> Bool 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 # isConcrete :: SBV T -> Bool Source # isSymbolic :: SBV T -> Bool Source #
HasKind T Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.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 # isUserSort :: T -> Bool Source # isChar :: T -> Bool Source # isString :: T -> Bool Source # isList :: T -> Bool Source # isSet :: T -> Bool Source # isTuple :: T -> Bool Source # isMaybe :: T -> Bool Source # isEither :: T -> Bool Source # isArray :: T -> Bool Source # showType :: T -> String Source #
SatModel T Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Tao Methods parseCVs :: [CV] -> Maybe (T, [CV]) Source # cvtModel :: (T -> Maybe b) -> Maybe (T, [CV]) -> Maybe (b, [CV]) Source #

type ST = SBV T Source #

Symbolic version of the type T.

tao :: IO Proof Source #

Prove that:

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

means that op is commutative.

We have:

>>> tao
Lemma: tao                              Q.E.D.
[Proven] tao