Error: Parse error: Unsupported extension: TypeAbstractions ▫︎ Found: "-----------------------------------------------------------------------------\n-- |\n-- Module : Data.SBV.Tools.KnuckleDragger\n-- Copyright : (c) Levent Erkok\n-- License : BSD3\n-- Maintainer: [email protected]\n-- Stability : experimental\n--\n-- A lightweight theorem proving like interface, built on top of SBV.\n-- Inspired by and modeled after Philip Zucker's tool with the same\n-- name, see <http://github.com/philzook58/knuckledragger>.\n--\n-- See the directory Documentation.SBV.Examples.KnuckleDragger for various examples.\n-----------------------------------------------------------------------------\n\n{-# LANGUAGE ConstraintKinds #-}\n{-# LANGUAGE DataKinds #-}\n{-# LANGUAGE DerivingStrategies #-}\n{-# LANGUAGE FlexibleContexts #-}\n{-# LANGUAGE FlexibleInstances #-}\n{-# LANGUAGE FunctionalDependencies #-}\n{-# LANGUAGE GeneralizedNewtypeDeriving #-}\n{-# LANGUAGE MultiParamTypeClasses #-}\n{-# LANGUAGE NamedFieldPuns #-}\n{-# LANGUAGE TypeAbstractions #-}\n\n{-# OPTIONS_GHC -Wall -Werror #-}\n\nmodule Data.SBV.Tools.KnuckleDragger (\n -- * Propositions and their proofs\n Proposition, Proof\n -- * Adding axioms/definitions\n , axiom\n -- * Basic proofs\n , lemma, lemmaWith\n , theorem, theoremWith\n -- * Chain of reasoning\n , chainLemma, chainLemmaWith\n , chainTheorem, chainTheoremWith\n -- * Induction\n , Induction(..)\n -- * Faking proofs\n , sorry\n -- * Running KnuckleDragger proofs\n , KD, runKD, runKDWith, use\n ) where\n\nimport Data.SBV\nimport Data.SBV.Tools.KDKernel\nimport Data.SBV.Tools.KDUtils\n\nimport Control.Monad (when)\nimport Control.Monad.Trans (liftIO)\nimport Control.Monad.Reader (ask)\n\n-- | Bring an IO proof into current proof context.\nuse :: IO Proof -> KD Proof\nuse = liftIO\n\n-- | A class for doing equational reasoning style chained proofs. Use 'chainLemma' to prove a given theorem\n-- as a sequence of equalities, each step following from the previous.\nclass ChainLemma steps step | steps -> step where\n\n -- | Prove a property via a series of equality steps, using the default solver.\n -- Let @h@ be a list of already established lemmas. Let @p@ be a property we wanted to prove, named @name@.\n -- Consider a call of the form @chainLemma name P [A, B, C, D] H@. Note that @h@ is\n -- a list of already proven facts, ensured by the type signature. We proceed as follows:\n --\n -- * Prove: @h -> A == B@\n -- * Prove: @h && A == B -> B == C@\n -- * Prove: @h && A == B && B == C -> C == D@\n -- * Prove: @h && A == B && B == C && C == D -> P@\n -- * If all of the above steps succeed, conclude @p@.\n --\n -- Note that if the type of steps (i.e., @A@ .. @d@ above) is 'SBool', then we use implication\n -- as opposed to equality; which better captures line of reasoning.\n --\n -- So, chain-lemma is essentially modus-ponens, applied in a sequence of stepwise equality reasoning in the case of\n -- non-boolean steps.\n --\n -- If there are no helpers given (i.e., if @h@ is empty), then this call is equivalent to 'lemmaWith'.\n -- If @h@ is a singleton, then we error-out. A single step in @h@ indicates a user-error, since there's\n -- no sequence of steps to reason about.\n chainLemma :: Proposition a => String -> a -> steps -> [Proof] -> KD Proof\n\n -- | Same as chainLemma, except tagged as Theorem\n chainTheorem :: Proposition a => String -> a -> steps -> [Proof] -> KD Proof\n\n -- | Prove a property via a series of equality steps, using the given solver.\n chainLemmaWith :: Proposition a => SMTConfig -> String -> a -> steps -> [Proof] -> KD Proof\n\n -- | Same as chainLemmaWith, except tagged as Theorem\n chainTheoremWith :: Proposition a => SMTConfig -> String -> a -> steps -> [Proof] -> KD Proof\n\n -- | Internal, shouldn't be needed outside the library\n makeSteps :: steps -> [step]\n makeInter :: steps -> step -> step -> SBool\n\n chainLemma nm p steps by = do cfg <- ask\n chainLemmaWith cfg nm p steps by\n\n chainTheorem nm p steps by = do cfg <- ask\n chainTheoremWith cfg nm p steps by\n\n chainLemmaWith = chainGene

