-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.TP.Reverse
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Can we define the reverse function using no auxiliary functions, i.e., only
-- in terms of cons, head, tail, and itself (recursively)? This example
-- shows such a definition and proves that it is correct.
--
-- See Zohar Manna's 1974 "Mathematical Theory of Computation" book, where this
-- definition and its proof is presented as Example 5.36.
-----------------------------------------------------------------------------

{-# LANGUAGE CPP                 #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE OverloadedLists     #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeAbstractions    #-}
{-# LANGUAGE TypeApplications    #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.TP.Reverse where

import Prelude hiding (head, tail, null, reverse, length, init, last, (++))

import Data.SBV
import Data.SBV.List hiding (partition)
import Data.SBV.TP

import qualified Data.SBV.TP.List as TP

#ifdef DOCTEST
-- $setup
-- >>> :set -XTypeApplications
#endif

-- * Reversing with no auxiliaries

-- | This definition of reverse uses no helper functions, other than the usual
-- head, tail, cons, and uncons to reverse a given list. Note that efficiency
-- is not our concern here, we call 'rev' itself three times in the body.
rev :: SymVal a => SList a -> SList a
rev :: forall a. SymVal a => SList a -> SList a
rev = String -> (SList a -> SList a) -> SList a -> SList a
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"rev" ((SList a -> SList a) -> SList a -> SList a)
-> (SList a -> SList a) -> SList a -> SList a
forall a b. (a -> b) -> a -> b
$ \SList a
xs -> SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
xs SBool -> SBool -> SBool
.|| SList a -> SBool
forall a. SymVal a => SList a -> SBool
null (SList a -> SList a
forall a. SymVal a => SList a -> SList a
tail SList a
xs)) SList a
xs
                                     (let (SBV a
x, SList a
as)     = SList a -> (SBV a, SList a)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList a
xs
                                          (SBV a
hras, SList a
tas) = SList a -> (SBV a, SList a)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons (SList a -> SList a
forall a. SymVal a => SList a -> SList a
rev SList a
as)
                                      in SBV a
hras SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a -> SList a
forall a. SymVal a => SList a -> SList a
rev (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a -> SList a
forall a. SymVal a => SList a -> SList a
rev SList a
tas))

-- * Correctness proof

-- | Correctness the function 'rev'. We have:
--
-- >>> correctness @Integer
-- Inductive lemma: revLen
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Result:                               Q.E.D.
-- Inductive lemma: revApp
--   Step: Base                            Q.E.D.
--   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.
--   Result:                               Q.E.D.
-- Inductive lemma: revApp
--   Step: Base                            Q.E.D.
--   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.
--   Result:                               Q.E.D.
-- Lemma: revSnoc                          Q.E.D.
-- Inductive lemma: revApp
--   Step: Base                            Q.E.D.
--   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.
--   Result:                               Q.E.D.
-- Inductive lemma: revRev
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Result:                               Q.E.D.
-- Inductive lemma (strong): revCorrect
--   Step: Measure is non-negative         Q.E.D.
--   Step: 1 (2 way full case split)
--     Step: 1.1                           Q.E.D.
--     Step: 1.2 (2 way full case split)
--       Step: 1.2.1                       Q.E.D.
--       Step: 1.2.2.1                     Q.E.D.
--       Step: 1.2.2.2                     Q.E.D.
--       Step: 1.2.2.3                     Q.E.D.
--       Step: 1.2.2.4                     Q.E.D.
--       Step: 1.2.2.5 (simplify head)     Q.E.D.
--       Step: 1.2.2.6                     Q.E.D.
--       Step: 1.2.2.7 (simplify tail)     Q.E.D.
--       Step: 1.2.2.8                     Q.E.D.
--       Step: 1.2.2.9                     Q.E.D.
--       Step: 1.2.2.10                    Q.E.D.
--       Step: 1.2.2.11 (substitute)       Q.E.D.
--       Step: 1.2.2.12                    Q.E.D.
--       Step: 1.2.2.13                    Q.E.D.
--       Step: 1.2.2.14                    Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] revCorrect :: Ɐxs ∷ [Integer] → Bool
correctness :: forall a. SymVal a => IO (Proof (Forall "xs" [a] -> SBool))
correctness :: forall a. SymVal a => IO (Proof (Forall "xs" [a] -> SBool))
correctness = TP (Proof (Forall "xs" [a] -> SBool))
-> IO (Proof (Forall "xs" [a] -> SBool))
forall a. TP a -> IO a
runTP (TP (Proof (Forall "xs" [a] -> SBool))
 -> IO (Proof (Forall "xs" [a] -> SBool)))
