-----------------------------------------------------------------------------
-- |
-- 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 { Formula -> Integer
fVar   :: Integer }
             | If  { Formula -> Formula
ifCond :: Formula
                   , Formula -> Formula
ifThen :: Formula
                   , Formula -> Formula
ifElse :: Formula
                   }

-- | Make formulas symbolic.
mkSymbolic [''Formula]

-- * Measuring formulas

-- | Depth of nested If constructors in the condition position.
ifDepth :: SFormula -> SInteger
ifDepth :: SBV Formula -> SBV Integer
ifDepth = String
-> (SBV Formula -> SBV Integer) -> SBV Formula -> SBV Integer
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"ifDepth" ((SBV Formula -> SBV Integer) -> SBV Formula -> SBV Integer)
-> (SBV Formula -> SBV Integer) -> SBV Formula -> SBV Integer
forall a b. (a -> b) -> a -> b
$ \SBV Formula
f -> [sCase|Formula f of
                                           If c _ _ -> 1 + ifDepth c
                                           _        -> 0
                                        |]

-- | \(\mathit{ifDepth}(f) \geq 0\)
--
-- >>> runTP ifDepthNonNeg
-- Lemma: ifDepthNonNeg                    Q.E.D.
-- [Proven] ifDepthNonNeg :: Ɐf ∷ Formula → Bool
ifDepthNonNeg :: TP (Proof (Forall "f" Formula -> SBool))
ifDepthNonNeg :: TP (Proof (Forall "f" Formula -> SBool))
ifDepthNonNeg = String
-> (Forall "f" Formula -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "f" Formula -> SBool))
forall a. Inductive a => String -> a -> [ProofObj] -> TP (Proof a)
inductiveLemma String
"ifDepthNonNeg" (\(Forall SBV Formula
f) -> SBV Formula -> SBV Integer
ifDepth SBV Formula
f SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Integer
0) []

-- | Complexity of a formula (for termination measure).
ifComplexity :: SFormula -> SInteger
ifComplexity :: SBV Formula -> SBV Integer
ifComplexity = String
-> (SBV Formula -> SBV Integer) -> SBV Formula -> SBV Integer
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"ifComplexity" ((SBV Formula -> SBV Integer) -> SBV Formula -> SBV Integer)
-> (SBV Formula -> SBV Integer) -> SBV Formula -> SBV Integer
forall a b. (a -> b) -> a -> b
$ \SBV Formula
f ->
  [sCase|Formula f of
    If c l r -> ifComplexity c * (ifComplexity l + ifComplexity r)
    _        -> 1
  |]

-- | \(\mathit{ifComplexity}(f) > 0\)
--
-- >>> runTP ifComplexityPos
-- Lemma: ifComplexityPos                  Q.E.D.
-- [Proven] ifComplexityPos :: Ɐf ∷ Formula → Bool
ifComplexityPos :: TP (Proof (Forall "f" Formula -> SBool))
ifComplexityPos :: TP (Proof (Forall "f" Formula -> SBool))
ifComplexityPos = String
-> (Forall "f" Formula -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "f" Formula -> SBool))
forall a. Inductive a => String -> a -> [ProofObj] -> TP (Proof a)
inductiveLemma String
"ifComplexityPos" (\(Forall SBV Formula
f) -> SBV Formula -> SBV Integer
ifComplexity SBV Formula
f SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Integer
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              Q.E.D.
-- [Proven] ifComplexitySmaller :: Ɐc ∷ Formula → Ɐl ∷ Formula → Ɐr ∷ Formula → Bool
ifComplexitySmaller :: TP (Proof (Forall "c" Formula -> Forall "l" Formula -> Forall "r" Formula -> SBool))
ifComplexitySmaller :: TP
  (Proof
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool))
ifComplexitySmaller = do
  Proof (Forall "f" Formula -> SBool)