Error: Parse error: Unsupported extension: TypeAbstractions ▫︎ Found: "-----------------------------------------------------------------------------\n-- |\n-- Module : Documentation.SBV.Examples.KnuckleDragger.AppendRev\n-- Copyright : (c) Levent Erkok\n-- License : BSD3\n-- Maintainer: [email protected]\n-- Stability : experimental\n--\n-- Example use of the KnuckleDragger, on list append and reverses.\n-----------------------------------------------------------------------------\n\n{-# LANGUAGE DataKinds #-}\n{-# LANGUAGE DeriveAnyClass #-}\n{-# LANGUAGE DeriveDataTypeable #-}\n{-# LANGUAGE ScopedTypeVariables #-}\n{-# LANGUAGE StandaloneDeriving #-}\n{-# LANGUAGE TemplateHaskell #-}\n{-# LANGUAGE TypeAbstractions #-}\n{-# LANGUAGE TypeApplications #-}\n\n{-# OPTIONS_GHC -Wall -Werror #-}\n\nmodule Documentation.SBV.Examples.KnuckleDragger.AppendRev where\n\nimport Prelude hiding (reverse, (++))\n\nimport Data.SBV\nimport Data.SBV.Tools.KnuckleDragger\n\nimport Data.SBV.List ((.:), (++), reverse)\nimport qualified Data.SBV.List as SL\n\n-- | Use an uninterpreted type for the elements\ndata Elt\nmkUninterpretedSort ''Elt\n\n-- | @xs ++ [] == xs@\n--\n-- We have:\n--\n-- >>> appendNull\n-- Lemma: appendNull Q.E.D.\n-- [Proven] appendNull\nappendNull :: IO Proof\nappendNull = runKD $ lemma \"appendNull\"\n (\\(Forall @\"xs\" (xs :: SList Elt)) -> xs ++ SL.nil .== xs)\n []\n\n-- | @(x : xs) ++ ys == x : (xs ++ ys)@\n--\n-- We have:\n--\n-- >>> consApp\n-- Lemma: consApp Q.E.D.\n-- [Proven] consApp\nconsApp :: IO Proof\nconsApp = runKD $ lemma \"consApp\"\n (\\(Forall @\"x\" (x :: SElt)) (Forall @\"xs\" xs) (Forall @\"ys\" ys) -> (x .: xs) ++ ys .== x .: (xs ++ ys))\n []\n\n-- | @(xs ++ ys) ++ zs == xs ++ (ys ++ zs)@\n--\n-- We have:\n--\n-- >>> appendAssoc\n-- Lemma: appendAssoc Q.E.D.\n-- [Proven] appendAssoc\nappendAssoc :: IO Proof\nappendAssoc = runKD $ do\n let p :: SymVal a => SList a -> SList a -> SList a -> SBool\n p xs ys zs = xs ++ (ys ++ zs) .== (xs ++ ys) ++ zs\n\n lemma \"appendAssoc\"\n (\\(Forall @\"xs\" (xs :: SList Elt)) (Forall @\"ys\" ys) (Forall @\"zs\" zs) -> p xs ys zs)\n []\n\n-- | @reverse (reverse xs) == xs@\n--\n-- We have:\n--\n-- >>> reverseReverse\n-- Lemma: revApp Q.E.D.\n-- Lemma: reverseReverse Q.E.D.\n-- [Proven] reverseReverse\nreverseReverse :: IO Proof\nreverseReverse = runKD $ do\n\n -- Helper lemma: @reverse (xs ++ ys) .== reverse ys ++ reverse xs@\n let ra :: SymVal a => SList a -> SList a -> SBool\n ra xs ys = reverse (xs ++ ys) .== reverse ys ++ reverse xs\n\n revApp <- lemma \"revApp\" (\\(Forall @\"xs\" (xs :: SList Elt)) (Forall @\"ys\" ys) -> ra xs ys)\n -- induction is always done on the last argument, so flip to make sure we induct on xs\n [induct (flip (ra @elt))]\n\n let p :: SymVal a => SList a -> SBool\n p xs = reverse (reverse xs) .== xs\n\n lemma \"reverseReverse\"\n (\\(Forall @\"xs\" (xs :: SList Elt)) -> p xs)\n [induct (p @elt), revApp]\n"

Error: Parse error: Unsupported extension: TypeAbstractions ▫︎ Found: "-----------------------------------------------------------------------------\n-- |\n-- Module : Documentation.SBV.Examples.KnuckleDragger.Basics\n-- Copyright : (c) Levent Erkok\n-- License : BSD3\n-- Maintainer: [email protected]\n-- Stability : experimental\n--\n-- Some basic KD usage.\n-----------------------------------------------------------------------------\n\n{-# LANGUAGE CPP #-}\n{-# LANGUAGE DataKinds #-}\n{-# LANGUAGE DeriveAnyClass #-}\n{-# LANGUAGE DeriveDataTypeable #-}\n{-# LANGUAGE TemplateHaskell #-}\n{-# LANGUAGE TypeAbstractions #-}\n{-# LANGUAGE StandaloneDeriving #-}\n\n{-# OPTIONS_GHC -Wall -Werror #-}\n\nmodule Documentation.SBV.Examples.KnuckleDragger.Basics where\n\nimport Data.SBV\nimport Data.SBV.Tools.KnuckleDragger\n\n\n-- $setup\n-- >>> -- For doctest purposes only:\n-- >>> :set -XScopedTypeVariables\n-- >>> import Control.Exception\n\n\n-- | @strue@ is provable.\n--\n-- We have:\n--\n-- >>> trueIsProvable\n-- Lemma: true Q.E.D.\n-- [Proven] true\ntrueIsProvable :: IO Proof\ntrueIsProvable = runKD $ lemma \"true\" sTrue []\n\n-- | @sFalse@ isn't provable.\n--\n-- We have:\n--\n-- >>> falseIsn'tProvable `catch` (\\(_ :: SomeException) -> pure ())\n-- Lemma: sFalse\n-- *** Failed to prove sFalse.\n-- Falsifiable\nfalseIsn'tProvable :: IO ()\nfalseIsn'tProvable = runKD $ do\n _won'tGoThrough <- lemma \"sFalse\" sFalse []\n pure ()\n\n-- | Basic quantification example: For every integer, there's a larger integer.\n--\n-- We have:\n-- >>> largerIntegerExists\n-- Lemma: largerIntegerExists Q.E.D.\n-- [Proven] largerIntegerExists\nlargerIntegerExists :: IO Proof\nlargerIntegerExists = runKD $ lemma \"largerIntegerExists\"\n (\\(Forall @\"x\" x) (Exists @\"y\" y) -> x .< (y :: SInteger))\n []\n\n-- | Use an uninterpreted type for the domain\ndata T\nmkUninterpretedSort ''T\n\n-- | Pushing a universal through conjunction. We have:\n--\n-- >>> forallConjunction\n-- Lemma: forallConjunction Q.E.D.\n-- [Proven] forallConjunction\nforallConjunction :: IO Proof\nforallConjunction = runKD $ do\n let p, q :: ST -> SBool\n p = uninterpret \"p\"\n q = uninterpret \"q\"\n\n qb = quantifiedBool\n\n lemma \"forallConjunction\"\n ( (qb (\\(Forall @\"x\" x) -> p x) .&& qb (\\(Forall @\"x\" x) -> q x))\n .<=> -----------------------------------------------------------------\n qb (\\(Forall @\"x\" x) -> p x .&& q x)\n )\n []\n\n-- | Pushing an existential through disjunction. We have:\n--\n-- >>> existsDisjunction\n-- Lemma: existsDisjunction Q.E.D.\n-- [Proven] existsDisjunction\nexistsDisjunction :: IO Proof\nexistsDisjunction = runKD $ do\n let p, q :: ST -> SBool\n p = uninterpret \"p\"\n q = uninterpret \"q\"\n\n qb = quantifiedBool\n\n lemma \"existsDisjunction\"\n ( (qb (\\(Exists @\"x\" x) -> p x) .|| qb (\\(Exists @\"x\" x) -> q x))\n .<=> -----------------------------------------------------------------\n qb (\\(Exists @\"x\" x) -> p x .|| q x)\n )\n []\n\n-- | We cannot push a universal through a disjunction. We have:\n--\n-- >>> forallDisjunctionNot `catch` (\\(_ :: SomeException) -> pure ())\n-- Lemma: forallConjunctionNot\n-- *** Failed to prove forallConjunctionNot.\n-- Falsifiable. Counter-example:\n-- p :: T -> Bool\n-- p T_2 = True\n-- p T_0 = True\n-- p _ = False\n-- <BLANKLINE>\n-- q :: T -> Bool\n-- q T_2 = False\n-- q T_0 = False\n-- q _ = True\n--\n-- Note how @p@ assigns two selected values to @true@ and everything else to @false@, while @q@ does the exact opposite.\n-- So, there is no common value that satisfies both, providing a counter-example. (It's not clear why the solver finds\n-- a model with two distinct values, as one would have sufficed. But it is still a valud model.)\nforallDisjunctionNot :: IO ()\nforallDisjunctionNot = runKD $ do\n let p, q :: ST -> SBool\n p = uninterpret \"p\"\n q = uninterpret \"q\"\n\n qb = quantifiedBool\n\n -- This won't prove!\n _won'tGoThrough <- lemma \"forallConjunctionNot\"\n ( (qb (\\(Forall @\"x\" x) -> p x) .|| qb (\\(Forall @\"x\" x) -> q x))\n .<=> --------------------------