-> TP (Proof (Forall "xs" [a] -> SBool))
-> IO (Proof (Forall "xs" [a] -> SBool))
forall a b. (a -> b) -> a -> b
$ do

  -- Import a few helpers from "Data.SBV.TP.List"
  Proof (Forall "xs" [a] -> SBool)
revLen  <- forall a. SymVal a => TP (Proof (Forall "xs" [a] -> SBool))
TP.revLen  @a
  Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
revApp  <- forall a.
SymVal a =>
TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
TP.revApp  @a
  Proof (Forall "x" a -> Forall "xs" [a] -> SBool)
revSnoc <- forall a.
SymVal a =>
TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool))
TP.revSnoc @a
  Proof (Forall "xs" [a] -> SBool)
revRev  <- forall a. SymVal a => TP (Proof (Forall "xs" [a] -> SBool))
TP.revRev  @a

  SMTConfig
-> String
-> (Forall "xs" [a] -> SBool)
-> MeasureArgs (Forall "xs" [a] -> SBool) Integer
-> (Proof (Forall "xs" [a] -> SBool)
    -> StepArgs (Forall "xs" [a] -> SBool) [a])
-> TP (Proof (Forall "xs" [a] -> SBool))
forall a m t.
(SInductive a, Proposition a, Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> a
-> MeasureArgs a m
-> (Proof a -> StepArgs a t)
-> TP (Proof a)
forall m t.
(Proposition (Forall "xs" [a] -> SBool), Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> (Forall "xs" [a] -> SBool)
-> MeasureArgs (Forall "xs" [a] -> SBool) m
-> (Proof (Forall "xs" [a] -> SBool)
    -> StepArgs (Forall "xs" [a] -> SBool) t)
-> TP (Proof (Forall "xs" [a] -> SBool))
sInductWith SMTConfig
cvc5 String
"revCorrect"
    (\(Forall SBV [a]
xs) -> SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
rev SBV [a]
xs SBV [a] -> SBV [a] -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
reverse SBV [a]
xs)
    MeasureArgs (Forall "xs" [a] -> SBool) Integer
SBV [a] -> SInteger
forall a. SymVal a => SList a -> SInteger
length ((Proof (Forall "xs" [a] -> SBool)
  -> StepArgs (Forall "xs" [a] -> SBool) [a])
 -> TP (Proof (Forall "xs" [a] -> SBool)))
-> (Proof (Forall "xs" [a] -> SBool)
    -> StepArgs (Forall "xs" [a] -> SBool) [a])
-> TP (Proof (Forall "xs" [a] -> SBool))
forall a b. (a -> b) -> a -> b
$
    \Proof (Forall "xs" [a] -> SBool)
ih SBV [a]
xs -> [] [SBool] -> TPProofRaw (SBV [a]) -> (SBool, TPProofRaw (SBV [a]))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
rev SBV [a]
xs
                 SBV [a] -> ChainsTo (SBV [a]) -> ChainsTo (SBV [a])
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV [a]
-> TPProofRaw (SBV [a])
-> (SBV a -> SBV [a] -> TPProofRaw (SBV [a]))
-> TPProofRaw (SBV [a])
forall a r.
SymVal a =>
SList a
-> TPProofRaw r
-> (SBV a -> SList a -> TPProofRaw r)
-> TPProofRaw r
split SBV [a]
xs TPProofRaw (SBV [a])
forall a. Trivial a => a
trivial
                          (\SBV a
a SBV [a]
as -> SBV [a]
-> TPProofRaw (SBV [a])
-> (SBV a -> SBV [a] -> TPProofRaw (SBV [a]))
-> TPProofRaw (SBV [a])
forall a r.
SymVal a =>
SList a
-> TPProofRaw r
-> (SBV a -> SList a -> TPProofRaw r)
-> TPProofRaw r
split SBV [a]
as TPProofRaw (SBV [a])
forall a. Trivial a => a
trivial
                                          (\SBV a
_ SBV [a]
_ -> SBV [a] -> SBV a
forall a. SymVal a => SList a -> SBV a
head (SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
rev SBV [a]
as) SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
rev (SBV a
a SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
rev (SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
tail (SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
rev SBV [a]
as)))
                                                SBV [a] -> Proof Bool -> Hinted (SBV [a])
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [a] -> SBool)
ih Proof (Forall "xs" [a] -> SBool)
-> IArgs (Forall "xs" [a] -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SBV [a]
as
                                                TPProofRaw (SBV [a])
-> ChainsTo (TPProofRaw (SBV [a]))
-> ChainsTo (TPProofRaw (SBV [a]))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV [a] -> SBV a
forall a. SymVal a => SList a -> SBV a
head (SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
reverse SBV [a]
as) SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
rev (SBV a
a SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
rev (SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
tail (SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
reverse SBV [a]
as)))
                                                SBV [a] -> Proof Bool -> Hinted (SBV [a])
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [a] -> SBool)
ih Proof (Forall "xs" [a] -> SBool)
-> IArgs (Forall "xs" [a] -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" (SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
tail (SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
rev SBV [a]
as))
                                                TPProofRaw (SBV [a])
-> ChainsTo (TPProofRaw (SBV [a]))
-> ChainsTo (TPProofRaw (SBV [a]))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV [a] -> SBV a
forall a. SymVal a => SList a -> SBV a
head (SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
reverse SBV [a]
as) SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
rev (SBV a
a SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
rev (SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
tail (SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
reverse SBV [a]
as)))
                                                SBV [a] -> Proof Bool -> Hinted (SBV [a])
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "x" a -> Forall "xs" [a] -> SBool)
revSnoc Proof (Forall "x" a -> Forall "xs" [a] -> SBool)
-> IArgs (Forall "x" a -> Forall "xs" [a] -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" (SBV [a] -> SBV a
forall a. SymVal a => SList a -> SBV a
last SBV [a]
as), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" (SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
init SBV [a]
as))
                                                TPProofRaw (SBV [a])
