sbv-13.6: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Documentation.SBV.Examples.TP.ConstFold

Description

Correctness of constant folding for a simple expression language.

Synopsis

Documentation

type Exp = Expr String Integer Source #

Base expression type (used in quantifiers).

type EL = [(String, Integer)] Source #

Base environment-list type (used in quantifiers).

type SE = SExpr String Integer Source #

Symbolic expression over strings and integers.

type E = Env String Integer Source #

Symbolic environment over strings and integers.

Simplification

simplify :: SE -> SE Source #

Simplify an expression at the top level, assuming sub-expressions are already folded. The rules are:

  • Sqr (Con v)         → Con (v*v)
  • Inc (Con v)         → Con (v+1)
  • Add (Con 0) x       → x
  • Add x (Con 0)       → x
  • Add (Con a) (Con b) → Con (a+b)
  • Mul (Con 0) x       → Con 0
  • Mul x (Con 0)       → Con 0
  • Mul (Con 1) x       → x
  • Mul x (Con 1)       → x
  • Mul (Con a) (Con b) → Con (a*b)
  • Let nm (Con v) b    → subst nm v b

Substitution

subst :: SString -> SInteger -> SE -> SE Source #

Substitute a variable with a value in an expression. Capture-avoiding: if a Let-bound variable shadows the target, we do not substitute in the body.

  • Var x         → if x == nm then Con v else Var x
  • Con c         → Con c
  • Sqr a         → Sqr (subst nm v a)
  • Inc a         → Inc (subst nm v a)
  • Add a b       → Add (subst nm v a) (subst nm v b)
  • Mul a b       → Mul (subst nm v a) (subst nm v b)
  • Let x a b     → Let x (subst nm v a) (if x == nm then b else subst nm v b)

Constant folding

cfold :: SE -> SE Source #

Constant fold an expression bottom-up: first fold sub-expressions, then simplify.

Correctness

measureNonNeg :: TP (Proof (Forall "e" Exp -> SBool)) Source #

The size measure is always non-negative.

>>> runTP measureNonNeg
Lemma: measureNonNeg                    Q.E.D.
[Proven] measureNonNeg :: Ɐe ∷ (Expr [Char] Integer) → Bool

sqrCong :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)) Source #

Congruence for squaring: if a == b then a*a == b*b.

>>> runTP sqrCong
Lemma: sqrCong                          Q.E.D.
[Proven] sqrCong :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool

addCongL :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "c" Integer -> SBool)) Source #

Congruence for addition on the left: if a == b then a+c == b+c.

>>> runTP addCongL
Lemma: addCongL                         Q.E.D.
[Proven] addCongL :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐc ∷ Integer → Bool

addCongR :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "c" Integer -> SBool)) Source #

Congruence for addition on the right: if b == c then a+b == a+c.

>>> runTP addCongR
Lemma: addCongR                         Q.E.D.
[Proven] addCongR :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐc ∷ Integer → Bool

mulCongL :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "c" Integer -> SBool)) Source #

Congruence for multiplication on the left: if a == b then a*c == b*c.

>>> runTP mulCongL
Lemma: mulCongL                         Q.E.D.
[Proven] mulCongL :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐc ∷ Integer → Bool

mulCongR :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "c" Integer -> SBool)) Source #

Congruence for multiplication on the right: if b == c then a*b == a*c.

>>> runTP mulCongR
Lemma: mulCongR                         Q.E.D.
[Proven] mulCongR :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐc ∷ Integer → Bool

sqrHelper :: TP (Proof (Forall "env" EL -> Forall "a" Exp -> SBool)) Source #

Unfolding interpInEnv over Sqr.

>>> runTP sqrHelper
Lemma: sqrHelper                        Q.E.D.
[Proven] sqrHelper :: Ɐenv ∷ [([Char], Integer)] → Ɐa ∷ (Expr [Char] Integer) → Bool

addHelper :: TP (Proof (Forall "env" EL -> Forall "a" Exp -> Forall "b" Exp -> SBool)) Source #