Error: Parse error: Unsupported extension: TypeAbstractions ▫︎ Found: "-----------------------------------------------------------------------------\n-- |\n-- Module : Documentation.SBV.Examples.KnuckleDragger.CaseSplit\n-- Copyright : (c) Levent Erkok\n-- License : BSD3\n-- Maintainer: [email protected]\n-- Stability : experimental\n--\n-- Use KnuckleDragger to prove @2n^2 + n + 1@ is never divisible by @3@.\n-----------------------------------------------------------------------------\n\n{-# LANGUAGE DataKinds #-}\n{-# LANGUAGE TypeAbstractions #-}\n\n{-# OPTIONS_GHC -Wall -Werror #-}\n\nmodule Documentation.SBV.Examples.KnuckleDragger.CaseSplit where\n\nimport Prelude hiding (sum, length)\n\nimport Data.SBV\nimport Data.SBV.Tools.KnuckleDragger\n\n-- | The default settings for z3 have trouble running this proof out-of-the-box.\n-- We have to pass auto_config=false to z3!\nz3NoAutoConfig :: SMTConfig\nz3NoAutoConfig = z3{extraArgs = [\"auto_config=false\"]}\n\n-- | Prove that @2n^2 + n + 1@ is not divisible by @3@.\n--\n-- We have:\n--\n-- >>> notDiv3\n-- Chain: case_n_mod_3_eq_0\n-- Lemma: case_n_mod_3_eq_0.1 Q.E.D.\n-- Lemma: case_n_mod_3_eq_0.2 Q.E.D.\n-- Lemma: case_n_mod_3_eq_0 Q.E.D.\n-- Chain: case_n_mod_3_eq_1\n-- Lemma: case_n_mod_3_eq_1.1 Q.E.D.\n-- Lemma: case_n_mod_3_eq_1.2 Q.E.D.\n-- Lemma: case_n_mod_3_eq_1 Q.E.D.\n-- Chain: case_n_mod_3_eq_2\n-- Lemma: case_n_mod_3_eq_2.1 Q.E.D.\n-- Lemma: case_n_mod_3_eq_2.2 Q.E.D.\n-- Lemma: case_n_mod_3_eq_2 Q.E.D.\n-- Lemma: notDiv3 Q.E.D.\n-- [Proven] notDiv3\nnotDiv3 :: IO Proof\nnotDiv3 = runKDWith z3NoAutoConfig $ do\n\n let s n = 2 * n * n + n + 1\n p n = s n `sEMod` 3 ./= 0\n\n -- Do the proof in 3 phases; one each for the possible value of n `mod` 3 being 0, 1, and 2\n -- Note that we use the euclidian definition of division/modulus.\n\n -- Case 0: n = 0 (mod 3)\n case0 <- chainLemma \"case_n_mod_3_eq_0\"\n (\\(Forall @\"n\" n) -> (n `sEMod` 3 .== 0) .=> p n)\n (\\n -> let k = n `sEDiv` 3\n in [ n `sEMod` 3 .== 0\n , n .== 3 * k\n , s n .== s (3 * k)\n ])\n []\n\n -- Case 1: n = 1 (mod 3)\n case1 <- chainLemma \"case_n_mod_3_eq_1\"\n (\\(Forall @\"n\" n) -> (n `sEMod` 3 .== 1) .=> p n)\n (\\n -> let k = n `sEDiv` 3\n in [ n `sEMod` 3 .== 1\n , n .== 3 * k + 1\n , s n .== s (3 * k + 1)\n ])\n []\n\n -- Case 2: n = 2 (mod 3)\n case2 <- chainLemma \"case_n_mod_3_eq_2\"\n (\\(Forall @\"n\" n) -> (n `sEMod` 3 .== 2) .=> p n)\n (\\n -> let k = n `sEDiv` 3\n in [ n `sEMod` 3 .== 2\n , n .== 3 * k + 2\n , s n .== s (3 * k + 2)\n ])\n []\n\n -- Note that z3 is smart enough to figure out the above cases are complete, so\n -- no extra completeness helper is needed.\n lemma \"notDiv3\"\n (\\(Forall @\"n\" n) -> p n)\n [case0, case1, case2]\n"