-> ChainsTo (TPProofRaw (SBV [a]))
-> ChainsTo (TPProofRaw (SBV [a]))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let w :: SBV [a]
w = SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
init SBV [a]
as
                                                       b :: SBV a
b = SBV [a] -> SBV a
forall a. SymVal a => SList a -> SBV a
last SBV [a]
as
                                                in SBV [a] -> SBV a
forall a. SymVal a => SList a -> SBV a
head (SBV a
b SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
reverse SBV [a]
w) SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
rev (SBV a
a SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
rev (SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
tail (SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
reverse SBV [a]
as)))
                                                SBV [a] -> String -> Hinted (SBV [a])
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"simplify head"
                                                TPProofRaw (SBV [a])
-> ChainsTo (TPProofRaw (SBV [a]))
-> ChainsTo (TPProofRaw (SBV [a]))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV a
b SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
rev (SBV a
a SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
rev (SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
tail (SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
reverse SBV [a]
as)))
                                                SBV [a] -> Proof Bool -> Hinted (SBV [a])
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "x" a -> Forall "xs" [a] -> SBool)
revSnoc Proof (Forall "x" a -> Forall "xs" [a] -> SBool)
-> IArgs (Forall "x" a -> Forall "xs" [a] -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" (SBV [a] -> SBV a
forall a. SymVal a => SList a -> SBV a
last SBV [a]
xs), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" (SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
init SBV [a]
as))
                                                TPProofRaw (SBV [a])