icp <- String
-> TP (Proof (Forall "f" Formula -> SBool))
-> TP (Proof (Forall "f" Formula -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"ifComplexityPos" TP (Proof (Forall "f" Formula -> SBool))
ifComplexityPos

  String
-> (Forall "c" Formula
    -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "c" Formula
         -> Forall "l" Formula -> Forall "r" Formula -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"ifComplexitySmaller"
        (\(Forall SBV Formula
c) (Forall SBV Formula
l) (Forall SBV Formula
r) ->
           let ic :: SBV Integer
ic = SBV Formula -> SBV Integer
ifComplexity (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
c SBV Formula
l SBV Formula
r)
           in SBV Formula -> SBV Integer
ifComplexity SBV Formula
c SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Integer
ic SBool -> SBool -> SBool
.&& SBV Formula -> SBV Integer
ifComplexity SBV Formula
l SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Integer
ic SBool -> SBool -> SBool
.&& SBV Formula -> SBV Integer
ifComplexity SBV Formula
r SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Integer
ic)
        [Proof (Forall "f" Formula -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "f" Formula -> SBool)
icp]

-- * Normalization

-- | Check if a formula is in normal form (no nested If in condition position).
isNormal :: SFormula -> SBool
isNormal :: SBV Formula -> SBool
isNormal = String -> (SBV Formula -> SBool) -> SBV Formula -> SBool
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"isNormal" ((SBV Formula -> SBool) -> SBV Formula -> SBool)
-> (SBV Formula -> SBool) -> SBV Formula -> SBool
forall a b. (a -> b) -> a -> b
$ \SBV Formula
f ->
  [sCase|Formula 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 :: SBV Formula -> SBV Formula
normalize = String
-> (SBV Formula -> SBV Formula) -> SBV Formula -> SBV Formula
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"normalize" ((SBV Formula -> SBV Formula) -> SBV Formula -> SBV Formula)
-> (SBV Formula -> SBV Formula) -> SBV Formula -> SBV Formula
forall a b. (a -> b) -> a -> b
$ \SBV Formula
f ->
  [sCase|Formula 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.
-- [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 :: 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.
  Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "c" Integer -> SBool)
helper <- String
-> (Forall "a" Integer
    -> Forall "b" Integer -> Forall "c" Integer -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "c" Integer -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"helper"
                  (\(Forall @"a" SBV Integer
a) (Forall @"b" SBV Integer
b) (Forall @"c" SBV Integer
c) -> SBV Integer
a SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer
b SBool -> SBool -> SBool
.=> SBV Integer
a SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer
c SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* (SBV Integer
c :: SInteger))
                  []

  String
-> (Forall "p" Formula
    -> Forall "q" Formula
    -> Forall "s" Formula
    -> Forall "l" Formula
    -> Forall "r" Formula
    -> SBool)
-> StepArgs
     (Forall "p" Formula
      -> Forall "q" Formula
      -> Forall "s" Formula
      -> Forall "l" Formula
      -> Forall "r" Formula
      -> SBool)
     Integer
-> TP
     (Proof
        (Forall "p" Formula
         -> Forall "q" Formula
         -> Forall "s" Formula
         -> Forall "l" Formula
         -> Forall "r" Formula
         -> SBool))
forall t.
(Proposition
   (Forall "p" Formula
    -> Forall "q" Formula
    -> Forall "s" Formula
    -> Forall "l" Formula
    -> Forall "r" Formula
    -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "p" Formula
    -> Forall "q" Formula
    -> Forall "s" Formula
    -> Forall "l" Formula
    -> Forall "r" Formula
    -> SBool)
-> StepArgs
     (Forall "p" Formula
      -> Forall "q" Formula
      -> Forall "s" Formula
      -> Forall "l" Formula
      -> Forall "r" Formula
      -> SBool)
     t
-> TP
     (Proof
        (Forall "p" Formula
         -> Forall "q" Formula
         -> Forall "s" Formula
         -> Forall "l" Formula
         -> Forall "r" Formula
         -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"normalizePreservesComplexity"
       (\(Forall SBV Formula
p) (Forall SBV Formula
q) (Forall SBV Formula
s) (Forall SBV Formula
l) (Forall SBV Formula
r) ->
          SBV Formula -> SBV Integer
ifComplexity (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
p (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
q SBV Formula
l SBV Formula
r) (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
s SBV Formula
l SBV Formula
r)) SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Formula -> SBV Integer
ifComplexity (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
p SBV Formula
q SBV Formula
s) SBV Formula
l SBV Formula
r)) (StepArgs
   (Forall "p" Formula
    -> Forall "q" Formula
    -> Forall "s" Formula
    -> Forall "l" Formula
    -> Forall "r" Formula
    -> SBool)
   Integer
 -> TP
      (Proof
         (Forall "p" Formula
          -> Forall "q" Formula
          -> Forall "s" Formula
          -> Forall "l" Formula
          -> Forall "r" Formula
          -> SBool)))
-> StepArgs
     (Forall "p" Formula
      -> Forall "q" Formula
      -> Forall "s" Formula
      -> Forall "l" Formula
      -> Forall "r" Formula
      -> SBool)
     Integer
-> TP
     (Proof
        (Forall "p" Formula
         -> Forall "q" Formula
         -> Forall "s" Formula
         -> Forall "l" Formula
         -> Forall "r" Formula
         -> SBool))
forall a b. (a -> b) -> a -> b
$
       \SBV Formula
p SBV Formula
q SBV Formula
s SBV Formula
l SBV Formula
r ->
         let cp :: SBV Integer
cp = SBV Formula -> SBV Integer
ifComplexity SBV Formula
p
             cq :: SBV Integer
cq = SBV Formula -> SBV Integer
ifComplexity SBV Formula
q
             cs :: SBV Integer
cs = SBV Formula -> SBV Integer
ifComplexity SBV Formula
s
             cl :: SBV Integer
cl = SBV Formula -> SBV Integer
ifComplexity SBV Formula
l
             cr :: SBV Integer
cr = SBV Formula -> SBV Integer
ifComplexity SBV Formula
r
         in [] [SBool]
-> TPProofRaw (SBV Integer) -> (SBool, TPProofRaw (SBV Integer))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV Formula -> SBV Integer
ifComplexity (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
p (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
q SBV Formula
l SBV Formula
r) (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
s SBV Formula
l SBV Formula
r))
               SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Integer
cp SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* (SBV Formula -> SBV Integer
ifComplexity (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
q SBV Formula
l SBV Formula
r) SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Formula -> SBV Integer
ifComplexity (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
s SBV Formula
l SBV Formula
r))
               SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Integer
cp SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* (SBV Integer
cq SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* (SBV Integer
cl SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
cr) SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
cs SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* (SBV Integer
cl SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
cr))
               SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Integer
cp SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* ((SBV Integer
cq SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
cs) SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* (SBV Integer
cl SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
cr))
               SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Integer
cp SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* (SBV Integer
cq SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
cs)) SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* (SBV Integer
cl SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
cr)
               SBV Integer -> Proof Bool -> Hinted (SBV Integer)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "c" Integer -> SBool)
helper Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "c" Integer -> SBool)
-> IArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "c" Integer -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"a" (SBV Formula -> SBV Integer
ifComplexity (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
p SBV Formula
q SBV Formula
s)), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" (SBV Integer
cp SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* (SBV Integer
cq SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
cs)), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"c" (SBV Integer
cl SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
cr))
               TPProofRaw (SBV Integer)
-> ChainsTo (TPProofRaw (SBV Integer))
-> ChainsTo (TPProofRaw (SBV Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Formula -> SBV Integer
ifComplexity (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
p SBV Formula
q SBV Formula
s) SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* (SBV Integer
cl SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
cr)
               SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Formula -> SBV Integer
ifComplexity (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
p SBV Formula
q SBV Formula
s) SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* (SBV Formula -> SBV Integer
ifComplexity SBV Formula
l SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Formula -> SBV Integer
ifComplexity SBV Formula
r)
               SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Formula -> SBV Integer
ifComplexity (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
p SBV Formula
q SBV Formula
s) SBV Formula
l SBV Formula
r)
               SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV Integer)
TPProofRaw (SBV Integer)
forall a. TPProofRaw a
qed

-- * Variable bindings

-- | A binding associates a variable ID with a boolean value.
data Binding = Binding { Binding -> Integer
varId :: Integer
                       , Binding -> Bool
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 :: SBV Integer -> SList Binding -> SBool
lookUp = String
-> (SBV Integer -> SList Binding -> SBool)
-> SBV Integer
-> SList Binding
-> SBool
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"lookUp" ((SBV Integer -> SList Binding -> SBool)
 -> SBV Integer -> SList Binding -> SBool)
-> (SBV Integer -> SList Binding -> SBool)
-> SBV Integer
-> SList Binding
-> SBool
forall a b. (a -> b) -> a -> b
$ \SBV Integer
vid SList Binding
bs ->
  SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList Binding -> SBool
forall a. SymVal a => SList a -> SBool
null SList Binding
bs)
      SBool
sFalse
      [sCase|Binding (head bs) of
         Binding bId bVal -> ite (vid .== bId)
                                 bVal
                                 (lookUp vid (tail bs))
      |]

-- | Check if a variable is assigned in the bindings.
isAssigned :: SInteger -> SList Binding -> SBool
isAssigned :: SBV Integer -> SList Binding -> SBool
isAssigned = String
-> (SBV Integer -> SList Binding -> SBool)
-> SBV Integer
-> SList Binding
-> SBool
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"isAssigned" ((SBV Integer -> SList Binding -> SBool)
 -> SBV Integer -> SList Binding -> SBool)
-> (SBV Integer -> SList Binding -> SBool)
-> SBV Integer
-> SList Binding
-> SBool
forall a b. (a -> b) -> a -> b
$ \SBV Integer
vid SList Binding
bs ->
  SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList Binding -> SBool
forall a. SymVal a => SList a -> SBool
null SList Binding
bs)
      SBool
sFalse
      [sCase|Binding (head bs) of
         Binding bId _ -> bId .== vid .|| isAssigned vid (tail bs)
      |]

-- | Add a binding assuming the variable is true.
assumeTrue :: SInteger -> SList Binding -> SList Binding
assumeTrue :: SBV Integer -> SList Binding -> SList Binding
assumeTrue SBV Integer
vid SList Binding
bs = SBV Integer -> SBool -> SBV Binding
sBinding SBV Integer
vid SBool
sTrue SBV Binding -> SList Binding -> SList Binding
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Binding
bs

-- | Add a binding assuming the variable is false.
assumeFalse :: SInteger -> SList Binding -> SList Binding
assumeFalse :: SBV Integer -> SList Binding -> SList Binding
assumeFalse SBV Integer
vid SList Binding
bs = SBV Integer -> SBool -> SBV Binding
sBinding SBV Integer
vid SBool
sFalse SBV Binding -> SList Binding -> SList Binding
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Binding
bs

-- | Adding a binding preserves existing assignments.
--
-- >>> runTP isAssignedExtends
-- Lemma: isAssignedExtends                Q.E.D.
-- [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 :: TP
  (Proof
     (Forall "i" Integer
      -> Forall "n" Integer
      -> Forall "v" Bool
      -> Forall "bs" [Binding]
      -> SBool))
isAssignedExtends = String
-> (Forall "i" Integer
    -> Forall "n" Integer
    -> Forall "v" Bool
    -> Forall "bs" [Binding]
    -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "i" Integer
         -> Forall "n" Integer
         -> Forall "v" Bool
         -> Forall "bs" [Binding]
         -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"isAssignedExtends"
                          (\(Forall SBV Integer
i) (Forall SBV Integer
n) (Forall SBool
v) (Forall SList Binding
bs) -> SBV Integer -> SList Binding -> SBool
isAssigned SBV Integer
i SList Binding
bs SBool -> SBool -> SBool
.=> SBV Integer -> SList Binding -> SBool
isAssigned SBV Integer
i (SBV Integer -> SBool -> SBV Binding
sBinding SBV Integer
n SBool
v SBV Binding -> SList Binding -> SList Binding
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Binding
bs))
                          []

-- | Looking up a variable in extended bindings: if already assigned, value is preserved.
--
-- >>> runTP lookUpExtends
-- Lemma: lookUpExtends                    Q.E.D.
-- [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 :: TP
  (Proof
     (Forall "i" Integer
      -> Forall "n" Integer
      -> Forall "v" Bool
      -> Forall "bs" [Binding]
      -> SBool))
lookUpExtends = String
-> (Forall "i" Integer
    -> Forall "n" Integer
    -> Forall "v" Bool
    -> Forall "bs" [Binding]
    -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "i" Integer
         -> Forall "n" Integer
         -> Forall "v" Bool
         -> Forall "bs" [Binding]
         -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"lookUpExtends"
                      (\(Forall SBV Integer
i) (Forall SBV Integer
n) (Forall SBool
v) (Forall SList Binding
bs) ->
                                SBV Integer -> SList Binding -> SBool
isAssigned SBV Integer
i SList Binding
bs SBool -> SBool -> SBool
.&& SBV Integer
i SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SBV Integer
n SBool -> SBool -> SBool
.=> SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
i (SBV Integer -> SBool -> SBV Binding
sBinding SBV Integer
n SBool
v SBV Binding -> SList Binding -> SList Binding
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Binding
bs) SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
i SList Binding
bs)
                      []

-- | Looking up a variable that was just added returns the added value.
--
-- >>> runTP lookUpSame
-- Lemma: lookUpSame                       Q.E.D.
-- [Proven] lookUpSame :: Ɐn ∷ Integer → Ɐv ∷ Bool → Ɐbs ∷ [Binding] → Bool
lookUpSame :: TP (Proof (Forall "n" Integer -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool))
lookUpSame :: TP
  (Proof
     (Forall "n" Integer
      -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool))
lookUpSame = String
-> (Forall "n" Integer
    -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "n" Integer
         -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"lookUpSame" (\(Forall SBV Integer
n) (Forall SBool
v) (Forall SList Binding
bs) -> SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
n (SBV Integer -> SBool -> SBV Binding
sBinding SBV Integer
n SBool
v SBV Binding -> SList Binding -> SList Binding
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Binding
bs) SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBool
v) []

-- | Adding a binding for a variable makes it assigned.
--
-- >>> runTP isAssignedSame
-- Lemma: isAssignedSame                   Q.E.D.
-- [Proven] isAssignedSame :: Ɐn ∷ Integer → Ɐv ∷ Bool → Ɐbs ∷ [Binding] → Bool
isAssignedSame :: TP (Proof (Forall "n" Integer -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool))
isAssignedSame :: TP
  (Proof
     (Forall "n" Integer
      -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool))
isAssignedSame = String
-> (Forall "n" Integer
    -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "n" Integer
         -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"isAssignedSame" (\(Forall SBV Integer
n) (Forall SBool
v) (Forall SList Binding
bs) -> SBV Integer -> SList Binding -> SBool
isAssigned SBV Integer
n (SBV Integer -> SBool -> SBV Binding
sBinding SBV Integer
n SBool
v SBV Binding -> SList Binding -> SList Binding
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Binding
bs)) []

-- * Formula evaluation

-- | Evaluate a formula under a binding environment.
eval :: SFormula -> SList Binding -> SBool
eval :: SBV Formula -> SList Binding -> SBool
eval = String
-> (SBV Formula -> SList Binding -> SBool)
-> SBV Formula
-> SList Binding
-> SBool
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"eval" ((SBV Formula -> SList Binding -> SBool)
 -> SBV Formula -> SList Binding -> SBool)
-> (SBV Formula -> SList Binding -> SBool)
-> SBV Formula
-> SList Binding
-> SBool
forall a b. (a -> b) -> a -> b
$ \SBV Formula
f SList Binding
bs ->
  [sCase|Formula f of
    Var n    -> lookUp n bs
    If c l r -> ite (eval c bs) (eval l bs) (eval r bs)
    FTrue    -> sTrue
    FFalse   -> sFalse
  |]

-- * Tautology checking

-- | Check if a normalized formula is a tautology.
isTautology' :: SFormula -> SList Binding -> SBool
isTautology' :: SBV Formula -> SList Binding -> SBool
isTautology' = String
-> (SBV Formula -> SList Binding -> SBool)
-> SBV Formula
-> SList Binding
-> SBool
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"isTautology'" ((SBV Formula -> SList Binding -> SBool)
 -> SBV Formula -> SList Binding -> SBool)
-> (SBV Formula -> SList Binding -> SBool)
-> SBV Formula
-> SList Binding
-> SBool
forall a b. (a -> b) -> a -> b
$ \SBV Formula
f SList Binding
bs ->
  [sCase|Formula 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 :: SBV Formula -> SBool
isTautology SBV Formula
f = SBV Formula -> SList Binding -> SBool
isTautology' (SBV Formula -> SBV Formula
normalize SBV Formula
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.
-- [Proven] lookUpStable :: Ɐa ∷ [Binding] → Ɐx ∷ Integer → Ɐb ∷ [Binding] → Bool
lookUpStable :: TP (Proof (Forall "a" [Binding] -> Forall "x" Integer -> Forall "b" [Binding] -> SBool))
lookUpStable :: TP
  (Proof
     (Forall "a" [Binding]
      -> Forall "x" Integer -> Forall "b" [Binding] -> SBool))
lookUpStable =
  String
-> (Forall "a" [Binding]
    -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
-> (Proof
      (IHType
         (Forall "a" [Binding]
          -> Forall "x" Integer -> Forall "b" [Binding] -> SBool))
    -> IHArg
         (Forall "a" [Binding]
          -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
    -> IStepArgs
         (Forall "a" [Binding]
          -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
         Bool)
-> TP
     (Proof
        (Forall "a" [Binding]
         -> Forall "x" Integer -> Forall "b" [Binding] -> SBool))
forall t.
(Proposition
   (Forall "a" [Binding]
    -> Forall "x" Integer -> Forall "b" [Binding] -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" [Binding]
    -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
-> (Proof
      (IHType
         (Forall "a" [Binding]
          -> Forall "x" Integer -> Forall "b" [Binding] -> SBool))
    -> IHArg
         (Forall "a" [Binding]
          -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
    -> IStepArgs
         (Forall "a" [Binding]
          -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
         t)
-> TP
     (Proof
        (Forall "a" [Binding]
         -> Forall "x" Integer -> Forall "b" [Binding] -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
induct String
"lookUpStable"
         (\(Forall SList Binding
a) (Forall SBV Integer
x) (Forall SList Binding
b) -> SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
x (SList Binding
a SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
b) SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Integer -> SList Binding -> SBool
isAssigned SBV Integer
x SList Binding
a) (SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
x SList Binding
a) (SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
x SList Binding
b)) ((Proof
    (IHType
       (Forall "a" [Binding]
        -> Forall "x" Integer -> Forall "b" [Binding] -> SBool))
  -> IHArg
       (Forall "a" [Binding]
        -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
  -> IStepArgs
       (Forall "a" [Binding]
        -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
       Bool)
 -> TP
      (Proof
         (Forall "a" [Binding]
          -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)))
-> (Proof
      (IHType
         (Forall "a" [Binding]
          -> Forall "x" Integer -> Forall "b" [Binding] -> SBool))
    -> IHArg
         (Forall "a" [Binding]
          -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
    -> IStepArgs
         (Forall "a" [Binding]
          -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
         Bool)
-> TP
     (Proof
        (Forall "a" [Binding]
         -> Forall "x" Integer -> Forall "b" [Binding] -> SBool))
forall a b. (a -> b) -> a -> b
$
         \Proof
  (IHType
     (Forall "a" [Binding]
      -> Forall "x" Integer -> Forall "b" [Binding] -> SBool))
ih (SBV Binding
binding, SList Binding
a) SBV Integer
x SList Binding
b ->
           let vid :: SBV Integer
vid = SBV Binding -> SBV Integer
svarId SBV Binding
binding
               val :: SBool
val = SBV Binding -> SBool
svalue SBV Binding
binding
           in [] [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
x ((SBV Binding
binding SBV Binding -> SList Binding -> SList Binding
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Binding
a) SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
b)
                 SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SBV Integer
vid SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer
x SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Integer -> SList Binding -> SBool
isAssigned SBV Integer
x (SBV Binding
binding SBV Binding -> SList Binding -> SList Binding
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Binding
a)) (SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
x (SBV Binding
binding SBV Binding -> SList Binding -> SList Binding
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Binding
a)) (SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
x SList Binding
b)
                                       SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
val
                                       SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                          , SBV Integer
vid SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SBV Integer
x SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
x (SList Binding
a SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
b)
                                       SBool
-> Proof (Forall "x" Integer -> Forall "b" [Binding] -> SBool)
-> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (IHType
     (Forall "a" [Binding]
      -> Forall "x" Integer -> Forall "b" [Binding] -> SBool))
Proof (Forall "x" Integer -> Forall "b" [Binding] -> SBool)
ih
                                       TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Integer -> SList Binding -> SBool
isAssigned SBV Integer
x SList Binding
a) (SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
x SList Binding
a) (SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
x SList Binding
b)
                                       SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
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.
-- [Proven] trueIsAssigned :: Ɐa ∷ [Binding] → Ɐx ∷ Integer → Bool
trueIsAssigned :: TP (Proof (Forall "a" [Binding] -> Forall "x" Integer -> SBool))
trueIsAssigned :: TP (Proof (Forall "a" [Binding] -> Forall "x" Integer -> SBool))
trueIsAssigned =
  String
-> (Forall "a" [Binding] -> Forall "x" Integer -> SBool)
-> (Proof
      (IHType (Forall "a" [Binding] -> Forall "x" Integer -> SBool))
    -> IHArg (Forall "a" [Binding] -> Forall "x" Integer -> SBool)
    -> IStepArgs
         (Forall "a" [Binding] -> Forall "x" Integer -> SBool) Bool)
-> TP (Proof (Forall "a" [Binding] -> Forall "x" Integer -> SBool))
forall t.
(Proposition (Forall "a" [Binding] -> Forall "x" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" [Binding] -> Forall "x" Integer -> SBool)
-> (Proof
      (IHType (Forall "a" [Binding] -> Forall "x" Integer -> SBool))
    -> IHArg (Forall "a" [Binding] -> Forall "x" Integer -> SBool)
    -> IStepArgs
         (Forall "a" [Binding] -> Forall "x" Integer -> SBool) t)
-> TP (Proof (Forall "a" [Binding] -> Forall "x" Integer -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
induct String
"trueIsAssigned"
         (\(Forall SList Binding
a) (Forall SBV Integer
x) -> SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
x SList Binding
a SBool -> SBool -> SBool
.=> SBV Integer -> SList Binding -> SBool
isAssigned SBV Integer
x SList Binding
a) ((Proof
    (IHType (Forall "a" [Binding] -> Forall "x" Integer -> SBool))
  -> IHArg (Forall "a" [Binding] -> Forall "x" Integer -> SBool)
  -> IStepArgs
       (Forall "a" [Binding] -> Forall "x" Integer -> SBool) Bool)
 -> TP
      (Proof (Forall "a" [Binding] -> Forall "x" Integer -> SBool)))
-> (Proof
      (IHType (Forall "a" [Binding] -> Forall "x" Integer -> SBool))
    -> IHArg (Forall "a" [Binding] -> Forall "x" Integer -> SBool)
    -> IStepArgs
         (Forall "a" [Binding] -> Forall "x" Integer -> SBool) Bool)
-> TP (Proof (Forall "a" [Binding] -> Forall "x" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
         \Proof
  (IHType (Forall "a" [Binding] -> Forall "x" Integer -> SBool))
ih (SBV Binding
binding, SList Binding
a) SBV Integer
x ->
           let vid :: SBV Integer
vid = [sCase|Binding binding of Binding v _ -> v|]
           in [SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
x (SBV Binding
binding SBV Binding -> SList Binding -> SList Binding
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Binding
a)]
           [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV Integer -> SList Binding -> SBool
isAssigned SBV Integer
x (SBV Binding
binding SBV Binding -> SList Binding -> SList Binding
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Binding
a)
           SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SBV Integer
vid SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer
x SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial
                    , SBV Integer
vid SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SBV Integer
x SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SBV Integer -> SList Binding -> SBool
isAssigned SBV Integer
x SList Binding
a
                                 SBool -> Proof (Forall "x" Integer -> SBool) -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (IHType (Forall "a" [Binding] -> Forall "x" Integer -> SBool))
Proof (Forall "x" Integer -> SBool)
ih
                                 TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                 SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
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.
-- [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 :: TP
  (Proof
     (Forall "f" Formula
      -> Forall "x" Integer
      -> Forall "v" Bool
      -> Forall "bs" [Binding]
      -> SBool))
evalStable = do
  Proof (Forall "f" Formula -> SBool)
icp <- String
-> TP (Proof (Forall "f" Formula -> SBool))
-> TP (Proof (Forall "f" Formula -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"ifComplexityPos"     TP (Proof (Forall "f" Formula -> SBool))
ifComplexityPos
  Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs <- String
-> TP
     (Proof
        (Forall "c" Formula
         -> Forall "l" Formula -> Forall "r" Formula -> SBool))
-> TP
     (Proof
        (Forall "c" Formula
         -> Forall "l" Formula -> Forall "r" Formula -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"ifComplexitySmaller" TP
  (Proof
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool))
ifComplexitySmaller

  String
-> (Forall "f" Formula
    -> Forall "x" Integer
    -> Forall "v" Bool
    -> Forall "bs" [Binding]
    -> SBool)
-> (MeasureArgs
      (Forall "f" Formula
       -> Forall "x" Integer
       -> Forall "v" Bool
       -> Forall "bs" [Binding]
       -> SBool)
      Integer,
    [ProofObj])
-> (Proof
      (Forall "f" Formula
       -> Forall "x" Integer
       -> Forall "v" Bool
       -> Forall "bs" [Binding]
       -> SBool)
    -> StepArgs
         (Forall "f" Formula
          -> Forall "x" Integer
          -> Forall "v" Bool
          -> Forall "bs" [Binding]
          -> SBool)
         Bool)
-> TP
     (Proof
        (Forall "f" Formula
         -> Forall "x" Integer
         -> Forall "v" Bool
         -> Forall "bs" [Binding]
         -> SBool))
forall a m t.
(SInductive a, Proposition a, Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
String
-> a
-> (MeasureArgs a m, [ProofObj])
-> (Proof a -> StepArgs a t)
-> TP (Proof a)
forall m t.
(Proposition
   (Forall "f" Formula
    -> Forall "x" Integer
    -> Forall "v" Bool
    -> Forall "bs" [Binding]
    -> SBool),
 Zero m, SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "f" Formula
    -> Forall "x" Integer
    -> Forall "v" Bool
    -> Forall "bs" [Binding]
    -> SBool)
-> (MeasureArgs
      (Forall "f" Formula
       -> Forall "x" Integer
       -> Forall "v" Bool
       -> Forall "bs" [Binding]
       -> SBool)
      m,
    [ProofObj])
-> (Proof
      (Forall "f" Formula
       -> Forall "x" Integer
       -> Forall "v" Bool
       -> Forall "bs" [Binding]
       -> SBool)
    -> StepArgs
         (Forall "f" Formula
          -> Forall "x" Integer
          -> Forall "v" Bool
          -> Forall "bs" [Binding]
          -> SBool)
         t)
-> TP
     (Proof
        (Forall "f" Formula
         -> Forall "x" Integer
         -> Forall "v" Bool
         -> Forall "bs" [Binding]
         -> SBool))
sInduct String
"evalStable"
          (\(Forall SBV Formula
f) (Forall SBV Integer
x) (Forall SBool
v) (Forall SList Binding
bs) -> SBool
v SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
x SList Binding
bs SBool -> SBool -> SBool
.=> SBV Formula -> SList Binding -> SBool
eval SBV Formula
f (SBV Integer -> SBool -> SBV Binding
sBinding SBV Integer
x SBool
v SBV Binding -> SList Binding -> SList Binding
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Binding
bs) SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Formula -> SList Binding -> SBool
eval SBV Formula
f SList Binding
bs)
          (\SBV Formula
f SBV Integer
_ SBool
_ SList Binding
_ -> SBV Formula -> SBV Integer
ifComplexity SBV Formula
f, [Proof (Forall "f" Formula -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "f" Formula -> SBool)
icp]) ((Proof
    (Forall "f" Formula
     -> Forall "x" Integer
     -> Forall "v" Bool
     -> Forall "bs" [Binding]
     -> SBool)
  -> StepArgs
       (Forall "f" Formula
        -> Forall "x" Integer
        -> Forall "v" Bool
        -> Forall "bs" [Binding]
        -> SBool)
       Bool)
 -> TP
      (Proof
         (Forall "f" Formula
          -> Forall "x" Integer
          -> Forall "v" Bool
          -> Forall "bs" [Binding]
          -> SBool)))
-> (Proof
      (Forall "f" Formula
       -> Forall "x" Integer
       -> Forall "v" Bool
       -> Forall "bs" [Binding]
       -> SBool)
    -> StepArgs
         (Forall "f" Formula
          -> Forall "x" Integer
          -> Forall "v" Bool
          -> Forall "bs" [Binding]
          -> SBool)
         Bool)
-> TP
     (Proof
        (Forall "f" Formula
         -> Forall "x" Integer
         -> Forall "v" Bool
         -> Forall "bs" [Binding]
         -> SBool))
forall a b. (a -> b) -> a -> b
$
          \Proof
  (Forall "f" Formula
   -> Forall "x" Integer
   -> Forall "v" Bool
   -> Forall "bs" [Binding]
   -> SBool)
ih SBV Formula
f SBV Integer
x SBool
v SList Binding
bs ->
               let b :: SBV Binding
b = SBV Integer -> SBool -> SBV Binding
sBinding SBV Integer
x SBool
v
               in [SBool
v SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
x SList Binding
bs]
               [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SBV Formula -> SBool
isFTrue  SBV Formula
f SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial
                        , SBV Formula -> SBool
isFFalse SBV Formula
f SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial
                        , SBV Formula -> SBool
isVar    SBV Formula
f SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial
                        , SBV Formula -> SBool
isIf     SBV Formula
f SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==>
                            let c :: SBV Formula
c = SBV Formula -> SBV Formula
sifCond SBV Formula
f
                                l :: SBV Formula
l = SBV Formula -> SBV Formula
sifThen SBV Formula
f
                                r :: SBV Formula
r = SBV Formula -> SBV Formula
sifElse SBV Formula
f
                            in SBV Formula -> SList Binding -> SBool
eval SBV Formula
f (SBV Binding
b SBV Binding -> SList Binding -> SList Binding
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Binding
bs)
                            SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Formula -> SList Binding -> SBool
eval (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
c SBV Formula
l SBV Formula
r) (SBV Binding
b SBV Binding -> SList Binding -> SList Binding
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Binding
bs)
                            SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Formula -> SList Binding -> SBool
eval SBV Formula
c (SBV Binding
b SBV Binding -> SList Binding -> SList Binding
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Binding
bs)) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
l (SBV Binding
b SBV Binding -> SList Binding -> SList Binding
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Binding
bs)) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
r (SBV Binding
b SBV Binding -> SList Binding -> SList Binding
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Binding
bs))
                            SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "f" Formula
   -> Forall "x" Integer
   -> Forall "v" Bool
   -> Forall "bs" [Binding]
   -> SBool)
ih  Proof
  (Forall "f" Formula
   -> Forall "x" Integer
   -> Forall "v" Bool
   -> Forall "bs" [Binding]
   -> SBool)
-> IArgs
     (Forall "f" Formula
      -> Forall "x" Integer
      -> Forall "v" Bool
      -> Forall "bs" [Binding]
      -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
c, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SBV Integer
x, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"v" SBool
v, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" SList Binding
bs)
                            TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> IArgs
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"c" SBV Formula
c, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"r" SBV Formula
r)
                            Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (TPProofRaw SBool))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Formula -> SList Binding -> SBool
eval SBV Formula
c SList Binding
bs) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
l (SBV Binding
b SBV Binding -> SList Binding -> SList Binding
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Binding
bs)) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
r (SBV Binding
b SBV Binding -> SList Binding -> SList Binding
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Binding
bs))
                            SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "f" Formula
   -> Forall "x" Integer
   -> Forall "v" Bool
   -> Forall "bs" [Binding]
   -> SBool)
ih  Proof
  (Forall "f" Formula
   -> Forall "x" Integer
   -> Forall "v" Bool
   -> Forall "bs" [Binding]
   -> SBool)
-> IArgs
     (Forall "f" Formula
      -> Forall "x" Integer
      -> Forall "v" Bool
      -> Forall "bs" [Binding]
      -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SBV Integer
x, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"v" SBool
v, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" SList Binding
bs)
                            TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> IArgs
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"c" SBV Formula
c, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"r" SBV Formula
r)
                            Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (TPProofRaw SBool))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Formula -> SList Binding -> SBool
eval SBV Formula
c SList Binding
bs) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
l SList Binding
bs) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
r (SBV Binding
b SBV Binding -> SList Binding -> SList Binding
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Binding
bs))
                            SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "f" Formula
   -> Forall "x" Integer
   -> Forall "v" Bool
   -> Forall "bs" [Binding]
   -> SBool)
ih  Proof
  (Forall "f" Formula
   -> Forall "x" Integer
   -> Forall "v" Bool
   -> Forall "bs" [Binding]
   -> SBool)
-> IArgs
     (Forall "f" Formula
      -> Forall "x" Integer
      -> Forall "v" Bool
      -> Forall "bs" [Binding]
      -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
r, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SBV Integer
x, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"v" SBool
v, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" SList Binding
bs)
                            TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> IArgs
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"c" SBV Formula
c, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"r" SBV Formula
r)
                            Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (TPProofRaw SBool))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Formula -> SList Binding -> SBool
eval SBV Formula
c SList Binding
bs) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
l SList Binding
bs) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
r SList Binding
bs)
                            SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Formula -> SList Binding -> SBool
eval (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
c SBV Formula
l SBV Formula
r) SList Binding
bs
                            SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
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.
-- [Proven] tautologyImpliesEval :: Ɐf ∷ Formula → Ɐa ∷ [Binding] → Ɐb ∷ [Binding] → Bool
tautologyImpliesEval :: TP (Proof (Forall "f" Formula -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool))
tautologyImpliesEval :: TP
  (Proof
     (Forall "f" Formula
      -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool))
tautologyImpliesEval = do

  Proof (Forall "f" Formula -> SBool)
icp <- String
-> TP (Proof (Forall "f" Formula -> SBool))
-> TP (Proof (Forall "f" Formula -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"ifComplexityPos"     TP (Proof (Forall "f" Formula -> SBool))
ifComplexityPos
  Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs <- String
-> TP
     (Proof
        (Forall "c" Formula
         -> Forall "l" Formula -> Forall "r" Formula -> SBool))
-> TP
     (Proof
        (Forall "c" Formula
         -> Forall "l" Formula -> Forall "r" Formula -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"ifComplexitySmaller" TP
  (Proof
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool))
ifComplexitySmaller
  Proof
  (Forall "a" [Binding]
   -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
lus <- String
-> TP
     (Proof
        (Forall "a" [Binding]
         -> Forall "x" Integer -> Forall "b" [Binding] -> SBool))
-> TP
     (Proof
        (Forall "a" [Binding]
         -> Forall "x" Integer -> Forall "b" [Binding] -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"lookUpStable"        TP
  (Proof
     (Forall "a" [Binding]
      -> Forall "x" Integer -> Forall "b" [Binding] -> SBool))
lookUpStable
  Proof (Forall "a" [Binding] -> Forall "x" Integer -> SBool)
tia <- String
-> TP (Proof (Forall "a" [Binding] -> Forall "x" Integer -> SBool))
-> TP (Proof (Forall "a" [Binding] -> Forall "x" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"trueIsAssigned"      TP (Proof (Forall "a" [Binding] -> Forall "x" Integer -> SBool))
trueIsAssigned
  Proof
  (Forall "f" Formula
   -> Forall "x" Integer
   -> Forall "v" Bool
   -> Forall "bs" [Binding]
   -> SBool)
evs <- String
-> TP
     (Proof
        (Forall "f" Formula
         -> Forall "x" Integer
         -> Forall "v" Bool
         -> Forall "bs" [Binding]
         -> SBool))
-> TP
     (Proof
        (Forall "f" Formula
         -> Forall "x" Integer
         -> Forall "v" Bool
         -> Forall "bs" [Binding]
         -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"evalStable"          TP
  (Proof
     (Forall "f" Formula
      -> Forall "x" Integer
      -> Forall "v" Bool
      -> Forall "bs" [Binding]
      -> SBool))
evalStable

  String
-> (Forall "f" Formula
    -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
-> (MeasureArgs
      (Forall "f" Formula
       -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
      Integer,
    [ProofObj])
-> (Proof
      (Forall "f" Formula
       -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
    -> StepArgs
         (Forall "f" Formula
          -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
         Bool)
-> TP
     (Proof
        (Forall "f" Formula
         -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool))
forall a m t.
(SInductive a, Proposition a, Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
String
-> a
-> (MeasureArgs a m, [ProofObj])
-> (Proof a -> StepArgs a t)
-> TP (Proof a)
forall m t.
(Proposition
   (Forall "f" Formula
    -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool),
 Zero m, SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "f" Formula
    -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
-> (MeasureArgs
      (Forall "f" Formula
       -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
      m,
    [ProofObj])
-> (Proof
      (Forall "f" Formula
       -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
    -> StepArgs
         (Forall "f" Formula
          -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
         t)
-> TP
     (Proof
        (Forall "f" Formula
         -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool))
sInduct String
"tautologyImpliesEval"
          (\(Forall SBV Formula
f) (Forall SList Binding
a) (Forall SList Binding
b) -> SBV Formula -> SBool
isNormal SBV Formula
f SBool -> SBool -> SBool
.&& SBV Formula -> SList Binding -> SBool
isTautology' SBV Formula
f SList Binding
b SBool -> SBool -> SBool
.=> SBV Formula -> SList Binding -> SBool
eval SBV Formula
f (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a))
          (\SBV Formula
f SList Binding
_ SList Binding
_ -> SBV Formula -> SBV Integer
ifComplexity SBV Formula
f, [Proof (Forall "f" Formula -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "f" Formula -> SBool)
icp]) ((Proof
    (Forall "f" Formula
     -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
  -> StepArgs
       (Forall "f" Formula
        -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
       Bool)
 -> TP
      (Proof
         (Forall "f" Formula
          -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)))
-> (Proof
      (Forall "f" Formula
       -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
    -> StepArgs
         (Forall "f" Formula
          -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
         Bool)
-> TP
     (Proof
        (Forall "f" Formula
         -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool))
forall a b. (a -> b) -> a -> b
$
          \Proof
  (Forall "f" Formula
   -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
ih SBV Formula
f SList Binding
a SList Binding
b ->
                [SBV Formula -> SBool
isNormal SBV Formula
f, SBV Formula -> SList Binding -> SBool
isTautology' SBV Formula
f SList Binding
b]
             [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SBV Formula -> SBool
isFTrue  SBV Formula
f SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial
                      , SBV Formula -> SBool
isFFalse SBV Formula
f SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial
                      , SBV Formula -> SBool
isVar    SBV Formula
f SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> let n :: SBV Integer
n = SBV Formula -> SBV Integer
sfVar SBV Formula
f
                                       in SBV Formula -> SList Binding -> SBool
eval SBV Formula
f (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)
                                       SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Formula -> SList Binding -> SBool
eval (SBV Integer -> SBV Formula
sVar SBV Integer
n) (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)
                                       SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
n (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)
                                       SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" [Binding]
   -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
lus Proof
  (Forall "a" [Binding]
   -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
-> IArgs
     (Forall "a" [Binding]
      -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"a" SList Binding
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SBV Integer
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SList Binding
a)
                                       TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Integer -> SList Binding -> SBool
isAssigned SBV Integer
n SList Binding
b) (SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
n SList Binding
b) (SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
n SList Binding
a)
                                       SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" [Binding] -> Forall "x" Integer -> SBool)
tia Proof (Forall "a" [Binding] -> Forall "x" Integer -> SBool)
-> IArgs (Forall "a" [Binding] -> Forall "x" Integer -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"a" SList Binding
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SBV Integer
n)
                                       TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
n SList Binding
b
                                       SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                       SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                      , SBV Formula -> SBool
isIf SBV Formula
f     SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==>
                          let c :: SBV Formula
c = SBV Formula -> SBV Formula
sifCond SBV Formula
f
                              l :: SBV Formula
l = SBV Formula -> SBV Formula
sifThen SBV Formula
f
                              r :: SBV Formula
r = SBV Formula -> SBV Formula
sifElse SBV Formula
f
                          in [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SBV Formula -> SBool
isFTrue  SBV Formula
c SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SBV Formula -> SList Binding -> SBool
eval (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
c SBV Formula
l SBV Formula
r) (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)
                                                 SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Formula -> SList Binding -> SBool
eval SBV Formula
c (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
l (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
r (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a))
                                                 SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> IArgs
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"c" SBV Formula
c, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"r" SBV Formula
r)
                                                 TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "f" Formula
   -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
ih  Proof
  (Forall "f" Formula
   -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
-> IArgs
     (Forall "f" Formula
      -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"a" SList Binding
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SList Binding
b)
                                                 Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (TPProofRaw SBool))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                                 SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                                   , SBV Formula -> SBool
isFFalse SBV Formula
c SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SBV Formula -> SList Binding -> SBool
eval (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
c SBV Formula
l SBV Formula
r) (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)
                                                 SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Formula -> SList Binding -> SBool
eval SBV Formula
c (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
l (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
r (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a))
                                                 SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Formula -> SList Binding -> SBool
eval SBV Formula
r (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)
                                                 SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> IArgs
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"c" SBV Formula
c, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"r" SBV Formula
r)
                                                 TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "f" Formula
   -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
ih  Proof
  (Forall "f" Formula
   -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
-> IArgs
     (Forall "f" Formula
      -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
r, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"a" SList Binding
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SList Binding
b)
                                                 Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (TPProofRaw SBool))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                                 SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                                   , SBV Formula -> SBool
isVar    SBV Formula
c SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> let n :: SBV Integer
n = SBV Formula -> SBV Integer
sfVar SBV Formula
c
                                                    in [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SBV Integer -> SList Binding -> SBool
isAssigned SBV Integer
n SList Binding
b SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==>
                                                                    SBV Formula -> SList Binding -> SBool
eval (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf (SBV Integer -> SBV Formula
sVar SBV Integer
n) SBV Formula
l SBV Formula
r) (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)
                                                                 SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Formula -> SList Binding -> SBool
eval (SBV Integer -> SBV Formula
sVar SBV Integer
n) (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
l (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
r (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a))
                                                                 SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
n (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
l (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
r (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a))
                                                                 SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" [Binding]
   -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
lus Proof
  (Forall "a" [Binding]
   -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
-> IArgs
     (Forall "a" [Binding]
      -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"a" SList Binding
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SBV Integer
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SList Binding
a)
                                                                 TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
n SList Binding
b) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
l (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
r (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a))
                                                                 SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> IArgs
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"c" SBV Formula
c, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"r" SBV Formula
r)
                                                                 TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "f" Formula
   -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
ih  Proof
  (Forall "f" Formula
   -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
-> IArgs
     (Forall "f" Formula
      -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"a" SList Binding
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SList Binding
b)
                                                                 Hinted (TPProofRaw SBool)
-> Proof Bool -> Hinted (Hinted (TPProofRaw SBool))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "f" Formula
   -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
ih  Proof
  (Forall "f" Formula
   -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
-> IArgs
     (Forall "f" Formula
      -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
r, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"a" SList Binding
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SList Binding
b)
                                                                 Hinted (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (Hinted (TPProofRaw SBool)))
-> ChainsTo (Hinted (Hinted (TPProofRaw SBool)))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                                                 SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                                                             , SBool -> SBool
sNot (SBV Integer -> SList Binding -> SBool
isAssigned SBV Integer
n SList Binding
b) SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==>
                                                                 [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
n SList Binding
a SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==>
                                                                             SBV Formula -> SList Binding -> SBool
eval (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf (SBV Integer -> SBV Formula
sVar SBV Integer
n) SBV Formula
l SBV Formula
r) (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)
                                                                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Formula -> SList Binding -> SBool
eval (SBV Integer -> SBV Formula
sVar SBV Integer
n) (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
l (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
r (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a))
                                                                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
n (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
l (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
r (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a))
                                                                          SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" [Binding]
   -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
lus Proof
  (Forall "a" [Binding]
   -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
-> IArgs
     (Forall "a" [Binding]
      -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"a" SList Binding
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SBV Integer
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SList Binding
a)
                                                                          TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
n SList Binding
a) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
l (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
r (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a))
                                                                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Formula -> SList Binding -> SBool
eval SBV Formula
l (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)
                                                                          SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "f" Formula
   -> Forall "x" Integer
   -> Forall "v" Bool
   -> Forall "bs" [Binding]
   -> SBool)
evs Proof
  (Forall "f" Formula
   -> Forall "x" Integer
   -> Forall "v" Bool
   -> Forall "bs" [Binding]
   -> SBool)
-> IArgs
     (Forall "f" Formula
      -> Forall "x" Integer
      -> Forall "v" Bool
      -> Forall "bs" [Binding]
      -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SBV Integer
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"v" (SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
n SList Binding
a), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a))
                                                                          TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" [Binding]
   -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
lus Proof
  (Forall "a" [Binding]
   -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
-> IArgs
     (Forall "a" [Binding]
      -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"a" SList Binding
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SBV Integer
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SList Binding
a)
                                                                          Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (TPProofRaw SBool))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Formula -> SList Binding -> SBool
eval SBV Formula
l (SBV Integer -> SBool -> SBV Binding
sBinding SBV Integer
n (SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
n SList Binding
a) SBV Binding -> SList Binding -> SList Binding
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a))
                                                                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Formula -> SList Binding -> SBool
eval SBV Formula
l (SBV Integer -> SBool -> SBV Binding
sBinding SBV Integer
n SBool
sTrue SBV Binding -> SList Binding -> SList Binding
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a))
                                                                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Formula -> SList Binding -> SBool
eval SBV Formula
l (SBV Integer -> SList Binding -> SList Binding
assumeTrue SBV Integer
n SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)
                                                                          SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> IArgs
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"c" SBV Formula
c, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"r" SBV Formula
r)
                                                                          TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "f" Formula
   -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
ih  Proof
  (Forall "f" Formula
   -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
-> IArgs
     (Forall "f" Formula
      -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"a" SList Binding
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" (SBV Integer -> SList Binding -> SList Binding
assumeTrue SBV Integer
n SList Binding
b))
                                                                          Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (TPProofRaw SBool))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                                                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                                                                       , SBool -> SBool
sNot (SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
n SList Binding
a) SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==>
                                                                             SBV Formula -> SList Binding -> SBool
eval (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf (SBV Integer -> SBV Formula
sVar SBV Integer
n) SBV Formula
l SBV Formula
r) (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)
                                                                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Formula -> SList Binding -> SBool
eval (SBV Integer -> SBV Formula
sVar SBV Integer
n) (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
l (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
r (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a))
                                                                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
n (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
l (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
r (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a))
                                                                          SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" [Binding]
   -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
lus Proof
  (Forall "a" [Binding]
   -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
-> IArgs
     (Forall "a" [Binding]
      -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"a" SList Binding
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SBV Integer
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SList Binding
a)
                                                                          TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
n SList Binding
a) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
l (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
r (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a))
                                                                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Formula -> SList Binding -> SBool
eval SBV Formula
r (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)
                                                                          SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "f" Formula
   -> Forall "x" Integer
   -> Forall "v" Bool
   -> Forall "bs" [Binding]
   -> SBool)
evs Proof
  (Forall "f" Formula
   -> Forall "x" Integer
   -> Forall "v" Bool
   -> Forall "bs" [Binding]
   -> SBool)
-> IArgs
     (Forall "f" Formula
      -> Forall "x" Integer
      -> Forall "v" Bool
      -> Forall "bs" [Binding]
      -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
r, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SBV Integer
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"v" (SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
n SList Binding
a), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a))
                                                                          TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" [Binding]
   -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
lus Proof
  (Forall "a" [Binding]
   -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
-> IArgs
     (Forall "a" [Binding]
      -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"a" SList Binding
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SBV Integer
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SList Binding
a)
                                                                          Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (TPProofRaw SBool))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Formula -> SList Binding -> SBool
eval SBV Formula
r (SBV Integer -> SBool -> SBV Binding
sBinding SBV Integer
n (SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
n SList Binding
a) SBV Binding -> SList Binding -> SList Binding
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a))
                                                                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Formula -> SList Binding -> SBool
eval SBV Formula
r (SBV Integer -> SBool -> SBV Binding
sBinding SBV Integer
n SBool
sFalse SBV Binding -> SList Binding -> SList Binding
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a))
                                                                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Formula -> SList Binding -> SBool
eval SBV Formula
r (SBV Integer -> SList Binding -> SList Binding
assumeFalse SBV Integer
n SList Binding
b SList Binding -> SList Binding -> SList Binding
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Binding
a)
                                                                          SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> IArgs
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"c" SBV Formula
c, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"r" SBV Formula
r)
                                                                          TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "f" Formula
   -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
ih  Proof
  (Forall "f" Formula
   -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
-> IArgs
     (Forall "f" Formula
      -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
r, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"a" SList Binding
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" (SBV Integer -> SList Binding -> SList Binding
assumeFalse SBV Integer
n SList Binding
b))
                                                                          Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (TPProofRaw SBool))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                                                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                                                                       ]
                                                             ]
                                   , SBV Formula -> SBool
isIf SBV Formula
c     SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
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.
-- [Proven] normalizeCorrect :: Ɐf ∷ Formula → Bool
normalizeCorrect :: TP (Proof (Forall "f" Formula -> SBool))
normalizeCorrect :: TP (Proof (Forall "f" Formula -> SBool))
normalizeCorrect = do
  Proof (Forall "f" Formula -> SBool)
icp <- String
-> TP (Proof (Forall "f" Formula -> SBool))
-> TP (Proof (Forall "f" Formula -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"ifComplexityPos"              TP (Proof (Forall "f" Formula -> SBool))
ifComplexityPos
  Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs <- String
-> TP
     (Proof
        (Forall "c" Formula
         -> Forall "l" Formula -> Forall "r" Formula -> SBool))
-> TP
     (Proof
        (Forall "c" Formula
         -> Forall "l" Formula -> Forall "r" Formula -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"ifComplexitySmaller"          TP
  (Proof
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool))
ifComplexitySmaller
  Proof
  (Forall "p" Formula
   -> Forall "q" Formula
   -> Forall "s" Formula
   -> Forall "l" Formula
   -> Forall "r" Formula
   -> SBool)
npc <- String
-> TP
     (Proof
        (Forall "p" Formula
         -> Forall "q" Formula
         -> Forall "s" Formula
         -> Forall "l" Formula
         -> Forall "r" Formula
         -> SBool))
-> TP
     (Proof
        (Forall "p" Formula
         -> Forall "q" Formula
         -> Forall "s" Formula
         -> Forall "l" Formula
         -> Forall "r" Formula
         -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"normalizePreservesComplexity" TP
  (Proof
     (Forall "p" Formula
      -> Forall "q" Formula
      -> Forall "s" Formula
      -> Forall "l" Formula
      -> Forall "r" Formula
      -> SBool))
normalizePreservesComplexity
  Proof (Forall "f" Formula -> SBool)
idn <- String
-> TP (Proof (Forall "f" Formula -> SBool))
-> TP (Proof (Forall "f" Formula -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"ifDepthNonNeg"                TP (Proof (Forall "f" Formula -> SBool))
ifDepthNonNeg

  SMTConfig
-> String
-> (Forall "f" Formula -> SBool)
-> (MeasureArgs (Forall "f" Formula -> SBool) (Integer, Integer),
    [ProofObj])
-> (Proof (Forall "f" Formula -> SBool)
    -> StepArgs (Forall "f" Formula -> SBool) Bool)
-> TP (Proof (Forall "f" Formula -> SBool))
forall a m t.
(SInductive a, Proposition a, Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> a
-> (MeasureArgs a m, [ProofObj])
-> (Proof a -> StepArgs a t)
-> TP (Proof a)
forall m t.
(Proposition (Forall "f" Formula -> SBool), Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> (Forall "f" Formula -> SBool)
-> (MeasureArgs (Forall "f" Formula -> SBool) m, [ProofObj])
-> (Proof (Forall "f" Formula -> SBool)
    -> StepArgs (Forall "f" Formula -> SBool) t)
-> TP (Proof (Forall "f" Formula -> SBool))
sInductWith SMTConfig
cvc5 String
"normalizeCorrect"
              (\(Forall SBV Formula
f) -> SBV Formula -> SBool
isNormal (SBV Formula -> SBV Formula
normalize SBV Formula
f))
              (\SBV Formula
f -> (SBV Integer, SBV Integer) -> SBV (Integer, Integer)
forall tup a. Tuple tup a => a -> SBV tup
tuple (SBV Formula -> SBV Integer
ifComplexity SBV Formula
f, SBV Formula -> SBV Integer
ifDepth SBV Formula
f), [Proof (Forall "f" Formula -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "f" Formula -> SBool)
icp, Proof (Forall "f" Formula -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "f" Formula -> SBool)
idn]) ((Proof (Forall "f" Formula -> SBool)
  -> StepArgs (Forall "f" Formula -> SBool) Bool)
 -> TP (Proof (Forall "f" Formula -> SBool)))
-> (Proof (Forall "f" Formula -> SBool)
    -> StepArgs (Forall "f" Formula -> SBool) Bool)
-> TP (Proof (Forall "f" Formula -> SBool))
forall a b. (a -> b) -> a -> b
$
              \Proof (Forall "f" Formula -> SBool)
ih SBV Formula
f -> []
                    [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV Formula -> SBool
isNormal (SBV Formula -> SBV Formula
normalize SBV Formula
f)
                    SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SBV Formula -> SBool
isFTrue  SBV Formula
f SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial
                             , SBV Formula -> SBool
isFFalse SBV Formula
f SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial
                             , SBV Formula -> SBool
isVar    SBV Formula
f SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial
                             , SBV Formula -> SBool
isIf     SBV Formula
f SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> let c :: SBV Formula
c = SBV Formula -> SBV Formula
sifCond SBV Formula
f
                                                  l :: SBV Formula
l = SBV Formula -> SBV Formula
sifThen SBV Formula
f
                                                  r :: SBV Formula
r = SBV Formula -> SBV Formula
sifElse SBV Formula
f
                                              in [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SBV Formula -> SBool
isIf SBV Formula
c SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==>
                                                           let p :: SBV Formula
p  = SBV Formula -> SBV Formula
sifCond SBV Formula
c
                                                               q :: SBV Formula
q  = SBV Formula -> SBV Formula
sifThen SBV Formula
c
                                                               rc :: SBV Formula
rc = SBV Formula -> SBV Formula
sifElse SBV Formula
c
                                                               transformed :: SBV Formula
transformed = SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
p (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
q SBV Formula
l SBV Formula
r) (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
rc SBV Formula
l SBV Formula
r)
                                                           in SBV Formula -> SBool
isNormal (SBV Formula -> SBV Formula
normalize SBV Formula
transformed)
                                                           SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "p" Formula
   -> Forall "q" Formula
   -> Forall "s" Formula
   -> Forall "l" Formula
   -> Forall "r" Formula
   -> SBool)
npc Proof
  (Forall "p" Formula
   -> Forall "q" Formula
   -> Forall "s" Formula
   -> Forall "l" Formula
   -> Forall "r" Formula
   -> SBool)
-> IArgs
     (Forall "p" Formula
      -> Forall "q" Formula
      -> Forall "s" Formula
      -> Forall "l" Formula
      -> Forall "r" Formula
      -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"p" SBV Formula
p, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"q" SBV Formula
q, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"s" SBV Formula
rc, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"r" SBV Formula
r)
                                                           TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "f" Formula -> SBool)
ih Proof (Forall "f" Formula -> SBool)
-> IArgs (Forall "f" Formula -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
transformed
                                                           Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (TPProofRaw SBool))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                                           SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                                                       , SBool -> SBool
sNot (SBV Formula -> SBool
isIf SBV Formula
c) SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==>
                                                              SBV Formula -> SBool
isNormal (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
c (SBV Formula -> SBV Formula
normalize SBV Formula
l) (SBV Formula -> SBV Formula
normalize SBV Formula
r))
                                                           SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool
sNot (SBV Formula -> SBool
isIf SBV Formula
c) SBool -> SBool -> SBool
.&& SBV Formula -> SBool
isNormal (SBV Formula -> SBV Formula
normalize SBV Formula
l) SBool -> SBool -> SBool
.&& SBV Formula -> SBool
isNormal (SBV Formula -> SBV Formula
normalize SBV Formula
r)
                                                           SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Formula -> SBool
isNormal (SBV Formula -> SBV Formula
normalize SBV Formula
l) SBool -> SBool -> SBool
.&& SBV Formula -> SBool
isNormal (SBV Formula -> SBV Formula
normalize SBV Formula
r)
                                                           SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> IArgs
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"c" SBV Formula
c, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"r" SBV Formula
r)
                                                           TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "f" Formula -> SBool)
ih  Proof (Forall "f" Formula -> SBool)
-> IArgs (Forall "f" Formula -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
l
                                                           Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (TPProofRaw SBool))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Formula -> SBool
isNormal (SBV Formula -> SBV Formula
normalize SBV Formula
r)
                                                           SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> IArgs
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"c" SBV Formula
c, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"r" SBV Formula
r)
                                                           TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "f" Formula -> SBool)
ih  Proof (Forall "f" Formula -> SBool)
-> IArgs (Forall "f" Formula -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
r
                                                           Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (TPProofRaw SBool))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                                           SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
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.
-- [Proven] normalizeSame :: Ɐf ∷ Formula → Bool
normalizeSame :: TP (Proof (Forall "f" Formula -> SBool))
normalizeSame :: TP (Proof (Forall "f" Formula -> SBool))
normalizeSame = do
  Proof (Forall "f" Formula -> SBool)
icp <- String
-> TP (Proof (Forall "f" Formula -> SBool))
-> TP (Proof (Forall "f" Formula -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"ifComplexityPos"     TP (Proof (Forall "f" Formula -> SBool))
ifComplexityPos
  Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs <- String
-> TP
     (Proof
        (Forall "c" Formula
         -> Forall "l" Formula -> Forall "r" Formula -> SBool))
-> TP
     (Proof
        (Forall "c" Formula
         -> Forall "l" Formula -> Forall "r" Formula -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"ifComplexitySmaller" TP
  (Proof
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool))
ifComplexitySmaller

  String
-> (Forall "f" Formula -> SBool)
-> (MeasureArgs (Forall "f" Formula -> SBool) Integer, [ProofObj])
-> (Proof (Forall "f" Formula -> SBool)
    -> StepArgs (Forall "f" Formula -> SBool) Formula)
-> TP (Proof (Forall "f" Formula -> SBool))
forall a m t.
(SInductive a, Proposition a, Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
String
-> a
-> (MeasureArgs a m, [ProofObj])
-> (Proof a -> StepArgs a t)
-> TP (Proof a)
forall m t.
(Proposition (Forall "f" Formula -> SBool), Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "f" Formula -> SBool)
-> (MeasureArgs (Forall "f" Formula -> SBool) m, [ProofObj])
-> (Proof (Forall "f" Formula -> SBool)
    -> StepArgs (Forall "f" Formula -> SBool) t)
-> TP (Proof (Forall "f" Formula -> SBool))
sInduct String
"normalizeSame"
          (\(Forall SBV Formula
f) -> SBV Formula -> SBool
isNormal SBV Formula
f SBool -> SBool -> SBool
.=> SBV Formula -> SBV Formula
normalize SBV Formula
f SBV Formula -> SBV Formula -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Formula
f)
          (MeasureArgs (Forall "f" Formula -> SBool) Integer
SBV Formula -> SBV Integer
ifComplexity, [Proof (Forall "f" Formula -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "f" Formula -> SBool)
icp]) ((Proof (Forall "f" Formula -> SBool)
  -> StepArgs (Forall "f" Formula -> SBool) Formula)
 -> TP (Proof (Forall "f" Formula -> SBool)))
-> (Proof (Forall "f" Formula -> SBool)
    -> StepArgs (Forall "f" Formula -> SBool) Formula)
-> TP (Proof (Forall "f" Formula -> SBool))
forall a b. (a -> b) -> a -> b
$
          \Proof (Forall "f" Formula -> SBool)
ih SBV Formula
f -> [SBV Formula -> SBool
isNormal SBV Formula
f]
                [SBool]
-> TPProofRaw (SBV Formula) -> (SBool, TPProofRaw (SBV Formula))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- [(SBool, TPProofRaw (SBV Formula))] -> TPProofRaw (SBV Formula)
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SBV Formula -> SBool
isFTrue  SBV Formula
f SBool
-> TPProofRaw (SBV Formula) -> (SBool, TPProofRaw (SBV Formula))
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw (SBV Formula)
forall a. Trivial a => a
trivial
                         , SBV Formula -> SBool
isFFalse SBV Formula
f SBool
-> TPProofRaw (SBV Formula) -> (SBool, TPProofRaw (SBV Formula))
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw (SBV Formula)
forall a. Trivial a => a
trivial
                         , SBV Formula -> SBool
isVar    SBV Formula
f SBool
-> TPProofRaw (SBV Formula) -> (SBool, TPProofRaw (SBV Formula))
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw (SBV Formula)
forall a. Trivial a => a
trivial
                         , SBV Formula -> SBool
isIf     SBV Formula
f SBool
-> TPProofRaw (SBV Formula) -> (SBool, TPProofRaw (SBV Formula))
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> let c :: SBV Formula
c = SBV Formula -> SBV Formula
sifCond SBV Formula
f
                                              l :: SBV Formula
l = SBV Formula -> SBV Formula
sifThen SBV Formula
f
                                              r :: SBV Formula
r = SBV Formula -> SBV Formula
sifElse SBV Formula
f
                                          in SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
c (SBV Formula -> SBV Formula
normalize SBV Formula
l) (SBV Formula -> SBV Formula
normalize SBV Formula
r)
                                          SBV Formula -> Proof Bool -> Hinted (SBV Formula)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> IArgs
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"c" SBV Formula
c, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"r" SBV Formula
r)
                                          TPProofRaw (SBV Formula)
-> Proof Bool -> Hinted (TPProofRaw (SBV Formula))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "f" Formula -> SBool)
ih Proof (Forall "f" Formula -> SBool)
-> IArgs (Forall "f" Formula -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
l
                                          Hinted (TPProofRaw (SBV Formula))
-> ChainsTo (Hinted (TPProofRaw (SBV Formula)))
-> ChainsTo (Hinted (TPProofRaw (SBV Formula)))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
c SBV Formula
l (SBV Formula -> SBV Formula
normalize SBV Formula
r)
                                          SBV Formula -> Proof Bool -> Hinted (SBV Formula)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> IArgs
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"c" SBV Formula
c, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"r" SBV Formula
r)
                                          TPProofRaw (SBV Formula)
-> Proof Bool -> Hinted (TPProofRaw (SBV Formula))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "f" Formula -> SBool)
ih Proof (Forall "f" Formula -> SBool)
-> IArgs (Forall "f" Formula -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
r
                                          Hinted (TPProofRaw (SBV Formula))
-> ChainsTo (Hinted (TPProofRaw (SBV Formula)))
-> ChainsTo (Hinted (TPProofRaw (SBV Formula)))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
c SBV Formula
l SBV Formula
r
                                          SBV Formula -> ChainsTo (SBV Formula) -> ChainsTo (SBV Formula)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV Formula)
TPProofRaw (SBV Formula)
forall a. TPProofRaw a
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.
-- [Proven] normalizeRespectsTruth :: Ɐf ∷ Formula → Ɐbs ∷ [Binding] → Bool
normalizeRespectsTruth :: TP (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
normalizeRespectsTruth :: TP (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
normalizeRespectsTruth = do
  Proof (Forall "f" Formula -> SBool)
icp <- String
-> TP (Proof (Forall "f" Formula -> SBool))
-> TP (Proof (Forall "f" Formula -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"ifComplexityPos"              TP (Proof (Forall "f" Formula -> SBool))
ifComplexityPos
  Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs <- String
-> TP
     (Proof
        (Forall "c" Formula
         -> Forall "l" Formula -> Forall "r" Formula -> SBool))
-> TP
     (Proof
        (Forall "c" Formula
         -> Forall "l" Formula -> Forall "r" Formula -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"ifComplexitySmaller"          TP
  (Proof
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool))
ifComplexitySmaller
  Proof
  (Forall "p" Formula
   -> Forall "q" Formula
   -> Forall "s" Formula
   -> Forall "l" Formula
   -> Forall "r" Formula
   -> SBool)
npc <- String
-> TP
     (Proof
        (Forall "p" Formula
         -> Forall "q" Formula
         -> Forall "s" Formula
         -> Forall "l" Formula
         -> Forall "r" Formula
         -> SBool))
-> TP
     (Proof
        (Forall "p" Formula
         -> Forall "q" Formula
         -> Forall "s" Formula
         -> Forall "l" Formula
         -> Forall "r" Formula
         -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"normalizePreservesComplexity" TP
  (Proof
     (Forall "p" Formula
      -> Forall "q" Formula
      -> Forall "s" Formula
      -> Forall "l" Formula
      -> Forall "r" Formula
      -> SBool))
normalizePreservesComplexity
  Proof (Forall "f" Formula -> SBool)
idn <- String
-> TP (Proof (Forall "f" Formula -> SBool))
-> TP (Proof (Forall "f" Formula -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"ifDepthNonNeg"                TP (Proof (Forall "f" Formula -> SBool))
ifDepthNonNeg

  SMTConfig
-> String
-> (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> (MeasureArgs
      (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
      (Integer, Integer),
    [ProofObj])
-> (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
    -> StepArgs
         (Forall "f" Formula -> Forall "bs" [Binding] -> SBool) Bool)
-> TP
     (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
forall a m t.
(SInductive a, Proposition a, Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> a
-> (MeasureArgs a m, [ProofObj])
-> (Proof a -> StepArgs a t)
-> TP (Proof a)
forall m t.
(Proposition
   (Forall "f" Formula -> Forall "bs" [Binding] -> SBool),
 Zero m, SymVal t, EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> (MeasureArgs
      (Forall "f" Formula -> Forall "bs" [Binding] -> SBool) m,
    [ProofObj])
-> (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
    -> StepArgs
         (Forall "f" Formula -> Forall "bs" [Binding] -> SBool) t)
-> TP
     (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
sInductWith SMTConfig
cvc5 String
"normalizeRespectsTruth"
              (\(Forall SBV Formula
f) (Forall SList Binding
bs) -> SBV Formula -> SList Binding -> SBool
eval (SBV Formula -> SBV Formula
normalize SBV Formula
f) SList Binding
bs SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Formula -> SList Binding -> SBool
eval SBV Formula
f SList Binding
bs)
              (\SBV Formula
f SList Binding
_ -> (SBV Integer, SBV Integer) -> SBV (Integer, Integer)
forall tup a. Tuple tup a => a -> SBV tup
tuple (SBV Formula -> SBV Integer
ifComplexity SBV Formula
f, SBV Formula -> SBV Integer
ifDepth SBV Formula
f), [Proof (Forall "f" Formula -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "f" Formula -> SBool)
icp, Proof (Forall "f" Formula -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "f" Formula -> SBool)
idn]) ((Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
  -> StepArgs
       (Forall "f" Formula -> Forall "bs" [Binding] -> SBool) Bool)
 -> TP
      (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)))
-> (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
    -> StepArgs
         (Forall "f" Formula -> Forall "bs" [Binding] -> SBool) Bool)
-> TP
     (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
forall a b. (a -> b) -> a -> b
$
              \Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
ih SBV Formula
f SList Binding
bs -> []
                       [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SBV Formula -> SBool
isFTrue  SBV Formula
f SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial
                                , SBV Formula -> SBool
isFFalse SBV Formula
f SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial
                                , SBV Formula -> SBool
isVar    SBV Formula
f SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial
                                , SBV Formula -> SBool
isIf     SBV Formula
f SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> let c :: SBV Formula
c = SBV Formula -> SBV Formula
sifCond SBV Formula
f
                                                     l :: SBV Formula
l = SBV Formula -> SBV Formula
sifThen SBV Formula
f
                                                     r :: SBV Formula
r = SBV Formula -> SBV Formula
sifElse SBV Formula
f
                                                 in [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SBV Formula -> SBool
isIf SBV Formula
c SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==>
                                                              let p :: SBV Formula
p  = SBV Formula -> SBV Formula
sifCond SBV Formula
c
                                                                  q :: SBV Formula
q  = SBV Formula -> SBV Formula
sifThen SBV Formula
c
                                                                  rc :: SBV Formula
rc = SBV Formula -> SBV Formula
sifElse SBV Formula
c
                                                                  transformed :: SBV Formula
transformed = SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
p (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
q SBV Formula
l SBV Formula
r) (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
rc SBV Formula
l SBV Formula
r)
                                                              in SBV Formula -> SList Binding -> SBool
eval (SBV Formula -> SBV Formula
normalize (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
c SBV Formula
l SBV Formula
r)) SList Binding
bs SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Formula -> SList Binding -> SBool
eval (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
c SBV Formula
l SBV Formula
r) SList Binding
bs
                                                              SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "p" Formula
   -> Forall "q" Formula
   -> Forall "s" Formula
   -> Forall "l" Formula
   -> Forall "r" Formula
   -> SBool)
npc Proof
  (Forall "p" Formula
   -> Forall "q" Formula
   -> Forall "s" Formula
   -> Forall "l" Formula
   -> Forall "r" Formula
   -> SBool)
-> IArgs
     (Forall "p" Formula
      -> Forall "q" Formula
      -> Forall "s" Formula
      -> Forall "l" Formula
      -> Forall "r" Formula
      -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"p" SBV Formula
p, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"q" SBV Formula
q, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"s" SBV Formula
rc, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"r" SBV Formula
r)
                                                              TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
ih  Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> IArgs (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
transformed, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" SList Binding
bs)
                                                              Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (TPProofRaw SBool))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                                              SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                                                          , SBool -> SBool
sNot (SBV Formula -> SBool
isIf SBV Formula
c) SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==>
                                                                 SBV Formula -> SList Binding -> SBool
eval (SBV Formula -> SBV Formula
normalize (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
c SBV Formula
l SBV Formula
r)) SList Binding
bs SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Formula -> SList Binding -> SBool
eval (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
c SBV Formula
l SBV Formula
r) SList Binding
bs
                                                              SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Formula -> SList Binding -> SBool
eval (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
c (SBV Formula -> SBV Formula
normalize SBV Formula
l) (SBV Formula -> SBV Formula
normalize SBV Formula
r)) SList Binding
bs SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Formula -> SList Binding -> SBool
eval (SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
sIf SBV Formula
c SBV Formula
l SBV Formula
r) SList Binding
bs
                                                              SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Formula -> SList Binding -> SBool
eval SBV Formula
c SList Binding
bs) (SBV Formula -> SList Binding -> SBool
eval (SBV Formula -> SBV Formula
normalize SBV Formula
l) SList Binding
bs) (SBV Formula -> SList Binding -> SBool
eval (SBV Formula -> SBV Formula
normalize SBV Formula
r) SList Binding
bs) SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Formula -> SList Binding -> SBool
eval SBV Formula
c SList Binding
bs) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
l SList Binding
bs) (SBV Formula -> SList Binding -> SBool
eval SBV Formula
r SList Binding
bs)
                                                              SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> IArgs
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"c" SBV Formula
c, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"r" SBV Formula
r)
                                                              TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
ih  Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> IArgs (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" SList Binding
bs)
                                                              Hinted (TPProofRaw SBool)
-> Proof Bool -> Hinted (Hinted (TPProofRaw SBool))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
ih  Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> IArgs (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
r, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" SList Binding
bs)
                                                              Hinted (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (Hinted (TPProofRaw SBool)))
-> ChainsTo (Hinted (Hinted (TPProofRaw SBool)))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                                              SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
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.
-- [Proven] soundness :: Ɐf ∷ Formula → Ɐbindings ∷ [Binding] → Bool
soundness :: TP (Proof (Forall "f" Formula -> Forall "bindings" [Binding] -> SBool))
soundness :: TP
  (Proof
     (Forall "f" Formula -> Forall "bindings" [Binding] -> SBool))
soundness = do
  Proof
  (Forall "f" Formula
   -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
tie <- SMTConfig
-> String
-> TP
     (Proof
        (Forall "f" Formula
         -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool))
-> TP
     (Proof
        (Forall "f" Formula
         -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool))
forall a. SMTConfig -> String -> TP (Proof a) -> TP (Proof a)
recallWith SMTConfig
cvc5 String
"tautologyImpliesEval"   TP
  (Proof
     (Forall "f" Formula
      -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool))
tautologyImpliesEval
  Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
nrt <- String
-> TP
     (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
-> TP
     (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall          String
"normalizeRespectsTruth" TP (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
normalizeRespectsTruth
  Proof (Forall "f" Formula -> SBool)
nc  <- String
-> TP (Proof (Forall "f" Formula -> SBool))
-> TP (Proof (Forall "f" Formula -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall          String
"normalizeCorrect"       TP (Proof (Forall "f" Formula -> SBool))
normalizeCorrect

  String
-> (Forall "f" Formula -> Forall "bindings" [Binding] -> SBool)
-> StepArgs
     (Forall "f" Formula -> Forall "bindings" [Binding] -> SBool) Bool
-> TP
     (Proof
        (Forall "f" Formula -> Forall "bindings" [Binding] -> SBool))
forall t.
(Proposition
   (Forall "f" Formula -> Forall "bindings" [Binding] -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "f" Formula -> Forall "bindings" [Binding] -> SBool)
-> StepArgs
     (Forall "f" Formula -> Forall "bindings" [Binding] -> SBool) t
-> TP
     (Proof
        (Forall "f" Formula -> Forall "bindings" [Binding] -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"soundness"
       (\(Forall SBV Formula
f) (Forall SList Binding
bindings) -> SBV Formula -> SBool
isTautology SBV Formula
f SBool -> SBool -> SBool
.=> SBV Formula -> SList Binding -> SBool
eval SBV Formula
f SList Binding
bindings) (StepArgs
   (Forall "f" Formula -> Forall "bindings" [Binding] -> SBool) Bool
 -> TP
      (Proof
         (Forall "f" Formula -> Forall "bindings" [Binding] -> SBool)))
-> StepArgs
     (Forall "f" Formula -> Forall "bindings" [Binding] -> SBool) Bool
-> TP
     (Proof
        (Forall "f" Formula -> Forall "bindings" [Binding] -> SBool))
forall a b. (a -> b) -> a -> b
$
       \SBV Formula
f SList Binding
bindings -> [SBV Formula -> SBool
isTautology SBV Formula
f]
                   [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV Formula -> SList Binding -> SBool
eval SBV Formula
f SList Binding
bindings
                   SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
nrt Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> IArgs (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
f, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" SList Binding
bindings)
                   TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Formula -> SList Binding -> SBool
eval (SBV Formula -> SBV Formula
normalize SBV Formula
f) SList Binding
bindings
                   SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "f" Formula -> SBool)
nc  Proof (Forall "f" Formula -> SBool)
-> IArgs (Forall "f" Formula -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
f
                   TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "f" Formula
   -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
tie Proof
  (Forall "f" Formula
   -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
-> IArgs
     (Forall "f" Formula
      -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" (SBV Formula -> SBV Formula
normalize SBV Formula
f), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"a" SList Binding
bindings, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" [])
                   Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (TPProofRaw SBool))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                   SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed

-- * Completeness

-- | Result of attempting to falsify a formula.
data FalsifyResult = FalsifyResult { FalsifyResult -> Bool
falsified :: Bool
                                   , FalsifyResult -> [Binding]
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' :: SBV Formula -> SList Binding -> SBV FalsifyResult
falsify' = String
-> (SBV Formula -> SList Binding -> SBV FalsifyResult)
-> SBV Formula
-> SList Binding
-> SBV FalsifyResult
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"falsify'" ((SBV Formula -> SList Binding -> SBV FalsifyResult)
 -> SBV Formula -> SList Binding -> SBV FalsifyResult)
-> (SBV Formula -> SList Binding -> SBV FalsifyResult)
-> SBV Formula
-> SList Binding
-> SBV FalsifyResult
forall a b. (a -> b) -> a -> b
$ \SBV Formula
f SList Binding
bs ->
  [sCase|Formula 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 :: SBV Formula -> SBV FalsifyResult
falsify SBV Formula
f = SBV Formula -> SList Binding -> SBV FalsifyResult
falsify' (SBV Formula -> SBV Formula
normalize SBV Formula
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.
-- [Proven] nonTautIsFalsified :: Ɐf ∷ Formula → Ɐbs ∷ [Binding] → Bool
nonTautIsFalsified :: TP (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
nonTautIsFalsified :: TP (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
nonTautIsFalsified = do
  Proof (Forall "f" Formula -> SBool)
icp <- String
-> TP (Proof (Forall "f" Formula -> SBool))
-> TP (Proof (Forall "f" Formula -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"ifComplexityPos"     TP (Proof (Forall "f" Formula -> SBool))
ifComplexityPos
  Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs <- String
-> TP
     (Proof
        (Forall "c" Formula
         -> Forall "l" Formula -> Forall "r" Formula -> SBool))
-> TP
     (Proof
        (Forall "c" Formula
         -> Forall "l" Formula -> Forall "r" Formula -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"ifComplexitySmaller" TP
  (Proof
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool))
ifComplexitySmaller

  String
-> (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> (MeasureArgs
      (Forall "f" Formula -> Forall "bs" [Binding] -> SBool) Integer,
    [ProofObj])
-> (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
    -> StepArgs
         (Forall "f" Formula -> Forall "bs" [Binding] -> SBool) Bool)
-> TP
     (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
forall a m t.
(SInductive a, Proposition a, Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
String
-> a
-> (MeasureArgs a m, [ProofObj])
-> (Proof a -> StepArgs a t)
-> TP (Proof a)
forall m t.
(Proposition
   (Forall "f" Formula -> Forall "bs" [Binding] -> SBool),
 Zero m, SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> (MeasureArgs
      (Forall "f" Formula -> Forall "bs" [Binding] -> SBool) m,
    [ProofObj])
-> (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
    -> StepArgs
         (Forall "f" Formula -> Forall "bs" [Binding] -> SBool) t)
-> TP
     (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
sInduct String
"nonTautIsFalsified"
          (\(Forall SBV Formula
f) (Forall SList Binding
bs) -> SBV Formula -> SBool
isNormal SBV Formula
f SBool -> SBool -> SBool
.&& SBool -> SBool
sNot (SBV Formula -> SList Binding -> SBool
isTautology' SBV Formula
f SList Binding
bs) SBool -> SBool -> SBool
.=> SBV FalsifyResult -> SBool
sfalsified (SBV Formula -> SList Binding -> SBV FalsifyResult
falsify' SBV Formula
f SList Binding
bs))
          (\SBV Formula
f SList Binding
_ -> SBV Formula -> SBV Integer
ifComplexity SBV Formula
f, [Proof (Forall "f" Formula -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "f" Formula -> SBool)
icp]) ((Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
  -> StepArgs
       (Forall "f" Formula -> Forall "bs" [Binding] -> SBool) Bool)
 -> TP
      (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)))
-> (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
    -> StepArgs
         (Forall "f" Formula -> Forall "bs" [Binding] -> SBool) Bool)
-> TP
     (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
forall a b. (a -> b) -> a -> b
$
          \Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
ih SBV Formula
f SList Binding
bs -> [SBV Formula -> SBool
isNormal SBV Formula
f, SBool -> SBool
sNot (SBV Formula -> SList Binding -> SBool
isTautology' SBV Formula
f SList Binding
bs)]
                   [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SBV Formula -> SBool
isFTrue  SBV Formula
f SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial
                            , SBV Formula -> SBool
isFFalse SBV Formula
f SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial
                            , SBV Formula -> SBool
isVar    SBV Formula
f SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial
                            , SBV Formula -> SBool
isIf     SBV Formula
f SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> let c :: SBV Formula
c = SBV Formula -> SBV Formula
sifCond SBV Formula
f
                                                 l :: SBV Formula
l = SBV Formula -> SBV Formula
sifThen SBV Formula
f
                                                 r :: SBV Formula
r = SBV Formula -> SBV Formula
sifElse SBV Formula
f
                                             in SBV FalsifyResult -> SBool
sfalsified (SBV Formula -> SList Binding -> SBV FalsifyResult
falsify' SBV Formula
f SList Binding
bs)
                                             SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> IArgs
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"c" SBV Formula
c, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"r" SBV Formula
r)
                                             TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
ih  Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> IArgs (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" SList Binding
bs)
                                             Hinted (TPProofRaw SBool)
-> Proof Bool -> Hinted (Hinted (TPProofRaw SBool))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
ih  Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> IArgs (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
r, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" SList Binding
bs)
                                             Hinted (Hinted (TPProofRaw SBool))
-> Proof Bool -> Hinted (Hinted (Hinted (TPProofRaw SBool)))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
ih  Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> IArgs (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" (SBV Integer -> SList Binding -> SList Binding
assumeTrue (SBV Formula -> SBV Integer
sfVar SBV Formula
c) SList Binding
bs))
                                             Hinted (Hinted (Hinted (TPProofRaw SBool)))
-> Proof Bool
-> Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool))))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
ih  Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> IArgs (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
r, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" (SBV Integer -> SList Binding -> SList Binding
assumeFalse (SBV Formula -> SBV Integer
sfVar SBV Formula
c) SList Binding
bs))
                                             Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool))))
-> ChainsTo (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool)))))
-> ChainsTo (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool)))))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                             SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
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.
-- [Proven] falsifyExtendsBindings :: Ɐf ∷ Formula → Ɐbs ∷ [Binding] → Ɐi ∷ Integer → Bool
falsifyExtendsBindings :: TP (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool))
falsifyExtendsBindings :: TP
  (Proof
     (Forall "f" Formula
      -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool))
falsifyExtendsBindings = do
  Proof (Forall "f" Formula -> SBool)
icp <- String
-> TP (Proof (Forall "f" Formula -> SBool))
-> TP (Proof (Forall "f" Formula -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"ifComplexityPos"     TP (Proof (Forall "f" Formula -> SBool))
ifComplexityPos
  Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs <- String
-> TP
     (Proof
        (Forall "c" Formula
         -> Forall "l" Formula -> Forall "r" Formula -> SBool))
-> TP
     (Proof
        (Forall "c" Formula
         -> Forall "l" Formula -> Forall "r" Formula -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"ifComplexitySmaller" TP
  (Proof
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool))
ifComplexitySmaller
  Proof
  (Forall "i" Integer
   -> Forall "n" Integer
   -> Forall "v" Bool
   -> Forall "bs" [Binding]
   -> SBool)
iae <- String
-> TP
     (Proof
        (Forall "i" Integer
         -> Forall "n" Integer
         -> Forall "v" Bool
         -> Forall "bs" [Binding]
         -> SBool))
-> TP
     (Proof
        (Forall "i" Integer
         -> Forall "n" Integer
         -> Forall "v" Bool
         -> Forall "bs" [Binding]
         -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"isAssignedExtends"   TP
  (Proof
     (Forall "i" Integer
      -> Forall "n" Integer
      -> Forall "v" Bool
      -> Forall "bs" [Binding]
      -> SBool))
isAssignedExtends
  Proof
  (Forall "i" Integer
   -> Forall "n" Integer
   -> Forall "v" Bool
   -> Forall "bs" [Binding]
   -> SBool)
lue <- String
-> TP
     (Proof
        (Forall "i" Integer
         -> Forall "n" Integer
         -> Forall "v" Bool
         -> Forall "bs" [Binding]
         -> SBool))
-> TP
     (Proof
        (Forall "i" Integer
         -> Forall "n" Integer
         -> Forall "v" Bool
         -> Forall "bs" [Binding]
         -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"lookUpExtends"       TP
  (Proof
     (Forall "i" Integer
      -> Forall "n" Integer
      -> Forall "v" Bool
      -> Forall "bs" [Binding]
      -> SBool))
lookUpExtends

  String
-> (Forall "f" Formula
    -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
-> (MeasureArgs
      (Forall "f" Formula
       -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
      Integer,
    [ProofObj])
-> (Proof
      (Forall "f" Formula
       -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
    -> StepArgs
         (Forall "f" Formula
          -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
         Bool)
-> TP
     (Proof
        (Forall "f" Formula
         -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool))
forall a m t.
(SInductive a, Proposition a, Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
String
-> a
-> (MeasureArgs a m, [ProofObj])
-> (Proof a -> StepArgs a t)
-> TP (Proof a)
forall m t.
(Proposition
   (Forall "f" Formula
    -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool),
 Zero m, SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "f" Formula
    -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
-> (MeasureArgs
      (Forall "f" Formula
       -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
      m,
    [ProofObj])
-> (Proof
      (Forall "f" Formula
       -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
    -> StepArgs
         (Forall "f" Formula
          -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
         t)
-> TP
     (Proof
        (Forall "f" Formula
         -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool))
sInduct String
"falsifyExtendsBindings"
          (\(Forall SBV Formula
f) (Forall SList Binding
bs) (Forall SBV Integer
i) ->
             SBV Integer -> SList Binding -> SBool
isAssigned SBV Integer
i SList Binding
bs SBool -> SBool -> SBool
.&& SBV FalsifyResult -> SBool
sfalsified (SBV Formula -> SList Binding -> SBV FalsifyResult
falsify' SBV Formula
f SList Binding
bs) SBool -> SBool -> SBool
.=>
             SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
i (SBV FalsifyResult -> SList Binding
scex (SBV Formula -> SList Binding -> SBV FalsifyResult
falsify' SBV Formula
f SList Binding
bs)) SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
i SList Binding
bs)
          (\SBV Formula
f SList Binding
_ SBV Integer
_ -> SBV Formula -> SBV Integer
ifComplexity SBV Formula
f, [Proof (Forall "f" Formula -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "f" Formula -> SBool)
icp]) ((Proof
    (Forall "f" Formula
     -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
  -> StepArgs
       (Forall "f" Formula
        -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
       Bool)
 -> TP
      (Proof
         (Forall "f" Formula
          -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)))
-> (Proof
      (Forall "f" Formula
       -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
    -> StepArgs
         (Forall "f" Formula
          -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
         Bool)
-> TP
     (Proof
        (Forall "f" Formula
         -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
          \Proof
  (Forall "f" Formula
   -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
ih SBV Formula
f SList Binding
bs SBV Integer
i -> [SBV Integer -> SList Binding -> SBool
isAssigned SBV Integer
i SList Binding
bs, SBV FalsifyResult -> SBool
sfalsified (SBV Formula -> SList Binding -> SBV FalsifyResult
falsify' SBV Formula
f SList Binding
bs)]
                     [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SBV Formula -> SBool
isFTrue  SBV Formula
f SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial
                              , SBV Formula -> SBool
isFFalse SBV Formula
f SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial
                              , SBV Formula -> SBool
isVar    SBV Formula
f SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> let n :: SBV Integer
n = SBV Formula -> SBV Integer
sfVar SBV Formula
f
                                               in SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
i (SBV FalsifyResult -> SList Binding
scex (SBV Formula -> SList Binding -> SBV FalsifyResult
falsify' SBV Formula
f SList Binding
bs)) SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
i SList Binding
bs
                                               SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "i" Integer
   -> Forall "n" Integer
   -> Forall "v" Bool
   -> Forall "bs" [Binding]
   -> SBool)
lue Proof
  (Forall "i" Integer
   -> Forall "n" Integer
   -> Forall "v" Bool
   -> Forall "bs" [Binding]
   -> SBool)
-> IArgs
     (Forall "i" Integer
      -> Forall "n" Integer
      -> Forall "v" Bool
      -> Forall "bs" [Binding]
      -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"i" SBV Integer
i, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SBV Integer
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"v" SBool
sFalse, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" SList Binding
bs)
                                               TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                               SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                              , SBV Formula -> SBool
isIf     SBV Formula
f SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> let c :: SBV Formula
c = SBV Formula -> SBV Formula
sifCond SBV Formula
f
                                                   l :: SBV Formula
l = SBV Formula -> SBV Formula
sifThen SBV Formula
f
                                                   r :: SBV Formula
r = SBV Formula -> SBV Formula
sifElse SBV Formula
f
                                                   n :: SBV Integer
n = SBV Formula -> SBV Integer
sfVar SBV Formula
c
                                               in SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
i (SBV FalsifyResult -> SList Binding
scex (SBV Formula -> SList Binding -> SBV FalsifyResult
falsify' SBV Formula
f SList Binding
bs)) SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
i SList Binding
bs
                                               SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> IArgs
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"c" SBV Formula
c, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"r" SBV Formula
r)
                                               TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "i" Integer
   -> Forall "n" Integer
   -> Forall "v" Bool
   -> Forall "bs" [Binding]
   -> SBool)
iae Proof
  (Forall "i" Integer
   -> Forall "n" Integer
   -> Forall "v" Bool
   -> Forall "bs" [Binding]
   -> SBool)
-> IArgs
     (Forall "i" Integer
      -> Forall "n" Integer
      -> Forall "v" Bool
      -> Forall "bs" [Binding]
      -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"i" SBV Integer
i, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SBV Integer
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"v" SBool
sTrue,  forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" SList Binding
bs)
                                               Hinted (TPProofRaw SBool)
-> Proof Bool -> Hinted (Hinted (TPProofRaw SBool))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "i" Integer
   -> Forall "n" Integer
   -> Forall "v" Bool
   -> Forall "bs" [Binding]
   -> SBool)
iae Proof
  (Forall "i" Integer
   -> Forall "n" Integer
   -> Forall "v" Bool
   -> Forall "bs" [Binding]
   -> SBool)
-> IArgs
     (Forall "i" Integer
      -> Forall "n" Integer
      -> Forall "v" Bool
      -> Forall "bs" [Binding]
      -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"i" SBV Integer
i, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SBV Integer
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"v" SBool
sFalse, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" SList Binding
bs)
                                               Hinted (Hinted (TPProofRaw SBool))
-> Proof Bool -> Hinted (Hinted (Hinted (TPProofRaw SBool)))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "i" Integer
   -> Forall "n" Integer
   -> Forall "v" Bool
   -> Forall "bs" [Binding]
   -> SBool)
lue Proof
  (Forall "i" Integer
   -> Forall "n" Integer
   -> Forall "v" Bool
   -> Forall "bs" [Binding]
   -> SBool)
-> IArgs
     (Forall "i" Integer
      -> Forall "n" Integer
      -> Forall "v" Bool
      -> Forall "bs" [Binding]
      -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"i" SBV Integer
i, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SBV Integer
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"v" SBool
sTrue,  forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" SList Binding
bs)
                                               Hinted (Hinted (Hinted (TPProofRaw SBool)))
-> Proof Bool
-> Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool))))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "i" Integer
   -> Forall "n" Integer
   -> Forall "v" Bool
   -> Forall "bs" [Binding]
   -> SBool)
lue Proof
  (Forall "i" Integer
   -> Forall "n" Integer
   -> Forall "v" Bool
   -> Forall "bs" [Binding]
   -> SBool)
-> IArgs
     (Forall "i" Integer
      -> Forall "n" Integer
      -> Forall "v" Bool
      -> Forall "bs" [Binding]
      -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"i" SBV Integer
i, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SBV Integer
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"v" SBool
sFalse, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" SList Binding
bs)
                                               Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool))))
-> Proof Bool
-> Hinted (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool)))))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "f" Formula
   -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
ih  Proof
  (Forall "f" Formula
   -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
-> IArgs
     (Forall "f" Formula
      -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" SList Binding
bs, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"i" SBV Integer
i)
                                               Hinted (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool)))))
-> Proof Bool
-> Hinted
     (Hinted (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool))))))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "f" Formula
   -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
ih  Proof
  (Forall "f" Formula
   -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
-> IArgs
     (Forall "f" Formula
      -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
r, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" SList Binding
bs, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"i" SBV Integer
i)
                                               Hinted
  (Hinted (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool))))))
-> Proof Bool
-> Hinted
     (Hinted
        (Hinted (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool)))))))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "f" Formula
   -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
ih  Proof
  (Forall "f" Formula
   -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
-> IArgs
     (Forall "f" Formula
      -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" (SBV Integer -> SList Binding -> SList Binding
assumeTrue SBV Integer
n SList Binding
bs), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"i" SBV Integer
i)
                                               Hinted
  (Hinted
     (Hinted (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool)))))))
-> Proof Bool
-> Hinted
     (Hinted
        (Hinted
           (Hinted (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool))))))))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "f" Formula
   -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
ih  Proof
  (Forall "f" Formula
   -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
-> IArgs
     (Forall "f" Formula
      -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
r, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" (SBV Integer -> SList Binding -> SList Binding
assumeFalse SBV Integer
n SList Binding
bs), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"i" SBV Integer
i)
                                               Hinted
  (Hinted
     (Hinted
        (Hinted (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool))))))))
-> ChainsTo
     (Hinted
        (Hinted
           (Hinted
              (Hinted (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool)))))))))
-> ChainsTo
     (Hinted
        (Hinted
           (Hinted
              (Hinted (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool)))))))))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                               SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
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.
-- [Proven] falsifyFalsifies :: Ɐf ∷ Formula → Ɐbs ∷ [Binding] → Bool
falsifyFalsifies :: TP (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
falsifyFalsifies :: TP (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
falsifyFalsifies = do
  Proof (Forall "f" Formula -> SBool)
icp <- String
-> TP (Proof (Forall "f" Formula -> SBool))
-> TP (Proof (Forall "f" Formula -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"ifComplexityPos"        TP (Proof (Forall "f" Formula -> SBool))
ifComplexityPos
  Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs <- String
-> TP
     (Proof
        (Forall "c" Formula
         -> Forall "l" Formula -> Forall "r" Formula -> SBool))
-> TP
     (Proof
        (Forall "c" Formula
         -> Forall "l" Formula -> Forall "r" Formula -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"ifComplexitySmaller"    TP
  (Proof
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool))
ifComplexitySmaller
  Proof
  (Forall "f" Formula
   -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
feb <- String
-> TP
     (Proof
        (Forall "f" Formula
         -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool))
-> TP
     (Proof
        (Forall "f" Formula
         -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"falsifyExtendsBindings" TP
  (Proof
     (Forall "f" Formula
      -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool))
falsifyExtendsBindings
  Proof
  (Forall "n" Integer
   -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool)
lus <- String
-> TP
     (Proof
        (Forall "n" Integer
         -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool))
-> TP
     (Proof
        (Forall "n" Integer
         -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"lookUpSame"             TP
  (Proof
     (Forall "n" Integer
      -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool))
lookUpSame
  Proof
  (Forall "n" Integer
   -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool)
ias <- String
-> TP
     (Proof
        (Forall "n" Integer
         -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool))
-> TP
     (Proof
        (Forall "n" Integer
         -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"isAssignedSame"         TP
  (Proof
     (Forall "n" Integer
      -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool))
isAssignedSame

  String
-> (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> (MeasureArgs
      (Forall "f" Formula -> Forall "bs" [Binding] -> SBool) Integer,
    [ProofObj])
-> (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
    -> StepArgs
         (Forall "f" Formula -> Forall "bs" [Binding] -> SBool) Bool)
-> TP
     (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
forall a m t.
(SInductive a, Proposition a, Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
String
-> a
-> (MeasureArgs a m, [ProofObj])
-> (Proof a -> StepArgs a t)
-> TP (Proof a)
forall m t.
(Proposition
   (Forall "f" Formula -> Forall "bs" [Binding] -> SBool),
 Zero m, SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> (MeasureArgs
      (Forall "f" Formula -> Forall "bs" [Binding] -> SBool) m,
    [ProofObj])
-> (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
    -> StepArgs
         (Forall "f" Formula -> Forall "bs" [Binding] -> SBool) t)
-> TP
     (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
sInduct String
"falsifyFalsifies"
          (\(Forall SBV Formula
f) (Forall SList Binding
bs) -> SBV Formula -> SBool
isNormal SBV Formula
f SBool -> SBool -> SBool
.&& SBV FalsifyResult -> SBool
sfalsified (SBV Formula -> SList Binding -> SBV FalsifyResult
falsify' SBV Formula
f SList Binding
bs) SBool -> SBool -> SBool
.=> SBool -> SBool
sNot (SBV Formula -> SList Binding -> SBool
eval SBV Formula
f (SBV FalsifyResult -> SList Binding
scex (SBV Formula -> SList Binding -> SBV FalsifyResult
falsify' SBV Formula
f SList Binding
bs))))
          (\SBV Formula
f SList Binding
_ -> SBV Formula -> SBV Integer
ifComplexity SBV Formula
f, [Proof (Forall "f" Formula -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "f" Formula -> SBool)
icp]) ((Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
  -> StepArgs
       (Forall "f" Formula -> Forall "bs" [Binding] -> SBool) Bool)
 -> TP
      (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)))
-> (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
    -> StepArgs
         (Forall "f" Formula -> Forall "bs" [Binding] -> SBool) Bool)
-> TP
     (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
forall a b. (a -> b) -> a -> b
$
          \Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
ih SBV Formula
f SList Binding
bs -> [SBV Formula -> SBool
isNormal SBV Formula
f, SBV FalsifyResult -> SBool
sfalsified (SBV Formula -> SList Binding -> SBV FalsifyResult
falsify' SBV Formula
f SList Binding
bs)]
                   [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SBV Formula -> SBool
isFTrue  SBV Formula
f SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SBool -> SBool
sNot (SBV Formula -> SList Binding -> SBool
eval SBV Formula
f (SBV FalsifyResult -> SList Binding
scex (SBV Formula -> SList Binding -> SBV FalsifyResult
falsify' SBV Formula
f SList Binding
bs)))
                                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool
sNot (SBV Formula -> SList Binding -> SBool
eval SBV Formula
sFTrue (SBV FalsifyResult -> SList Binding
scex (SBV Formula -> SList Binding -> SBV FalsifyResult
falsify' SBV Formula
sFTrue SList Binding
bs)))
                                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool
sNot SBool
sTrue
                                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sFalse
                                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                            , SBV Formula -> SBool
isFFalse SBV Formula
f SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SBool -> SBool
sNot (SBV Formula -> SList Binding -> SBool
eval SBV Formula
f (SBV FalsifyResult -> SList Binding
scex (SBV Formula -> SList Binding -> SBV FalsifyResult
falsify' SBV Formula
f SList Binding
bs)))
                                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool
sNot (SBV Formula -> SList Binding -> SBool
eval SBV Formula
sFFalse SList Binding
bs)
                                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool
sNot SBool
sFalse
                                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                            , SBV Formula -> SBool
isVar    SBV Formula
f SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> let n :: SBV Integer
n = SBV Formula -> SBV Integer
sfVar SBV Formula
f
                                             in SBool -> SBool
sNot (SBV Formula -> SList Binding -> SBool
eval SBV Formula
f (SBV FalsifyResult -> SList Binding
scex (SBV Formula -> SList Binding -> SBV FalsifyResult
falsify' SBV Formula
f SList Binding
bs)))
                                             SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool
sNot (SBV Formula -> SList Binding -> SBool
eval (SBV Integer -> SBV Formula
sVar SBV Integer
n) (SBV FalsifyResult -> SList Binding
scex (SBV Formula -> SList Binding -> SBV FalsifyResult
falsify' (SBV Integer -> SBV Formula
sVar SBV Integer
n) SList Binding
bs)))
                                             SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool
sNot (SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
n (SBV FalsifyResult -> SList Binding
scex (SBV Formula -> SList Binding -> SBV FalsifyResult
falsify' (SBV Integer -> SBV Formula
sVar SBV Integer
n) SList Binding
bs)))
                                             SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                             SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                            , SBV Formula -> SBool
isIf     SBV Formula
f SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> let c :: SBV Formula
c = SBV Formula -> SBV Formula
sifCond SBV Formula
f
                                                 l :: SBV Formula
l = SBV Formula -> SBV Formula
sifThen SBV Formula
f
                                                 r :: SBV Formula
r = SBV Formula -> SBV Formula
sifElse SBV Formula
f
                                             in [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SBV Formula -> SBool
isFTrue  SBV Formula
c SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SBool -> SBool
sNot (SBV Formula -> SList Binding -> SBool
eval SBV Formula
f (SBV FalsifyResult -> SList Binding
scex (SBV Formula -> SList Binding -> SBV FalsifyResult
falsify' SBV Formula
f SList Binding
bs)))
                                                                    SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> IArgs
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"c" SBV Formula
c, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"r" SBV Formula
r)
                                                                    TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
ih  Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> IArgs (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" SList Binding
bs)
                                                                    Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (TPProofRaw SBool))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                                                    SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                                                      , SBV Formula -> SBool
isFFalse SBV Formula
c SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SBool -> SBool
sNot (SBV Formula -> SList Binding -> SBool
eval SBV Formula
f (SBV FalsifyResult -> SList Binding
scex (SBV Formula -> SList Binding -> SBV FalsifyResult
falsify' SBV Formula
f SList Binding
bs)))
                                                                    SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> IArgs
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"c" SBV Formula
c, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"r" SBV Formula
r)
                                                                    TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
ih  Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> IArgs (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
r, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" SList Binding
bs)
                                                                    Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (TPProofRaw SBool))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                                                    SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                                                      , SBV Formula -> SBool
isVar    SBV Formula
c SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> let n :: SBV Integer
n = SBV Formula -> SBV Integer
sfVar SBV Formula
c
                                                                       in [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SBV Integer -> SList Binding -> SBool
isAssigned SBV Integer
n SList Binding
bs SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==>
                                                                                      [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
n SList Binding
bs SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==>
                                                                                                  SBool -> SBool
sNot (SBV Formula -> SList Binding -> SBool
eval SBV Formula
f (SBV FalsifyResult -> SList Binding
scex (SBV Formula -> SList Binding -> SBV FalsifyResult
falsify' SBV Formula
f SList Binding
bs)))
                                                                                               SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> IArgs
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"c" SBV Formula
c, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"r" SBV Formula
r)
                                                                                               TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "f" Formula
   -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
feb Proof
  (Forall "f" Formula
   -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
-> IArgs
     (Forall "f" Formula
      -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" SList Binding
bs, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"i" SBV Integer
n)
                                                                                               Hinted (TPProofRaw SBool)
-> Proof Bool -> Hinted (Hinted (TPProofRaw SBool))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
ih  Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> IArgs (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" SList Binding
bs)
                                                                                               Hinted (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (Hinted (TPProofRaw SBool)))
-> ChainsTo (Hinted (Hinted (TPProofRaw SBool)))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                                                                               SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                                                                                            , SBool -> SBool
sNot (SBV Integer -> SList Binding -> SBool
lookUp SBV Integer
n SList Binding
bs) SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==>
                                                                                                  SBool -> SBool
sNot (SBV Formula -> SList Binding -> SBool
eval SBV Formula
f (SBV FalsifyResult -> SList Binding
scex (SBV Formula -> SList Binding -> SBV FalsifyResult
falsify' SBV Formula
f SList Binding
bs)))
                                                                                               SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> IArgs
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"c" SBV Formula
c, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"r" SBV Formula
r)
                                                                                               TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "f" Formula
   -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
feb Proof
  (Forall "f" Formula
   -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
-> IArgs
     (Forall "f" Formula
      -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
r, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" SList Binding
bs, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"i" SBV Integer
n)
                                                                                               Hinted (TPProofRaw SBool)
-> Proof Bool -> Hinted (Hinted (TPProofRaw SBool))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
ih  Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> IArgs (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
r, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" SList Binding
bs)
                                                                                               Hinted (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (Hinted (TPProofRaw SBool)))
-> ChainsTo (Hinted (Hinted (TPProofRaw SBool)))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                                                                               SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                                                                                            ]
                                                                                , SBool -> SBool
sNot (SBV Integer -> SList Binding -> SBool
isAssigned SBV Integer
n SList Binding
bs) SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==>
                                                                                      let resL :: SBV FalsifyResult
resL = SBV Formula -> SList Binding -> SBV FalsifyResult
falsify' SBV Formula
l (SBV Integer -> SList Binding -> SList Binding
assumeTrue SBV Integer
n SList Binding
bs)
                                                                                      in [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SBV FalsifyResult -> SBool
sfalsified SBV FalsifyResult
resL SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==>
                                                                                                     SBool -> SBool
sNot (SBV Formula -> SList Binding -> SBool
eval SBV Formula
f (SBV FalsifyResult -> SList Binding
scex (SBV Formula -> SList Binding -> SBV FalsifyResult
falsify' SBV Formula
f SList Binding
bs)))
                                                                                                  SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> IArgs
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"c" SBV Formula
c, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"r" SBV Formula
r)
                                                                                                  TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "n" Integer
   -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool)
ias Proof
  (Forall "n" Integer
   -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool)
-> IArgs
     (Forall "n" Integer
      -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SBV Integer
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"v" SBool
sTrue, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" SList Binding
bs)
                                                                                                  Hinted (TPProofRaw SBool)
-> Proof Bool -> Hinted (Hinted (TPProofRaw SBool))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "n" Integer
   -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool)
lus Proof
  (Forall "n" Integer
   -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool)
-> IArgs
     (Forall "n" Integer
      -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SBV Integer
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"v" SBool
sTrue, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" SList Binding
bs)
                                                                                                  Hinted (Hinted (TPProofRaw SBool))
-> Proof Bool -> Hinted (Hinted (Hinted (TPProofRaw SBool)))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "f" Formula
   -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
feb Proof
  (Forall "f" Formula
   -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
-> IArgs
     (Forall "f" Formula
      -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" (SBV Integer -> SList Binding -> SList Binding
assumeTrue SBV Integer
n SList Binding
bs), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"i" SBV Integer
n)
                                                                                                  Hinted (Hinted (Hinted (TPProofRaw SBool)))
-> Proof Bool
-> Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool))))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
ih  Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> IArgs (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" (SBV Integer -> SList Binding -> SList Binding
assumeTrue SBV Integer
n SList Binding
bs))
                                                                                                  Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool))))
-> ChainsTo (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool)))))
-> ChainsTo (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool)))))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                                                                                  SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                                                                                               , SBool -> SBool
sNot (SBV FalsifyResult -> SBool
sfalsified SBV FalsifyResult
resL) SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==>
                                                                                                     SBool -> SBool
sNot (SBV Formula -> SList Binding -> SBool
eval SBV Formula
f (SBV FalsifyResult -> SList Binding
scex (SBV Formula -> SList Binding -> SBV FalsifyResult
falsify' SBV Formula
f SList Binding
bs)))
                                                                                                  SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
ibs Proof
  (Forall "c" Formula
   -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> IArgs
     (Forall "c" Formula
      -> Forall "l" Formula -> Forall "r" Formula -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"c" SBV Formula
c, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SBV Formula
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"r" SBV Formula
r)
                                                                                                  TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "n" Integer
   -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool)
ias Proof
  (Forall "n" Integer
   -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool)
-> IArgs
     (Forall "n" Integer
      -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SBV Integer
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"v" SBool
sFalse, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" SList Binding
bs)
                                                                                                  Hinted (TPProofRaw SBool)
-> Proof Bool -> Hinted (Hinted (TPProofRaw SBool))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "n" Integer
   -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool)
lus Proof
  (Forall "n" Integer
   -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool)
-> IArgs
     (Forall "n" Integer
      -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SBV Integer
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"v" SBool
sFalse, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" SList Binding
bs)
                                                                                                  Hinted (Hinted (TPProofRaw SBool))
-> Proof Bool -> Hinted (Hinted (Hinted (TPProofRaw SBool)))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "f" Formula
   -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
feb Proof
  (Forall "f" Formula
   -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
-> IArgs
     (Forall "f" Formula
      -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
r, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" (SBV Integer -> SList Binding -> SList Binding
assumeFalse SBV Integer
n SList Binding
bs), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"i" SBV Integer
n)
                                                                                                  Hinted (Hinted (Hinted (TPProofRaw SBool)))
-> Proof Bool
-> Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool))))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
ih  Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> IArgs (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"f" SBV Formula
r, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" (SBV Integer -> SList Binding -> SList Binding
assumeFalse SBV Integer
n SList Binding
bs))
                                                                                                  Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool))))
-> ChainsTo (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool)))))
-> ChainsTo (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool)))))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                                                                                  SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                                                                                               ]
                                                                                ]
                                                      , SBV Formula -> SBool