Error: Parse error: Unsupported extension: TypeAbstractions ▫︎ Found: "-----------------------------------------------------------------------------\n-- |\n-- Module : Documentation.SBV.Examples.KnuckleDragger.EquationalReasoning\n-- Copyright : (c) Levent Erkok\n-- License : BSD3\n-- Maintainer: [email protected]\n-- Stability : experimental\n--\n-- Various equalities that arise in functional-programming. A good source\n-- is the classic book \"Introduction to Functional Programming using Haskell,\"\n-- second edition. (Section 4.6 and others.)\n-----------------------------------------------------------------------------\n\n{-# LANGUAGE CPP #-}\n{-# LANGUAGE DataKinds #-}\n{-# LANGUAGE DeriveAnyClass #-}\n{-# LANGUAGE DeriveDataTypeable #-}\n{-# LANGUAGE StandaloneDeriving #-}\n{-# LANGUAGE TemplateHaskell #-}\n{-# LANGUAGE TypeAbstractions #-}\n\n{-# OPTIONS_GHC -Wall -Werror #-}\n\nmodule Documentation.SBV.Examples.KnuckleDragger.EquationalReasoning where\n\nimport Prelude hiding (concat, map, foldl, foldr, (<>), (++))\n\nimport Data.SBV\nimport Data.SBV.List\nimport Data.SBV.Tools.KnuckleDragger\n\n-- | Data declaration for an uninterpreted type, usually indicating source.\ndata A\nmkUninterpretedSort ''A\n\n-- | Data declaration for an uninterpreted type, usually indicating target.\ndata B\nmkUninterpretedSort ''B\n\n-- | Data declaration for an uninterpreted type, usually indicating an intermediate value.\ndata C\nmkUninterpretedSort ''C\n\n-- * Fold-map fusion\n\n-- | @foldr f a . map g = foldr (f . g) a@\n--\n-- We have:\n--\n-- >>> foldMapFusion\n-- Lemma: foldMapFusion Q.E.D.\n-- [Proven] foldMapFusion\nfoldMapFusion :: IO Proof\nfoldMapFusion = runKD $ do\n let a :: SA\n a = uninterpret \"a\"\n\n g :: SC -> SB\n g = uninterpret \"g\"\n\n f :: SB -> SA -> SA\n f = uninterpret \"f\"\n\n p xs = foldr f a (map g xs) .== foldr (f . g) a xs\n\n lemma \"foldMapFusion\" (\\(Forall @\"xs\" xs) -> p xs) [induct p]\n\n-- * Foldr over append\n\n-- | @foldr f a (xs ++ ys) == foldr f (foldr f a ys) xs@\n--\n-- We have:\n--\n-- >>> foldrOverAppend\n-- Lemma: foldrOverAppend Q.E.D.\n-- [Proven] foldrOverAppend\nfoldrOverAppend :: IO Proof\nfoldrOverAppend = runKD $ do\n let a :: SA\n a = uninterpret \"a\"\n\n f :: SA -> SA -> SA\n f = uninterpret \"f\"\n\n p xs ys = foldr f a (xs ++ ys) .== foldr f (foldr f a ys) xs\n\n lemma \"foldrOverAppend\"\n (\\(Forall @\"xs\" xs) (Forall @\"ys\" ys) -> p xs ys)\n -- Induction is done on the last element. Here we want to induct on xs, hence the flip below.\n [induct (flip p)]\n\n{-\n --- Can't converge\n-- * Bookkeeping law\n\n-- | Provided @f@ is associative and @A@ is its right-unit: we have:\n--\n-- | @foldr f a . concat == foldr f a . map (foldr f a)@\n--\n-- We have:\n--\n-- >>> bookKeeping\nbookKeeping :: IO Proof\nbookKeeping = runKD $ do\n let a :: SA\n a = uninterpret \"a\"\n\n f :: SA -> SA -> SA\n f = uninterpret \"f\"\n\n p xss = foldr f a (concat xss) .== foldr f a (map (foldr f a) xss)\n\n assoc <- axiom \"f is associative\" (\\(Forall @\"x\" x) (Forall @\"y\" y) (Forall @\"z\" z) -> x `f` (y `f` z) .== (x `f` y) `f` z)\n unit <- axiom \"a is right-unit\" (\\(Forall @\"x\" x) -> x `f` a .== x)\n\n foa <- use foldrOverAppend\n\n chainLemma \"bookKeeping\"\n (\\(Forall @\"xss\" xss) -> p xss)\n (\\xs xss -> [ -- foldr f a (concat (xs .: xss))\n -- , foldr f a (xs ++ concat xss)\n -- , foldr f (foldr f a (concat xss)) xs\n -- , foldr f (foldr f a (map (foldr f a) xss)) xs\n\n f (foldr f a xs) (foldr f a (map (foldr f a) xss))\n , foldr f (foldr f a (map (foldr f a) xss)) (singleton (foldr f a xs))\n , foldr f a (singleton (foldr f a xs) ++ map (foldr f a) xss)\n , foldr f a (foldr f a xs .: map (foldr f a) xss)\n , foldr f a (map (foldr f a) (xs .: xss))\n ])\n [assoc, unit, foa, induct p]\n-}\n\n{---------------------\n --- Can't converge\n\n-- | Fusion for foldr:\n--\n-- @\n-- Given f a = b and f (g x y) = h x (f y), for all x and y\n-- We have: f . foldr g a = foldr h b\n-- @\n--\n-- We have:\n--\n-- >>> foldrFusion\nfoldrFusion :: IO Proof\nfoldrFusion = runKD $ do\n let

