From 2086552f7d9da788d626dea1c737865697b958e1 Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Wed, 4 Dec 2024 03:12:30 -0800 Subject: [PATCH] some updates --- .../SBV/Examples/KnuckleDragger/FoldLaws.hs | 154 ++++++++++++++++++ .../SBV/Examples/KnuckleDragger/FoldrFoldl.hs | 88 ---------- .../KnuckleDragger/Sqrt2IsIrrational.hs | 2 +- sbv.cabal | 2 +- 4 files changed, 156 insertions(+), 90 deletions(-) create mode 100644 Documentation/SBV/Examples/KnuckleDragger/FoldLaws.hs delete mode 100644 Documentation/SBV/Examples/KnuckleDragger/FoldrFoldl.hs diff --git a/Documentation/SBV/Examples/KnuckleDragger/FoldLaws.hs b/Documentation/SBV/Examples/KnuckleDragger/FoldLaws.hs new file mode 100644 index 000000000..640103b5b --- /dev/null +++ b/Documentation/SBV/Examples/KnuckleDragger/FoldLaws.hs @@ -0,0 +1,154 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Documentation.SBV.Examples.KnuckleDragger.FoldrLaws +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer: erkokl@gmail.com +-- Stability : experimental +-- +-- Various fold related laws, inspired by Section 4.6 of Richard Bird's +-- classic book "Introduction to Functional Programming using Haskell," +-- second edition. +----------------------------------------------------------------------------- + +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeAbstractions #-} + +{-# OPTIONS_GHC -Wall -Werror #-} + +module Documentation.SBV.Examples.KnuckleDragger.FoldLaws 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 + +-- TODO: Can't converge on this either.. +-- | First duality theorem. Given: +-- +-- @ +-- x @ (y @ z) = (x @ y) @ z (associativity of @) +-- and e @ x = x (left unit) +-- and x @ e = x (right unit) +-- @ +-- +-- Prove: +-- +-- @ +-- foldr (@) e xs = foldl (@) e xs +-- @ +-- +-- We have: +-- +-- >>> firstDuality +firstDuality :: IO Proof +firstDuality = runKD $ do + let (@) :: SA -> SA -> SA + (@) = uninterpret "|@|" + + e :: SA + e = uninterpret "e" + + axm1 <- axiom "@ is associative" (\(Forall @"x" x) (Forall @"y" y) (Forall @"z" z) -> x @ (y @ z) .== (x @ y) @ z) + axm2 <- axiom "e is left unit" (\(Forall @"x" x) -> e @ x .== x) + axm3 <- axiom "e is right unit" (\(Forall @"x" x) -> x @ e .== x) + + let p xs = foldr (@) e xs .== foldl (@) e xs + + -- Helper: foldl (@) (y @ z) xs = y @ foldl (@) z xs + h <- 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] + + 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. + +-- | Given: +-- @ +-- (x <> y) @ z = x \<> (y \@ z) +-- and e \@ x = x \<> e +-- @ +-- +-- Proves: +-- +-- @ +-- foldl (\@\) e xs = foldr (\<>) e xs@ +-- @ +-- +-- 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 + h <- 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, h, induct p] +-} diff --git a/Documentation/SBV/Examples/KnuckleDragger/FoldrFoldl.hs b/Documentation/SBV/Examples/KnuckleDragger/FoldrFoldl.hs deleted file mode 100644 index 05823a892..000000000 --- a/Documentation/SBV/Examples/KnuckleDragger/FoldrFoldl.hs +++ /dev/null @@ -1,88 +0,0 @@ ------------------------------------------------------------------------------ --- | --- Module : Documentation.SBV.Examples.KnuckleDragger.FoldrFoldl --- Copyright : (c) Levent Erkok --- License : BSD3 --- Maintainer: erkokl@gmail.com --- 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 ------------------------------------------------------------------------------ - -{-# 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] diff --git a/Documentation/SBV/Examples/KnuckleDragger/Sqrt2IsIrrational.hs b/Documentation/SBV/Examples/KnuckleDragger/Sqrt2IsIrrational.hs index a6813e98b..8e165bc53 100644 --- a/Documentation/SBV/Examples/KnuckleDragger/Sqrt2IsIrrational.hs +++ b/Documentation/SBV/Examples/KnuckleDragger/Sqrt2IsIrrational.hs @@ -13,7 +13,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeAbstractions #-} -{-# OPTIONS_GHC -Wall -Werror -Wno-unused-matches #-} +{-# OPTIONS_GHC -Wall -Werror #-} module Documentation.SBV.Examples.KnuckleDragger.Sqrt2IsIrrational where diff --git a/sbv.cabal b/sbv.cabal index 3dfec21b9..45922dafe 100644 --- a/sbv.cabal +++ b/sbv.cabal @@ -160,7 +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.FoldLaws , Documentation.SBV.Examples.KnuckleDragger.Kleene , Documentation.SBV.Examples.KnuckleDragger.Induction , Documentation.SBV.Examples.KnuckleDragger.ListLen