Skip to content

Commit

Permalink
KD: Make induction a tactic and generalize
Browse files Browse the repository at this point in the history
  • Loading branch information
@LeventErkok
LeventErkok committed Sep 10, 2024
1 parent 85ebd1c commit 6ce6437
Show file tree
Hide file tree
Showing 5 changed files with 80 additions and 94 deletions.
91 changes: 39 additions & 52 deletions Data/SBV/Tools/KDKernel.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,8 +27,6 @@ module Data.SBV.Tools.KDKernel (
, sorry
) where

import Control.Monad (when)

import Data.List (intercalate, sort, nub)

import System.IO (hFlush, stdout)
Expand Down Expand Up @@ -87,21 +85,17 @@ finish what skip = do putStrLn $ replicate (ribbonLength - skip) ' ' ++ what
-- if you assert nonsense, then you get nonsense back. So, calls to 'axiom' should be limited to
-- definitions, or basic axioms (like commutativity, associativity) of uninterpreted function symbols.
axiom :: Proposition a => String -> a -> IO Proven
axiom = axiomGen True
axiom nm p = do start False "Axiom" [nm] >>= finish "Axiom."

pure (internalAxiom nm p) { isUserAxiom = True }

-- | Internal axiom generator; so we can keep truck of KnuckleDrugger's trusted axioms, vs. user given axioms.
-- Not exported.
internalAxiom :: Proposition a => String -> a -> IO Proven
internalAxiom = axiomGen False

-- | Generate an axiom. We only "display" the user-given axioms, not internal ones.
axiomGen :: Proposition a => Bool -> String -> a -> IO Proven
axiomGen isUserAxiom nm p = do when isUserAxiom $ start False "Axiom" [nm] >>= finish "Axiom."

pure Proven{ rootOfTrust = None
, isUserAxiom = isUserAxiom
, getProof = label nm (quantifiedBool p)
}
internalAxiom :: Proposition a => String -> a -> Proven
internalAxiom nm p = Proven { rootOfTrust = None
, isUserAxiom = False
, getProof = label nm (quantifiedBool p)
}

-- | A manifestly false theorem. This is useful when we want to prove a theorem that the underlying solver
-- cannot deal with, or if we want to postpone the proof for the time being. KnuckleDragger will keep
Expand Down Expand Up @@ -195,22 +189,22 @@ theoremWith cfg nm = lemmaGen cfg "Theorem" [nm]
-- | Given a predicate, return an induction principle for it. Typically, we only have one viable
-- induction principle for a given type, but we allow for alternative ones.
class Induction a where
inductionPrinciple :: (a -> SBool) -> IO Proven
inductionPrincipleAlt1 :: (a -> SBool) -> IO Proven
inductionPrincipleAlt2 :: (a -> SBool) -> IO Proven
induct :: (a -> SBool) -> Proven
inductAlt1 :: (a -> SBool) -> Proven
inductAlt2 :: (a -> SBool) -> Proven

-- The second and third principles are the same as first by default, unless we provide them explicitly.
inductionPrincipleAlt1 = inductionPrinciple
inductionPrincipleAlt2 = inductionPrinciple
inductAlt1 = induct
inductAlt2 = induct

-- Induction for multiple argument predicates, inducting over the first argument
inductionPrinciple2 :: SymVal b => (a -> SBV b -> SBool) -> IO Proven
inductionPrinciple3 :: (SymVal b, SymVal c) => (a -> SBV b -> SBV c -> SBool) -> IO Proven
inductionPrinciple4 :: (SymVal b, SymVal c, SymVal d) => (a -> SBV b -> SBV c -> SBV d -> SBool) -> IO Proven
induct2 :: SymVal b => (a -> SBV b -> SBool) -> Proven
induct3 :: (SymVal b, SymVal c) => (a -> SBV b -> SBV c -> SBool) -> Proven
induct4 :: (SymVal b, SymVal c, SymVal d) => (a -> SBV b -> SBV c -> SBV d -> SBool) -> Proven

