From cc2e013d50bf7ad7fb794c18182807d5016fa7ae Mon Sep 17 00:00:00 2001
From: Levent Erkok <erkokl@gmail.com>
Date: Mon, 7 Oct 2024 11:55:58 -0700
Subject: [PATCH] add the Tao example

---
 .../SBV/Examples/KnuckleDragger/Tao.hs        | 62 +++++++++++++++++++
 sbv.cabal                                     |  1 +
 2 files changed, 63 insertions(+)
 create mode 100644 Documentation/SBV/Examples/KnuckleDragger/Tao.hs

diff --git a/Documentation/SBV/Examples/KnuckleDragger/Tao.hs b/Documentation/SBV/Examples/KnuckleDragger/Tao.hs
new file mode 100644
index 00000000..3152ae7a
--- /dev/null
+++ b/Documentation/SBV/Examples/KnuckleDragger/Tao.hs
@@ -0,0 +1,62 @@
+-----------------------------------------------------------------------------
+-- |
+-- 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 = runKD $ do
+   let op :: ST -> ST -> ST
+       op = uninterpret "op"
+
+   lemma "tao" (    quantifiedBool (\(Forall @"x" x) (Forall @"y" y) -> ((x `op` x) `op` y) .== y `op` x)
+                .=> quantifiedBool (\(Forall @"x" x) (Forall @"y" y) -> (x `op` y) .== (y `op` x)))
+               []
diff --git a/sbv.cabal b/sbv.cabal
index 0408fd5b..1c05c0bc 100644
--- a/sbv.cabal
+++ b/sbv.cabal
@@ -162,6 +162,7 @@ Library
                   , Documentation.SBV.Examples.KnuckleDragger.ListLen
                   , Documentation.SBV.Examples.KnuckleDragger.RevLen
                   , Documentation.SBV.Examples.KnuckleDragger.Sqrt2IsIrrational
+                  , Documentation.SBV.Examples.KnuckleDragger.Tao
                   , Documentation.SBV.Examples.Misc.Definitions
                   , Documentation.SBV.Examples.Misc.Enumerate
                   , Documentation.SBV.Examples.Misc.FirstOrderLogic