From b7246b0d6981e7d848ab35ab85d82c0bac23cf7e Mon Sep 17 00:00:00 2001
From: Levent Erkok <erkokl@gmail.com>
Date: Mon, 9 Dec 2024 18:44:13 -0800
Subject: [PATCH] bit more progress

---
 Data/SBV/SMT/SMTLib2.hs                       |  8 +++---
 .../KnuckleDragger/EquationalReasoning.hs     | 28 ++++++-------------
 2 files changed, 12 insertions(+), 24 deletions(-)

diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs
index eb9c5c2c..9be3f053 100644
--- a/Data/SBV/SMT/SMTLib2.hs
+++ b/Data/SBV/SMT/SMTLib2.hs
@@ -321,8 +321,8 @@ cvt ctx curProgInfo kindInfo isSat comments allInputs (_, consts) tbls uis defs
                  getFuncs :: Op -> Op -> Maybe (SMTLambda, SMTLambda)
                  getFuncs (SeqOp (SBVZipWith a b c f)) (SeqOp (SBVZipWith x y z g)) | [a, b, c] == [x, y, z] = Just (f, g)
                  getFuncs (SeqOp (SBVMap     a b   f)) (SeqOp (SBVMap     x y   g)) | [a, b   ] == [x, y   ] = Just (f, g)
-                 getFuncs (SeqOp (SBVFoldl   a b   f)) (SeqOp (SBVMap     x y   g)) | [a, b   ] == [x, y   ] = Just (f, g)
-                 getFuncs (SeqOp (SBVFoldr   a b   f)) (SeqOp (SBVMap     x y   g)) | [a, b   ] == [x, y   ] = Just (f, g)
+                 getFuncs (SeqOp (SBVFoldl   a b   f)) (SeqOp (SBVFoldl   x y   g)) | [a, b   ] == [x, y   ] = Just (f, g)
+                 getFuncs (SeqOp (SBVFoldr   a b   f)) (SeqOp (SBVFoldr   x y   g)) | [a, b   ] == [x, y   ] = Just (f, g)
                  getFuncs (SeqOp (SBVFilter  a     f)) (SeqOp (SBVFilter  x     g)) | [a      ] == [x      ] = Just (f, g)
                  getFuncs (SeqOp (SBVAll     a     f)) (SeqOp (SBVAll     x     g)) | [a      ] == [x      ] = Just (f, g)
                  getFuncs (SeqOp (SBVAny     a     f)) (SeqOp (SBVAny     x     g)) | [a      ] == [x      ] = Just (f, g)
@@ -340,8 +340,8 @@ cvt ctx curProgInfo kindInfo isSat comments allInputs (_, consts) tbls uis defs
 
                             paramsOf (SeqOp (SBVZipWith k1 k2 _ _)) = [("xs", KList k1), ("ys", KList k2)]
                             paramsOf (SeqOp (SBVMap     k1    _ _)) = [("xs", KList k1)]
-                            paramsOf (SeqOp (SBVFoldl   k1 _    _)) = [("xs", KList k1)]
-                            paramsOf (SeqOp (SBVFoldr   k1 _    _)) = [("xs", KList k1)]
+                            paramsOf (SeqOp (SBVFoldl   k1 k2   _)) = [("b", k2), ("xs", KList k1)]
+                            paramsOf (SeqOp (SBVFoldr   k1 k2   _)) = [("b", k2), ("xs", KList k1)]
                             paramsOf (SeqOp (SBVFilter  k1      _)) = [("xs", KList k1)]
                             paramsOf (SeqOp (SBVAll     k1      _)) = [("xs", KList k1)]
                             paramsOf (SeqOp (SBVAny     k1      _)) = [("xs", KList k1)]
diff --git a/Documentation/SBV/Examples/KnuckleDragger/EquationalReasoning.hs b/Documentation/SBV/Examples/KnuckleDragger/EquationalReasoning.hs
index 57300d87..5cbf6e9d 100644
--- a/Documentation/SBV/Examples/KnuckleDragger/EquationalReasoning.hs
+++ b/Documentation/SBV/Examples/KnuckleDragger/EquationalReasoning.hs
@@ -29,6 +29,8 @@ import Data.SBV
 import Data.SBV.List
 import Data.SBV.Tools.KnuckleDragger
 
+import Documentation.SBV.Examples.KnuckleDragger.Lists(revCons)
+
 -- | Data declaration for an uninterpreted type, usually indicating source.
 data A
 mkUninterpretedSort ''A
@@ -130,7 +132,6 @@ foldrOverAppend = runKD $ do
 
    lemma "foldrOverAppend" (\(Forall @"xs" xs) -> p xs) [induct p]
 
-{- Can't converge
 -- * Foldl over append
 
 -- | @foldl f a (xs ++ ys) == foldl f (foldl f a xs) ys@
@@ -145,20 +146,10 @@ 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)]
--}
+       p xs = quantifiedBool $ \(Forall @"a" a) (Forall @"ys" ys) -> foldl f a (xs ++ ys) .== foldl f (foldl f a xs) ys
+
+   lemma "foldlOverAppend" (\(Forall @"xs" xs) -> p xs) [induct p]
 
-{- can't converge
 -- * Foldr-foldl correspondence
 
 -- | @foldr f e xs == foldl (flip f) e (reverse xs)@
@@ -176,18 +167,15 @@ foldrFoldlReverse = runKD $ do
 
        p xs = foldr f e xs .== foldl (flip f) e (reverse xs)
 
-   rc <- use $ runKD revCons
+   rc <- use 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 xs -> [ foldr f e (x .: xs)
+                        , x `f` foldr f e xs
                         , x `f` foldl (flip f) e (reverse xs)
                         ])
               [rc, induct p]
--}
 
 {-
  --- Can't converge