inductionPrinciple2 f = inductionPrinciple $ \a -> quantifiedBool (\(Forall b) -> f a b)
inductionPrinciple3 f = inductionPrinciple $ \a -> quantifiedBool (\(Forall b) (Forall c) -> f a b c)
inductionPrinciple4 f = inductionPrinciple $ \a -> quantifiedBool (\(Forall b) (Forall c) (Forall d) -> f a b c d)
induct2 f = induct $ \a -> quantifiedBool (\(Forall b) -> f a b)
induct3 f = induct $ \a -> quantifiedBool (\(Forall b) (Forall c) -> f a b c)
induct4 f = induct $ \a -> quantifiedBool (\(Forall b) (Forall c) (Forall d) -> f a b c d)

-- | Induction over SInteger. We provide various induction principles here: The first one
-- is over naturals, will only prove predicates that explicitly restrict the argument to >= 0.
Expand All @@ -219,43 +213,36 @@ class Induction a where
instance Induction SInteger where

-- | Induction over naturals. Will prove predicates of the form @\n -> n >= 0 .=> predicate n@.
inductionPrinciple p = do
let qb = quantifiedBool
induct p = internalAxiom "Nat.induction" principle
where qb = quantifiedBool

principle = p 0 .&& qb (\(Forall n) -> (n .>= 0 .&& p n) .=> p (n+1))
.=> qb -----------------------------------------------------------
(\(Forall n) -> n .>= 0 .=> p n)
principle = p 0 .&& qb (\(Forall n) -> (n .>= 0 .&& p n) .=> p (n+1))
.=> qb -----------------------------------------------------------
(\(Forall n) -> n .>= 0 .=> p n)

internalAxiom "Nat.induction" principle

-- | Induction over integers, using the strategy that @P(n)@ is equivalent to @P(n+1)@
-- (i.e., not just @P(n) => P(n+1)@), thus covering the entire range.
inductionPrincipleAlt1 p = do
let qb = quantifiedBool
inductAlt1 p = internalAxiom "Integer.induction" principle
where qb = quantifiedBool

principle = p 0 .&& qb (\(Forall i) -> p i .== p (i+1))
.=> qb ---------------------------------------------
(\(Forall i) -> p i)

internalAxiom "Integer.induction" principle
principle = p 0 .&& qb (\(Forall i) -> p i .== p (i+1))
.=> qb ---------------------------------------------
(\(Forall i) -> p i)

-- | Induction over integers, using the strategy that @P(n) => P(n+1)@ and @P(n) => P(n-1)@.
inductionPrincipleAlt2 p = do
let qb = quantifiedBool

principle = p 0 .&& qb (\(Forall i) -> p i .=> p (i+1) .&& p (i-1))
.=> qb ---------------------------------------------------------
(\(Forall i) -> p i)
inductAlt2 p = internalAxiom "Integer.splitInduction" principle
where qb = quantifiedBool

internalAxiom "Integer.splitInduction" principle
principle = p 0 .&& qb (\(Forall i) -> p i .=> p (i+1) .&& p (i-1))
.=> qb ---------------------------------------------------------
(\(Forall i) -> p i)

-- | Induction over lists
instance SymVal a => Induction (SList a) where
inductionPrinciple p = do
let qb a = quantifiedBool a

principle = p SL.nil .&& qb (\(Forall x) (Forall xs) -> p xs .=> p (x SL..: xs))
.=> qb ----------------------------------------------------------------------
(\(Forall xs) -> p xs)
induct p = internalAxiom "List(a).induction" principle
where qb a = quantifiedBool a

internalAxiom "List(a).induction" principle
principle = p SL.nil .&& qb (\(Forall x) (Forall xs) -> p xs .=> p (x SL..: xs))
.=> qb ----------------------------------------------------------------------
(\(Forall xs) -> p xs)
45 changes: 23 additions & 22 deletions Documentation/SBV/Examples/KnuckleDragger/AppendRev.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,22 +10,30 @@
-----------------------------------------------------------------------------

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeApplications #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.KnuckleDragger.AppendRev where

import Prelude hiding (sum, length, reverse, (++))
import Prelude hiding (reverse, (++))

import Data.SBV
import Data.SBV.Tools.KnuckleDragger

import Data.SBV.List ((.:), (++), reverse)
import qualified Data.SBV.List as SL

-- | Use an uninterpreted type for the elements
data Elt
mkUninterpretedSort ''Elt

-- | @xs ++ [] == xs@
--
-- We have:
Expand All @@ -34,8 +42,8 @@ import qualified Data.SBV.List as SL
-- Lemma: appendNull Q.E.D.
appendNull :: IO Proven
appendNull = lemma "appendNull"
(\(Forall @"xs" (xs :: SList Integer)) -> xs ++ SL.nil .== xs)
[]
(\(Forall @"xs" (xs :: SList Elt)) -> xs ++ SL.nil .== xs)
[]