Unfolding interpInEnv over Add.

>>> runTP addHelper
Lemma: addHelper                        Q.E.D.
[Proven] addHelper :: Ɐenv ∷ [([Char], Integer)] → Ɐa ∷ (Expr [Char] Integer) → Ɐb ∷ (Expr [Char] Integer) → Bool

mulHelper :: TP (Proof (Forall "env" EL -> Forall "a" Exp -> Forall "b" Exp -> SBool)) Source #

Unfolding interpInEnv over Mul.

>>> runTP mulHelper
Lemma: mulHelper                        Q.E.D.
[Proven] mulHelper :: Ɐenv ∷ [([Char], Integer)] → Ɐa ∷ (Expr [Char] Integer) → Ɐb ∷ (Expr [Char] Integer) → Bool

letHelper :: TP (Proof (Forall "env" EL -> Forall "nm" String -> Forall "a" Exp -> Forall "b" Exp -> SBool)) Source #

Unfolding interpInEnv over Let.

>>> runTP letHelper
Lemma: letHelper                        Q.E.D.
[Proven] letHelper :: Ɐenv ∷ [([Char], Integer)] → Ɐnm ∷ [Char] → Ɐa ∷ (Expr [Char] Integer) → Ɐb ∷ (Expr [Char] Integer) → Bool

Environment lemmas

lookupSwap :: TP (Proof (Forall "k" String -> Forall "b1" (String, Integer) -> Forall "b2" (String, Integer) -> Forall "env" EL -> SBool)) Source #

Swapping two adjacent bindings with distinct keys does not affect lookup.

>>> runTP lookupSwap
Lemma: lookupSwap
  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] lookupSwap :: Ɐk ∷ [Char] → Ɐb1 ∷ ([Char], Integer) → Ɐb2 ∷ ([Char], Integer) → Ɐenv ∷ [([Char], Integer)] → Bool

lookupSwapPfx :: TP (Proof (Forall "pfx" EL -> Forall "k" String -> Forall "b1" (String, Integer) -> Forall "b2" (String, Integer) -> Forall "env" EL -> SBool)) Source #

Generalized swap: swapping two adjacent distinct-keyed bindings behind a prefix does not affect lookup.

>>> runTP lookupSwapPfx
Lemma: lookupSwap                       Q.E.D.
Inductive lemma (strong): lookupSwapPfx
  Step: Measure is non-negative         Q.E.D.
  Step: 1 (2 way case split)
    Step: 1.1 (base)                    Q.E.D.
    Step: 1.2.1 (cons)                  Q.E.D.
    Step: 1.2.2                         Q.E.D.
    Step: 1.2.3                         Q.E.D.
    Step: 1.2.4                         Q.E.D.
    Step: 1.2.5                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
[Proven] lookupSwapPfx :: Ɐpfx ∷ [([Char], Integer)] → Ɐk ∷ [Char] → Ɐb1 ∷ ([Char], Integer) → Ɐb2 ∷ ([Char], Integer) → Ɐenv ∷ [([Char], Integer)] → Bool

lookupShadow :: TP (Proof (Forall "k" String -> Forall "b1" (String, Integer) -> Forall "b2" (String, Integer) -> Forall "env" EL -> SBool)) Source #

A shadowed binding does not affect lookup: if the same key appears first, the second is irrelevant.

>>> runTP lookupShadow
Lemma: lookupShadow                     Q.E.D.
[Proven] lookupShadow :: Ɐk ∷ [Char] → Ɐb1 ∷ ([Char], Integer) → Ɐb2 ∷ ([Char], Integer) → Ɐenv ∷ [([Char], Integer)] → Bool

lookupShadowPfx :: TP (Proof (Forall "pfx" EL -> Forall "k" String -> Forall "b1" (String, Integer) -> Forall "b2" (String, Integer) -> Forall "env" EL -> SBool)) Source #

Generalized shadow: a shadowed binding behind a prefix does not affect lookup.