Error: Parse error: Unsupported extension: TypeAbstractions ▫︎ Found: "-----------------------------------------------------------------------------\n-- |\n-- Module : Documentation.SBV.Examples.KnuckleDragger.Induction\n-- Copyright : (c) Levent Erkok\n-- License : BSD3\n-- Maintainer: [email protected]\n-- Stability : experimental\n--\n-- Example use of the KnuckleDragger, for some inductive proofs\n-----------------------------------------------------------------------------\n\n{-# LANGUAGE DataKinds #-}\n{-# LANGUAGE TypeAbstractions #-}\n\n{-# OPTIONS_GHC -Wall -Werror #-}\n\nmodule Documentation.SBV.Examples.KnuckleDragger.Induction where\n\nimport Prelude hiding (sum, length)\n\nimport Data.SBV\nimport Data.SBV.Tools.KnuckleDragger\n\n-- | Prove that sum of constants @c@ from @0@ to @n@ is @n*c@.\n--\n-- We have:\n--\n-- >>> sumConstProof\n-- Lemma: sumConst_correct Q.E.D.\n-- [Proven] sumConst_correct\nsumConstProof :: IO Proof\nsumConstProof = runKD $ do\n let sum :: SInteger -> SInteger -> SInteger\n sum = smtFunction \"sum\" $ \\c n -> ite (n .== 0) 0 (c + sum c (n-1))\n\n spec :: SInteger -> SInteger -> SInteger\n spec c n = c * n\n\n p :: SInteger -> SInteger -> SBool\n p c n = observe \"imp\" (sum c n) .== observe \"spec\" (spec c n)\n\n lemma \"sumConst_correct\" (\\(Forall @\"c\" c) (Forall @\"n\" n) -> n .>= 0 .=> p c n) [induct p]\n\n-- | Prove that sum of numbers from @0@ to @n@ is @n*(n-1)/2@.\n--\n-- We have:\n--\n-- >>> sumProof\n-- Lemma: sum_correct Q.E.D.\n-- [Proven] sum_correct\nsumProof :: IO Proof\nsumProof = runKD $ do\n let sum :: SInteger -> SInteger\n sum = smtFunction \"sum\" $ \\n -> ite (n .== 0) 0 (n + sum (n - 1))\n\n spec :: SInteger -> SInteger\n spec n = (n * (n+1)) `sDiv` 2\n\n p :: SInteger -> SBool\n p n = observe \"imp\" (sum n) .== observe \"spec\" (spec n)\n\n lemma \"sum_correct\" (\\(Forall @\"n\" n) -> n .>= 0 .=> p n) [induct p]\n\n-- | Prove that sum of square of numbers from @0@ to @n@ is @n*(n+1)*(2n+1)/6@.\n--\n-- We have:\n--\n-- >>> sumSquareProof\n-- Lemma: sumSquare_correct Q.E.D.\n-- [Proven] sumSquare_correct\nsumSquareProof :: IO Proof\nsumSquareProof = runKD $ do\n let sumSquare :: SInteger -> SInteger\n sumSquare = smtFunction \"sumSquare\" $ \\n -> ite (n .== 0) 0 (n * n + sumSquare (n - 1))\n\n spec :: SInteger -> SInteger\n spec n = (n * (n+1) * (2*n+1)) `sDiv` 6\n\n p :: SInteger -> SBool\n p n = observe \"imp\" (sumSquare n) .== observe \"spec\" (spec n)\n\n lemma \"sumSquare_correct\" (\\(Forall @\"n\" n) -> n .>= 0 .=> p n) [induct p]\n\n-- | Prove that @11^n - 4^n@ is always divisible by 7. Note that power operator is hard for\n-- SMT solvers to deal with due to non-linearity. For this example, we use cvc5 to discharge\n-- the final goal, where z3 can't converge on it.\n--\n-- We have:\n--\n-- >>> elevenMinusFour\n-- Lemma: pow0 Q.E.D.\n-- Lemma: powN Q.E.D.\n-- Lemma: elevenMinusFour Q.E.D.\n-- [Proven] elevenMinusFour\nelevenMinusFour :: IO Proof\nelevenMinusFour = runKD $ do\n let pow :: SInteger -> SInteger -> SInteger\n pow = smtFunction \"pow\" $ \\x y -> ite (y .== 0) 1 (x * pow x (y - 1))\n\n emf :: SInteger -> SBool\n emf n = 7 `sDivides` (11 `pow` n - 4 `pow` n)\n\n pow0 <- lemma \"pow0\" (\\(Forall @\"x\" x) -> x `pow` 0 .== 1) []\n powN <- lemma \"powN\" (\\(Forall @\"x\" x) (Forall @\"n\" n) -> n .>= 0 .=> x `pow` (n+1) .== x * x `pow` n) []\n\n lemmaWith cvc5 \"elevenMinusFour\" (\\(Forall @\"n\" n) -> n .>= 0 .=> emf n) [pow0, powN, induct emf]\n"