-- | @(x : xs) ++ ys == x : (xs ++ ys)@
--
Expand All @@ -45,8 +53,8 @@ appendNull = lemma "appendNull"
-- Lemma: consApp Q.E.D.
consApp :: IO Proven
consApp = lemma "consApp"
(\(Forall @"x" (x :: SInteger)) (Forall @"xs" xs) (Forall @"ys" ys) -> (x .: xs) ++ ys .== x .: (xs ++ ys))
[]
(\(Forall @"x" (x :: SElt)) (Forall @"xs" xs) (Forall @"ys" ys) -> (x .: xs) ++ ys .== x .: (xs ++ ys))
[]

-- | @(xs ++ ys) ++ zs == xs ++ (ys ++ zs)@
--
Expand All @@ -62,15 +70,12 @@ appendAssoc = do
let p :: SymVal a => SList a -> SList a -> SList a -> SBool
p xs ys zs = xs ++ (ys ++ zs) .== (xs ++ ys) ++ zs

-- Do the proof over integers. We use 'inductionPrinciple3', since our predicate has 3 arguments.
induct <- inductionPrinciple3 (p @Integer)

-- Get a hold on to the consApp lemma that we'll need
lconsApp <- consApp

lemma "appendAssoc"
(\(Forall @"xs" (xs :: SList Integer)) (Forall @"ys" ys) (Forall @"zs" zs) -> p xs ys zs)
[lconsApp , induct]
(\(Forall @"xs" (xs :: SList Elt)) (Forall @"ys" ys) (Forall @"zs" zs) -> p xs ys zs)
[lconsApp , induct3 (p @Elt)]

-- | @reverse (xs ++ ys) == reverse ys ++ reverse xs@
-- We have:
Expand All @@ -95,19 +100,19 @@ revApp = do
lAppendAssoc <- appendAssoc

