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 ScopedTypeVariables #-}\n{-# LANGUAGE TypeAbstractions #-}\n{-# LANGUAGE TypeApplications #-}\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 , induct, inductAlt1, inductAlt2\n , inductiveLemma, inductiveLemmaWith\n , inductiveTheorem, inductiveTheoremWith\n -- * Faking proofs\n , sorry\n -- * Running KnuckleDragger proofs\n , KD, runKD, runKDWith, use\n ) where\n\nimport Data.SBV\nimport Data.SBV.Core.Data (SolverContext(internalVariable))\nimport Data.SBV.Core.Symbolic (isEmptyModel)\n\nimport Data.SBV.Control.Utils (getConfig)\nimport Data.SBV.Control hiding (getProof)\n\nimport Data.SBV.Tools.KDKernel\nimport Data.SBV.Tools.KDUtils\n\nimport Control.Monad (when)\nimport Control.Monad.Trans (MonadIO, liftIO)\n\nimport Data.List (intercalate)\n\nimport qualified Data.SBV.List as SL\n\nimport Data.Proxy\nimport GHC.TypeLits (KnownSymbol, symbolVal)\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 a 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 bail out. A single step in @h@ indicates a usage mistake, 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 Pr

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 lemma: case_n_mod_3_eq_0\n-- Step : 1 Q.E.D.\n-- Step : 2 Q.E.D.\n-- Result: Q.E.D.\n-- Chain lemma: case_n_mod_3_eq_1\n-- Step : 1 Q.E.D.\n-- Step : 2 Q.E.D.\n-- Result: Q.E.D.\n-- Chain lemma: case_n_mod_3_eq_2\n-- Step : 1 Q.E.D.\n-- Step : 2 Q.E.D.\n-- Result: 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.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\n-- Axiom: par_comm\n-- Axiom: par_idem\n-- Axiom: par_zero\n-- Axiom: seq_assoc\n-- Axiom: seq_zero\n-- Axiom: seq_one\n-- Axiom: rdistrib\n-- Axiom: ldistrib\n-- Axiom: unfold\n-- Axiom: least_fix\n-- Lemma: par_lzero Q.E.D.\n-- Lemma: par_monotone Q.E.D.\n-- Lemma: seq_monotone Q.E.D.\n-- Chain lemma: star_star_1\n-- Step : 1 Q.E.D.\n-- Step : 2 Q.E.D.\n-- Step : 3 Q.E.D.\n-- Step : 4 Q.E.D.\n-- Result: 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\" $ \\(Forall @\"x\" x) (Forall @\"e\" e) (Forall @\"f\" f) -> ((f + e * x) <= x) .=> ((star e * f) <= x)\n\n -- Collect the basic axi

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-- A variety of KnuckleDragger proofs on list processing functions.\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\n{-# OPTIONS_GHC -Wall -Werror -Wno-unused-do-bind #-}\n\nmodule Documentation.SBV.Examples.KnuckleDragger.Lists where\n\nimport Prelude (IO, ($), Integer, Num(..), pure, id, (.), flip)\n\nimport Data.SBV\nimport Data.SBV.List\nimport Data.SBV.Tools.KnuckleDragger\n\n\n-- $setup\n-- >>> -- For doctest purposes only:\n-- >>> :set -XScopedTypeVariables\n-- >>> import Data.SBV\n-- >>> import Control.Exception\n\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-- * Appending null\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 $\n lemma \"appendNull\"\n (\\(Forall @\"xs\" (xs :: SList A)) -> xs ++ nil .== xs)\n []\n\n-- * Moving cons over append\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 $\n lemma \"consApp\"\n (\\(Forall @\"x\" (x :: SA)) (Forall @\"xs\" xs) (Forall @\"ys\" ys) -> (x .: xs) ++ ys .== x .: (xs ++ ys))\n []\n\n-- * Associativity of append\n\n-- | @(xs ++ ys) ++ zs == xs ++ (ys ++ zs)@\n--\n-- We have:\n--\n-- >>> appendAssoc\n-- Lemma: appendAssoc Q.E.D.\n-- [Proven] appendAssoc\n--\n-- Surprisingly, z3 can prove this without any induction. (Since SBV's append translates directly to\n-- the concatenation of sequences in SMTLib, it must trigger an internal axiom (heuristic?) in z3\n-- that proves it right out-of-the-box!)\nappendAssoc :: IO Proof\nappendAssoc = runKD $\n lemma \"appendAssoc\"\n (\\(Forall @\"xs\" (xs :: SList A)) (Forall @\"ys\" ys) (Forall @\"zs\" zs) ->\n xs ++ (ys ++ zs) .== (xs ++ ys) ++ zs)\n []\n\n-- * Reverse and append\n\n-- | @reverse (x:xs) == reverse xs ++ [x]@\n--\n-- >>> revCons\n-- Lemma: revCons Q.E.D.\n-- [Proven] revCons\nrevCons :: IO Proof\nrevCons = runKD $\n lemma \"revCons\"\n (\\(Forall @\"x\" (x :: SA)) (Forall @\"xs\" xs) -> reverse (x .: xs) .== reverse xs ++ singleton x)\n []\n\n-- | @reverse (xs ++ ys) .== reverse ys ++ reverse xs@\n--\n-- We have:\n--\n-- >>> revApp\n-- Lemma: revApp Q.E.D.\n-- [Proven] revApp\nrevApp :: IO Proof\nrevApp = runKD $ do\n let p :: SList A -> SList A -> SBool\n p xs ys = reverse (xs ++ ys) .== reverse ys ++ reverse xs\n\n lemma \"revApp\"\n (\\(Forall @\"xs\" (xs :: SList A)) (Forall @\"ys\" ys) -> p xs ys)\n -- induction is done on the last argument, so we use flip to make sure we induct on xs\n [induct (flip p)]\n\n-- * Reversing twice is identity\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 let p :: SList A -> SBool\n p xs = reverse (reverse xs) .== xs\n\n ra <- use revApp\n\n lemma \"reverseReverse\" (\\(Forall @\"xs\" xs) -> p xs) [induct p, ra]\n\n-- * Lengths of lists\n\n-- | @Length (x : xs) = 1 + length xs@\n--\n-- We have:\n--\n-- >>> lengthTail\n-- Lemma: lengthTail Q.E.D.\n-- [P

Error: Parse error: Unsupported extension: TypeAbstractions ▫︎ Found: "-----------------------------------------------------------------------------\n-- |\n-- Module : Documentation.SBV.Examples.KnuckleDragger.Numeric\n-- Copyright : (c) Levent Erkok\n-- License : BSD3\n-- Maintainer: [email protected]\n-- Stability : experimental\n--\n-- Example use of inductive KnuckleDragger proofs, over integers.\n-----------------------------------------------------------------------------\n\n{-# LANGUAGE DataKinds #-}\n{-# LANGUAGE TypeAbstractions #-}\n\n{-# OPTIONS_GHC -Wall -Werror #-}\n\nmodule Documentation.SBV.Examples.KnuckleDragger.Numeric 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 c :: SInteger\n c = uninterpret \"c\"\n\n sum :: SInteger -> SInteger\n sum = smtFunction \"sum\" $ \\n -> ite (n .== 0) 0 (c + sum (n-1))\n\n spec :: SInteger -> SInteger\n spec n = c * n\n\n p :: SInteger -> SBool\n p n = sum n .== spec n\n\n lemma \"sumConst_correct\" (\\(Forall @\"n\" n) -> n .>= 0 .=> p n) [induct p]\n\n-- | Prove that sum of numbers from @0@ to @n@ is @n*(n-1)/2@.\n--\n-- In this case we use the induction tactic, and while it does get the job done, it's rather\n-- slow. See 'sumProof2' for an alternative approach that is faster. 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 = sum n .== spec n\n\n lemma \"sum_correct\" (\\(Forall @\"n\" n) -> n .>= 0 .=> p n) [induct p]\n\n-- | An alternate proof of proving sum of numbers from @0@ to @n@ is @n*(n-1)/2@, much faster\n-- than 'sumProof'. In this case, instead of just letting z3 find the inductive argument itself,\n-- we explicitly state the inductive steps, which goes a lot faster. We have:\n--\n-- >>> sumProof2\n-- Inductive lemma: sum_correct\n-- Base: sum_correct.Base Q.E.D.\n-- Help: sum_correct.L1 vs L2 Q.E.D.\n-- Help: sum_correct.L2 vs R1 Q.E.D.\n-- Step: sum_correct.Step Q.E.D.\n-- [Proven] sum_correct\nsumProof2 :: IO Proof\nsumProof2 = 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 = sum n .== spec n\n\n -- An explicit inductive proof, note that we don't have to spell out\n -- all the steps, as z3 is able to fill out the arithmetic part fairly quickly.\n inductiveLemma \"sum_correct\"\n (\\(Forall @\"n\" n) -> n .>= 0 .=> p n)\n (\\k -> ( [ sum (k+1)\n , (k+1) + sum k -- inductive hypothesis\n ]\n , [ spec (k+1)\n ]\n ))\n []\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-- Inductive lemma: sumSquare_correct\n-- Base: sumSquare_correct.Base Q.E.D.\n-- Help: sumSquare_correct.L1 vs L2 Q.E.D.\n-- Help: sumSquare_correct.L2 vs L3 Q.E.D.\n-- Help: sumSquare_correct.L3 vs L4 Q.E.D.\n-- Help: sumSquare_correct.L4 vs L5 Q.E.D.\n-- Help: sumSquare_correct.L5 vs L6 Q.E.D.\n-- Help: sumSquare_correct.L6 vs L7 Q.E.D.\n-- Help: sumSquare_correct.R1 vs R2 Q.E.D.\n-- Help: sumSquare_correct.L7 vs R2 Q.E.D.\n-- Step: sumSquare_correct.Step 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 = sumSquare n .== spec n\n\n inductiveLemma \"sumSquare_correct\"\n (\\(Forall @\"n\" n) -> n .>= 0 .

Error: Parse error: Unsupported extension: TypeAbstractions ▫︎ Found: "-----------------------------------------------------------------------------\n-- |\n-- Module : Documentation.SBV.Examples.KnuckleDragger.ShefferStroke\n-- Copyright : (c) Levent Erkok\n-- License : BSD3\n-- Maintainer: [email protected]\n-- Stability : experimental\n--\n-- Inspired by https://www.philipzucker.com/cody_sheffer/, proving\n-- that the axioms of sheffer stroke (i.e., nand in traditional boolean\n-- logic), imply it is a boolean algebra.\n-----------------------------------------------------------------------------\n\n{-# LANGUAGE CPP #-}\n{-# LANGUAGE DataKinds #-}\n{-# LANGUAGE DeriveDataTypeable #-}\n{-# LANGUAGE DeriveAnyClass #-}\n{-# LANGUAGE NamedFieldPuns #-}\n{-# LANGUAGE StandaloneDeriving #-}\n{-# LANGUAGE TemplateHaskell #-}\n{-# LANGUAGE TypeAbstractions #-}\n\n{-# OPTIONS_GHC -Wall -Werror #-}\n\nmodule Documentation.SBV.Examples.KnuckleDragger.ShefferStroke where\n\nimport Data.SBV\nimport Data.SBV.Tools.KnuckleDragger\n\n-- * The sheffer stroke\n\n-- | The abstract type for the domain.\ndata Stroke\nmkUninterpretedSort ''Stroke\n\n-- | The sheffer stroke operator\n(⏐) :: SStroke -> SStroke -> SStroke\n(⏐) = uninterpret \"⏐\"\ninfixl 7 ⏐\n\n-- | Negation in terms of ⏐\nﬧ :: SStroke -> SStroke\nﬧ x = x ⏐ x\n\n-- | First Sheffer axiom @ﬧﬧa == a@\nsheffer1 :: KD Proof\nsheffer1 = axiom \"ﬧﬧa == a\" $ \\(Forall @\"a\" a) -> ﬧ (ﬧ a) .== a\n\n-- | Second Sheffer axiom @A ⏐ (b ⏐ ﬧb) == ﬧa@\nsheffer2 :: KD Proof\nsheffer2 = axiom \"a ⏐ (b ⏐ ﬧb) == ﬧa\" $ \\(Forall @\"a\" a) (Forall @\"b\" b) -> a ⏐ (b ⏐ ﬧ b) .== ﬧ a\n\n-- | Third Sheffer axiom @ﬧ(a ⏐ (b ⏐ c)) == (ﬧb ⏐ a) ⏐ (ﬧc ⏐ a)@\nsheffer3 :: KD Proof\nsheffer3 = axiom \"ﬧ(a ⏐ (b ⏐ c)) == (ﬧb ⏐ a) ⏐ (ﬧc ⏐ a)\"\n $ \\(Forall @\"a\" a) (Forall @\"b\" b) (Forall @\"c\" c) -> ﬧ (a ⏐ (b ⏐ c)) .== (ﬧ b ⏐ a) ⏐ (ﬧ c ⏐ a)\n\n-- * Infimum, supremum, bottom, and top\n\n-- | Infimum: Greatest lower bound.\n(⨅) :: SStroke -> SStroke -> SStroke\na ⨅ b = ﬧ a ⏐ ﬧ b\n\n-- | Supremum: Least upper bound.\n(⨆) :: SStroke -> SStroke -> SStroke\na ⨆ b = ﬧ (a ⏐ b)\n\n-- | The unique bottom element\nz :: SStroke\nz = elt ⏐ ﬧ elt\n where elt = uninterpret \"z_witness\"\n\n-- | The unique top element\nu :: SStroke\nu = ﬧ z\n\n-- * Sheffer's stroke defines a boolean algebra\n\n-- | Prove that Sheffer stroke axioms imply it is a boolean algebra. We have:\n--\n-- TODO: Due to doctest issues, the output here does not get tested.\n-- See: https://github.com/yav/haskell-lexer/issues/14, which seems to be the root cause.\n-- >>> shefferBooleanAlgebra\nshefferBooleanAlgebra :: IO Proof\nshefferBooleanAlgebra = runKDWith z3{kdOptions = (kdOptions z3) {ribbonLength = 60}} $ do\n\n sh1 <- sheffer1\n sh2 <- sheffer2\n sh3 <- sheffer3\n\n commut <- chainLemma \"a ⏐ b == b ⏐ a\"\n (\\(Forall @\"a\" a) (Forall @\"b\" b) -> a ⏐ b .== b ⏐ a)\n (\\a b -> [ a ⏐ b\n , ﬧ (ﬧ (a ⏐ b))\n , ﬧ (ﬧ (a ⏐ ﬧ (ﬧ b)))\n , ﬧ (ﬧ (ﬧ (ﬧ b) ⏐ a))\n , b ⏐ a\n ])\n [sh1, sh3]\n\n all_bot <- chainLemma \"a ⏐ ﬧa == b ⏐ ﬧb\"\n (\\(Forall @\"a\" a) (Forall @\"b\" b) -> a ⏐ ﬧ a .== b ⏐ ﬧ b)\n (\\a b -> [ a ⏐ ﬧ a\n , ﬧ ((a ⏐ ﬧ a) ⏐ (b ⏐ ﬧ b))\n , ﬧ ((b ⏐ ﬧ b) ⏐ (a ⏐ ﬧ a))\n , ﬧ (ﬧ (b ⏐ ﬧ b))\n , b ⏐ ﬧ b\n ])\n [sh1, sh2, commut]\n\n commut1 <- lemma \"a ⊔ b == b ⊔ a\"\n (\\(Forall @\"a\" a) (Forall @\"b\" b) -> a ⨆ b .== b ⨆ a)\n [commut]\n\n commut2 <- lemma \"a ⊓ b == b ⊓ a\"\n (\\(Forall @\"a\" a) (Forall @\"b\" b) -> a ⨅ b .== b ⨅ a)\n [commut]\n\n ident1 <- lemma \"a ⊔ z = a\"\n (\\(Forall @\"a\" a) -> a ⨆ z .== a)\n [sh1, sh2]\n\n ident2 <- lemma \"a ⊓ u = a\"\n (\\(Forall @\"a\" a) -> a ⨅ u .== a)\n [sh1, sh2]\n\n distrib1 <- lemma \"a ⊔ (b ⊓ c) == (a ⊔ b) ⊓ (a ⊔ c)\"\n (\\(Forall @\"a\" a) (Forall @\"b\" b) (Forall @\"c\" c) -> a ⨆ (b ⨅ c) .== (a ⨆ b) ⨅ (a ⨆ c))\n [sh1, sh3, commut]\n\n distrib2 <- lemma \"a ⊓ (b ⊔ c) == (a ⊓ b) ⊔ (a ⊓ c)\"\n (\\(Forall @\"a\" a) (Forall @\"b\" b) (Forall @\"c\" c) -> a ⨅ (b ⨆ c) .== (a ⨅ b) ⨆ (a ⨅ c))\n [sh1, sh3, commut]\n\n compl1 <- lemma \"a ⊔ ﬧa == u\"\n (\\(Forall @\"a\" a) -> a ⨆ ﬧ a .== u)\n [sh1, s

Error: Parse error: Unsupported extension: TypeAbstractions ▫︎ Found: "-----------------------------------------------------------------------------\n-- |\n-- Module : Documentation.SBV.Examples.KnuckleDragger.Sqrt2IsIrrational\n-- Copyright : (c) Levent Erkok\n-- License : BSD3\n-- Maintainer: [email protected]\n-- Stability : experimental\n--\n-- Prove that square-root of 2 is irrational.\n-----------------------------------------------------------------------------\n\n{-# LANGUAGE DataKinds #-}\n{-# LANGUAGE ScopedTypeVariables #-}\n{-# LANGUAGE TypeAbstractions #-}\n\n{-# OPTIONS_GHC -Wall -Werror #-}\n\nmodule Documentation.SBV.Examples.KnuckleDragger.Sqrt2IsIrrational where\n\nimport Prelude hiding (even, odd)\n\nimport Data.SBV\nimport Data.SBV.Tools.KnuckleDragger\n\n-- | Prove that square-root of @2@ is irrational. That is, we can never find @A@ and @b@ such that\n-- @sqrt 2 == a / b@ and @A@ and @b@ are co-prime.\n--\n-- In order not to deal with reals and square-roots, we prove the integer-only alternative:\n-- If @A^2 = 2b^2@, then @A@ and @b@ cannot be co-prime. We proceed by establishing the\n-- following helpers first:\n--\n-- (1) An odd number squared is odd: @odd x -> odd x^2@\n-- (2) An even number that is a perfect square must be the square of an even number: @even x^2 -> even x@.\n-- (3) If a number is even, then its square must be a multiple of 4: @even x .=> x*x % 4 == 0@.\n--\n-- Using these helpers, we can argue:\n--\n-- (4) Start with the premise @A^2 = 2b^2@.\n-- (5) Thus, @A^2@ must be even. (Since it equals @2b^2@ by a.)\n-- (6) Thus, @A@ must be even. (Using 2 and b.)\n-- (7) Thus, @A^2@ must be divisible by @4@. (Using 3 and c. That is, 2b^2 == 4*K for someK.)\n-- (8) Thus, @b^2@ must be even. (Using d, b^2 = 2K.)\n-- (9) Thus, @b@ must be even. (Using 2 and e.)\n-- (10) Since @A@ and @b@ are both even, they cannot be co-prime. (Using c and f.)\n--\n-- Note that our proof is mostly about the first 3 facts above, then z3 and KnuckleDragger fills in the rest.\n--\n-- We have:\n--\n-- >>> sqrt2IsIrrational\n-- Chain lemma: oddSquaredIsOdd\n-- Step : 1 Q.E.D.\n-- Step : 2 Q.E.D.\n-- Result: Q.E.D.\n-- Lemma: squareEvenImpliesEven Q.E.D.\n-- Chain lemma: evenSquaredIsMult4\n-- Step : 1 Q.E.D.\n-- Result: Q.E.D.\n-- Lemma: sqrt2IsIrrational Q.E.D.\n-- [Proven] sqrt2IsIrrational\nsqrt2IsIrrational :: IO Proof\nsqrt2IsIrrational = runKD $ do\n let even, odd :: SInteger -> SBool\n even = (2 `sDivides`)\n odd = sNot . even\n\n sq :: SInteger -> SInteger\n sq x = x * x\n\n -- Prove that an odd number squared gives you an odd number.\n -- We need to help the solver by guiding it through how it can\n -- be decomposed as @2k+1@.\n --\n -- Interestingly, the solver doesn't need the analogous theorem that even number\n -- squared is even, possibly because the even/odd definition above is enough for\n -- it to deduce that fact automatically.\n oddSquaredIsOdd <- chainLemma \"oddSquaredIsOdd\"\n (\\(Forall @\"a\" a) -> odd a .=> odd (sq a))\n (\\a -> let k = a `sDiv` 2\n in [ odd a\n , sq a .== sq (2 * k + 1)\n , a .== 2 * k + 1\n ])\n []\n\n -- Prove that if a perfect square is even, then it be the square of an even number. For z3, the above proof\n -- is enough to establish this.\n squareEvenImpliesEven <- lemma \"squareEvenImpliesEven\"\n (\\(Forall @\"a\" a) -> even (sq a) .=> even a)\n [oddSquaredIsOdd]\n\n -- Prove that if @A@ is an even number, then its square is four times the square of another.\n -- Happily, z3 needs nchainLemma helpers to establish this all on its own.\n evenSquaredIsMult4 <- chainLemma \"evenSquaredIsMult4\"\n (\\(Forall @\"a\" a) -> even a .=> 4 `sDivides` sq a)\n (\\a -> let k = a `sDiv` 2\n in [ even a\n , sq a .== sq (k * 2)\n ])\n []\n\n -- Define what it means to be co-prime. Note that we use euclidian notion of modulus here\n -- as z3 deals with that much better. Two numbers are co-prime if 1 is their only common divisor.\n let coPrime :: SInteger -> SInteger -> SBool\n coPrime x y = quantifiedBool (\\(Forall @\"z\" z) -> (x `sEMod` z .== 0 .&& y `sEMod` z .== 0) .=> z .== 1)

Error: Parse error: Unsupported extension: TypeAbstractions ▫︎ Found: "-----------------------------------------------------------------------------\n-- |\n-- Module : Documentation.SBV.Examples.KnuckleDragger.Tao\n-- Copyright : (c) Levent Erkok\n-- License : BSD3\n-- Maintainer: [email protected]\n-- Stability : experimental\n--\n-- Proves a problem originating in algebra:\n-- https://mathoverflow.net/questions/450890/is-there-an-identity-between-the-commutative-identity-and-the-constant-identity/\n--\n-- Apparently this was posed by Terrence Tao: https://mathstodon.xyz/@tao/110736805384878353\n--\n-- Essentially, for an arbitrary binary operation op, we prove that\n--\n-- @\n-- (x op x) op y == y op x\n-- @\n--\n-- Implies that @op@ must be commutative.\n-----------------------------------------------------------------------------\n\n\n{-# LANGUAGE DeriveAnyClass #-}\n{-# LANGUAGE DeriveDataTypeable #-}\n{-# LANGUAGE DataKinds #-}\n{-# LANGUAGE TypeAbstractions #-}\n{-# LANGUAGE StandaloneDeriving #-}\n{-# LANGUAGE TemplateHaskell #-}\n\n{-# OPTIONS_GHC -Wall -Werror #-}\n\nmodule Documentation.SBV.Examples.KnuckleDragger.Tao where\n\nimport Data.SBV\nimport Data.SBV.Tools.KnuckleDragger\n\n-- | Create an uninterpreted type to do the proofs over.\ndata T\nmkUninterpretedSort ''T\n\n-- | Prove that:\n--\n-- @\n-- (x op x) op y == y op x\n-- @\n--\n-- means that @op@ is commutative.\n--\n-- We have:\n--\n-- >>> tao\n-- Lemma: tao Q.E.D.\n-- [Proven] tao\ntao :: IO Proof\ntao = runKD $ do\n let op :: ST -> ST -> ST\n op = uninterpret \"op\"\n\n lemma \"tao\" ( quantifiedBool (\\(Forall @\"x\" x) (Forall @\"y\" y) -> ((x `op` x) `op` y) .== y `op` x)\n .=> quantifiedBool (\\(Forall @\"x\" x) (Forall @\"y\" y) -> (x `op` y) .== (y `op` x)))\n []\n"

Error: Parse error: Expression syntax in pattern: Forall @"x" ▫︎ Found: " skolemEx4 = sat cs\n where cs :: ConstraintSet\n> cs = do constrain $ taggedSkolemize \"c1\" $ \\(Forall @\"x\" x) (Exists @\"y\" y) -> x .== (y :: SInteger)\n constrain $ taggedSkolemize \"c2\" $ \\(Forall @\"x\" x) (Exists @\"y\" y) -> x .== (y-1 :: SInteger)\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 HigherOrderArg kb f\n" ▫︎ Perhaps: "Combine with Data/SBV/List.hs:478: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/