isIf     SBV Formula
c SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SBool -> SBool
sNot (SBV Formula -> SList Binding -> SBool
eval SBV Formula
f (SBV FalsifyResult -> SList Binding
scex (SBV Formula -> SList Binding -> SBV FalsifyResult
falsify' SBV Formula
f SList Binding
bs)))
                                                                    SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue  -- Contradicts isNormal
                                                                    SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
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.
-- [Proven] completenessHelper :: Ɐf ∷ Formula → Bool
completenessHelper :: TP (Proof (Forall "f" Formula -> SBool))
completenessHelper :: TP (Proof (Forall "f" Formula -> SBool))
completenessHelper = do
  Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
ff  <- String
-> TP
     (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
-> TP
     (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall        String
"falsifyFalsifies"   TP (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
falsifyFalsifies
  Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
nti <- String
-> TP
     (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
-> TP
     (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall        String
"nonTautIsFalsified" TP (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
nonTautIsFalsified
  Proof (Forall "f" Formula -> SBool)
nc  <- SMTConfig
-> String
-> TP (Proof (Forall "f" Formula -> SBool))
-> TP (Proof (Forall "f" Formula -> SBool))
forall a. SMTConfig -> String -> TP (Proof a) -> TP (Proof a)
recallWith SMTConfig
z3 String
"normalizeCorrect"   TP (Proof (Forall "f" Formula -> SBool))
normalizeCorrect

  String
-> (Forall "f" Formula -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "f" Formula -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"completenessHelper"
        (\(Forall SBV Formula
f) -> SBool -> SBool
sNot (SBV Formula -> SBool
isTautology SBV Formula
f) SBool -> SBool -> SBool
.=> SBool -> SBool
sNot (SBV Formula -> SList Binding -> SBool
eval (SBV Formula -> SBV Formula
normalize SBV Formula
f) (SBV FalsifyResult -> SList Binding
scex (SBV Formula -> SBV FalsifyResult
falsify SBV Formula
f))))
        [Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
ff, Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
nti, Proof (Forall "f" Formula -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "f" Formula -> SBool)
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.
-- [Proven] completeness :: Ɐf ∷ Formula → Bool
completeness :: TP (Proof (Forall "f" Formula -> SBool))
completeness :: TP (Proof (Forall "f" Formula -> SBool))
completeness = do
  Proof (Forall "f" Formula -> SBool)
ch  <- String
-> TP (Proof (Forall "f" Formula -> SBool))
-> TP (Proof (Forall "f" Formula -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall        String
"completenessHelper"     TP (Proof (Forall "f" Formula -> SBool))
completenessHelper
  Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
nrt <- SMTConfig
-> String
-> TP
     (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
-> TP
     (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
forall a. SMTConfig -> String -> TP (Proof a) -> TP (Proof a)
recallWith SMTConfig
z3 String
"normalizeRespectsTruth" TP (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
normalizeRespectsTruth

  String
-> (Forall "f" Formula -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "f" Formula -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"completeness"
        (\(Forall SBV Formula
f) -> SBool -> SBool
sNot (SBV Formula -> SBool
isTautology SBV Formula
f) SBool -> SBool -> SBool
.=> SBool -> SBool
sNot (SBV Formula -> SList Binding -> SBool
eval SBV Formula
f (SBV FalsifyResult -> SList Binding
scex (SBV Formula -> SBV FalsifyResult
falsify SBV Formula
f))))
        [Proof (Forall "f" Formula -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "f" Formula -> SBool)
ch, Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)
nrt]