>>> runTP lookupShadowPfx
Lemma: lookupShadow                     Q.E.D.
Inductive lemma (strong): lookupShadowPfx
  Step: Measure is non-negative         Q.E.D.
  Step: 1 (2 way case split)
    Step: 1.1 (base)                    Q.E.D.
    Step: 1.2.1 (cons)                  Q.E.D.
    Step: 1.2.2                         Q.E.D.
    Step: 1.2.3                         Q.E.D.
    Step: 1.2.4                         Q.E.D.
    Step: 1.2.5                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
[Proven] lookupShadowPfx :: Ɐpfx ∷ [([Char], Integer)] → Ɐk ∷ [Char] → Ɐb1 ∷ ([Char], Integer) → Ɐb2 ∷ ([Char], Integer) → Ɐenv ∷ [([Char], Integer)] → Bool

envSwap :: TP (Proof (Forall "e" Exp -> Forall "pfx" EL -> Forall "env" EL -> Forall "b1" (String, Integer) -> Forall "b2" (String, Integer) -> SBool)) Source #

Swapping two adjacent distinct-keyed bindings in the environment does not affect interpretation. The pfx parameter allows the swap to happen at any depth in the environment.

>>> runTPWith cvc5 envSwap
Lemma: measureNonNeg                    Q.E.D.
Lemma: lookupSwapPfx                    Q.E.D.
Lemma: sqrCong                          Q.E.D.
Lemma: sqrHelper                        Q.E.D.
Lemma: addCongL                         Q.E.D.
Lemma: addCongR                         Q.E.D.
Lemma: addHelper                        Q.E.D.
Lemma: mulCongL                         Q.E.D.
Lemma: mulCongR                         Q.E.D.
Lemma: mulHelper                        Q.E.D.
Lemma: letHelper                        Q.E.D.
Inductive lemma (strong): envSwap
  Step: Measure is non-negative         Q.E.D.
  Step: 1 (7 way case split)
    Step: 1.1 (Var)                     Q.E.D.
    Step: 1.2 (Con)                     Q.E.D.
    Step: 1.3.1 (Sqr)                   Q.E.D.
    Step: 1.3.2                         Q.E.D.
    Step: 1.3.3                         Q.E.D.
    Step: 1.4 (Inc)                     Q.E.D.
    Step: 1.5.1 (Add)                   Q.E.D.
    Step: 1.5.2                         Q.E.D.
    Step: 1.5.3                         Q.E.D.
    Step: 1.5.4                         Q.E.D.
    Step: 1.6.1 (Mul)                   Q.E.D.
    Step: 1.6.2                         Q.E.D.
    Step: 1.6.3                         Q.E.D.
    Step: 1.6.4                         Q.E.D.
    Step: 1.7.1 (Let)                   Q.E.D.
    Step: 1.7.2                         Q.E.D.
    Step: 1.7.3                         Q.E.D.
    Step: 1.7.4                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
[Proven] envSwap :: Ɐe ∷ (Expr [Char] Integer) → Ɐpfx ∷ [([Char], Integer)] → Ɐenv ∷ [([Char], Integer)] → Ɐb1 ∷ ([Char], Integer) → Ɐb2 ∷ ([Char], Integer) → Bool

envShadow :: TP (Proof (Forall "e" Exp -> Forall "pfx" EL -> Forall "env" EL -> Forall "b1" (String, Integer) -> Forall "b2" (String, Integer) -> SBool)) Source #

A shadowed binding in the environment does not affect interpretation. The pfx parameter allows the shadow to occur at any depth.

