An attempt at proving foldr-foldl equivalence

Not converging

Documentation/SBV/Examples/KnuckleDragger/FoldrFoldl.hs

@@ -0,0 +1,88 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module    : Documentation.SBV.Examples.KnuckleDragger.FoldrFoldl
+-- Copyright : (c) Levent Erkok
+-- License   : BSD3
+-- Maintainer: [email protected]
+-- Stability : experimental
+--
+-- Proves the equality @foldl (\@\) e xs = foldr (\<>) e xs@
+-- Given @(x \<> y) \@ z = x \<> (y \@ z)@ and @e \@ x = x \<> e@.
+--
+-- Inspired by <https://stackoverflow.com/questions/79037764/substitution-in-proofs-with-recursive-formulas>
+-----------------------------------------------------------------------------
+
+{-# LANGUAGE CPP                 #-}
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE DeriveAnyClass      #-}
+{-# LANGUAGE DeriveDataTypeable  #-}
+{-# LANGUAGE StandaloneDeriving  #-}
+{-# LANGUAGE TemplateHaskell     #-}
+{-# LANGUAGE TypeAbstractions    #-}
+
+{-# OPTIONS_GHC -Wall -Werror -Wno-unused-do-bind #-}
+
+module Documentation.SBV.Examples.KnuckleDragger.FoldrFoldl where
+
+import Prelude hiding (foldl, foldr, (<>))
+
+import Data.SBV
+import Data.SBV.List
+import Data.SBV.Tools.KnuckleDragger
+
+-- | Data declaration for an uninterpreted source type.
+data A
+mkUninterpretedSort ''A
+
+-- | Data declaration for an uninterpreted target type.
+data B
+mkUninterpretedSort ''B
+
+-- | We have:
+--
+-- >>> foldrFoldl
+foldrFoldl :: IO Proof
+foldrFoldl = runKD $ do
+
+   let -- Declare the operators as uninterpreted functions
+       (@) :: SB -> SA -> SB
+       (@) = uninterpret "|@|"
+
+       (<>) :: SA -> SB -> SB
+       (<>) = uninterpret "|<>|"
+
+       -- The unit element
+       e :: SB
+       e = uninterpret "e"
+
+       -- Equivalence predicate
+       p :: SList A -> SBool
+       p xs = foldl (@) e xs .== foldr (<>) e xs
+
+
+   -- Assumptions about the operators
+
+   -- (x <> y) @ z == x <> (y @ z)
+   axm1 <- axiom "<> over @" $ \(Forall @"x" x) (Forall @"y" y) (Forall @"z" z)
+                                  -> (x <> y) @ z .== x <> (y @ z)
+
+   -- e @ x == x <> e
+   axm2 <- axiom "unit" $ \(Forall @"x" x) -> e @ x .== x <> e
+
+   -- Helper: foldl (@) (y <> z) xs = y <> foldl (@) z xs
+   h1 <- do
+      let hp y z xs = foldl (@) (y <> z) xs .== y <> foldl (@) z xs
+
+      chainLemma "foldl over @"
+                 (\(Forall @"y" y) (Forall @"z" z) (Forall @"xs" xs) -> hp y z xs)
+                 (\y z x xs -> [ foldl (@) (y <> z) (x .: xs)
+                               , foldl (@) ((y <> z) @ x) xs
+                               , foldl (@) (y <> (z @ x)) xs
+                               -- this transition is hard
+                               , y <> foldl (@) (z @ x) xs
+                               , y <> foldl (@) z (x .: xs)
+                               ])
+                 [axm1, axm2, induct hp]
+
+   -- Final proof:
+   lemma "foldrFoldl" (\(Forall @"xs" xs) -> p xs) [axm1, axm2, h1, induct p]

sbv.cabal

@@ -160,6 +160,7 @@ Library
                   , Documentation.SBV.Examples.KnuckleDragger.AppendRev
                   , Documentation.SBV.Examples.KnuckleDragger.Basics
                   , Documentation.SBV.Examples.KnuckleDragger.CaseSplit
+                  , Documentation.SBV.Examples.KnuckleDragger.FoldrFoldl
                   , Documentation.SBV.Examples.KnuckleDragger.Kleene
                   , Documentation.SBV.Examples.KnuckleDragger.Induction
                   , Documentation.SBV.Examples.KnuckleDragger.ListLen