From df6be03150edd702aebdc265d1ac883c09da28c9 Mon Sep 17 00:00:00 2001
From: Levent Erkok <erkokl@gmail.com>
Date: Thu, 5 Dec 2024 16:44:06 -0800
Subject: [PATCH] KD: foldr over append

---
 .../KnuckleDragger/EquationalReasoning.hs     | 57 ++++++++++++++++++-
 1 file changed, 55 insertions(+), 2 deletions(-)

diff --git a/Documentation/SBV/Examples/KnuckleDragger/EquationalReasoning.hs b/Documentation/SBV/Examples/KnuckleDragger/EquationalReasoning.hs
index b8054df2..bcc62f4e 100644
--- a/Documentation/SBV/Examples/KnuckleDragger/EquationalReasoning.hs
+++ b/Documentation/SBV/Examples/KnuckleDragger/EquationalReasoning.hs
@@ -23,7 +23,7 @@
 
 module Documentation.SBV.Examples.KnuckleDragger.EquationalReasoning where
 
-import Prelude hiding (map, foldl, foldr, (<>))
+import Prelude hiding (concat, map, foldl, foldr, (<>), (++))
 
 import Data.SBV
 import Data.SBV.List
@@ -65,6 +65,60 @@ foldMapFusion = runKD $ do
 
   lemma "foldMapFusion" (\(Forall @"xs" xs) -> p xs) [induct p]
 
+-- * Foldr over append
+
+-- | @foldr f a (xs ++ ys) == foldr f (foldr f a ys) xs@
+--
+-- We have:
+--
+-- >>> foldrOverAppend
+-- Lemma: foldrOverAppend                  Q.E.D.
+-- [Proven] foldrOverAppend
+foldrOverAppend :: IO Proof
+foldrOverAppend = runKD $ do
+   let a :: SA
+       a = uninterpret "a"
+
+       f :: SA -> SA -> SA
+       f = uninterpret "f"
+
+       p xs ys = foldr f a (xs ++ ys) .== foldr f (foldr f a ys) xs
+
+   lemma "foldrOverAppend"
+          (\(Forall @"xs" xs) (Forall @"ys" ys) -> p xs ys)
+          -- Induction is done on the last element. Here we want to induct on xs, hence the flip below.
+          [induct (flip p)]
+
+{-
+-- * Bookkeeping law
+
+-- | @foldr f a . concat == foldr f a . map (foldr f a)@, provided @f@ is associative and @a@ is its
+-- left-unit.
+--
+-- We have:
+--
+-- >>> bookKeeping
+bookKeeping :: IO Proof
+bookKeeping = runKD $ do
+   let a :: SA
+       a = uninterpret "a"
+
+       f :: SA -> SA -> SA
+       f = uninterpret "f"
+
+       p xss = foldr f a (concat xss) .== foldr f a (map (foldr f a) xss)
+
+   assoc <- axiom "f is associative" (\(Forall @"x" x) (Forall @"y" y) (Forall @"z" z) -> x `f` (y `f` z) .== (x `f` y) `f` z)
+   unit  <- axiom "a is left-unit"   (\(Forall @"x" x) -> a `f` x .== x)
+
+   chainLemma "bookKeeping"
+              (\(Forall @"xss" xss) -> p xss)
+              (\xs xss -> [ foldr f a (concat (xs .: xss))
+                        , foldr f a (xs ++ concat xss)
+                        , foldr f (foldr f a (concat xss)) xs
+                        ])
+              [assoc, unit, induct p]
+-}
 
 {---------------------
  --- Can't converge
@@ -166,7 +220,6 @@ firstDuality  = runKD $ do
    lemma "firstDuality" (\(Forall @"xs" xs) -> p xs) [axm1, axm2, axm3, h, induct p]
 -}
 
-----------------------------------------------------------------------------------------
 {- TODO: Can't converge on this one. The strengthened induction axiom requires a very careful
    instantiation of the inductive hypothesis, which I can't get through. Perhaps we need proper
    support for patterns.