>>> runTPWith cvc5 envShadow
Lemma: measureNonNeg                    Q.E.D.
Lemma: lookupShadowPfx                  Q.E.D.
Lemma: sqrCong                          Q.E.D.
Lemma: sqrHelper                        Q.E.D.
Lemma: addCongL                         Q.E.D.
Lemma: addCongR                         Q.E.D.
Lemma: addHelper                        Q.E.D.
Lemma: mulCongL                         Q.E.D.
Lemma: mulCongR                         Q.E.D.
Lemma: mulHelper                        Q.E.D.
Lemma: letHelper                        Q.E.D.
Inductive lemma (strong): envShadow
  Step: Measure is non-negative         Q.E.D.
  Step: 1 (7 way case split)
    Step: 1.1 (Var)                     Q.E.D.
    Step: 1.2 (Con)                     Q.E.D.
    Step: 1.3.1 (Sqr)                   Q.E.D.
    Step: 1.3.2                         Q.E.D.
    Step: 1.3.3                         Q.E.D.
    Step: 1.4 (Inc)                     Q.E.D.
    Step: 1.5.1 (Add)                   Q.E.D.
    Step: 1.5.2                         Q.E.D.
    Step: 1.5.3                         Q.E.D.
    Step: 1.5.4                         Q.E.D.
    Step: 1.6.1 (Mul)                   Q.E.D.
    Step: 1.6.2                         Q.E.D.
    Step: 1.6.3                         Q.E.D.
    Step: 1.6.4                         Q.E.D.
    Step: 1.7.1 (Let)                   Q.E.D.
    Step: 1.7.2                         Q.E.D.
    Step: 1.7.3                         Q.E.D.
    Step: 1.7.4                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
[Proven] envShadow :: Ɐe ∷ (Expr [Char] Integer) → Ɐpfx ∷ [([Char], Integer)] → Ɐenv ∷ [([Char], Integer)] → Ɐb1 ∷ ([Char], Integer) → Ɐb2 ∷ ([Char], Integer) → Bool

Substitution correctness

varHelper :: TP (Proof (Forall "env" EL -> Forall "nm" String -> SBool)) Source #

Unfolding interpInEnv over Var.

>>> runTP varHelper
Lemma: varHelper                        Q.E.D.
[Proven] varHelper :: Ɐenv ∷ [([Char], Integer)] → Ɐnm ∷ [Char] → Bool

substCorrect :: TP (Proof (Forall "e" Exp -> Forall "nm" String -> Forall "v" Integer -> Forall "env" EL -> SBool)) Source #

Substitution preserves semantics: interpreting in an extended environment is the same as substituting and interpreting in the original environment.

>>> runTPWith cvc5 substCorrect
Lemma: measureNonNeg                    Q.E.D.
Lemma: sqrCong                          Q.E.D.
Lemma: sqrHelper                        Q.E.D.
Lemma: addHelper                        Q.E.D.
Lemma: mulCongL                         Q.E.D.
Lemma: mulCongR                         Q.E.D.
Lemma: mulHelper                        Q.E.D.
Lemma: letHelper                        Q.E.D.
Lemma: varHelper                        Q.E.D.
Lemma: envSwap                          Q.E.D.
Lemma: envShadow                        Q.E.D.
Inductive lemma (strong): substCorrect
  Step: Measure is non-negative         Q.E.D.
  Step: 1 (7 way case split)
    Step: 1.1 (2 way case split)
      Step: 1.1.1.1 (Var)               Q.E.D.
      Step: 1.1.1.2                     Q.E.D.
      Step: 1.1.1.3                     Q.E.D.
      Step: 1.1.1.4                     Q.E.D.
      Step: 1.1.1.5                     Q.E.D.
      Step: 1.1.2.1 (Var)               Q.E.D.
      Step: 1.1.2.2                     Q.E.D.
      Step: 1.1.2.3                     Q.E.D.
      Step: 1.1.2.4                     Q.E.D.
      Step: 1.1.2.5                     Q.E.D.
      Step: 1.1.Completeness            Q.E.D.
    Step: 1.2 (Con)                     Q.E.D.
    Step: 1.3.1 (Sqr)                   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.4 (Inc)                     Q.E.D.
    Step: 1.5.1 (Add)                   Q.E.D.
    Step: 1.5.2                         Q.E.D.
    Step: 1.5.3                         Q.E.D.
    Step: 1.5.4                         Q.E.D.
    Step: 1.6.1 (Mul)                   Q.E.D.
    Step: 1.6.2                         Q.E.D.
    Step: 1.6.3                         Q.E.D.
    Step: 1.6.4                         Q.E.D.
    Step: 1.6.5                         Q.E.D.
    Step: 1.7.1 (Let)                   Q.E.D.
    Step: 1.7.2 (2 way case split)
      Step: 1.7.2.1.1                   Q.E.D.
      Step: 1.7.2.1.2 (shadow)          Q.E.D.
      Step: 1.7.2.1.3                   Q.E.D.
      Step: 1.7.2.1.4                   Q.E.D.
      Step: 1.7.2.1.5                   Q.E.D.
      Step: 1.7.2.2.1                   Q.E.D.
      Step: 1.7.2.2.2 (swap)            Q.E.D.
      Step: 1.7.2.2.3                   Q.E.D.
      Step: 1.7.2.2.4                   Q.E.D.
      Step: 1.7.2.2.5                   Q.E.D.
      Step: 1.7.2.2.6                   Q.E.D.
      Step: 1.7.2.Completeness          Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