-> ChainsTo (TPProofRaw (SBV [a]))
-> ChainsTo (TPProofRaw (SBV [a]))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV a
b SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
rev (SBV a
a SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
rev (SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
tail (SBV a
b SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
reverse SBV [a]
w)))
                                                SBV [a] -> String -> Hinted (SBV [a])
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"simplify tail"
                                                TPProofRaw (SBV [a])
-> ChainsTo (TPProofRaw (SBV [a]))
-> ChainsTo (TPProofRaw (SBV [a]))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV a
b SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
rev (SBV a
a SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
rev (SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
reverse SBV [a]
w))
                                                SBV [a] -> Proof Bool -> Hinted (SBV [a])
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [a] -> SBool)
ih     Proof (Forall "xs" [a] -> SBool)
-> IArgs (Forall "xs" [a] -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" (SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
reverse SBV [a]
w)
                                                TPProofRaw (SBV [a]) -> Proof Bool -> Hinted (TPProofRaw (SBV [a]))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [a] -> SBool)
revLen Proof (Forall "xs" [a] -> SBool)
-> IArgs (Forall "xs" [a] -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SBV [a]
w
                                                Hinted (TPProofRaw (SBV [a]))
-> ChainsTo (Hinted (TPProofRaw (SBV [a])))
-> ChainsTo (Hinted (TPProofRaw (SBV [a])))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV a
b SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
rev (SBV a
a SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
reverse (SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
reverse SBV [a]
w))
                                                SBV [a] -> Proof Bool -> Hinted (SBV [a])
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [a] -> SBool)
revRev Proof (Forall "xs" [a] -> SBool)
-> IArgs (Forall "xs" [a] -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SBV [a]
w
                                                TPProofRaw (SBV [a])
-> ChainsTo (TPProofRaw (SBV [a]))
-> ChainsTo (TPProofRaw (SBV [a]))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV a
b SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
rev (SBV a
a SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a]
w)
                                                SBV [a] -> Proof (Forall "xs" [a] -> SBool) -> Hinted (SBV [a])
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [a] -> SBool)
ih
                                                TPProofRaw (SBV [a])
-> ChainsTo (TPProofRaw (SBV [a]))
-> ChainsTo (TPProofRaw (SBV [a]))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV a
b SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
reverse (SBV a
a SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a]
w)
                                                SBV [a] -> String -> Hinted (SBV [a])
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"substitute"
                                                TPProofRaw (SBV [a])
-> ChainsTo (TPProofRaw (SBV [a]))
-> ChainsTo (TPProofRaw (SBV [a]))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV [a] -> SBV a
forall a. SymVal a => SList a -> SBV a
last SBV [a]
as SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
reverse (SBV a
a SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
init SBV [a]
as)
                                                SBV [a] -> Proof Bool -> Hinted (SBV [a])
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
revApp Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
-> IArgs (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" (SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
init SBV [a]
as), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" [SBV [a] -> SBV a
forall a. SymVal a => SList a -> SBV a
last SBV [a]
as])
                                                TPProofRaw (SBV [a])
-> ChainsTo (TPProofRaw (SBV [a]))
-> ChainsTo (TPProofRaw (SBV [a]))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
reverse (SBV a
a SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
init SBV [a]
as SBV [a] -> SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a -> SList a
++ [SBV [a] -> SBV a
forall a. SymVal a => SList a -> SBV a
last SBV [a]
as])
                                                SBV [a] -> ChainsTo (SBV [a]) -> ChainsTo (SBV [a])
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
reverse (SBV a
a SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a]
as)
                                                SBV [a] -> ChainsTo (SBV [a]) -> ChainsTo (SBV [a])
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
reverse SBV [a]
xs
                                                SBV [a] -> ChainsTo (SBV [a]) -> ChainsTo (SBV [a])
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV [a])
TPProofRaw (SBV [a])
forall a. TPProofRaw a
qed))

{- HLint ignore correctness "Use last"          -}
{- HLint ignore correctness "Redundant reverse" -}