sbv-14.0: Documentation/SBV/Examples/TP/TautologyChecker.hs
-----------------------------------------------------------------------------
-- |
-- Module : Documentation.SBV.Examples.TP.TautologyChecker
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- A verified tautology checker (unordered BDD-style SAT solver) in SBV.
-- This is a port of the Imandra proof by Grant Passmore, originally
-- inspired by Boyer-Moore '79.
-- See <https://raw.githubusercontent.com/imandra-ai/imandrax-examples/refs/heads/main/src/tautology.iml>
--
-- We define a simple formula type with If-then-else, normalize formulas into a canonical form, and prove
-- both soundness and completeness of the tautology checker. The canonical form is essentially an
-- unordered-BDD, making it easy to evaluate it.
-----------------------------------------------------------------------------
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedLists #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.TP.TautologyChecker where
import Prelude hiding (null, tail, head, (++))
import Data.SBV
import Data.SBV.List
import Data.SBV.TP
import Data.SBV.Tuple
#ifdef DOCTEST
-- $setup
-- >>> import Data.SBV
-- >>> import Data.SBV.TP
#endif
-- * Formula representation
-- | A propositional formula with variables and if-then-else.
data Formula = FTrue
| FFalse
| Var { fVar :: Integer }
| If { ifCond :: Formula
, ifThen :: Formula
, ifElse :: Formula
}
-- | Make formulas symbolic.
mkSymbolic [''Formula]
-- * Measuring formulas
-- | Depth of nested If constructors in the condition position.
ifDepth :: SFormula -> SInteger
ifDepth = smtFunction "ifDepth"
$ \f -> [sCase| f of
If c _ _ -> 1 + ifDepth c
_ -> 0
|]
-- | \(\mathit{ifDepth}(f) \geq 0\)
--
-- >>> runTP ifDepthNonNeg
-- Lemma: ifDepthNonNeg Q.E.D.
-- Functions proven terminating: ifDepth
-- [Proven] ifDepthNonNeg :: Ɐf ∷ Formula → Bool
ifDepthNonNeg :: TP (Proof (Forall "f" Formula -> SBool))
ifDepthNonNeg = inductiveLemma "ifDepthNonNeg" (\(Forall f) -> ifDepth f .>= 0) []
-- | Complexity of a formula (for termination measure).
ifComplexity :: SFormula -> SInteger
ifComplexity = smtFunction "ifComplexity"
$ \f -> [sCase| f of
If c l r -> ifComplexity c * (ifComplexity l + ifComplexity r)
_ -> 1
|]
-- | \(\mathit{ifComplexity}(f) > 0\)
--
-- >>> runTP ifComplexityPos
-- Lemma: ifComplexityPos Q.E.D.
-- Functions proven terminating: ifComplexity
-- [Proven] ifComplexityPos :: Ɐf ∷ Formula → Bool
ifComplexityPos :: TP (Proof (Forall "f" Formula -> SBool))
ifComplexityPos = inductiveLemma "ifComplexityPos" (\(Forall f) -> ifComplexity f .> 0) []
-- | The branches of an If have smaller complexity than the whole.
--
-- \(\mathit{ifComplexity}(c) < \mathit{ifComplexity}(\mathit{If}(c, l, r)) \land \mathit{ifComplexity}(l) < \mathit{ifComplexity}(\mathit{If}(c, l, r)) \land \mathit{ifComplexity}(r) < \mathit{ifComplexity}(\mathit{If}(c, l, r))\)
--
-- >>> runTP ifComplexitySmaller
-- Lemma: ifComplexityPos Q.E.D.
-- Lemma: ifComplexitySmaller
-- Step: 1 Q.E.D.
-- Result: Q.E.D.
-- Functions proven terminating: ifComplexity
-- [Proven] ifComplexitySmaller :: Ɐc ∷ Formula → Ɐl ∷ Formula → Ɐr ∷ Formula → Bool
ifComplexitySmaller :: TP (Proof (Forall "c" Formula -> Forall "l" Formula -> Forall "r" Formula -> SBool))
ifComplexitySmaller = do
icp <- recall ifComplexityPos
calc "ifComplexitySmaller"
(\(Forall c) (Forall l) (Forall r) ->
let ic = ifComplexity (sIf c l r)
in ifComplexity c .< ic .&& ifComplexity l .< ic .&& ifComplexity r .< ic) $
\c l r ->
let ic = ifComplexity (sIf c l r)
cc = ifComplexity c
cl = ifComplexity l
cr = ifComplexity r
in [] |- cc .< ic .&& cl .< ic .&& cr .< ic
?? icp `at` Inst @"f" c
?? icp `at` Inst @"f" l
?? icp `at` Inst @"f" r
=: sTrue
=: qed
-- * Normalization
-- | Check if a formula is in normal form (no nested If in condition position).
isNormal :: SFormula -> SBool
isNormal = smtFunction "isNormal"
$ \f -> [sCase| f of
If c p q -> sNot (isIf c) .&& isNormal p .&& isNormal q
_ -> sTrue
|]
-- | Normalize a formula by eliminating nested Ifs in condition position.
--
-- The key transformation is:
--
-- @
-- If (If (p, q, r), left, right)
-- =
-- If (p, If (q, left, right), If (r, left, right))
-- @
--
-- Note that this transformation increases the size of the formula, but reduces its complexity.
normalize :: SFormula -> SFormula
normalize = smtFunctionWithMeasure "normalize"
( \f -> tuple (ifComplexity f, ifDepth f)
, [ measureLemma ifDepthNonNeg
, measureLemma ifComplexityPos
, measureLemmaWith z3 ifComplexitySmaller
, measureLemmaWith z3 normalizePreservesComplexity
]
)
$ \f -> [sCase| f of
If (If p q r) left right -> normalize (sIf p (sIf q left right) (sIf r left right))
If c left right -> sIf c (normalize left) (normalize right)
_ -> f
|]
-- | The normalization transformation preserves complexity.
--
-- \(\mathit{ifComplexity}(\mathit{If}(p, \mathit{If}(q, l, r), \mathit{If}(s, l, r))) = \mathit{ifComplexity}(\mathit{If}(\mathit{If}(p, q, s), l, r))\)
--
-- >>> runTP normalizePreservesComplexity
-- Lemma: helper Q.E.D.
-- Lemma: normalizePreservesComplexity
-- Step: 1 Q.E.D.
-- Step: 2 Q.E.D.
-- Step: 3 Q.E.D.
-- Step: 4 Q.E.D.
-- Step: 5 Q.E.D.
-- Step: 6 Q.E.D.
-- Step: 7 Q.E.D.
-- Result: Q.E.D.
-- Functions proven terminating: ifComplexity
-- [Proven] normalizePreservesComplexity :: Ɐp ∷ Formula → Ɐq ∷ Formula → Ɐs ∷ Formula → Ɐl ∷ Formula → Ɐr ∷ Formula → Bool
normalizePreservesComplexity :: TP (Proof (Forall "p" Formula -> Forall "q" Formula -> Forall "s" Formula -> Forall "l" Formula -> Forall "r" Formula -> SBool))
normalizePreservesComplexity = do
-- The following is a trivial lemma, but without it the solver don't seem to be able to make progress since
-- it needs to instantiate it properly. So we help the solver out explicitly.
helper <- lemma "helper"
(\(Forall @"a" a) (Forall @"b" b) (Forall @"c" c) -> a .== b .=> a * c .== b * (c :: SInteger))
[]
calc "normalizePreservesComplexity"
(\(Forall p) (Forall q) (Forall s) (Forall l) (Forall r) ->
ifComplexity (sIf p (sIf q l r) (sIf s l r)) .== ifComplexity (sIf (sIf p q s) l r)) $
\p q s l r ->
let cp = ifComplexity p
cq = ifComplexity q
cs = ifComplexity s
cl = ifComplexity l
cr = ifComplexity r
in [] |- ifComplexity (sIf p (sIf q l r) (sIf s l r))
=: cp * (ifComplexity (sIf q l r) + ifComplexity (sIf s l r))
=: cp * (cq * (cl + cr) + cs * (cl + cr))
=: cp * ((cq + cs) * (cl + cr))
=: (cp * (cq + cs)) * (cl + cr)
?? helper `at` (Inst @"a" (ifComplexity (sIf p q s)), Inst @"b" (cp * (cq + cs)), Inst @"c" (cl + cr))
=: ifComplexity (sIf p q s) * (cl + cr)
=: ifComplexity (sIf p q s) * (ifComplexity l + ifComplexity r)
=: ifComplexity (sIf (sIf p q s) l r)
=: qed
-- * Variable bindings
-- | A binding associates a variable ID with a boolean value.
data Binding = Binding { varId :: Integer
, value :: Bool
}
-- | Make bindings symbolic.
mkSymbolic [''Binding]
-- | Look up a variable in the binding list. If it's not in the list, then it's false.
lookUp :: SInteger -> SList Binding -> SBool
lookUp = smtFunction "lookUp"
$ \vid bs -> [sCase| bs of
[] -> sFalse
Binding bId bVal : rest | vid .== bId -> bVal
| True -> lookUp vid rest
|]
-- | Check if a variable is assigned in the bindings.
isAssigned :: SInteger -> SList Binding -> SBool
isAssigned = smtFunction "isAssigned"
$ \vid bs -> [sCase| bs of
[] -> sFalse
Binding bId _ : rst | bId .== vid -> sTrue
| True -> isAssigned vid rst
|]
-- | Add a binding assuming the variable is true.
assumeTrue :: SInteger -> SList Binding -> SList Binding
assumeTrue vid bs = sBinding vid sTrue .: bs
-- | Add a binding assuming the variable is false.
assumeFalse :: SInteger -> SList Binding -> SList Binding
assumeFalse vid bs = sBinding vid sFalse .: bs
-- | Adding a binding preserves existing assignments.
--
-- >>> runTP isAssignedExtends
-- Lemma: isAssignedExtends Q.E.D.
-- Functions proven terminating: isAssigned
-- [Proven] isAssignedExtends :: Ɐi ∷ Integer → Ɐn ∷ Integer → Ɐv ∷ Bool → Ɐbs ∷ [Binding] → Bool
isAssignedExtends :: TP (Proof (Forall "i" Integer -> Forall "n" Integer -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool))
isAssignedExtends = lemma "isAssignedExtends"
(\(Forall i) (Forall n) (Forall v) (Forall bs) -> isAssigned i bs .=> isAssigned i (sBinding n v .: bs))
[]
-- | Looking up a variable in extended bindings: if already assigned, value is preserved.
--
-- >>> runTP lookUpExtends
-- Lemma: lookUpExtends Q.E.D.
-- Functions proven terminating: isAssigned, lookUp
-- [Proven] lookUpExtends :: Ɐi ∷ Integer → Ɐn ∷ Integer → Ɐv ∷ Bool → Ɐbs ∷ [Binding] → Bool
lookUpExtends :: TP (Proof (Forall "i" Integer -> Forall "n" Integer -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool))
lookUpExtends = lemma "lookUpExtends"
(\(Forall i) (Forall n) (Forall v) (Forall bs) ->
isAssigned i bs .&& i ./= n .=> lookUp i (sBinding n v .: bs) .== lookUp i bs)
[]
-- | Looking up a variable that was just added returns the added value.
--
-- >>> runTP lookUpSame
-- Lemma: lookUpSame Q.E.D.
-- Functions proven terminating: lookUp
-- [Proven] lookUpSame :: Ɐn ∷ Integer → Ɐv ∷ Bool → Ɐbs ∷ [Binding] → Bool
lookUpSame :: TP (Proof (Forall "n" Integer -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool))
lookUpSame = lemma "lookUpSame" (\(Forall n) (Forall v) (Forall bs) -> lookUp n (sBinding n v .: bs) .== v) []
-- | Adding a binding for a variable makes it assigned.
--
-- >>> runTP isAssignedSame
-- Lemma: isAssignedSame Q.E.D.
-- Functions proven terminating: isAssigned
-- [Proven] isAssignedSame :: Ɐn ∷ Integer → Ɐv ∷ Bool → Ɐbs ∷ [Binding] → Bool
isAssignedSame :: TP (Proof (Forall "n" Integer -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool))
isAssignedSame = lemma "isAssignedSame" (\(Forall n) (Forall v) (Forall bs) -> isAssigned n (sBinding n v .: bs)) []
-- * Formula evaluation
-- | Evaluate a formula under a binding environment.
eval :: SFormula -> SList Binding -> SBool
eval = smtFunction "eval"
$ \f bs -> [sCase| f of
Var n -> lookUp n bs
If c l r | eval c bs -> eval l bs
| True -> eval r bs
FTrue -> sTrue
FFalse -> sFalse
|]
-- * Tautology checking
-- | Check if a normalized formula is a tautology.
isTautology' :: SFormula -> SList Binding -> SBool
isTautology' = smtFunction "isTautology'" $ \f bs ->
[sCase| f of
-- Trivial cases
FTrue -> sTrue
FFalse -> sFalse
-- Variable
Var _ -> eval f bs
-- Constant branches
If FTrue l _ -> isTautology' l bs
If FFalse _ r -> isTautology' r bs
-- Branching on a variable
If (Var n) l r
-- We have already this variable, so evaluate based on the current choice
| isAssigned n bs, eval (sVar n) bs -> isTautology' l bs
| isAssigned n bs -> isTautology' r bs
-- We haven't yet assigned this variable. Both branches should work out:
| True -> isTautology' l (assumeTrue n bs)
.&& isTautology' r (assumeFalse n bs)
If _ _ _ -> sFalse -- Contradicts isNormal assumption
|]
-- | Main tautology checker.
isTautology :: SFormula -> SBool
isTautology f = isTautology' (normalize f) []
-- * Soundness
-- | \(\mathit{lookUp}(x, a \mathbin{+\!\!+} b) = \mathit{if } \mathit{isAssigned}(x, a) \mathit{ then } \mathit{lookUp}(x, a) \mathit{ else } \mathit{lookUp}(x, b)\)
--
-- If we look up a variable in a concatenated binding list, we first check
-- the first list, and only if not found there, check the second.
--
-- >>> runTP lookUpStable
-- Inductive lemma: lookUpStable
-- Step: Base Q.E.D.
-- Step: 1 (2 way case split)
-- Step: 1.1.1 Q.E.D.
-- Step: 1.1.2 Q.E.D.
-- Step: 1.2.1 Q.E.D.
-- Step: 1.2.2 Q.E.D.
-- Step: 1.Completeness Q.E.D.
-- Result: Q.E.D.
-- Functions proven terminating: isAssigned, lookUp
-- [Proven] lookUpStable :: Ɐa ∷ [Binding] → Ɐx ∷ Integer → Ɐb ∷ [Binding] → Bool
lookUpStable :: TP (Proof (Forall "a" [Binding] -> Forall "x" Integer -> Forall "b" [Binding] -> SBool))
lookUpStable =
induct "lookUpStable"
(\(Forall a) (Forall x) (Forall b) -> lookUp x (a ++ b) .== ite (isAssigned x a) (lookUp x a) (lookUp x b)) $
\ih (binding, a) x b ->
let vid = svarId binding
val = svalue binding
in [] |- lookUp x ((binding .: a) ++ b)
=: cases [ vid .== x ==> ite (isAssigned x (binding .: a)) (lookUp x (binding .: a)) (lookUp x b)
=: val
=: qed
, vid ./= x ==> lookUp x (a ++ b)
?? ih
=: ite (isAssigned x a) (lookUp x a) (lookUp x b)
=: qed
]
-- | \(\mathit{lookUp}(x, a) \implies \mathit{isAssigned}(x, a)\)
--
-- >>> runTP trueIsAssigned
-- Inductive lemma: trueIsAssigned
-- Step: Base Q.E.D.
-- Step: 1 (2 way case split)
-- Step: 1.1 Q.E.D.
-- Step: 1.2.1 Q.E.D.
-- Step: 1.2.2 Q.E.D.
-- Step: 1.Completeness Q.E.D.
-- Result: Q.E.D.
-- Functions proven terminating: isAssigned, lookUp
-- [Proven] trueIsAssigned :: Ɐa ∷ [Binding] → Ɐx ∷ Integer → Bool
trueIsAssigned :: TP (Proof (Forall "a" [Binding] -> Forall "x" Integer -> SBool))
trueIsAssigned =
induct "trueIsAssigned"
(\(Forall a) (Forall x) -> lookUp x a .=> isAssigned x a) $
\ih (binding, a) x ->
let vid = [sCase| binding of Binding v _ -> v|]
in [lookUp x (binding .: a)]
|- isAssigned x (binding .: a)
=: cases [ vid .== x ==> trivial
, vid ./= x ==> isAssigned x a
?? ih
=: sTrue
=: qed
]
-- | \(\mathit{value} = \mathit{lookUp}(x, bs) \implies \mathit{eval}(f, \{x \mapsto \mathit{value}\} :: bs) = \mathit{eval}(f, bs)\)
--
-- If we add a redundant binding (same id and value) to the front, evaluation doesn't change.
--
-- >>> runTPWith cvc5 evalStable
-- Lemma: ifComplexityPos Q.E.D.
-- Lemma: ifComplexitySmaller Q.E.D.
-- Inductive lemma (strong): evalStable
-- Step: Measure is non-negative Q.E.D.
-- Step: 1 (4 way case split)
-- Step: 1.1 Q.E.D.
-- Step: 1.2 Q.E.D.
-- Step: 1.3 Q.E.D.
-- Step: 1.4.1 Q.E.D.
-- Step: 1.4.2 Q.E.D.
-- Step: 1.4.3 Q.E.D.
-- Step: 1.4.4 Q.E.D.
-- Step: 1.4.5 Q.E.D.
-- Step: 1.4.6 Q.E.D.
-- Step: 1.Completeness Q.E.D.
-- Result: Q.E.D.
-- Functions proven terminating: eval, ifComplexity, lookUp
-- [Proven] evalStable :: Ɐf ∷ Formula → Ɐx ∷ Integer → Ɐv ∷ Bool → Ɐbs ∷ [Binding] → Bool
evalStable :: TP (Proof (Forall "f" Formula -> Forall "x" Integer -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool))
evalStable = do
icp <- recall ifComplexityPos
ibs <- recall ifComplexitySmaller
sInduct "evalStable"
(\(Forall f) (Forall x) (Forall v) (Forall bs) -> v .== lookUp x bs .=> eval f (sBinding x v .: bs) .== eval f bs)
(\f _ _ _ -> ifComplexity f, [proofOf icp]) $
\ih f x v bs ->
let b = sBinding x v
in [v .== lookUp x bs]
|- cases [ isFTrue f ==> trivial
, isFFalse f ==> trivial
, isVar f ==> trivial
, isIf f ==>
let c = sifCond f
l = sifThen f
r = sifElse f
in eval f (b .: bs)
=: eval (sIf c l r) (b .: bs)
=: ite (eval c (b .: bs)) (eval l (b .: bs)) (eval r (b .: bs))
?? ih `at` (Inst @"f" c, Inst @"x" x, Inst @"v" v, Inst @"bs" bs)
?? ibs `at` (Inst @"c" c, Inst @"l" l, Inst @"r" r)
=: ite (eval c bs) (eval l (b .: bs)) (eval r (b .: bs))
?? ih `at` (Inst @"f" l, Inst @"x" x, Inst @"v" v, Inst @"bs" bs)
?? ibs `at` (Inst @"c" c, Inst @"l" l, Inst @"r" r)
=: ite (eval c bs) (eval l bs) (eval r (b .: bs))
?? ih `at` (Inst @"f" r, Inst @"x" x, Inst @"v" v, Inst @"bs" bs)
?? ibs `at` (Inst @"c" c, Inst @"l" l, Inst @"r" r)
=: ite (eval c bs) (eval l bs) (eval r bs)
=: eval (sIf c l r) bs
=: qed
]
-- | Key soundness lemma: If a normalized formula is a tautology under bindings @b@,
-- then it evaluates to true under @b ++ a@ for any @a@.
--
-- >>> runTPWith (tpRibbon 50 cvc5) tautologyImpliesEval
-- Lemma: ifComplexityPos Q.E.D.
-- Lemma: ifComplexitySmaller Q.E.D.
-- Lemma: lookUpStable Q.E.D.
-- Lemma: trueIsAssigned Q.E.D.
-- Lemma: evalStable Q.E.D.
-- Inductive lemma (strong): tautologyImpliesEval
-- Step: Measure is non-negative Q.E.D.
-- Step: 1 (4 way case split)
-- Step: 1.1 Q.E.D.
-- Step: 1.2 Q.E.D.
-- Step: 1.3.1 Q.E.D.
-- Step: 1.3.2 Q.E.D.
-- Step: 1.3.3 Q.E.D.
-- Step: 1.3.4 Q.E.D.
-- Step: 1.3.5 Q.E.D.
-- Step: 1.4 (4 way case split)
-- Step: 1.4.1.1 Q.E.D.
-- Step: 1.4.1.2 Q.E.D.
-- Step: 1.4.2.1 Q.E.D.
-- Step: 1.4.2.2 Q.E.D.
-- Step: 1.4.2.3 Q.E.D.
-- Step: 1.4.3 (2 way case split)
-- Step: 1.4.3.1.1 Q.E.D.
-- Step: 1.4.3.1.2 Q.E.D.
-- Step: 1.4.3.1.3 Q.E.D.
-- Step: 1.4.3.1.4 Q.E.D.
-- Step: 1.4.3.2 (2 way case split)
-- Step: 1.4.3.2.1.1 Q.E.D.
-- Step: 1.4.3.2.1.2 Q.E.D.
-- Step: 1.4.3.2.1.3 Q.E.D.
-- Step: 1.4.3.2.1.4 Q.E.D.
-- Step: 1.4.3.2.1.5 Q.E.D.
-- Step: 1.4.3.2.1.6 Q.E.D.
-- Step: 1.4.3.2.1.7 Q.E.D.
-- Step: 1.4.3.2.1.8 Q.E.D.
-- Step: 1.4.3.2.2.1 Q.E.D.
-- Step: 1.4.3.2.2.2 Q.E.D.
-- Step: 1.4.3.2.2.3 Q.E.D.
-- Step: 1.4.3.2.2.4 Q.E.D.
-- Step: 1.4.3.2.2.5 Q.E.D.
-- Step: 1.4.3.2.2.6 Q.E.D.
-- Step: 1.4.3.2.2.7 Q.E.D.
-- Step: 1.4.3.2.2.8 Q.E.D.
-- Step: 1.4.3.2.Completeness Q.E.D.
-- Step: 1.4.3.Completeness Q.E.D.
-- Step: 1.4.4 Q.E.D.
-- Step: 1.4.Completeness Q.E.D.
-- Step: 1.Completeness Q.E.D.
-- Result: Q.E.D.
-- Functions proven terminating: eval, ifComplexity, isAssigned, isNormal, isTautology', lookUp
-- [Proven] tautologyImpliesEval :: Ɐf ∷ Formula → Ɐa ∷ [Binding] → Ɐb ∷ [Binding] → Bool
tautologyImpliesEval :: TP (Proof (Forall "f" Formula -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool))
tautologyImpliesEval = do
icp <- recall ifComplexityPos
ibs <- recall ifComplexitySmaller
lus <- recall lookUpStable
tia <- recall trueIsAssigned
evs <- recall evalStable
sInduct "tautologyImpliesEval"
(\(Forall f) (Forall a) (Forall b) -> isNormal f .&& isTautology' f b .=> eval f (b ++ a))
(\f _ _ -> ifComplexity f, [proofOf icp]) $
\ih f a b ->
[isNormal f, isTautology' f b]
|- cases [ isFTrue f ==> trivial
, isFFalse f ==> trivial
, isVar f ==> let n = sfVar f
in eval f (b ++ a)
=: eval (sVar n) (b ++ a)
=: lookUp n (b ++ a)
?? lus `at` (Inst @"a" b, Inst @"x" n, Inst @"b" a)
=: ite (isAssigned n b) (lookUp n b) (lookUp n a)
?? tia `at` (Inst @"a" b, Inst @"x" n)
=: lookUp n b
=: sTrue
=: qed
, isIf f ==>
let c = sifCond f
l = sifThen f
r = sifElse f
in cases [ isFTrue c ==> eval (sIf c l r) (b ++ a)
=: ite (eval c (b ++ a)) (eval l (b ++ a)) (eval r (b ++ a))
?? ibs `at` (Inst @"c" c, Inst @"l" l, Inst @"r" r)
?? ih `at` (Inst @"f" l, Inst @"a" a, Inst @"b" b)
=: sTrue
=: qed
, isFFalse c ==> eval (sIf c l r) (b ++ a)
=: ite (eval c (b ++ a)) (eval l (b ++ a)) (eval r (b ++ a))
=: eval r (b ++ a)
?? ibs `at` (Inst @"c" c, Inst @"l" l, Inst @"r" r)
?? ih `at` (Inst @"f" r, Inst @"a" a, Inst @"b" b)
=: sTrue
=: qed
, isVar c ==> let n = sfVar c
in cases [ isAssigned n b ==>
eval (sIf (sVar n) l r) (b ++ a)
=: ite (eval (sVar n) (b ++ a)) (eval l (b ++ a)) (eval r (b ++ a))
=: ite (lookUp n (b ++ a)) (eval l (b ++ a)) (eval r (b ++ a))
?? lus `at` (Inst @"a" b, Inst @"x" n, Inst @"b" a)
=: ite (lookUp n b) (eval l (b ++ a)) (eval r (b ++ a))
?? ibs `at` (Inst @"c" c, Inst @"l" l, Inst @"r" r)
?? ih `at` (Inst @"f" l, Inst @"a" a, Inst @"b" b)
?? ih `at` (Inst @"f" r, Inst @"a" a, Inst @"b" b)
=: sTrue
=: qed
, sNot (isAssigned n b) ==>
cases [ lookUp n a ==>
eval (sIf (sVar n) l r) (b ++ a)
=: ite (eval (sVar n) (b ++ a)) (eval l (b ++ a)) (eval r (b ++ a))
=: ite (lookUp n (b ++ a)) (eval l (b ++ a)) (eval r (b ++ a))
?? lus `at` (Inst @"a" b, Inst @"x" n, Inst @"b" a)
=: ite (lookUp n a) (eval l (b ++ a)) (eval r (b ++ a))
=: eval l (b ++ a)
?? evs `at` (Inst @"f" l, Inst @"x" n, Inst @"v" (lookUp n a), Inst @"bs" (b ++ a))
?? lus `at` (Inst @"a" b, Inst @"x" n, Inst @"b" a)
=: eval l (sBinding n (lookUp n a) .: (b ++ a))
=: eval l (sBinding n sTrue .: (b ++ a))
=: eval l (assumeTrue n b ++ a)
?? ibs `at` (Inst @"c" c, Inst @"l" l, Inst @"r" r)
?? ih `at` (Inst @"f" l, Inst @"a" a, Inst @"b" (assumeTrue n b))
=: sTrue
=: qed
, sNot (lookUp n a) ==>
eval (sIf (sVar n) l r) (b ++ a)
=: ite (eval (sVar n) (b ++ a)) (eval l (b ++ a)) (eval r (b ++ a))
=: ite (lookUp n (b ++ a)) (eval l (b ++ a)) (eval r (b ++ a))
?? lus `at` (Inst @"a" b, Inst @"x" n, Inst @"b" a)
=: ite (lookUp n a) (eval l (b ++ a)) (eval r (b ++ a))
=: eval r (b ++ a)
?? evs `at` (Inst @"f" r, Inst @"x" n, Inst @"v" (lookUp n a), Inst @"bs" (b ++ a))
?? lus `at` (Inst @"a" b, Inst @"x" n, Inst @"b" a)
=: eval r (sBinding n (lookUp n a) .: (b ++ a))
=: eval r (sBinding n sFalse .: (b ++ a))
=: eval r (assumeFalse n b ++ a)
?? ibs `at` (Inst @"c" c, Inst @"l" l, Inst @"r" r)
?? ih `at` (Inst @"f" r, Inst @"a" a, Inst @"b" (assumeFalse n b))
=: sTrue
=: qed
]
]
, isIf c ==> trivial -- Contradicts isNormal
]
]
-- * Normalization correctness
-- | \(\mathit{isNormal}(\mathit{normalize}(f))\)
--
-- Normalization produces normalized formulas.
--
-- >>> runTPWith (tpRibbon 50 z3) normalizeCorrect
-- Lemma: ifComplexityPos Q.E.D.
-- Lemma: ifComplexitySmaller Q.E.D.
-- Lemma: normalizePreservesComplexity Q.E.D.
-- Lemma: ifDepthNonNeg Q.E.D.
-- Inductive lemma (strong): normalizeCorrect
-- Step: Measure is non-negative Q.E.D.
-- Step: 1 (4 way case split)
-- Step: 1.1 Q.E.D.
-- Step: 1.2 Q.E.D.
-- Step: 1.3 Q.E.D.
-- Step: 1.4 (2 way case split)
-- Step: 1.4.1.1 Q.E.D.
-- Step: 1.4.1.2 Q.E.D.
-- Step: 1.4.2.1 Q.E.D.
-- Step: 1.4.2.2 Q.E.D.
-- Step: 1.4.2.3 Q.E.D.
-- Step: 1.4.2.4 Q.E.D.
-- Step: 1.4.2.5 Q.E.D.
-- Step: 1.4.Completeness Q.E.D.
-- Step: 1.Completeness Q.E.D.
-- Result: Q.E.D.
-- Functions proven terminating: ifComplexity, ifDepth, isNormal, normalize
-- [Proven] normalizeCorrect :: Ɐf ∷ Formula → Bool
normalizeCorrect :: TP (Proof (Forall "f" Formula -> SBool))
normalizeCorrect = do
icp <- recall ifComplexityPos
ibs <- recall ifComplexitySmaller
npc <- recall normalizePreservesComplexity
idn <- recall ifDepthNonNeg
sInductWith cvc5 "normalizeCorrect"
(\(Forall f) -> isNormal (normalize f))
(\f -> tuple (ifComplexity f, ifDepth f), [proofOf icp, proofOf idn]) $
\ih f -> []
|- isNormal (normalize f)
=: cases [ isFTrue f ==> trivial
, isFFalse f ==> trivial
, isVar f ==> trivial
, isIf f ==> let c = sifCond f
l = sifThen f
r = sifElse f
in cases [ isIf c ==>
let p = sifCond c
q = sifThen c
rc = sifElse c
transformed = sIf p (sIf q l r) (sIf rc l r)
in isNormal (normalize transformed)
?? npc `at` (Inst @"p" p, Inst @"q" q, Inst @"s" rc, Inst @"l" l, Inst @"r" r)
?? ih `at` Inst @"f" transformed
=: sTrue
=: qed
, sNot (isIf c) ==>
isNormal (sIf c (normalize l) (normalize r))
=: sNot (isIf c) .&& isNormal (normalize l) .&& isNormal (normalize r)
=: isNormal (normalize l) .&& isNormal (normalize r)
?? ibs `at` (Inst @"c" c, Inst @"l" l, Inst @"r" r)
?? ih `at` Inst @"f" l
=: isNormal (normalize r)
?? ibs `at` (Inst @"c" c, Inst @"l" l, Inst @"r" r)
?? ih `at` Inst @"f" r
=: sTrue
=: qed
]
]
-- | \(\mathit{isNormal}(f) \implies \mathit{normalize}(f) = f\)
--
-- Normalizing a normalized formula is the identity.
--
-- >>> runTPWith (tpRibbon 50 z3) normalizeSame
-- Lemma: ifComplexityPos Q.E.D.
-- Lemma: ifComplexitySmaller Q.E.D.
-- Inductive lemma (strong): normalizeSame
-- Step: Measure is non-negative Q.E.D.
-- Step: 1 (4 way case split)
-- Step: 1.1 Q.E.D.
-- Step: 1.2 Q.E.D.
-- Step: 1.3 Q.E.D.
-- Step: 1.4.1 Q.E.D.
-- Step: 1.4.2 Q.E.D.
-- Step: 1.Completeness Q.E.D.
-- Result: Q.E.D.
-- Functions proven terminating: ifComplexity, isNormal, normalize
-- [Proven] normalizeSame :: Ɐf ∷ Formula → Bool
normalizeSame :: TP (Proof (Forall "f" Formula -> SBool))
normalizeSame = do
icp <- recall ifComplexityPos
ibs <- recall ifComplexitySmaller
sInduct "normalizeSame"
(\(Forall f) -> isNormal f .=> normalize f .== f)
(ifComplexity, [proofOf icp]) $
\ih f -> [isNormal f]
|- cases [ isFTrue f ==> trivial
, isFFalse f ==> trivial
, isVar f ==> trivial
, isIf f ==> let c = sifCond f
l = sifThen f
r = sifElse f
in sIf c (normalize l) (normalize r)
?? ibs `at` (Inst @"c" c, Inst @"l" l, Inst @"r" r)
?? ih `at` Inst @"f" l
=: sIf c l (normalize r)
?? ibs `at` (Inst @"c" c, Inst @"l" l, Inst @"r" r)
?? ih `at` Inst @"f" r
=: sIf c l r
=: qed
]
-- | \(\mathit{eval}(\mathit{normalize}(f), bs) = \mathit{eval}(f, bs)\)
--
-- Normalization preserves semantics.
--
-- >>> runTPWith (tpRibbon 50 z3) normalizeRespectsTruth
-- Lemma: ifComplexityPos Q.E.D.
-- Lemma: ifComplexitySmaller Q.E.D.
-- Lemma: normalizePreservesComplexity Q.E.D.
-- Lemma: ifDepthNonNeg Q.E.D.
-- Inductive lemma (strong): normalizeRespectsTruth
-- Step: Measure is non-negative Q.E.D.
-- Step: 1 (4 way case split)
-- Step: 1.1 Q.E.D.
-- Step: 1.2 Q.E.D.
-- Step: 1.3 Q.E.D.
-- Step: 1.4 (2 way case split)
-- Step: 1.4.1 Q.E.D.
-- Step: 1.4.2.1 Q.E.D.
-- Step: 1.4.2.2 Q.E.D.
-- Step: 1.4.2.3 Q.E.D.
-- Step: 1.4.Completeness Q.E.D.
-- Step: 1.Completeness Q.E.D.
-- Result: Q.E.D.
-- Functions proven terminating: eval, ifComplexity, ifDepth, lookUp, normalize
-- [Proven] normalizeRespectsTruth :: Ɐf ∷ Formula → Ɐbs ∷ [Binding] → Bool
normalizeRespectsTruth :: TP (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
normalizeRespectsTruth = do
icp <- recall ifComplexityPos
ibs <- recall ifComplexitySmaller
npc <- recall normalizePreservesComplexity
idn <- recall ifDepthNonNeg
sInductWith cvc5 "normalizeRespectsTruth"
(\(Forall f) (Forall bs) -> eval (normalize f) bs .== eval f bs)
(\f _ -> tuple (ifComplexity f, ifDepth f), [proofOf icp, proofOf idn]) $
\ih f bs -> []
|- cases [ isFTrue f ==> trivial
, isFFalse f ==> trivial
, isVar f ==> trivial
, isIf f ==> let c = sifCond f
l = sifThen f
r = sifElse f
in cases [ isIf c ==>
let p = sifCond c
q = sifThen c
rc = sifElse c
transformed = sIf p (sIf q l r) (sIf rc l r)
in eval (normalize (sIf c l r)) bs .== eval (sIf c l r) bs
?? npc `at` (Inst @"p" p, Inst @"q" q, Inst @"s" rc, Inst @"l" l, Inst @"r" r)
?? ih `at` (Inst @"f" transformed, Inst @"bs" bs)
=: sTrue
=: qed
, sNot (isIf c) ==>
eval (normalize (sIf c l r)) bs .== eval (sIf c l r) bs
=: eval (sIf c (normalize l) (normalize r)) bs .== eval (sIf c l r) bs
=: ite (eval c bs) (eval (normalize l) bs) (eval (normalize r) bs) .== ite (eval c bs) (eval l bs) (eval r bs)
?? ibs `at` (Inst @"c" c, Inst @"l" l, Inst @"r" r)
?? ih `at` (Inst @"f" l, Inst @"bs" bs)
?? ih `at` (Inst @"f" r, Inst @"bs" bs)
=: sTrue
=: qed
]
]
-- * Main soundness theorem
-- | \(\mathit{isTautology}(f) \implies \mathit{eval}(f, \mathit{bindings})\)
--
-- If the tautology checker says a formula is a tautology, then it evaluates
-- to true under any binding environment. This is the soundness theorem.
--
-- >>> runTP soundness
-- Lemma: tautologyImpliesEval Q.E.D.
-- Lemma: normalizeRespectsTruth Q.E.D.
-- Lemma: normalizeCorrect Q.E.D.
-- Lemma: soundness
-- Step: 1 Q.E.D.
-- Step: 2 Q.E.D.
-- Result: Q.E.D.
-- Functions proven terminating: eval, ifComplexity, ifDepth, isAssigned, isNormal, isTautology', lookUp, normalize
-- [Proven] soundness :: Ɐf ∷ Formula → Ɐbindings ∷ [Binding] → Bool
soundness :: TP (Proof (Forall "f" Formula -> Forall "bindings" [Binding] -> SBool))
soundness = do
tie <- recallWith cvc5 tautologyImpliesEval
nrt <- recall normalizeRespectsTruth
nc <- recall normalizeCorrect
calc "soundness"
(\(Forall f) (Forall bindings) -> isTautology f .=> eval f bindings) $
\f bindings -> [isTautology f]
|- eval f bindings
?? nrt `at` (Inst @"f" f, Inst @"bs" bindings)
=: eval (normalize f) bindings
?? nc `at` Inst @"f" f
?? tie `at` (Inst @"f" (normalize f), Inst @"a" bindings, Inst @"b" [])
=: sTrue
=: qed
-- * Completeness
-- | Result of attempting to falsify a formula.
data FalsifyResult = FalsifyResult { falsified :: Bool
, cex :: [Binding]
}
-- | Make FalsifyResult symbolic.
mkSymbolic [''FalsifyResult]
-- | Attempt to falsify a normalized formula under given bindings.
-- Returns whether falsification succeeded and the counterexample bindings.
falsify' :: SFormula -> SList Binding -> SFalsifyResult
falsify' = smtFunction "falsify'" $ \f bs ->
[sCase| f of
FTrue -> sFalsifyResult sFalse []
FFalse -> sFalsifyResult sTrue bs
Var i
| isAssigned i bs, eval (sVar i) bs -> sFalsifyResult sFalse []
| isAssigned i bs -> sFalsifyResult sTrue bs
| True -> sFalsifyResult sTrue (sBinding i sFalse .: bs)
If (Var i) l r
| isAssigned i bs, eval (sVar i) bs -> falsify' l bs
| isAssigned i bs -> falsify' r bs
| True -> let resL = falsify' l (assumeTrue i bs)
in ite (sNot (sfalsified resL))
(falsify' r (assumeFalse i bs))
resL
If FTrue l _ -> falsify' l bs
If FFalse _ r -> falsify' r bs
If _ _ _ -> sFalsifyResult sFalse [] -- Shouldn't happen for normal formulas
|]
-- | Falsify a formula by first normalizing it.
falsify :: SFormula -> SFalsifyResult
falsify f = falsify' (normalize f) []
-- * Completeness lemmas
-- | If a normalized formula is not a tautology, then falsify' returns falsified = true.
--
-- >>> runTPWith (tpRibbon 50 cvc5) nonTautIsFalsified
-- Lemma: ifComplexityPos Q.E.D.
-- Lemma: ifComplexitySmaller Q.E.D.
-- Inductive lemma (strong): nonTautIsFalsified
-- Step: Measure is non-negative Q.E.D.
-- Step: 1 (4 way case split)
-- Step: 1.1 Q.E.D.
-- Step: 1.2 Q.E.D.
-- Step: 1.3 Q.E.D.
-- Step: 1.4 Q.E.D.
-- Step: 1.Completeness Q.E.D.
-- Result: Q.E.D.
-- Functions proven terminating: eval, falsify', ifComplexity, isAssigned, isNormal, isTautology', lookUp
-- [Proven] nonTautIsFalsified :: Ɐf ∷ Formula → Ɐbs ∷ [Binding] → Bool
nonTautIsFalsified :: TP (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
nonTautIsFalsified = do
icp <- recall ifComplexityPos
ibs <- recall ifComplexitySmaller
sInduct "nonTautIsFalsified"
(\(Forall f) (Forall bs) -> isNormal f .&& sNot (isTautology' f bs) .=> sfalsified (falsify' f bs))
(\f _ -> ifComplexity f, [proofOf icp]) $
\ih f bs -> [isNormal f, sNot (isTautology' f bs)]
|- cases [ isFTrue f ==> trivial
, isFFalse f ==> trivial
, isVar f ==> trivial
, isIf f ==> let c = sifCond f
l = sifThen f
r = sifElse f
in sfalsified (falsify' f bs)
?? ibs `at` (Inst @"c" c, Inst @"l" l, Inst @"r" r)
?? ih `at` (Inst @"f" l, Inst @"bs" bs)
?? ih `at` (Inst @"f" r, Inst @"bs" bs)
?? ih `at` (Inst @"f" l, Inst @"bs" (assumeTrue (sfVar c) bs))
?? ih `at` (Inst @"f" r, Inst @"bs" (assumeFalse (sfVar c) bs))
=: sTrue
=: qed
]
-- | If a variable is assigned in the input bindings and falsify' succeeds,
-- the lookup value is preserved in the output bindings.
--
-- >>> runTPWith (tpRibbon 50 cvc5) falsifyExtendsBindings
-- Lemma: ifComplexityPos Q.E.D.
-- Lemma: ifComplexitySmaller Q.E.D.
-- Lemma: isAssignedExtends Q.E.D.
-- Lemma: lookUpExtends Q.E.D.
-- Inductive lemma (strong): falsifyExtendsBindings
-- Step: Measure is non-negative Q.E.D.
-- Step: 1 (4 way case split)
-- Step: 1.1 Q.E.D.
-- Step: 1.2 Q.E.D.
-- Step: 1.3 Q.E.D.
-- Step: 1.4 Q.E.D.
-- Step: 1.Completeness Q.E.D.
-- Result: Q.E.D.
-- Functions proven terminating: eval, falsify', ifComplexity, isAssigned, lookUp
-- [Proven] falsifyExtendsBindings :: Ɐf ∷ Formula → Ɐbs ∷ [Binding] → Ɐi ∷ Integer → Bool
falsifyExtendsBindings :: TP (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool))
falsifyExtendsBindings = do
icp <- recall ifComplexityPos
ibs <- recall ifComplexitySmaller
iae <- recall isAssignedExtends
lue <- recall lookUpExtends
sInduct "falsifyExtendsBindings"
(\(Forall f) (Forall bs) (Forall i) ->
isAssigned i bs .&& sfalsified (falsify' f bs) .=>
lookUp i (scex (falsify' f bs)) .== lookUp i bs)
(\f _ _ -> ifComplexity f, [proofOf icp]) $
\ih f bs i -> [isAssigned i bs, sfalsified (falsify' f bs)]
|- cases [ isFTrue f ==> trivial
, isFFalse f ==> trivial
, isVar f ==> let n = sfVar f
in lookUp i (scex (falsify' f bs)) .== lookUp i bs
?? lue `at` (Inst @"i" i, Inst @"n" n, Inst @"v" sFalse, Inst @"bs" bs)
=: sTrue
=: qed
, isIf f ==> let c = sifCond f
l = sifThen f
r = sifElse f
n = sfVar c
in lookUp i (scex (falsify' f bs)) .== lookUp i bs
?? ibs `at` (Inst @"c" c, Inst @"l" l, Inst @"r" r)
?? iae `at` (Inst @"i" i, Inst @"n" n, Inst @"v" sTrue, Inst @"bs" bs)
?? iae `at` (Inst @"i" i, Inst @"n" n, Inst @"v" sFalse, Inst @"bs" bs)
?? lue `at` (Inst @"i" i, Inst @"n" n, Inst @"v" sTrue, Inst @"bs" bs)
?? lue `at` (Inst @"i" i, Inst @"n" n, Inst @"v" sFalse, Inst @"bs" bs)
?? ih `at` (Inst @"f" l, Inst @"bs" bs, Inst @"i" i)
?? ih `at` (Inst @"f" r, Inst @"bs" bs, Inst @"i" i)
?? ih `at` (Inst @"f" l, Inst @"bs" (assumeTrue n bs), Inst @"i" i)
?? ih `at` (Inst @"f" r, Inst @"bs" (assumeFalse n bs), Inst @"i" i)
=: sTrue
=: qed
]
-- | If falsify' returns falsified = true, then evaluating the formula
-- with the returned bindings gives false.
--
-- >>> runTPWith (tpRibbon 50 cvc5) falsifyFalsifies
-- Lemma: ifComplexityPos Q.E.D.
-- Lemma: ifComplexitySmaller Q.E.D.
-- Lemma: falsifyExtendsBindings Q.E.D.
-- Lemma: lookUpSame Q.E.D.
-- Lemma: isAssignedSame Q.E.D.
-- Inductive lemma (strong): falsifyFalsifies
-- Step: Measure is non-negative Q.E.D.
-- Step: 1 (4 way case split)
-- Step: 1.1.1 Q.E.D.
-- Step: 1.1.2 Q.E.D.
-- Step: 1.1.3 Q.E.D.
-- Step: 1.2.1 Q.E.D.
-- Step: 1.2.2 Q.E.D.
-- Step: 1.2.3 Q.E.D.
-- Step: 1.3.1 Q.E.D.
-- Step: 1.3.2 Q.E.D.
-- Step: 1.3.3 Q.E.D.
-- Step: 1.4 (4 way case split)
-- Step: 1.4.1 Q.E.D.
-- Step: 1.4.2 Q.E.D.
-- Step: 1.4.3 (2 way case split)
-- Step: 1.4.3.1 (2 way case split)
-- Step: 1.4.3.1.1 Q.E.D.
-- Step: 1.4.3.1.2 Q.E.D.
-- Step: 1.4.3.1.Completeness Q.E.D.
-- Step: 1.4.3.2 (2 way case split)
-- Step: 1.4.3.2.1 Q.E.D.
-- Step: 1.4.3.2.2 Q.E.D.
-- Step: 1.4.3.2.Completeness Q.E.D.
-- Step: 1.4.3.Completeness Q.E.D.
-- Step: 1.4.4 Q.E.D.
-- Step: 1.4.Completeness Q.E.D.
-- Step: 1.Completeness Q.E.D.
-- Result: Q.E.D.
-- Functions proven terminating: eval, falsify', ifComplexity, isAssigned, isNormal, lookUp
-- [Proven] falsifyFalsifies :: Ɐf ∷ Formula → Ɐbs ∷ [Binding] → Bool
falsifyFalsifies :: TP (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
falsifyFalsifies = do
icp <- recall ifComplexityPos
ibs <- recall ifComplexitySmaller
feb <- recall falsifyExtendsBindings
lus <- recall lookUpSame
ias <- recall isAssignedSame
sInduct "falsifyFalsifies"
(\(Forall f) (Forall bs) -> isNormal f .&& sfalsified (falsify' f bs) .=> sNot (eval f (scex (falsify' f bs))))
(\f _ -> ifComplexity f, [proofOf icp]) $
\ih f bs -> [isNormal f, sfalsified (falsify' f bs)]
|- cases [ isFTrue f ==> sNot (eval f (scex (falsify' f bs)))
=: sNot (eval sFTrue (scex (falsify' sFTrue bs)))
=: sNot sTrue
=: sFalse
=: qed
, isFFalse f ==> sNot (eval f (scex (falsify' f bs)))
=: sNot (eval sFFalse bs)
=: sNot sFalse
=: sTrue
=: qed
, isVar f ==> let n = sfVar f
in sNot (eval f (scex (falsify' f bs)))
=: sNot (eval (sVar n) (scex (falsify' (sVar n) bs)))
=: sNot (lookUp n (scex (falsify' (sVar n) bs)))
=: sTrue
=: qed
, isIf f ==> let c = sifCond f
l = sifThen f
r = sifElse f
in cases [ isFTrue c ==> sNot (eval f (scex (falsify' f bs)))
?? ibs `at` (Inst @"c" c, Inst @"l" l, Inst @"r" r)
?? ih `at` (Inst @"f" l, Inst @"bs" bs)
=: sTrue
=: qed
, isFFalse c ==> sNot (eval f (scex (falsify' f bs)))
?? ibs `at` (Inst @"c" c, Inst @"l" l, Inst @"r" r)
?? ih `at` (Inst @"f" r, Inst @"bs" bs)
=: sTrue
=: qed
, isVar c ==> let n = sfVar c
in cases [ isAssigned n bs ==>
cases [ lookUp n bs ==>
sNot (eval f (scex (falsify' f bs)))
?? ibs `at` (Inst @"c" c, Inst @"l" l, Inst @"r" r)
?? feb `at` (Inst @"f" l, Inst @"bs" bs, Inst @"i" n)
?? ih `at` (Inst @"f" l, Inst @"bs" bs)
=: sTrue
=: qed
, sNot (lookUp n bs) ==>
sNot (eval f (scex (falsify' f bs)))
?? ibs `at` (Inst @"c" c, Inst @"l" l, Inst @"r" r)
?? feb `at` (Inst @"f" r, Inst @"bs" bs, Inst @"i" n)
?? ih `at` (Inst @"f" r, Inst @"bs" bs)
=: sTrue
=: qed
]
, sNot (isAssigned n bs) ==>
let resL = falsify' l (assumeTrue n bs)
in cases [ sfalsified resL ==>
sNot (eval f (scex (falsify' f bs)))
?? ibs `at` (Inst @"c" c, Inst @"l" l, Inst @"r" r)
?? ias `at` (Inst @"n" n, Inst @"v" sTrue, Inst @"bs" bs)
?? lus `at` (Inst @"n" n, Inst @"v" sTrue, Inst @"bs" bs)
?? feb `at` (Inst @"f" l, Inst @"bs" (assumeTrue n bs), Inst @"i" n)
?? ih `at` (Inst @"f" l, Inst @"bs" (assumeTrue n bs))
=: sTrue
=: qed
, sNot (sfalsified resL) ==>
sNot (eval f (scex (falsify' f bs)))
?? ibs `at` (Inst @"c" c, Inst @"l" l, Inst @"r" r)
?? ias `at` (Inst @"n" n, Inst @"v" sFalse, Inst @"bs" bs)
?? lus `at` (Inst @"n" n, Inst @"v" sFalse, Inst @"bs" bs)
?? feb `at` (Inst @"f" r, Inst @"bs" (assumeFalse n bs), Inst @"i" n)
?? ih `at` (Inst @"f" r, Inst @"bs" (assumeFalse n bs))
=: sTrue
=: qed
]
]
, isIf c ==> sNot (eval f (scex (falsify' f bs)))
=: sTrue -- Contradicts isNormal
=: qed
]
]
-- | Helper lemma for completeness: If a formula is not a tautology,
-- evaluating its normalization with falsify's bindings gives false.
--
-- >>> runTPWith cvc5 completenessHelper
-- Lemma: falsifyFalsifies Q.E.D.
-- Lemma: nonTautIsFalsified Q.E.D.
-- Lemma: normalizeCorrect Q.E.D.
-- Lemma: completenessHelper Q.E.D.
-- Functions proven terminating:
-- eval, falsify', ifComplexity, ifDepth, isAssigned, isNormal, isTautology', lookUp, normalize
-- [Proven] completenessHelper :: Ɐf ∷ Formula → Bool
completenessHelper :: TP (Proof (Forall "f" Formula -> SBool))
completenessHelper = do
ff <- recall falsifyFalsifies
nti <- recall nonTautIsFalsified
nc <- recallWith z3 normalizeCorrect
lemma "completenessHelper"
(\(Forall f) -> sNot (isTautology f) .=> sNot (eval (normalize f) (scex (falsify f))))
[proofOf ff, proofOf nti, proofOf nc]
-- * Main completeness theorem
-- | \(\lnot\mathit{isTautology}(f) \implies \lnot\mathit{eval}(f, \mathit{falsify}(f).\mathit{bindings})\)
--
-- If the tautology checker says a formula is not a tautology, then there exists
-- a binding environment (provided by falsify) under which it evaluates to false.
-- This is the completeness theorem.
--
-- >>> runTPWith cvc5 completeness
-- Lemma: completenessHelper Q.E.D.
-- Lemma: normalizeRespectsTruth Q.E.D.
-- Lemma: completeness Q.E.D.
-- Functions proven terminating:
-- eval, falsify', ifComplexity, ifDepth, isAssigned, isNormal, isTautology', lookUp, normalize
-- [Proven] completeness :: Ɐf ∷ Formula → Bool
completeness :: TP (Proof (Forall "f" Formula -> SBool))
completeness = do
ch <- recall completenessHelper
nrt <- recallWith z3 normalizeRespectsTruth
lemma "completeness"
(\(Forall f) -> sNot (isTautology f) .=> sNot (eval f (scex (falsify f))))
[proofOf ch, proofOf nrt]