[Proven] substCorrect :: Ɐe ∷ (Expr [Char] Integer) → Ɐnm ∷ [Char] → Ɐv ∷ Integer → Ɐenv ∷ [([Char], Integer)] → Bool

simpCorrect :: TP (Proof (Forall "e" Exp -> Forall "env" EL -> SBool)) Source #

Simplification preserves semantics.

>>> runTPWith cvc5 simpCorrect
Lemma: sqrCong                          Q.E.D.
Lemma: sqrHelper                        Q.E.D.
Lemma: addHelper                        Q.E.D.
Lemma: mulCongL                         Q.E.D.
Lemma: mulCongR                         Q.E.D.
Lemma: mulHelper                        Q.E.D.
Lemma: letHelper                        Q.E.D.
Lemma: substCorrect                     Q.E.D.
Lemma: simpCorrect
  Step: 1 (7 way case split)
    Step: 1.1.1 (Var)                   Q.E.D.
    Step: 1.1.2                         Q.E.D.
    Step: 1.1.3                         Q.E.D.
    Step: 1.2.1 (Con)                   Q.E.D.
    Step: 1.2.2                         Q.E.D.
    Step: 1.2.3                         Q.E.D.
    Step: 1.3.1 (Sqr)                   Q.E.D.
    Step: 1.3.2 (2 way case split)
      Step: 1.3.2.1.1                   Q.E.D.
      Step: 1.3.2.1.2 (Sqr Con)         Q.E.D.
      Step: 1.3.2.1.3                   Q.E.D.
      Step: 1.3.2.1.4                   Q.E.D.
      Step: 1.3.2.1.5                   Q.E.D.
      Step: 1.3.2.2.1                   Q.E.D.
      Step: 1.3.2.2.2 (Sqr _)           Q.E.D.
      Step: 1.3.2.Completeness          Q.E.D.
    Step: 1.4.1 (Inc)                   Q.E.D.
    Step: 1.4.2 (2 way case split)
      Step: 1.4.2.1.1                   Q.E.D.
      Step: 1.4.2.1.2 (Inc Con)         Q.E.D.
      Step: 1.4.2.1.3                   Q.E.D.
      Step: 1.4.2.2.1                   Q.E.D.
      Step: 1.4.2.2.2 (Inc _)           Q.E.D.
      Step: 1.4.2.Completeness          Q.E.D.
    Step: 1.5.1 (Add)                   Q.E.D.
    Step: 1.5.2 (6 way case split)
      Step: 1.5.2.1.1                   Q.E.D.
      Step: 1.5.2.1.2 (Add 0+b)         Q.E.D.
      Step: 1.5.2.1.3                   Q.E.D.
      Step: 1.5.2.2.1                   Q.E.D.
      Step: 1.5.2.2.2 (Add a+0)         Q.E.D.
      Step: 1.5.2.2.3                   Q.E.D.
      Step: 1.5.2.3.1                   Q.E.D.
      Step: 1.5.2.3.2 (Add Con)         Q.E.D.
      Step: 1.5.2.3.3                   Q.E.D.
      Step: 1.5.2.4 (2 way case split)
        Step: 1.5.2.4.1.1               Q.E.D.
        Step: 1.5.2.4.1.2 (Add 0,_)     Q.E.D.
        Step: 1.5.2.4.1.3               Q.E.D.
        Step: 1.5.2.4.2.1               Q.E.D.
        Step: 1.5.2.4.2.2 (Add C,_)     Q.E.D.
        Step: 1.5.2.4.Completeness      Q.E.D.
      Step: 1.5.2.5 (2 way case split)
        Step: 1.5.2.5.1.1               Q.E.D.
        Step: 1.5.2.5.1.2 (Add _,0)     Q.E.D.
        Step: 1.5.2.5.1.3               Q.E.D.
        Step: 1.5.2.5.2.1               Q.E.D.
        Step: 1.5.2.5.2.2 (Add _,C)     Q.E.D.
        Step: 1.5.2.5.Completeness      Q.E.D.
      Step: 1.5.2.6.1                   Q.E.D.
      Step: 1.5.2.6.2 (Add _,_)         Q.E.D.
      Step: 1.5.2.Completeness          Q.E.D.
    Step: 1.6.1 (Mul)                   Q.E.D.
    Step: 1.6.2 (8 way case split)
      Step: 1.6.2.1.1                   Q.E.D.
      Step: 1.6.2.1.2 (Mul 0*b)         Q.E.D.
      Step: 1.6.2.1.3                   Q.E.D.
      Step: 1.6.2.2.1                   Q.E.D.
      Step: 1.6.2.2.2 (Mul a*0)         Q.E.D.
      Step: 1.6.2.2.3                   Q.E.D.
      Step: 1.6.2.3.1                   Q.E.D.
      Step: 1.6.2.3.2 (Mul 1*b)         Q.E.D.
      Step: 1.6.2.3.3                   Q.E.D.
      Step: 1.6.2.3.4                   Q.E.D.
      Step: 1.6.2.3.5                   Q.E.D.
      Step: 1.6.2.4.1                   Q.E.D.
      Step: 1.6.2.4.2 (Mul a*1)         Q.E.D.
      Step: 1.6.2.4.3                   Q.E.D.
      Step: 1.6.2.4.4                   Q.E.D.
      Step: 1.6.2.4.5                   Q.E.D.
      Step: 1.6.2.5.1                   Q.E.D.
      Step: 1.6.2.5.2 (Mul Con)         Q.E.D.
      Step: 1.6.2.5.3                   Q.E.D.
      Step: 1.6.2.5.4                   Q.E.D.
      Step: 1.6.2.5.5                   Q.E.D.
      Step: 1.6.2.5.6                   Q.E.D.
      Step: 1.6.2.6 (3 way case split)
        Step: 1.6.2.6.1.1               Q.E.D.
        Step: 1.6.2.6.1.2 (Mul 0,_)     Q.E.D.
        Step: 1.6.2.6.1.3               Q.E.D.
        Step: 1.6.2.6.2.1               Q.E.D.
        Step: 1.6.2.6.2.2 (Mul 1,_)     Q.E.D.
        Step: 1.6.2.6.2.3               Q.E.D.
        Step: 1.6.2.6.2.4               Q.E.D.
        Step: 1.6.2.6.2.5               Q.E.D.
        Step: 1.6.2.6.3.1               Q.E.D.
        Step: 1.6.2.6.3.2 (Mul C,_)     Q.E.D.
        Step: 1.6.2.6.Completeness      Q.E.D.
      Step: 1.6.2.7 (3 way case split)
        Step: 1.6.2.7.1.1               Q.E.D.
        Step: 1.6.2.7.1.2 (Mul _,0)     Q.E.D.
        Step: 1.6.2.7.1.3               Q.E.D.
        Step: 1.6.2.7.2.1               Q.E.D.
        Step: 1.6.2.7.2.2 (Mul _,1)     Q.E.D.
        Step: 1.6.2.7.2.3               Q.E.D.
        Step: 1.6.2.7.2.4               Q.E.D.
        Step: 1.6.2.7.2.5               Q.E.D.
        Step: 1.6.2.7.3.1               Q.E.D.
        Step: 1.6.2.7.3.2 (Mul _,C)     Q.E.D.
        Step: 1.6.2.7.Completeness      Q.E.D.
      Step: 1.6.2.8.1                   Q.E.D.
      Step: 1.6.2.8.2 (Mul _,_)         Q.E.D.
      Step: 1.6.2.Completeness          Q.E.D.
    Step: 1.7.1 (Let)                   Q.E.D.
    Step: 1.7.2 (2 way case split)
      Step: 1.7.2.1.1                   Q.E.D.
      Step: 1.7.2.1.2 (Let Con)         Q.E.D.
      Step: 1.7.2.1.3                   Q.E.D.
      Step: 1.7.2.1.4                   Q.E.D.
      Step: 1.7.2.2.1                   Q.E.D.
      Step: 1.7.2.2.2 (Let _)           Q.E.D.
      Step: 1.7.2.Completeness          Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