revApp_induction_pre <- chainLemma "revApp_induction_pre"
(\(Forall @"x" (x :: SInteger)) (Forall @"xs" xs) (Forall @"ys" ys)
(\(Forall @"x" (x :: SElt)) (Forall @"xs" xs) (Forall @"ys" ys)
-> reverse ((x .: xs) ++ ys) .== (reverse (xs ++ ys)) ++ SL.singleton x)
(\(x :: SInteger) xs ys ->
(\(x :: SElt) xs ys ->
[ reverse ((x .: xs) ++ ys)
, reverse (x .: (xs ++ ys))
, reverse (xs ++ ys) ++ SL.singleton x
]
) [lconsApp]

revApp_induction_post <- chainLemma "revApp_induction_post"
(\(Forall @"x" (x :: SInteger)) (Forall @"xs" xs) (Forall @"ys" ys)
(\(Forall @"x" (x :: SElt)) (Forall @"xs" xs) (Forall @"ys" ys)
-> (reverse ys ++ reverse xs) ++ SL.singleton x .== reverse ys ++ reverse (x .: xs))
(\(x :: SInteger) xs ys ->
(\(x :: SElt) xs ys ->
[ (reverse ys ++ reverse xs) ++ SL.singleton x
, reverse ys ++ (reverse xs ++ SL.singleton x)
, reverse ys ++ reverse (x .: xs)
Expand All @@ -117,10 +122,8 @@ revApp = do
let q :: SymVal a => SList a -> SList a -> SBool
q xs ys = reverse (xs ++ ys) .== (reverse ys ++ reverse xs)

inductQ <- inductionPrinciple2 (q @Integer)

lemma "revApp" (\(Forall @"xs" (xs :: SList Integer)) (Forall @"ys" ys) -> reverse (xs ++ ys) .== reverse ys ++ reverse xs)
[sorry, revApp_induction_pre, inductQ, revApp_induction_post]
lemma "revApp" (\(Forall @"xs" (xs :: SList Elt)) (Forall @"ys" ys) -> reverse (xs ++ ys) .== reverse ys ++ reverse xs)
[sorry, revApp_induction_pre, induct2 (q @Elt), revApp_induction_post]

-- | @reverse (reverse xs) == xs@
--
Expand Down Expand Up @@ -150,8 +153,6 @@ reverseReverse = do
let p :: SymVal a => SList a -> SBool
p xs = reverse (reverse xs) .== xs

induct <- inductionPrinciple (p @Integer)

lemma "reverseReverse"
(\(Forall @"xs" (xs :: SList Integer)) -> p xs)
[induct, lRevApp, lAppendAssoc]
(\(Forall @"xs" (xs :: SList Elt)) -> p xs)
[induct (p @Elt), lRevApp, lAppendAssoc]
8 changes: 2 additions & 6 deletions Documentation/SBV/Examples/KnuckleDragger/Induction.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,9 +38,7 @@ sumProof = do
p :: SInteger -> SBool
p n = observe "imp" (sum n) .== observe "spec" (spec n)

induct <- inductionPrinciple p

lemma "sum_correct" (\(Forall @"n" n) -> n .>= 0 .=> p n) [induct]
lemma "sum_correct" (\(Forall @"n" n) -> n .>= 0 .=> p n) [induct p]

-- | Prove that sum of square of numbers from @0@ to @n@ is @n*(n+1)*(2n+1)/6@.
--
Expand All @@ -59,6 +57,4 @@ sumSquareProof = do
p :: SInteger -> SBool
p n = observe "imp" (sumSquare n) .== observe "spec" (spec n)

induct <- inductionPrinciple p

lemma "sumSquare_correct" (\(Forall @"n" n) -> n .>= 0 .=> p n) [induct]
lemma "sumSquare_correct" (\(Forall @"n" n) -> n .>= 0 .=> p n) [induct p]
26 changes: 15 additions & 11 deletions Documentation/SBV/Examples/KnuckleDragger/ListLen.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,11 @@
-----------------------------------------------------------------------------

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeApplications #-}

Expand All @@ -30,6 +34,10 @@ import qualified Data.SBV.List as SL
-- >>> :set -XScopedTypeVariables
-- >>> import Control.Exception

-- | Use an uninterpreted type for the elements
data Elt
mkUninterpretedSort ''Elt

-- | Prove that the length of a list is one more than the length of its tail.
--
-- We have:
Expand All @@ -38,22 +46,20 @@ import qualified Data.SBV.List as SL
-- Lemma: length_correct Q.E.D.
listLengthProof :: IO Proven
listLengthProof = do
let length :: SList Integer -> SInteger
let length :: SList Elt -> SInteger
length = smtFunction "length" $ \xs -> ite (SL.null xs) 0 (1 + length (SL.tail xs))

spec :: SList Integer -> SInteger
spec :: SList Elt -> SInteger
spec = SL.length

p :: SList Integer -> SBool
p :: SList Elt -> SBool
p xs = observe "imp" (length xs) .== observe "spec" (spec xs)

induct <- inductionPrinciple p

lemma "length_correct" (\(Forall @"xs" xs) -> p xs) [induct]
lemma "length_correct" (\(Forall @"xs" xs) -> p xs) [induct p]

-- | It is instructive to see what kind of counter-example we get if a lemma fails to prove.
-- Below, we do a variant of the 'listLengthProof', but with a bad implementation, and see the
-- counter-example. Our implementation returns an incorrect answer if the given list is longer
-- Below, we do a variant of the 'listLengthProof', but with a bad implementation over integers,
-- and see the counter-example. Our implementation returns an incorrect answer if the given list is longer
-- than 5 elements and have 42 in it. We have:
--
-- >>> badProof `catch` (\(_ :: SomeException) -> pure ())
Expand All @@ -77,8 +83,6 @@ badProof = do
p :: SList Integer -> SBool
p xs = observe "imp" (badLength xs) .== observe "spec" (spec xs)

induct <- inductionPrinciple p

lemma "bad" (\(Forall @"xs" xs) -> p xs) [induct]
lemma "bad" (\(Forall @"xs" xs) -> p xs) [induct p]

pure ()
4 changes: 1 addition & 3 deletions Documentation/SBV/Examples/KnuckleDragger/RevLen.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,8 +43,6 @@ revLen = do
let p :: SList Elt -> SBool
p xs = length (reverse xs) .== length xs

induct <- inductionPrinciple p

lemma "revLen"
(\(Forall @"xs" xs) -> p xs)
[induct]
[induct p]

0 comments on commit 6ce6437

Please sign in to comment.