-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.KnuckleDragger.Tao
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- 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.
-----------------------------------------------------------------------------


{-# LANGUAGE DeriveAnyClass     #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DataKinds          #-}
{-# LANGUAGE TypeAbstractions   #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell    #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.KnuckleDragger.Tao where

import Data.SBV
import Data.SBV.Tools.KnuckleDragger

-- | Create an uninterpreted type to do the proofs over.
data T
mkUninterpretedSort ''T

-- | 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
tao :: IO Proof
tao :: IO Proof
tao = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do
   let op :: ST -> ST -> ST
       op :: ST -> ST -> ST
op = String -> ST -> ST -> ST
forall a. SMTDefinable a => String -> a
uninterpret String
"op"

   String -> SBool -> [Proof] -> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"tao" (    (Forall "x" T -> Forall "y" T -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall @"x" ST
x) (Forall @"y" ST
y) -> ((ST
x ST -> ST -> ST
`op` ST
x) ST -> ST -> ST
`op` ST
y) ST -> ST -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== ST
y ST -> ST -> ST
`op` ST
x)
                SBool -> SBool -> SBool
.=> (Forall "x" T -> Forall "y" T -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall @"x" ST
x) (Forall @"y" ST
y) -> (ST
x ST -> ST -> ST
`op` ST
y) ST -> ST -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (ST
y ST -> ST -> ST
`op` ST
x)))
               []