Error: Parse error: Unsupported extension: TypeAbstractions ▫︎ Found: "-----------------------------------------------------------------------------\n-- |\n-- Module : Documentation.SBV.Examples.KnuckleDragger.Kleene\n-- Copyright : (c) Levent Erkok\n-- License : BSD3\n-- Maintainer: [email protected]\n-- Stability : experimental\n--\n-- Example use of the KnuckleDragger layer, proving some Kleene algebra theorems.\n--\n-- Based on <http://www.philipzucker.com/bryzzowski_kat/>\n-----------------------------------------------------------------------------\n\n{-# LANGUAGE DataKinds #-}\n{-# LANGUAGE DeriveAnyClass #-}\n{-# LANGUAGE DeriveDataTypeable #-}\n{-# LANGUAGE FlexibleInstances #-}\n{-# LANGUAGE ScopedTypeVariables #-}\n{-# LANGUAGE StandaloneDeriving #-}\n{-# LANGUAGE TemplateHaskell #-}\n{-# LANGUAGE TypeAbstractions #-}\n{-# LANGUAGE TypeSynonymInstances #-}\n\n{-# OPTIONS_GHC -Wall -Werror -Wno-unused-matches #-}\n\nmodule Documentation.SBV.Examples.KnuckleDragger.Kleene where\n\nimport Prelude hiding((<=))\n\nimport Data.SBV\nimport Data.SBV.Tools.KnuckleDragger\n\n-- | An uninterpreted sort, corresponding to the type of Kleene algebra strings.\ndata Kleene\nmkUninterpretedSort ''Kleene\n\n-- | Star operator over kleene algebras. We're leaving this uninterpreted.\nstar :: SKleene -> SKleene\nstar = uninterpret \"star\"\n\n-- | The 'Num' instance for Kleene makes it easy to write regular expressions\n-- in the more familiar form.\ninstance Num SKleene where\n (+) = uninterpret \"par\"\n (*) = uninterpret \"seq\"\n\n abs = error \"SKleene: not defined: abs\"\n signum = error \"SKleene: not defined: signum\"\n negate = error \"SKleene: not defined: signum\"\n\n fromInteger 0 = uninterpret \"zero\"\n fromInteger 1 = uninterpret \"one\"\n fromInteger n = error $ \"SKleene: not defined: fromInteger \" ++ show n\n\n-- | The set of strings matched by one regular expression is a subset of the second,\n-- if adding it to the second doesn't change the second set.\n(<=) :: SKleene -> SKleene -> SBool\nx <= y = x + y .== y\n\n-- | A sequence of Kleene algebra proofs. See <http://www.cs.cornell.edu/~kozen/Papers/ka.pdf>\n--\n-- We have:\n--\n-- >>> kleeneProofs\n-- Axiom: par_assoc Axiom.\n-- Axiom: par_comm Axiom.\n-- Axiom: par_idem Axiom.\n-- Axiom: par_zero Axiom.\n-- Axiom: seq_assoc Axiom.\n-- Axiom: seq_zero Axiom.\n-- Axiom: seq_one Axiom.\n-- Axiom: rdistrib Axiom.\n-- Axiom: ldistrib Axiom.\n-- Axiom: unfold Axiom.\n-- Axiom: least_fix Axiom.\n-- Lemma: par_lzero Q.E.D.\n-- Lemma: par_monotone Q.E.D.\n-- Lemma: seq_monotone Q.E.D.\n-- Chain: star_star_1\n-- Lemma: star_star_1.1 Q.E.D.\n-- Lemma: star_star_1.2 Q.E.D.\n-- Lemma: star_star_1.3 Q.E.D.\n-- Lemma: star_star_1.4 Q.E.D.\n-- Lemma: star_star_1 Q.E.D.\n-- Lemma: subset_eq Q.E.D.\n-- Lemma: star_star_2_2 Q.E.D.\n-- Lemma: star_star_2_3 Q.E.D.\n-- Lemma: star_star_2_1 Q.E.D.\n-- Lemma: star_star_2 Q.E.D.\nkleeneProofs :: IO ()\nkleeneProofs = runKD $ do\n\n -- Kozen axioms\n par_assoc <- axiom \"par_assoc\" $ \\(Forall @\"x\" (x :: SKleene)) (Forall @\"y\" y) (Forall @\"z\" z) -> x + (y + z) .== (x + y) + z\n par_comm <- axiom \"par_comm\" $ \\(Forall @\"x\" (x :: SKleene)) (Forall @\"y\" y) -> x + y .== y + x\n par_idem <- axiom \"par_idem\" $ \\(Forall @\"x\" (x :: SKleene)) -> x + x .== x\n par_zero <- axiom \"par_zero\" $ \\(Forall @\"x\" (x :: SKleene)) -> x + 0 .== x\n\n seq_assoc <- axiom \"seq_assoc\" $ \\(Forall @\"x\" (x :: SKleene)) (Forall @\"y\" y) (Forall @\"z\" z) -> x * (y * z) .== (x * y) * z\n seq_zero <- axiom \"seq_zero\" $ \\(Forall @\"x\" (x :: SKleene)) -> x * 0 .== 0\n seq_one <- axiom \"seq_one\" $ \\(Forall @\"x\" (x :: SKleene)) -> x * 1 .== x\n\n rdistrib <- axiom \"rdistrib\" $ \\(Forall @\"x\" (x :: SKleene)) (Forall @\"y\" y) (Forall @\"z\" z) -> x * (y + z) .== x * y + x * z\n ldistrib <- axiom \"ldistrib\" $ \\(Forall @\"x\" (x :: SKleene)) (Forall @\"y\" y) (Forall @\"z\" z) -> (y + z) * x .== y * x + z * x\n\n unfold <- axiom \"unfold\" $ \\(Forall @\"e\" e) -> star e .== 1 + e * star e\n\n least_fix <- axiom \"least_fix\" $

Error: Parse error: Unsupported extension: TypeAbstractions ▫︎ Found: "-----------------------------------------------------------------------------\n-- |\n-- Module : Documentation.SBV.Examples.KnuckleDragger.ListLen\n-- Copyright : (c) Levent Erkok\n-- License : BSD3\n-- Maintainer: [email protected]\n-- Stability : experimental\n--\n-- Example use of the KnuckleDragger, about lenghts of lists\n-----------------------------------------------------------------------------\n\n{-# LANGUAGE CPP #-}\n{-# LANGUAGE DataKinds #-}\n{-# LANGUAGE DeriveAnyClass #-}\n{-# LANGUAGE DeriveDataTypeable #-}\n{-# LANGUAGE ScopedTypeVariables #-}\n{-# LANGUAGE StandaloneDeriving #-}\n{-# LANGUAGE TemplateHaskell #-}\n{-# LANGUAGE TypeAbstractions #-}\n{-# LANGUAGE TypeApplications #-}\n\n{-# OPTIONS_GHC -Wall -Werror -Wno-unused-do-bind #-}\n\nmodule Documentation.SBV.Examples.KnuckleDragger.ListLen where\n\nimport Prelude hiding (sum, length, reverse, (++))\n\nimport Data.SBV\nimport Data.SBV.Tools.KnuckleDragger\n\nimport qualified Data.SBV.List as SL\n\n\n-- $setup\n-- >>> -- For doctest purposes only:\n-- >>> :set -XScopedTypeVariables\n-- >>> import Control.Exception\n\n\n-- | Use an uninterpreted type for the elements\ndata Elt\nmkUninterpretedSort ''Elt\n\n-- | Prove that the length of a list is one more than the length of its tail.\n--\n-- We have:\n--\n-- >>> listLengthProof\n-- Lemma: length_correct Q.E.D.\n-- [Proven] length_correct\nlistLengthProof :: IO Proof\nlistLengthProof = runKD $ do\n let length :: SList Elt -> SInteger\n length = smtFunction \"length\" $ \\xs -> ite (SL.null xs) 0 (1 + length (SL.tail xs))\n\n spec :: SList Elt -> SInteger\n spec = SL.length\n\n p :: SList Elt -> SBool\n p xs = observe \"imp\" (length xs) .== observe \"spec\" (spec xs)\n\n lemma \"length_correct\" (\\(Forall @\"xs\" xs) -> p xs) [induct p]\n\n-- | It is instructive to see what kind of counter-example we get if a lemma fails to prove.\n-- Below, we do a variant of the 'listLengthProof', but with a bad implementation over integers,\n-- and see the counter-example. Our implementation returns an incorrect answer if the given list is longer\n-- than 5 elements and have 42 in it. We have:\n--\n-- >>> badProof `catch` (\\(_ :: SomeException) -> pure ())\n-- Lemma: bad\n-- *** Failed to prove bad.\n-- Falsifiable. Counter-example:\n-- xs = [8,25,26,27,28,42] :: [Integer]\n-- imp = 42 :: Integer\n-- spec = 6 :: Integer\nbadProof :: IO ()\nbadProof = runKD $ do\n let length :: SList Integer -> SInteger\n length = smtFunction \"length\" $ \\xs -> ite (SL.null xs) 0 (1 + length (SL.tail xs))\n\n badLength :: SList Integer -> SInteger\n badLength xs = ite (SL.length xs .> 5 .&& 42 `SL.elem` xs) 42 (length xs)\n\n spec :: SList Integer -> SInteger\n spec = SL.length\n\n p :: SList Integer -> SBool\n p xs = observe \"imp\" (badLength xs) .== observe \"spec\" (spec xs)\n\n lemma \"bad\" (\\(Forall @\"xs\" xs) -> p xs) [induct p]\n\n pure ()\n\n-- | @Length (xs ++ ys) == length xs + length ys@\n--\n-- We have:\n--\n-- >>> lenAppend\n-- Lemma: lenAppend Q.E.D.\n-- [Proven] lenAppend\nlenAppend :: IO Proof\nlenAppend = runKD $ lemma \"lenAppend\"\n (\\(Forall @\"xs\" (xs :: SList Elt)) (Forall @\"ys\" ys) ->\n SL.length (xs SL.++ ys) .== SL.length xs + SL.length ys)\n []\n\n-- | @Length xs == length ys -> length (xs ++ ys) == 2 * length xs@\n--\n-- We have:\n--\n-- >>> lenAppend2\n-- Lemma: lenAppend2 Q.E.D.\n-- [Proven] lenAppend2\nlenAppend2 :: IO Proof\nlenAppend2 = runKD $ lemma \"lenAppend2\"\n (\\(Forall @\"xs\" (xs :: SList Elt)) (Forall @\"ys\" ys) ->\n SL.length xs .== SL.length ys\n .=> SL.length (xs SL.++ ys) .== 2 * SL.length xs)\n []\n"