[Proven] simpCorrect :: Ɐe ∷ (Expr [Char] Integer) → Ɐenv ∷ [([Char], Integer)] → Bool

cfoldCorrect :: TP (Proof (Forall "e" Exp -> Forall "env" EL -> SBool)) Source #

Constant folding preserves the semantics: interpreting an expression is the same as constant-folding it first and then interpreting the result.

>>> runTPWith cvc5 cfoldCorrect
Lemma: measureNonNeg                    Q.E.D.
Lemma: simpCorrect                      Q.E.D.
Lemma: sqrCong                          Q.E.D.
Lemma: sqrHelper                        Q.E.D.
Lemma: mulCongL                         Q.E.D.
Lemma: mulCongR                         Q.E.D.
Lemma: mulHelper                        Q.E.D.
Inductive lemma (strong): cfoldCorrect
  Step: Measure is non-negative         Q.E.D.
  Step: 1 (7 way case split)
    Step: 1.1.1 (case Var)              Q.E.D.
    Step: 1.1.2                         Q.E.D.
    Step: 1.1.3                         Q.E.D.
    Step: 1.2.1 (case Con)              Q.E.D.
    Step: 1.2.2                         Q.E.D.
    Step: 1.2.3                         Q.E.D.
    Step: 1.3.1 (case Sqr)              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.3.6                         Q.E.D.
    Step: 1.3.7                         Q.E.D.
    Step: 1.4.1 (case Inc)              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.5.1 (case Add)              Q.E.D.
    Step: 1.5.2                         Q.E.D.
    Step: 1.5.3                         Q.E.D.
    Step: 1.5.4                         Q.E.D.
    Step: 1.5.5                         Q.E.D.
    Step: 1.6.1 (case Mul)              Q.E.D.
    Step: 1.6.2                         Q.E.D.
    Step: 1.6.3                         Q.E.D.
    Step: 1.6.4                         Q.E.D.
    Step: 1.6.5                         Q.E.D.
    Step: 1.6.6                         Q.E.D.
    Step: 1.6.7                         Q.E.D.
    Step: 1.6.8                         Q.E.D.
    Step: 1.7.1 (case Let)              Q.E.D.
    Step: 1.7.2                         Q.E.D.
    Step: 1.7.3                         Q.E.D.
    Step: 1.7.4                         Q.E.D.
    Step: 1.7.5                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
[Proven] cfoldCorrect :: Ɐe ∷ (Expr [Char] Integer) → Ɐenv ∷ [([Char], Integer)] → Bool