From 34997824a03b51a701e63c16957f33d86c32faa5 Mon Sep 17 00:00:00 2001
From: Levent Erkok <erkokl@gmail.com>
Date: Fri, 6 Dec 2024 06:11:01 -0800
Subject: [PATCH] comments

---
 .../KnuckleDragger/EquationalReasoning.hs     | 72 +++++++++++++++++--
 1 file changed, 66 insertions(+), 6 deletions(-)

diff --git a/Documentation/SBV/Examples/KnuckleDragger/EquationalReasoning.hs b/Documentation/SBV/Examples/KnuckleDragger/EquationalReasoning.hs
index 66d461f9..6ae10159 100644
--- a/Documentation/SBV/Examples/KnuckleDragger/EquationalReasoning.hs
+++ b/Documentation/SBV/Examples/KnuckleDragger/EquationalReasoning.hs
@@ -23,12 +23,15 @@
 
 module Documentation.SBV.Examples.KnuckleDragger.EquationalReasoning where
 
-import Prelude hiding (concat, map, foldl, foldr, (<>), (++))
+import Prelude hiding (concat, map, foldl, foldr, reverse, (<>), (++))
 
 import Data.SBV
 import Data.SBV.List
 import Data.SBV.Tools.KnuckleDragger
 
+-- currently unused
+-- import Documentation.SBV.Examples.KnuckleDragger.Lists (revCons)
+
 -- | Data declaration for an uninterpreted type, usually indicating source.
 data A
 mkUninterpretedSort ''A
@@ -89,6 +92,65 @@ foldrOverAppend = runKD $ do
           -- Induction is done on the last element. Here we want to induct on xs, hence the flip below.
           [induct (flip p)]
 
+{- Can't converge
+-- * Foldl over append
+
+-- | @foldl f a (xs ++ ys) == foldl f (foldl f a xs) ys@
+--
+-- We have:
+--
+-- >>> foldlOverAppend
+-- Lemma: foldrOverAppend                  Q.E.D.
+-- [Proven] foldrOverAppend
+foldlOverAppend :: IO Proof
+foldlOverAppend = runKD $ do
+   let f :: SA -> SA -> SA
+       f = uninterpret "f"
+
+       p a xs ys = foldl f a (xs ++ ys) .== foldl f (foldl f a xs) ys
+
+   chainLemma "foldlOverAppend"
+               (\(Forall @"a" a) (Forall @"xs" xs) (Forall @"ys" ys) -> p a xs ys)
+               (\a x xs ys -> [ foldl f a ((x .: xs) ++ ys)
+                              , foldl f a (x .: (xs ++ ys))
+                              , foldl f (a `f` x) (xs ++ ys)
+                              , foldl f (foldl f (a `f` x) xs) ys
+                              ])
+               -- Induction is done on the last element. Here we want to induct on xs, hence the rearrangement below
+               [induct (flip . p)]
+-}
+
+{- can't converge
+-- * Foldr-foldl correspondence
+
+-- | @foldr f e xs == foldl (flip f) e (reverse xs)@
+--
+-- We have:
+--
+-- >> foldrFoldlReverse
+foldrFoldlReverse :: IO Proof
+foldrFoldlReverse = runKD $ do
+   let e :: SB
+       e = uninterpret "e"
+
+       f :: SA -> SB -> SB
+       f = uninterpret "f"
+
+       p xs = foldr f e xs .== foldl (flip f) e (reverse xs)
+
+   rc <- use $ runKD revCons
+
+   chainLemma "foldrFoldlDuality"
+              (\(Forall @"xs" xs) -> p xs)
+              (\x xs -> [ -- foldr f e (x .: xs)
+                        -- , x `f` foldr f e xs
+                          foldl (flip f) e (reverse (x .: xs))
+                        , foldl (flip f) e (reverse xs ++ singleton x)
+                        , x `f` foldl (flip f) e (reverse xs)
+                        ])
+              [rc, induct p]
+-}
+
 {-
  --- Can't converge
 -- * Bookkeeping law
@@ -131,9 +193,7 @@ bookKeeping = runKD $ do
               [assoc, unit, foa, induct p]
 -}
 
-{---------------------
- --- Can't converge
-
+{- no convergence
 -- | Fusion for foldr:
 --
 -- @
@@ -166,10 +226,10 @@ foldrFusion = runKD $ do
    -- f a == b
    h1 <- axiom "f a == b" $ f a .== b
 
-   -- forall x, y: f (g x) = h x (f y)
+   -- forall x, y: f (g x y) = h x (f y)
    h2 <- axiom "f (g x) = h x (f y)" $ \(Forall @"x" x) (Forall @"y" y) -> f (g x y) .== h x (f y)
 
-   chainLemmaWith z3{transcript = Just "bad.smt2"} "foldrFusion"
+   chainLemma "foldrFusion"
               (\(Forall @"xs" xs) -> p xs)
               (\x xs -> [ f (foldr g a (x .: xs))
                         , f (g x (foldr g a xs))