Error: Parse error: Unsupported extension: TypeAbstractions ▫︎ Found: "-----------------------------------------------------------------------------\n-- |\n-- Module : Documentation.SBV.Examples.KnuckleDragger.Lists\n-- Copyright : (c) Levent Erkok\n-- License : BSD3\n-- Maintainer: [email protected]\n-- Stability : experimental\n--\n-- Various KnuckleDragger proofs about lists\n-----------------------------------------------------------------------------\n\n{-# LANGUAGE CPP #-}\n{-# LANGUAGE DataKinds #-}\n{-# LANGUAGE DeriveAnyClass #-}\n{-# LANGUAGE DeriveDataTypeable #-}\n{-# LANGUAGE StandaloneDeriving #-}\n{-# LANGUAGE TemplateHaskell #-}\n{-# LANGUAGE TypeAbstractions #-}\n\n{-# OPTIONS_GHC -Wall -Werror -Wno-unused-do-bind #-}\n\nmodule Documentation.SBV.Examples.KnuckleDragger.Lists where\n\nimport Data.SBV\nimport Data.SBV.List\nimport Data.SBV.Tools.KnuckleDragger\n\nimport Prelude hiding(reverse, (++), any, all, notElem, filter, map)\n\n\n-- $setup\n-- >>> -- For doctest purposes only:\n-- >>> :set -XScopedTypeVariables\n-- >>> import Control.Exception\n-- >>> import Data.SBV.Tools.KnuckleDragger\n\n\n-- | A list of booleans is not all true, if any of them is false. We have:\n--\n-- >>> allAny\n-- Lemma: allAny Q.E.D.\n-- [Proven] allAny\nallAny :: IO Proof\nallAny = runKD $ lemma \"allAny\" (\\(Forall @\"xs\" xs) -> p xs) [induct p]\n where p xs = sNot (all id xs) .== any sNot xs\n\n-- | If an integer list doesn't have 2 as an element, then filtering for @> 2@ or @.>= 2@\n-- yields the same result. We have:\n--\n-- >>> filterEx\n-- Lemma: filterEx Q.E.D.\n-- [Proven] filterEx\nfilterEx :: IO Proof\nfilterEx = runKD $ lemma \"filterEx\" (\\(Forall @\"xs\" xs) -> p xs) [induct p]\n where p xs = (2 :: SInteger) `notElem` xs .=> (filter (.> 2) xs .== filter (.>= 2) xs)\n\n-- | The 'filterEx' example above, except we get a counter-example if `2` can be in the list. Note that\n-- we don't even need the induction tactic here. (Though having it wouldn't hurt.) We have:\n--\n-- >>> filterEx2 `catch` (\\(_ :: SomeException) -> pure ())\n-- Lemma: filterEx\n-- *** Failed to prove filterEx.\n-- Falsifiable. Counter-example:\n-- xs = [2] :: [Integer]\nfilterEx2 :: IO ()\nfilterEx2 = runKD $ do\n let p :: SList Integer -> SBool\n p xs = filter (.> 2) xs .== filter (.>= 2) xs\n\n lemma \"filterEx\" (\\(Forall @\"xs\" xs) -> p xs) []\n\n pure ()\n\n-- | Data declaration for an uninterpreted source type.\ndata A\nmkUninterpretedSort ''A\n\n-- | Data declaration for an uninterpreted target type.\ndata B\nmkUninterpretedSort ''B\n\n-- | @reverse (x:xs) == reverse xs ++ [x]@\n--\n-- >>> runKD revCons\n-- Lemma: revCons Q.E.D.\n-- [Proven] revCons\nrevCons :: KD Proof\nrevCons = do\n let p :: SA -> SList A -> SBool\n p x xs = reverse (x .: xs) .== reverse xs ++ singleton x\n\n lemma \"revCons\" (\\(Forall @\"x\" x) (Forall @\"xs\" xs) -> p x xs) []\n\n-- | @Map f (xs ++ ys) == map f xs ++ map f ys@\n--\n-- >>> runKD mapAppend\n-- Lemma: mapAppend Q.E.D.\n-- [Proven] mapAppend\nmapAppend :: KD Proof\nmapAppend = do\n let p :: (SA -> SB) -> SList A -> SList A -> SBool\n p g xs ys = map g (xs ++ ys) .== map g xs ++ map g ys\n\n -- For an arbitrary uninterpreted function 'f':\n f :: SA -> SB\n f = uninterpret \"f\"\n\n lemma \"mapAppend\"\n (\\(Forall @\"xs\" xs) (Forall @\"ys\" ys) -> p f xs ys)\n -- induction is done on the last argument, so flip to do it on xs\n [induct (flip (p f))]\n\n-- | @Map f . reverse == reverse . map f@\n--\n-- >>> runKD mapReverse\n-- Lemma: revCons Q.E.D.\n-- Lemma: mapAppend Q.E.D.\n-- Chain: mapReverse\n-- Lemma: mapReverse.1 Q.E.D.\n-- Lemma: mapReverse.2 Q.E.D.\n-- Lemma: mapReverse.3 Q.E.D.\n-- Lemma: mapReverse.4 Q.E.D.\n-- Lemma: mapReverse.5 Q.E.D.\n-- Lemma: mapReverse.6 Q.E.D.\n-- Lemma: mapReverse Q.E.D.\n-- [Proven] mapReverse\nmapReverse :: KD Proof\nmapReverse = do\n let p :: (SA -> SB) -> SList A -> SBool\n p g xs = reverse (map g xs) .== map g (reverse xs)\n\n -- For an arbitrary uninterpreted function 'f':\n f :: SA -> SB\n f = uninterpret \"f\"\n\n rCons <- revCons\n mApp <- mapAppend\n

Error: Parse error: Unsupported extension: TypeAbstractions ▫︎ Found: "-----------------------------------------------------------------------------\n-- |\n-- Module : Documentation.SBV.Examples.KnuckleDragger.RevLen\n-- Copyright : (c) Levent Erkok\n-- License : BSD3\n-- Maintainer: [email protected]\n-- Stability : experimental\n--\n-- Proof that reversing a list does not change its length.\n-----------------------------------------------------------------------------\n\n{-# LANGUAGE CPP #-}\n{-# LANGUAGE DataKinds #-}\n{-# LANGUAGE DeriveAnyClass #-}\n{-# LANGUAGE DeriveDataTypeable #-}\n{-# LANGUAGE StandaloneDeriving #-}\n{-# LANGUAGE TemplateHaskell #-}\n{-# LANGUAGE TypeAbstractions #-}\n\n{-# OPTIONS_GHC -Wall -Werror -Wno-unused-do-bind #-}\n\nmodule Documentation.SBV.Examples.KnuckleDragger.RevLen where\n\nimport Prelude hiding (length, reverse)\n\nimport Data.SBV\nimport Data.SBV.Tools.KnuckleDragger\n\nimport Data.SBV.List (reverse, length)\n\n\n-- $setup\n-- >>> -- For doctest purposes only:\n-- >>> :set -XScopedTypeVariables\n-- >>> import Control.Exception\n\n\n-- | Use an uninterpreted type for the elements\ndata Elt\nmkUninterpretedSort ''Elt\n\n-- | @Length xs == length (reverse xs)@\n--\n-- We have:\n--\n-- >>> revLen\n-- Lemma: revLen Q.E.D.\n-- [Proven] revLen\nrevLen :: IO Proof\nrevLen = runKD $ do\n let p :: SList Elt -> SBool\n p xs = length (reverse xs) .== length xs\n\n lemma \"revLen\"\n (\\(Forall @\"xs\" xs) -> p xs)\n [induct p]\n\n-- | An example where we attempt to prove a non-theorem. Notice the counter-example\n-- generated for:\n--\n-- @Length xs = ite (length xs .== 3) 5 (length xs)@\n--\n-- We have:\n--\n-- >>> badRevLen `catch` (\\(_ :: SomeException) -> pure ())\n-- Lemma: badRevLen\n-- *** Failed to prove badRevLen.\n-- Falsifiable. Counter-example:\n-- xs = [Elt_1,Elt_2,Elt_1] :: [Elt]\nbadRevLen :: IO ()\nbadRevLen = runKD $ do\n let p :: SList Elt -> SBool\n p xs = length (reverse xs) .== ite (length xs .== 3) 5 (length xs)\n\n lemma \"badRevLen\"\n (\\(Forall @\"xs\" xs) -> p xs)\n [induct p]\n\n pure ()\n"

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

Suggestion in foldl, foldr in module Data.SBV.List: Reduce duplication ▫︎ Found: "svb <- sbvToSV st base\nsvl <- sbvToSV st l\nlam <- lambdaStr st False kb f\n" ▫︎ Perhaps: "Combine with Data/SBV/List.hs:477:19-40"

Warning in module Data.SBV.Core.Data: Unused LANGUAGE pragma ▫︎ Found: "{-# LANGUAGE InstanceSigs #-}"

Warning in module Data.SBV.Core.Data: Redundant bracket ▫︎ Found: "(SInteger)" ▫︎ Perhaps: "SInteger"

Warning in module Data.SBV.Core.Data: Redundant bracket ▫︎ Found: "(KUnbounded)" ▫︎ Perhaps: "KUnbounded"

Warning in module Data.SBV.Core.Data: Redundant bracket ▫︎ Found: "(KUnbounded)" ▫︎ Perhaps: "KUnbounded"

Warning in module Data.SBV.Core.Data: Redundant bracket ▫︎ Found: "(SWord8)" ▫︎ Perhaps: "SWord8"

Warning in module Data.SBV.Core.Data: Redundant bracket ▫︎ Found: "(SWord16)" ▫︎ Perhaps: "SWord16"

Warning in module Data.SBV.Core.Data: Redundant bracket ▫︎ Found: "(SWord32)" ▫︎ Perhaps: "SWord32"

Warning in module Data.SBV.Core.Data: Redundant bracket ▫︎ Found: "(SWord64)" ▫︎ Perhaps: "SWord64"

Warning in module Data.SBV.Core.Data: Redundant bracket ▫︎ Found: "(SInt8)" ▫︎ Perhaps: "SInt8"

The `set-output` command is deprecated and will be disabled soon. Please upgrade to using Environment Files. For more information see: https://github.blog/changelog/2022-10-11-github-actions-deprecating-save-state-and-set-output-commands/

The `set-output` command is deprecated and will be disabled soon. Please upgrade to using Environment Files. For more information see: https://github.blog/changelog/2022-10-11-github-actions-deprecating-save-state-and-set-output-commands/