-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.KnuckleDragger.Lists
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- A variety of KnuckleDragger proofs on list processing functions. Note that
-- these proofs only hold for finite lists. SMT-solvers do not model infinite
-- lists, and hence all claims are for finite (but arbitrary-length) lists.
-----------------------------------------------------------------------------

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

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.KnuckleDragger.Lists where

import Prelude (IO, ($), Integer, Num(..), id, (.), flip)

import Data.SBV
import Data.SBV.List
import Data.SBV.Tuple
import Data.SBV.Tools.KnuckleDragger

import Control.Monad (void)
import Data.Proxy

#ifndef HADDOCK
-- $setup
-- >>> -- For doctest purposes only:
-- >>> :set -XScopedTypeVariables
-- >>> :set -XTypeApplications
-- >>> import Data.SBV
-- >>> import Data.Proxy
-- >>> import Control.Exception
#endif

-- | Data declaration for an uninterpreted type, usually indicating source.
data A
mkUninterpretedSort ''A

-- | Data declaration for an uninterpreted type, usually indicating target.
data B
mkUninterpretedSort ''B

-- | Data declaration for an uninterpreted type, usually indicating an intermediate value.
data C
mkUninterpretedSort ''C

-- * Appending null

-- | @xs ++ [] == xs@
--
-- We have:
--
-- >>> appendNull
-- Lemma: appendNull                       Q.E.D.
-- [Proven] appendNull
appendNull :: IO Proof
appendNull :: IO Proof
appendNull = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ String -> (Forall "xs" [A] -> SBool) -> [Proof] -> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"appendNull" (\(Forall @"xs" (SList A
xs :: SList A)) -> SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
forall a. SymVal a => SList a
nil SList A -> SList A -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList A
xs) []

-- * Moving cons over append

-- | @(x : xs) ++ ys == x : (xs ++ ys)@
--
-- We have:
--
-- >>> consApp
-- Lemma: consApp                          Q.E.D.
-- [Proven] consApp
consApp :: IO Proof
consApp :: IO Proof
consApp = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ String
-> (Forall "x" A -> Forall "xs" [A] -> Forall "ys" [A] -> SBool)
-> [Proof]
-> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"consApp" (\(Forall @"x" (SA
x :: SA)) (Forall @"xs" SList A
xs) (Forall @"ys" SList A
ys) -> (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs) SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys SList A -> SList A -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys)) []

-- * Associativity of append

-- | @(xs ++ ys) ++ zs == xs ++ (ys ++ zs)@
--
-- We have:
--
-- >>> appendAssoc
-- Lemma: appendAssoc                      Q.E.D.
-- [Proven] appendAssoc
--
-- Surprisingly, z3 can prove this without any induction. (Since SBV's append translates directly to
-- the concatenation of sequences in SMTLib, it must trigger an internal heuristic in z3
-- that proves it right out-of-the-box!)
appendAssoc :: IO Proof
appendAssoc :: IO Proof
appendAssoc = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$
   String
-> (Forall "xs" [A] -> Forall "ys" [A] -> Forall "zs" [A] -> SBool)
-> [Proof]
-> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"appendAssoc" (\(Forall @"xs" (SList A
xs :: SList A)) (Forall @"ys" SList A
ys) (Forall @"zs" SList A
zs) -> SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ (SList A
ys SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
zs) SList A -> SList A -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys) SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
zs) []

-- * Reverse and append

-- | @reverse (x:xs) == reverse xs ++ [x]@
--
-- >>> revCons
-- Lemma: revCons                          Q.E.D.
-- [Proven] revCons
revCons :: IO Proof
revCons :: IO Proof
revCons = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ String
-> (Forall "x" A -> Forall "xs" [A] -> SBool)
-> [Proof]
-> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"revCons" (\(Forall @"x" (SA
x :: SA)) (Forall @"xs" SList A
xs) -> SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs) SList A -> SList A -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SA -> SList A
forall a. SymVal a => SBV a -> SList a
singleton SA
x) []

-- | @reverse (xs ++ ys) .== reverse ys ++ reverse xs@
--
-- We have:
--
-- >>> revApp
-- Inductive lemma: revApp
--   Base: revApp.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.
--   Step: revApp.Step                     Q.E.D.
-- [Proven] revApp
revApp :: IO Proof
revApp :: IO Proof
revApp = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$
   String
-> (Forall "xs" [A] -> Forall "ys" [A] -> SBool)
-> (Proof
    -> SA -> SList A -> SList A -> (SBool, [ProofStep (SList A)]))
-> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
String -> a -> (Proof -> steps) -> KD Proof
induct String
"revApp"
          (\(Forall @"xs" (SList A
xs :: SList A)) (Forall @"ys" SList A
ys) -> SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse (SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys) SList A -> SList A -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse SList A
ys SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse SList A
xs) ((Proof
  -> SA -> SList A -> SList A -> (SBool, [ProofStep (SList A)]))
 -> KD Proof)
-> (Proof
    -> SA -> SList A -> SList A -> (SBool, [ProofStep (SList A)]))
-> KD Proof
forall a b. (a -> b) -> a -> b
$
          \Proof
ih (SA
x :: SA) SList A
xs SList A
ys -> [] [SBool] -> [ProofStep (SList A)] -> (SBool, [ProofStep (SList A)])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse ((SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs) SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys)
                                    SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys))
                                    SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse (SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys) SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SA -> SList A
forall a. SymVal a => SBV a -> SList a
singleton SA
x           SList A -> Proof -> ProofStep (SList A)
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
ih
                                    ProofStep (SList A)
-> ChainsTo (ProofStep (SList A)) -> ChainsTo (ProofStep (SList A))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse SList A
ys SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse SList A
xs) SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SA -> SList A
forall a. SymVal a => SBV a -> SList a
singleton SA
x
                                    SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse SList A
ys SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ (SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SA -> SList A
forall a. SymVal a => SBV a -> SList a
singleton SA
x)
                                    SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse SList A
ys SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs)
                                    SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep (SList A)]
ChainsTo (SList A)
forall a. [ProofStep a]
qed

-- * Reversing twice is identity

-- | @reverse (reverse xs) == xs@
--
-- We have:
--
-- >>> reverseReverse
-- Inductive lemma: revApp
--   Base: revApp.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.
--   Step: revApp.Step                     Q.E.D.
-- Inductive lemma: reverseReverse
--   Base: reverseReverse.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: reverseReverse.Step             Q.E.D.
-- [Proven] reverseReverse
reverseReverse :: IO Proof
reverseReverse :: IO Proof
reverseReverse = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do

   ra <- IO Proof -> KD Proof
use IO Proof
revApp

   induct "reverseReverse"
          (\(Forall @"xs" (SList A
xs :: SList A)) -> SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse (SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse SList A
xs) SList A -> SList A -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList A
xs) $
          \Proof
ih (SA
x :: SA) SList A
xs -> [] [SBool] -> [ProofStep (SList A)] -> (SBool, [ProofStep (SList A)])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse (SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs))
                                 SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse (SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SA -> SList A
forall a. SymVal a => SBV a -> SList a
singleton SA
x)           SList A -> Proof -> ProofStep (SList A)
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
ra
                                 ProofStep (SList A)
-> ChainsTo (ProofStep (SList A)) -> ChainsTo (ProofStep (SList A))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse (SA -> SList A
forall a. SymVal a => SBV a -> SList a
singleton SA
x) SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse (SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse SList A
xs) SList A -> Proof -> ProofStep (SList A)
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
ih
                                 ProofStep (SList A)
-> ChainsTo (ProofStep (SList A)) -> ChainsTo (ProofStep (SList A))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SA -> SList A
forall a. SymVal a => SBV a -> SList a
singleton SA
x SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
xs
                                 SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs
                                 SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep (SList A)]
ChainsTo (SList A)
forall a. [ProofStep a]
qed

-- * Lengths of lists

-- | @length (x : xs) = 1 + length xs@
--
-- We have:
--
-- >>> lengthTail
-- Lemma: lengthTail                       Q.E.D.
-- [Proven] lengthTail
lengthTail :: IO Proof
lengthTail :: IO Proof
lengthTail = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ String
-> (Forall "x" A -> Forall "xs" [A] -> SBool)
-> [Proof]
-> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"lengthTail" (\(Forall @"x" (SA
x :: SA)) (Forall @"xs" SList A
xs) -> SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList A
xs) []

-- | It is instructive to see what kind of counter-example we get if a lemma fails to prove.
-- Below, we do a variant of the 'lengthTail, but with a bad implementation over integers,
-- and see the counter-example. Our implementation returns an incorrect answer if the given list is longer
-- than 5 elements and have 42 in it. We have:
--
-- >>> badLengthProof `catch` (\(_ :: SomeException) -> pure ())
-- Lemma: badLengthProof
-- *** Failed to prove badLengthProof.
-- Falsifiable. Counter-example:
--   xs   = [15,11,13,16,27,42] :: [Integer]
--   imp  =                  42 :: Integer
--   spec =                   6 :: Integer
badLengthProof :: IO ()
badLengthProof :: IO ()
badLengthProof = KD () -> IO ()
forall a. KD a -> IO a
runKD (KD () -> IO ()) -> KD () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
   let badLength :: SList Integer -> SInteger
       badLength :: SList Integer -> SInteger
badLength SList Integer
xs = SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
xs SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
5 SBool -> SBool -> SBool
.&& SInteger
42 SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SList Integer
xs) SInteger
42 (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
xs)

   KD Proof -> KD ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (KD Proof -> KD ()) -> KD Proof -> KD ()
forall a b. (a -> b) -> a -> b
$ String -> (Forall "xs" [Integer] -> SBool) -> [Proof] -> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"badLengthProof" (\(Forall @"xs" SList Integer
xs) -> String -> SInteger -> SInteger
forall a. SymVal a => String -> SBV a -> SBV a
observe String
"imp" (SList Integer -> SInteger
badLength SList Integer
xs) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== String -> SInteger -> SInteger
forall a. SymVal a => String -> SBV a -> SBV a
observe String
"spec" (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
xs)) []

-- | @length (xs ++ ys) == length xs + length ys@
--
-- We have:
--
-- >>> lenAppend
-- Lemma: lenAppend                        Q.E.D.
-- [Proven] lenAppend
lenAppend :: IO Proof
lenAppend :: IO Proof
lenAppend = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ String
-> (Forall "xs" [A] -> Forall "ys" [A] -> SBool)
-> [Proof]
-> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"lenAppend" (\(Forall @"xs" (SList A
xs :: SList A)) (Forall @"ys" SList A
ys) -> SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList A
xs SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList A
ys) []

-- | @length xs == length ys -> length (xs ++ ys) == 2 * length xs@
--
-- We have:
--
-- >>> lenAppend2
-- Lemma: lenAppend2                       Q.E.D.
-- [Proven] lenAppend2
lenAppend2 :: IO Proof
lenAppend2 :: IO Proof
lenAppend2 = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$
    String
-> (Forall "xs" [A] -> Forall "ys" [A] -> SBool)
-> [Proof]
-> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"lenAppend2" (\(Forall @"xs" (SList A
xs :: SList A)) (Forall @"ys" SList A
ys) -> SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList A
xs SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList A
ys SBool -> SBool -> SBool
.=> SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList A
xs) []

-- * Any, all, and filtering

-- | @not (all id xs) == any not xs@
--
-- A list of booleans is not all true, if any of them is false. We have:
--
-- >>> allAny
-- Inductive lemma: allAny
--   Base: allAny.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: allAny.Step                     Q.E.D.
-- [Proven] allAny
allAny :: IO Proof
allAny :: IO Proof
allAny = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$
   String
-> (Forall "xs" [Bool] -> SBool)
-> (Proof -> SBool -> SList Bool -> (SBool, [ProofStep SBool]))
-> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
String -> a -> (Proof -> steps) -> KD Proof
induct String
"allAny"
          (\(Forall @"xs" SList Bool
xs) -> SBool -> SBool
sNot ((SBool -> SBool) -> SList Bool -> SBool
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SBool
all SBool -> SBool
forall a. a -> a
id SList Bool
xs) SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBool -> SBool) -> SList Bool -> SBool
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SBool
any SBool -> SBool
sNot SList Bool
xs) ((Proof -> SBool -> SList Bool -> (SBool, [ProofStep SBool]))
 -> KD Proof)
-> (Proof -> SBool -> SList Bool -> (SBool, [ProofStep SBool]))
-> KD Proof
forall a b. (a -> b) -> a -> b
$
          \Proof
ih SBool
x SList Bool
xs -> [] [SBool] -> [ProofStep SBool] -> (SBool, [ProofStep SBool])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- SBool -> SBool
sNot ((SBool -> SBool) -> SList Bool -> SBool
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SBool
all SBool -> SBool
forall a. a -> a
id (SBool
x SBool -> SList Bool -> SList Bool
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Bool
xs))
                         SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool
sNot (SBool
x SBool -> SBool -> SBool
.&& (SBool -> SBool) -> SList Bool -> SBool
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SBool
all SBool -> SBool
forall a. a -> a
id SList Bool
xs)
                         SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBool -> SBool
sNot SBool
x SBool -> SBool -> SBool
.|| SBool -> SBool
sNot ((SBool -> SBool) -> SList Bool -> SBool
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SBool
all SBool -> SBool
forall a. a -> a
id SList Bool
xs))   SBool -> Proof -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
ih
                         ProofStep SBool
-> ChainsTo (ProofStep SBool) -> ChainsTo (ProofStep SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool
sNot SBool
x SBool -> SBool -> SBool
.|| (SBool -> SBool) -> SList Bool -> SBool
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SBool
any SBool -> SBool
sNot SList Bool
xs
                         SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBool -> SBool) -> SList Bool -> SBool
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SBool
any SBool -> SBool
sNot (SBool
x SBool -> SList Bool -> SList Bool
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Bool
xs)
                         SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep SBool]
ChainsTo SBool
forall a. [ProofStep a]
qed

-- | If an integer list doesn't have 2 as an element, then filtering for @> 2@ or @.>= 2@
-- yields the same result. We have:
--
-- >>> filterEx
-- Inductive lemma: filterEx
--   Base: filterEx.Base                   Q.E.D.
--   Step: 1                               Q.E.D.
--   Asms: 2                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: filterEx.Step                   Q.E.D.
-- [Proven] filterEx
filterEx :: IO Proof
filterEx :: IO Proof
filterEx = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$
  String
-> (Forall "xs" [Integer] -> SBool)
-> (Proof
    -> SInteger
    -> SList Integer
    -> (SBool, [ProofStep (SList Integer)]))
-> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
String -> a -> (Proof -> steps) -> KD Proof
induct String
"filterEx"
         (\(Forall @"xs" SList Integer
xs) -> (SInteger
2 :: SInteger) SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`notElem` SList Integer
xs SBool -> SBool -> SBool
.=> ((SInteger -> SBool) -> SList Integer -> SList Integer
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter (SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
2) SList Integer
xs SList Integer -> SList Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SInteger -> SBool) -> SList Integer -> SList Integer
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter (SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
2) SList Integer
xs)) ((Proof
  -> SInteger
  -> SList Integer
  -> (SBool, [ProofStep (SList Integer)]))
 -> KD Proof)
-> (Proof
    -> SInteger
    -> SList Integer
    -> (SBool, [ProofStep (SList Integer)]))
-> KD Proof
forall a b. (a -> b) -> a -> b
$
         \Proof
ih SInteger
x SList Integer
xs -> let h :: SBool
h = (SInteger
2 :: SInteger) SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`notElem` (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.:  SList Integer
xs)
                  in [SBool
h] [SBool]
-> [ProofStep (SList Integer)]
-> (SBool, [ProofStep (SList Integer)])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- (SInteger -> SBool) -> SList Integer -> SList Integer
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter (SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
2) (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs)
                         SList Integer
-> ChainsTo (SList Integer) -> ChainsTo (SList Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
2) (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SInteger -> SBool) -> SList Integer -> SList Integer
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter (SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>  SInteger
2) SList Integer
xs) ((SInteger -> SBool) -> SList Integer -> SList Integer
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter (SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>  SInteger
2) SList Integer
xs) SList Integer -> [Helper] -> ProofStep (SList Integer)
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [SBool -> Helper
hyp SBool
h, Proof -> Helper
hprf Proof
ih]
                         ProofStep (SList Integer)
-> ChainsTo (ProofStep (SList Integer))
-> ChainsTo (ProofStep (SList Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
2) (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SInteger -> SBool) -> SList Integer -> SList Integer
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter (SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
2) SList Integer
xs) ((SInteger -> SBool) -> SList Integer -> SList Integer
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter (SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
2) SList Integer
xs)
                         SList Integer
-> ChainsTo (SList Integer) -> ChainsTo (SList Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep (SList Integer)]
ChainsTo (SList Integer)
forall a. [ProofStep a]
qed

-- | The 'filterEx' example above, except we get a counter-example if @2@ can be in the list. Note that
-- we don't need the induction tactic here.
--
-- >>> filterEx2 `catch` (\(_ :: SomeException) -> pure ())
-- Lemma: filterEx2
-- *** Failed to prove filterEx2.
-- Falsifiable. Counter-example:
--   xs = [2] :: [Integer]
filterEx2 :: IO ()
filterEx2 :: IO ()
filterEx2 = KD () -> IO ()
forall a. KD a -> IO a
runKD (KD () -> IO ()) -> KD () -> IO ()
forall a b. (a -> b) -> a -> b
$
   KD Proof -> KD ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (KD Proof -> KD ()) -> KD Proof -> KD ()
forall a b. (a -> b) -> a -> b
$ String -> (Forall "xs" [Integer] -> SBool) -> [Proof] -> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"filterEx2" (\(Forall @"xs" SList Integer
xs) -> (SInteger -> SBool) -> SList Integer -> SList Integer
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter (SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> (SInteger
2 :: SInteger)) SList Integer
xs SList Integer -> SList Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SInteger -> SBool) -> SList Integer -> SList Integer
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter (SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
2) SList Integer
xs) []

-- * Map, append, and reverse

-- | @f = g => map f xs = map g xs@
--
-- >>> mapEquiv
-- Inductive lemma: mapEquiv
--   Base: mapEquiv.Base                   Q.E.D.
--   Step: 1                               Q.E.D.
--   Asms: 2                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Asms: 3                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Step: mapEquiv.Step                   Q.E.D.
-- [Proven] mapEquiv
mapEquiv :: IO Proof
mapEquiv :: IO Proof
mapEquiv = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do
   let f, g :: SA -> SB
       f :: SA -> SB
f = String -> SA -> SB
forall a. SMTDefinable a => String -> a
uninterpret String
"f"
       g :: SA -> SB
g = String -> SA -> SB
forall a. SMTDefinable a => String -> a
uninterpret String
"g"

       f'eq'g :: SBool
       f'eq'g :: SBool
f'eq'g = (Forall "x" A -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool ((Forall "x" A -> SBool) -> SBool)
-> (Forall "x" A -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \(Forall @"x" SA
x) -> SA -> SB
f SA
x SB -> SB -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SA -> SB
g SA
x

   String
-> (Forall "xs" [A] -> SBool)
-> (Proof -> SA -> SList A -> (SBool, [ProofStep SBool]))
-> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
String -> a -> (Proof -> steps) -> KD Proof
induct String
"mapEquiv"
          (\(Forall @"xs" SList A
xs) -> SBool
f'eq'g SBool -> SBool -> SBool
.=> (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f SList A
xs SList B -> SList B -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
g SList A
xs) ((Proof -> SA -> SList A -> (SBool, [ProofStep SBool]))
 -> KD Proof)
-> (Proof -> SA -> SList A -> (SBool, [ProofStep SBool]))
-> KD Proof
forall a b. (a -> b) -> a -> b
$
          \Proof
ih SA
x SList A
xs -> [SBool
f'eq'g] [SBool] -> [ProofStep SBool] -> (SBool, [ProofStep SBool])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs) SList B -> SList B -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
g (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs)
                               SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SA -> SB
f SA
x SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f SList A
xs SList B -> SList B -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SA -> SB
g SA
x SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
g SList A
xs SBool -> SBool -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? SBool
f'eq'g
                               ProofStep SBool
-> ChainsTo (ProofStep SBool) -> ChainsTo (ProofStep SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SA -> SB
f SA
x SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f SList A
xs SList B -> SList B -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SA -> SB
f SA
x SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
g SList A
xs SBool -> [Helper] -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [SBool -> Helper
hyp SBool
f'eq'g, Proof -> Helper
hprf Proof
ih]
                               ProofStep SBool
-> ChainsTo (ProofStep SBool) -> ChainsTo (ProofStep SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SA -> SB
f SA
x SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f SList A
xs SList B -> SList B -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SA -> SB
f SA
x SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f SList A
xs
                               SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs) SList B -> SList B -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs)
                               SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep SBool]
ChainsTo SBool
forall a. [ProofStep a]
qed

-- | @map f (xs ++ ys) == map f xs ++ map f ys@
--
-- >>> mapAppend (uninterpret "f")
-- Inductive lemma: mapAppend
--   Base: mapAppend.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.
--   Step: mapAppend.Step                  Q.E.D.
-- [Proven] mapAppend
mapAppend :: (SA -> SB) -> IO Proof
mapAppend :: (SA -> SB) -> IO Proof
mapAppend SA -> SB
f = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do
   String
-> (Forall "xs" [A] -> Forall "ys" [A] -> SBool)
-> (Proof
    -> SA -> SList A -> SList A -> (SBool, [ProofStep (SList B)]))
-> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
String -> a -> (Proof -> steps) -> KD Proof
induct String
"mapAppend"
          (\(Forall @"xs" (SList A
xs :: SList A)) (Forall @"ys" SList A
ys) -> (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys) SList B -> SList B -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f SList A
xs SList B -> SList B -> SList B
forall a. SymVal a => SList a -> SList a -> SList a
++ (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f SList A
ys) ((Proof
  -> SA -> SList A -> SList A -> (SBool, [ProofStep (SList B)]))
 -> KD Proof)
-> (Proof
    -> SA -> SList A -> SList A -> (SBool, [ProofStep (SList B)]))
-> KD Proof
forall a b. (a -> b) -> a -> b
$
          \Proof
ih SA
x SList A
xs SList A
ys -> [] [SBool] -> [ProofStep (SList B)] -> (SBool, [ProofStep (SList B)])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f ((SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs) SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys)
                            SList B -> ChainsTo (SList B) -> ChainsTo (SList B)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys))
                            SList B -> ChainsTo (SList B) -> ChainsTo (SList B)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SA -> SB
f SA
x SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys)        SList B -> Proof -> ProofStep (SList B)
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
ih
                            ProofStep (SList B)
-> ChainsTo (ProofStep (SList B)) -> ChainsTo (ProofStep (SList B))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SA -> SB
f SA
x SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: ((SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f SList A
xs  SList B -> SList B -> SList B
forall a. SymVal a => SList a -> SList a -> SList a
++ (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f SList A
ys)
                            SList B -> ChainsTo (SList B) -> ChainsTo (SList B)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SB
f SA
x SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f SList A
xs) SList B -> SList B -> SList B
forall a. SymVal a => SList a -> SList a -> SList a
++ (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f SList A
ys
                            SList B -> ChainsTo (SList B) -> ChainsTo (SList B)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs) SList B -> SList B -> SList B
forall a. SymVal a => SList a -> SList a -> SList a
++ (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f SList A
ys
                            SList B -> ChainsTo (SList B) -> ChainsTo (SList B)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep (SList B)]
ChainsTo (SList B)
forall a. [ProofStep a]
qed

-- | @map f . reverse == reverse . map f@
--
-- >>> mapReverse
-- Inductive lemma: mapAppend
--   Base: mapAppend.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.
--   Step: mapAppend.Step                  Q.E.D.
-- Inductive lemma: mapReverse
--   Base: mapReverse.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.
--   Step: 6                               Q.E.D.
--   Step: mapReverse.Step                 Q.E.D.
-- [Proven] mapReverse
mapReverse :: IO Proof
mapReverse :: IO Proof
mapReverse = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do
     let -- For an arbitrary uninterpreted function 'f':
         f :: SA -> SB
         f :: SA -> SB
f = String -> SA -> SB
forall a. SMTDefinable a => String -> a
uninterpret String
"f"

     mApp <- IO Proof -> KD Proof
use ((SA -> SB) -> IO Proof
mapAppend SA -> SB
f)

     induct "mapReverse"
            (\(Forall @"xs" SList A
xs) -> SList B -> SList B
forall a. SymVal a => SList a -> SList a
reverse ((SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f SList A
xs) SList B -> SList B -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse SList A
xs)) $
            \Proof
ih SA
x SList A
xs -> [] [SBool] -> [ProofStep (SList B)] -> (SBool, [ProofStep (SList B)])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- SList B -> SList B
forall a. SymVal a => SList a -> SList a
reverse ((SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs))
                           SList B -> ChainsTo (SList B) -> ChainsTo (SList B)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList B -> SList B
forall a. SymVal a => SList a -> SList a
reverse (SA -> SB
f SA
x SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f SList A
xs)
                           SList B -> ChainsTo (SList B) -> ChainsTo (SList B)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList B -> SList B
forall a. SymVal a => SList a -> SList a
reverse ((SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f SList A
xs) SList B -> SList B -> SList B
forall a. SymVal a => SList a -> SList a -> SList a
++ SB -> SList B
forall a. SymVal a => SBV a -> SList a
singleton (SA -> SB
f SA
x)       SList B -> Proof -> ProofStep (SList B)
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
ih
                           ProofStep (SList B)
-> ChainsTo (ProofStep (SList B)) -> ChainsTo (ProofStep (SList B))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse SList A
xs) SList B -> SList B -> SList B
forall a. SymVal a => SList a -> SList a -> SList a
++ SB -> SList B
forall a. SymVal a => SBV a -> SList a
singleton (SA -> SB
f SA
x)
                           SList B -> ChainsTo (SList B) -> ChainsTo (SList B)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse SList A
xs) SList B -> SList B -> SList B
forall a. SymVal a => SList a -> SList a -> SList a
++ (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SA -> SList A
forall a. SymVal a => SBV a -> SList a
singleton SA
x)   SList B -> Proof -> ProofStep (SList B)
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
mApp
                           ProofStep (SList B)
-> ChainsTo (ProofStep (SList B)) -> ChainsTo (ProofStep (SList B))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SA -> SList A
forall a. SymVal a => SBV a -> SList a
singleton SA
x)
                           SList B -> ChainsTo (SList B) -> ChainsTo (SList B)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs))
                           SList B -> ChainsTo (SList B) -> ChainsTo (SList B)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep (SList B)]
ChainsTo (SList B)
forall a. [ProofStep a]
qed

-- * Reverse and length

-- | @length xs == length (reverse xs)@
--
-- We have:
--
-- >>> revLen
-- Inductive lemma: revLen
--   Base: revLen.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: revLen.Step                     Q.E.D.
-- [Proven] revLen
revLen :: IO Proof
revLen :: IO Proof
revLen = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$
   String
-> (Forall "xs" [A] -> SBool)
-> (Proof -> SA -> SList A -> (SBool, [ProofStep SInteger]))
-> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
String -> a -> (Proof -> steps) -> KD Proof
induct String
"revLen"
          (\(Forall @"xs" (SList A
xs :: SList A)) -> SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse SList A
xs) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList A
xs) ((Proof -> SA -> SList A -> (SBool, [ProofStep SInteger]))
 -> KD Proof)
-> (Proof -> SA -> SList A -> (SBool, [ProofStep SInteger]))
-> KD Proof
forall a b. (a -> b) -> a -> b
$
          \Proof
ih (SA
x :: SA) SList A
xs -> [] [SBool] -> [ProofStep SInteger] -> (SBool, [ProofStep SInteger])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs))
                                 SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SA -> SList A
forall a. SymVal a => SBV a -> SList a
singleton SA
x)
                                 SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse SList A
xs) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SA -> SList A
forall a. SymVal a => SBV a -> SList a
singleton SA
x)  SInteger -> Proof -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
ih
                                 ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList A
xs SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1
                                 SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs)
                                 SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep SInteger]
ChainsTo SInteger
forall a. [ProofStep a]
qed

-- | An example where we attempt to prove a non-theorem. Notice the counter-example
-- generated for:
--
-- @length xs = ite (length xs .== 3) 5 (length xs)@
--
-- We have:
--
-- >>> badRevLen `catch` (\(_ :: SomeException) -> pure ())
-- Lemma: badRevLen
-- *** Failed to prove badRevLen.
-- Falsifiable. Counter-example:
--   xs = [A_1,A_2,A_1] :: [A]
badRevLen :: IO ()
badRevLen :: IO ()
badRevLen = KD () -> IO ()
forall a. KD a -> IO a
runKD (KD () -> IO ()) -> KD () -> IO ()
forall a b. (a -> b) -> a -> b
$
   KD Proof -> KD ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (KD Proof -> KD ()) -> KD Proof -> KD ()
forall a b. (a -> b) -> a -> b
$ String -> (Forall "xs" [A] -> SBool) -> [Proof] -> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"badRevLen" (\(Forall @"xs" (SList A
xs :: SList A)) -> SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse SList A
xs) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList A
xs SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
3) SInteger
5 (SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList A
xs)) []

-- * Foldr-map fusion

-- | @foldr f a . map g = foldr (f . g) a@
--
-- We have:
--
-- >>> foldrMapFusion
-- Inductive lemma: foldrMapFusion
--   Base: foldrMapFusion.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: foldrMapFusion.Step             Q.E.D.
-- [Proven] foldrMapFusion
foldrMapFusion :: IO Proof
foldrMapFusion :: IO Proof
foldrMapFusion = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do
  let a :: SA
      a :: SA
a = String -> SA
forall a. SMTDefinable a => String -> a
uninterpret String
"a"

      g :: SC -> SB
      g :: SC -> SB
g = String -> SC -> SB
forall a. SMTDefinable a => String -> a
uninterpret String
"g"

      f :: SB -> SA -> SA
      f :: SB -> SA -> SA
f = String -> SB -> SA -> SA
forall a. SMTDefinable a => String -> a
uninterpret String
"f"

  String
-> (Forall "xs" [C] -> SBool)
-> (Proof -> SC -> SList C -> (SBool, [ProofStep SA]))
-> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
String -> a -> (Proof -> steps) -> KD Proof
induct String
"foldrMapFusion"
         (\(Forall @"xs" SList C
xs) -> (SB -> SA -> SA) -> SA -> SList B -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SB -> SA -> SA
f SA
a ((SC -> SB) -> SList C -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SC -> SB
g SList C
xs) SA -> SA -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SC -> SA -> SA) -> SA -> SList C -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr (SB -> SA -> SA
f (SB -> SA -> SA) -> (SC -> SB) -> SC -> SA -> SA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SC -> SB
g) SA
a SList C
xs) ((Proof -> SC -> SList C -> (SBool, [ProofStep SA])) -> KD Proof)
-> (Proof -> SC -> SList C -> (SBool, [ProofStep SA])) -> KD Proof
forall a b. (a -> b) -> a -> b
$
         \Proof
ih SC
x SList C
xs -> [] [SBool] -> [ProofStep SA] -> (SBool, [ProofStep SA])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- (SB -> SA -> SA) -> SA -> SList B -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SB -> SA -> SA
f SA
a ((SC -> SB) -> SList C -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SC -> SB
g (SC
x SC -> SList C -> SList C
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList C
xs))
                        SA -> ChainsTo SA -> ChainsTo SA
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SB -> SA -> SA) -> SA -> SList B -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SB -> SA -> SA
f SA
a (SC -> SB
g SC
x SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SC -> SB) -> SList C -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SC -> SB
g SList C
xs)
                        SA -> ChainsTo SA -> ChainsTo SA
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SC -> SB
g SC
x SB -> SA -> SA
`f` (SB -> SA -> SA) -> SA -> SList B -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SB -> SA -> SA
f SA
a ((SC -> SB) -> SList C -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SC -> SB
g SList C
xs) SA -> Proof -> ProofStep SA
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
ih
                        ProofStep SA -> ChainsTo (ProofStep SA) -> ChainsTo (ProofStep SA)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SC -> SB
g SC
x SB -> SA -> SA
`f` (SC -> SA -> SA) -> SA -> SList C -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr (SB -> SA -> SA
f (SB -> SA -> SA) -> (SC -> SB) -> SC -> SA -> SA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SC -> SB
g) SA
a SList C
xs
                        SA -> ChainsTo SA -> ChainsTo SA
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SC -> SA -> SA) -> SA -> SList C -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr (SB -> SA -> SA
f (SB -> SA -> SA) -> (SC -> SB) -> SC -> SA -> SA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SC -> SB
g) SA
a (SC
x SC -> SList C -> SList C
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList C
xs)
                        SA -> ChainsTo SA -> ChainsTo SA
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep SA]
ChainsTo SA
forall a. [ProofStep a]
qed

-- * Foldr-foldr fusion

-- |
--
-- @
--   Given f a = b and f (g x y) = h x (f y), for all x and y
--   We have: f . foldr g a = foldr h b
-- @
--
-- >>> foldrFusion
-- Inductive lemma: foldrFusion
--   Base: foldrFusion.Base                Q.E.D.
--   Step: 1                               Q.E.D.
--   Asms: 2                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Asms: 3                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Step: foldrFusion.Step                Q.E.D.
-- [Proven] foldrFusion
foldrFusion :: IO Proof
foldrFusion :: IO Proof
foldrFusion = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do
   let a :: SA
       a :: SA
a = String -> SA
forall a. SMTDefinable a => String -> a
uninterpret String
"a"

       b :: SB
       b :: SB
b = String -> SB
forall a. SMTDefinable a => String -> a
uninterpret String
"b"

       f :: SA -> SB
       f :: SA -> SB
f = String -> SA -> SB
forall a. SMTDefinable a => String -> a
uninterpret String
"f"

       g :: SC -> SA -> SA
       g :: SC -> SA -> SA
g = String -> SC -> SA -> SA
forall a. SMTDefinable a => String -> a
uninterpret String
"g"

       h :: SC -> SB -> SB
       h :: SC -> SB -> SB
h = String -> SC -> SB -> SB
forall a. SMTDefinable a => String -> a
uninterpret String
"h"

       -- Assumptions under which the equality holds
       h1 :: SBool
h1 = SA -> SB
f SA
a SB -> SB -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SB
b
       h2 :: SBool
h2 = (Forall "x" C -> Forall "y" A -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool ((Forall "x" C -> Forall "y" A -> SBool) -> SBool)
-> (Forall "x" C -> Forall "y" A -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \(Forall @"x" SC
x) (Forall @"y" SA
y) -> SA -> SB
f (SC -> SA -> SA
g SC
x SA
y) SB -> SB -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SC -> SB -> SB
h SC
x (SA -> SB
f SA
y)

   String
-> (Forall "xs" [C] -> SBool)
-> (Proof -> SC -> SList C -> (SBool, [ProofStep SB]))
-> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
String -> a -> (Proof -> steps) -> KD Proof
induct String
"foldrFusion"
          (\(Forall @"xs" SList C
xs) -> SBool
h1 SBool -> SBool -> SBool
.&& SBool
h2 SBool -> SBool -> SBool
.=> SA -> SB
f ((SC -> SA -> SA) -> SA -> SList C -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SC -> SA -> SA
g SA
a SList C
xs) SB -> SB -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SC -> SB -> SB) -> SB -> SList C -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SC -> SB -> SB
h SB
b SList C
xs) ((Proof -> SC -> SList C -> (SBool, [ProofStep SB])) -> KD Proof)
-> (Proof -> SC -> SList C -> (SBool, [ProofStep SB])) -> KD Proof
forall a b. (a -> b) -> a -> b
$
          \Proof
ih SC
x SList C
xs -> [SBool
h1, SBool
h2] [SBool] -> [ProofStep SB] -> (SBool, [ProofStep SB])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- SA -> SB
f ((SC -> SA -> SA) -> SA -> SList C -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SC -> SA -> SA
g SA
a (SC
x SC -> SList C -> SList C
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList C
xs))
                               SB -> ChainsTo SB -> ChainsTo SB
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SA -> SB
f (SC -> SA -> SA
g SC
x ((SC -> SA -> SA) -> SA -> SList C -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SC -> SA -> SA
g SA
a SList C
xs))   SB -> SBool -> ProofStep SB
forall a b. ProofHint a b => a -> b -> ProofStep a
?? SBool
h2
                               ProofStep SB -> ChainsTo (ProofStep SB) -> ChainsTo (ProofStep SB)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SC -> SB -> SB
h SC
x (SA -> SB
f ((SC -> SA -> SA) -> SA -> SList C -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SC -> SA -> SA
g SA
a SList C
xs))   SB -> [Helper] -> ProofStep SB
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [SBool -> Helper
hyp SBool
h1, SBool -> Helper
hyp SBool
h2, Proof -> Helper
hprf Proof
ih]
                               ProofStep SB -> ChainsTo (ProofStep SB) -> ChainsTo (ProofStep SB)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SC -> SB -> SB
h SC
x ((SC -> SB -> SB) -> SB -> SList C -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SC -> SB -> SB
h SB
b SList C
xs)
                               SB -> ChainsTo SB -> ChainsTo SB
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SC -> SB -> SB) -> SB -> SList C -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SC -> SB -> SB
h SB
b (SC
x SC -> SList C -> SList C
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList C
xs)
                               SB -> ChainsTo SB -> ChainsTo SB
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep SB]
ChainsTo SB
forall a. [ProofStep a]
qed

-- * Foldr over append

-- | @foldr f a (xs ++ ys) == foldr f (foldr f a ys) xs@
--
-- We have:
--
-- >>> foldrOverAppend
-- Inductive lemma: foldrOverAppend
--   Base: foldrOverAppend.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: foldrOverAppend.Step            Q.E.D.
-- [Proven] foldrOverAppend
foldrOverAppend :: IO Proof
foldrOverAppend :: IO Proof
foldrOverAppend = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do
   let a :: SA
       a :: SA
a = String -> SA
forall a. SMTDefinable a => String -> a
uninterpret String
"a"

       f :: SA -> SA -> SA
       f :: SA -> SA -> SA
f = String -> SA -> SA -> SA
forall a. SMTDefinable a => String -> a
uninterpret String
"f"

   String
-> (Forall "xs" [A] -> Forall "ys" [A] -> SBool)
-> (Proof -> SA -> SList A -> SList A -> (SBool, [ProofStep SA]))
-> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
String -> a -> (Proof -> steps) -> KD Proof
induct String
"foldrOverAppend"
          (\(Forall @"xs" SList A
xs) (Forall @"ys" SList A
ys) -> (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f SA
a (SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys) SA -> SA -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f ((SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f SA
a SList A
ys) SList A
xs) ((Proof -> SA -> SList A -> SList A -> (SBool, [ProofStep SA]))
 -> KD Proof)
-> (Proof -> SA -> SList A -> SList A -> (SBool, [ProofStep SA]))
-> KD Proof
forall a b. (a -> b) -> a -> b
$
          \Proof
ih SA
x SList A
xs SList A
ys -> [] [SBool] -> [ProofStep SA] -> (SBool, [ProofStep SA])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f SA
a ((SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs) SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys)
                            SA -> ChainsTo SA -> ChainsTo SA
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f SA
a (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys))
                            SA -> ChainsTo SA -> ChainsTo SA
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SA
x SA -> SA -> SA
`f` (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f SA
a (SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys)       SA -> Proof -> ProofStep SA
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
ih
                            ProofStep SA -> ChainsTo (ProofStep SA) -> ChainsTo (ProofStep SA)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SA
x SA -> SA -> SA
`f` (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f ((SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f SA
a SList A
ys) SList A
xs
                            SA -> ChainsTo SA -> ChainsTo SA
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f ((SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f SA
a SList A
ys) (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs)
                            SA -> ChainsTo SA -> ChainsTo SA
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep SA]
ChainsTo SA
forall a. [ProofStep a]
qed

-- * Foldl over append

-- | @foldl f a (xs ++ ys) == foldl f (foldl f a xs) ys@
--
-- We have:
--
-- >>> foldlOverAppend (uninterpret "f")
-- Inductive lemma: foldlOverAppend
--   Base: foldlOverAppend.Base            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: foldlOverAppend.Step            Q.E.D.
-- [Proven] foldlOverAppend
foldlOverAppend :: (SB -> SA -> SB) -> IO Proof
foldlOverAppend :: (SB -> SA -> SB) -> IO Proof
foldlOverAppend SB -> SA -> SB
f = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$
   String
-> (Forall "xs" [A] -> Forall "ys" [A] -> Forall "a" B -> SBool)
-> (Proof
    -> SA -> SList A -> SList A -> SB -> (SBool, [ProofStep SB]))
-> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
String -> a -> (Proof -> steps) -> KD Proof
induct String
"foldlOverAppend"
          (\(Forall @"xs" SList A
xs) (Forall @"ys" SList A
ys) (Forall @"a" SB
a) -> (SB -> SA -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SB -> SA -> SB
f SB
a (SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys) SB -> SB -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SB -> SA -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SB -> SA -> SB
f ((SB -> SA -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SB -> SA -> SB
f SB
a SList A
xs) SList A
ys) ((Proof
  -> SA -> SList A -> SList A -> SB -> (SBool, [ProofStep SB]))
 -> KD Proof)
-> (Proof
    -> SA -> SList A -> SList A -> SB -> (SBool, [ProofStep SB]))
-> KD Proof
forall a b. (a -> b) -> a -> b
$
          \Proof
ih SA
x SList A
xs SList A
ys SB
a -> [] [SBool] -> [ProofStep SB] -> (SBool, [ProofStep SB])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- (SB -> SA -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SB -> SA -> SB
f SB
a ((SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs) SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys)
                              SB -> ChainsTo SB -> ChainsTo SB
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SB -> SA -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SB -> SA -> SB
f SB
a (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys))
                              SB -> ChainsTo SB -> ChainsTo SB
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SB -> SA -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SB -> SA -> SB
f (SB
a SB -> SA -> SB
`f` SA
x) (SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys)
                              -- z3 is smart enough to instantiate the IH correctly below, but we're
                              -- using an explicit instantiation to be clear about the use of @a@ at a different value
                              SB -> Proof -> ProofStep SB
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
ih Proof -> (Inst "ys" [A], Inst "a" B) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList A
ys, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"a" (SB
a SB -> SA -> SB
`f` SA
x))
                              ProofStep SB -> ChainsTo (ProofStep SB) -> ChainsTo (ProofStep SB)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SB -> SA -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SB -> SA -> SB
f ((SB -> SA -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SB -> SA -> SB
f (SB
a SB -> SA -> SB
`f` SA
x) SList A
xs) SList A
ys
                              SB -> ChainsTo SB -> ChainsTo SB
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep SB]
ChainsTo SB
forall a. [ProofStep a]
qed

-- * Foldr-foldl correspondence

-- | @foldr f e xs == foldl (flip f) e (reverse xs)@
--
-- We have:
--
-- >>> foldrFoldlDuality
-- Inductive lemma: foldlOverAppend
--   Base: foldlOverAppend.Base            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: foldlOverAppend.Step            Q.E.D.
-- Inductive lemma: foldrFoldlDuality
--   Base: foldrFoldlDuality.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.
--   Step: 6                               Q.E.D.
--   Step: foldrFoldlDuality.Step          Q.E.D.
-- [Proven] foldrFoldlDuality
foldrFoldlDuality :: IO Proof
foldrFoldlDuality :: IO Proof
foldrFoldlDuality = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do
   let f :: SA -> SB -> SB
       f :: SA -> SB -> SB
f = String -> SA -> SB -> SB
forall a. SMTDefinable a => String -> a
uninterpret String
"f"

   foa <- IO Proof -> KD Proof
use ((SB -> SA -> SB) -> IO Proof
foldlOverAppend ((SA -> SB -> SB) -> SB -> SA -> SB
forall a b c. (a -> b -> c) -> b -> a -> c
flip SA -> SB -> SB
f))

   induct "foldrFoldlDuality"
          (\(Forall @"xs" SList A
xs) (Forall @"e" SB
e) -> (SA -> SB -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SB -> SB
f SB
e SList A
xs SB -> SB -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SB -> SA -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl ((SA -> SB -> SB) -> SB -> SA -> SB
forall a b c. (a -> b -> c) -> b -> a -> c
flip SA -> SB -> SB
f) SB
e (SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse SList A
xs)) $
          \Proof
ih SA
x SList A
xs SB
e ->
              let ff :: SB -> SA -> SB
ff  = (SA -> SB -> SB) -> SB -> SA -> SB
forall a b c. (a -> b -> c) -> b -> a -> c
flip SA -> SB -> SB
f
                  rxs :: SList A
rxs = SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse SList A
xs
              in [] [SBool] -> [ProofStep SB] -> (SBool, [ProofStep SB])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- (SA -> SB -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SB -> SB
f SB
e (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs) SB -> ChainsTo SB -> ChainsTo SB
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SA
x SA -> SB -> SB
`f` (SA -> SB -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SB -> SB
f SB
e SList A
xs                      SB -> Proof -> ProofStep SB
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
ih
                                           ProofStep SB -> ChainsTo (ProofStep SB) -> ChainsTo (ProofStep SB)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SA
x SA -> SB -> SB
`f` (SB -> SA -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SB -> SA -> SB
ff SB
e SList A
rxs
                                           SB -> ChainsTo SB -> ChainsTo SB
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SB -> SA -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SB -> SA -> SB
ff SB
e SList A
rxs SB -> SA -> SB
`ff` SA
x
                                           SB -> ChainsTo SB -> ChainsTo SB
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SB -> SA -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SB -> SA -> SB
ff ((SB -> SA -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SB -> SA -> SB
ff SB
e SList A
rxs) (SA -> SList A
forall a. SymVal a => SBV a -> SList a
singleton SA
x) SB -> Proof -> ProofStep SB
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
foa
                                           ProofStep SB -> ChainsTo (ProofStep SB) -> ChainsTo (ProofStep SB)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SB -> SA -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SB -> SA -> SB
ff SB
e (SList A
rxs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SA -> SList A
forall a. SymVal a => SBV a -> SList a
singleton SA
x)
                                           SB -> ChainsTo SB -> ChainsTo SB
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SB -> SA -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SB -> SA -> SB
ff SB
e (SList A -> SList A
forall a. SymVal a => SList a -> SList a
reverse (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs))
                                           SB -> ChainsTo SB -> ChainsTo SB
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep SB]
ChainsTo SB
forall a. [ProofStep a]
qed

-- * Foldr-foldl duality, generalized

-- | Given:
--
-- @
--     x \@ (y \@ z) = (x \@ y) \@ z     (associativity of @)
-- and e \@ x = x                     (left unit)
-- and x \@ e = x                     (right unit)
-- @
--
-- Prove:
--
-- @
--     foldr (\@) e xs = foldl (\@) e xs
-- @
--
-- We have:
--
-- >>> foldrFoldlDualityGeneralized
-- Inductive lemma: helper
--   Base: helper.Base                     Q.E.D.
--   Step: 1                               Q.E.D.
--   Asms: 2                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Asms: 3                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Step: helper.Step                     Q.E.D.
-- Inductive lemma: foldrFoldlDuality
--   Base: foldrFoldlDuality.Base          Q.E.D.
--   Step: 1                               Q.E.D.
--   Asms: 2                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Asms: 3                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Asms: 4                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Asms: 5                               Q.E.D.
--   Step: 5                               Q.E.D.
--   Step: 6                               Q.E.D.
--   Step: foldrFoldlDuality.Step          Q.E.D.
-- [Proven] foldrFoldlDuality
foldrFoldlDualityGeneralized :: IO Proof
foldrFoldlDualityGeneralized :: IO Proof
foldrFoldlDualityGeneralized  = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do
   let (@) :: SA -> SA -> SA
       @ :: SA -> SA -> SA
(@) = String -> SA -> SA -> SA
forall a. SMTDefinable a => String -> a
uninterpret String
"|@|"

       e :: SA
       e :: SA
e = String -> SA
forall a. SMTDefinable a => String -> a
uninterpret String
"e"

   -- Assumptions under which the equality holds
   let assoc :: SBool
assoc = (Forall "x" A -> Forall "y" A -> Forall "z" A -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool ((Forall "x" A -> Forall "y" A -> Forall "z" A -> SBool) -> SBool)
-> (Forall "x" A -> Forall "y" A -> Forall "z" A -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \(Forall @"x" SA
x) (Forall @"y" SA
y) (Forall @"z" SA
z) -> SA
x SA -> SA -> SA
@ (SA
y SA -> SA -> SA
@ SA
z) SA -> SA -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SA
x SA -> SA -> SA
@ SA
y) SA -> SA -> SA
@ SA
z
       lunit :: SBool
lunit = (Forall "x" A -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool ((Forall "x" A -> SBool) -> SBool)
-> (Forall "x" A -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \(Forall @"x" SA
x) -> SA
e SA -> SA -> SA
@ SA
x SA -> SA -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SA
x
       runit :: SBool
runit = (Forall "x" A -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool ((Forall "x" A -> SBool) -> SBool)
-> (Forall "x" A -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \(Forall @"x" SA
x) -> SA
x SA -> SA -> SA
@ SA
e SA -> SA -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SA
x

   -- Helper: foldl (@) (y @ z) xs = y @ foldl (@) z xs
   -- Note the instantiation of the IH at a different value for z. It turns out
   -- we don't have to actually specify this since z3 can figure it out by itself, but we're being explicit.
   helper <- String
-> (Forall "xs" [A] -> Forall "y" A -> Forall "z" A -> SBool)
-> (Proof -> SA -> SList A -> SA -> SA -> (SBool, [ProofStep SA]))
-> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
String -> a -> (Proof -> steps) -> KD Proof
induct String
"helper"
                     (\(Forall @"xs" SList A
xs) (Forall @"y" SA
y) (Forall @"z" SA
z) -> SBool
assoc SBool -> SBool -> SBool
.=> (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SA -> SA -> SA
(@) (SA
y SA -> SA -> SA
@ SA
z) SList A
xs SA -> SA -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SA
y SA -> SA -> SA
@ (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SA -> SA -> SA
(@) SA
z SList A
xs) ((Proof -> SA -> SList A -> SA -> SA -> (SBool, [ProofStep SA]))
 -> KD Proof)
-> (Proof -> SA -> SList A -> SA -> SA -> (SBool, [ProofStep SA]))
-> KD Proof
forall a b. (a -> b) -> a -> b
$
                     \Proof
ih SA
x SList A
xs SA
y SA
z -> [SBool
assoc] [SBool] -> [ProofStep SA] -> (SBool, [ProofStep SA])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SA -> SA -> SA
(@) (SA
y SA -> SA -> SA
@ SA
z) (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs)
                                             SA -> ChainsTo SA -> ChainsTo SA
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SA -> SA -> SA
(@) ((SA
y SA -> SA -> SA
@ SA
z) SA -> SA -> SA
@ SA
x) SList A
xs
                                             SA -> SBool -> ProofStep SA
forall a b. ProofHint a b => a -> b -> ProofStep a
?? SBool
assoc
                                             ProofStep SA -> ChainsTo (ProofStep SA) -> ChainsTo (ProofStep SA)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SA -> SA -> SA
(@) (SA
y SA -> SA -> SA
@ (SA
z SA -> SA -> SA
@ SA
x)) SList A
xs
                                             SA -> [Helper] -> ProofStep SA
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [SBool -> Helper
hyp SBool
assoc, Proof -> Helper
hprf (Proof
ih Proof -> (Inst "y" A, Inst "z" A) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"y" SA
y, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"z" (SA
z SA -> SA -> SA
@ SA
x)))]
                                             ProofStep SA -> ChainsTo (ProofStep SA) -> ChainsTo (ProofStep SA)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SA
y SA -> SA -> SA
@ (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SA -> SA -> SA
(@) (SA
z SA -> SA -> SA
@ SA
x) SList A
xs
                                             SA -> ChainsTo SA -> ChainsTo SA
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SA
y SA -> SA -> SA
@ (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SA -> SA -> SA
(@) SA
z (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs)
                                             SA -> ChainsTo SA -> ChainsTo SA
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep SA]
ChainsTo SA
forall a. [ProofStep a]
qed

   induct "foldrFoldlDuality"
          (\(Forall @"xs" SList A
xs) -> SBool
assoc SBool -> SBool -> SBool
.&& SBool
lunit SBool -> SBool -> SBool
.&& SBool
runit SBool -> SBool -> SBool
.=> (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
(@) SA
e SList A
xs SA -> SA -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SA -> SA -> SA
(@) SA
e SList A
xs) $
          \Proof
ih SA
x SList A
xs -> [SBool
assoc, SBool
lunit, SBool
runit] [SBool] -> [ProofStep SA] -> (SBool, [ProofStep SA])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
(@) SA
e (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs)
                                            SA -> ChainsTo SA -> ChainsTo SA
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SA
x SA -> SA -> SA
@ (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
(@) SA
e SList A
xs    SA -> [Helper] -> ProofStep SA
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [SBool -> Helper
hyp SBool
assoc, SBool -> Helper
hyp SBool
lunit, SBool -> Helper
hyp SBool
runit, Proof -> Helper
hprf Proof
ih]
                                            ProofStep SA -> ChainsTo (ProofStep SA) -> ChainsTo (ProofStep SA)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SA
x SA -> SA -> SA
@ (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SA -> SA -> SA
(@) SA
e SList A
xs    SA -> [Helper] -> ProofStep SA
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [SBool -> Helper
hyp SBool
assoc, Proof -> Helper
hprf Proof
helper]
                                            ProofStep SA -> ChainsTo (ProofStep SA) -> ChainsTo (ProofStep SA)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SA -> SA -> SA
(@) (SA
x SA -> SA -> SA
@ SA
e) SList A
xs  SA -> SBool -> ProofStep SA
forall a b. ProofHint a b => a -> b -> ProofStep a
?? SBool
runit
                                            ProofStep SA -> ChainsTo (ProofStep SA) -> ChainsTo (ProofStep SA)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SA -> SA -> SA
(@) SA
x SList A
xs        SA -> SBool -> ProofStep SA
forall a b. ProofHint a b => a -> b -> ProofStep a
?? SBool
lunit
                                            ProofStep SA -> ChainsTo (ProofStep SA) -> ChainsTo (ProofStep SA)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SA -> SA -> SA
(@) (SA
e SA -> SA -> SA
@ SA
x) SList A
xs
                                            SA -> ChainsTo SA -> ChainsTo SA
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SA -> SA -> SA
(@) SA
e (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs)
                                            SA -> ChainsTo SA -> ChainsTo SA
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep SA]
ChainsTo SA
forall a. [ProofStep a]
qed

-- * Another foldl-foldr correspondence

-- | Given:
--
-- @
--        (x \<+> y) \<*> z = x \<+> (y \<*> z)
--   and  x \<+> e = e \<*> x
-- @
--
-- Proves:
--
-- @
--    foldr (\<+>) e xs = foldl (\<*>) e xs
-- @
--
-- In Bird's Introduction to Functional Programming book (2nd edition) this is called the second duality theorem. We have:
--
-- >>> foldrFoldl
-- Inductive lemma: foldl over <*>/<+>
--   Base: foldl over <*>/<+>.Base         Q.E.D.
--   Step: 1                               Q.E.D.
--   Asms: 2                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Asms: 3                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Step: foldl over <*>/<+>.Step         Q.E.D.
-- Inductive lemma: foldrFoldl
--   Base: foldrFoldl.Base                 Q.E.D.
--   Step: 1                               Q.E.D.
--   Asms: 2                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Asms: 3                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Asms: 4                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Step: 5                               Q.E.D.
--   Step: foldrFoldl.Step                 Q.E.D.
-- [Proven] foldrFoldl
foldrFoldl :: IO Proof
foldrFoldl :: IO Proof
foldrFoldl = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do

   let -- Declare the operators as uninterpreted functions
       (<+>) :: SA -> SB -> SB
       <+> :: SA -> SB -> SB
(<+>) = String -> SA -> SB -> SB
forall a. SMTDefinable a => String -> a
uninterpret String
"<+>"

       (<*>) :: SB -> SA -> SB
       <*> :: SB -> SA -> SB
(<*>) = String -> SB -> SA -> SB
forall a. SMTDefinable a => String -> a
uninterpret String
"<*>"

       -- The unit element
       e :: SB
       e :: SB
e = String -> SB
forall a. SMTDefinable a => String -> a
uninterpret String
"e"

   -- Assumptions about the operators
   let -- (x <+> y) <*> z == x <+> (y <*> z)
       assoc :: SBool
assoc = (Forall "x" A -> Forall "y" B -> Forall "z" A -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool ((Forall "x" A -> Forall "y" B -> Forall "z" A -> SBool) -> SBool)
-> (Forall "x" A -> Forall "y" B -> Forall "z" A -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \(Forall @"x" SA
x) (Forall @"y" SB
y) (Forall @"z" SA
z) -> (SA
x SA -> SB -> SB
<+> SB
y) SB -> SA -> SB
<*> SA
z SB -> SB -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SA
x SA -> SB -> SB
<+> (SB
y SB -> SA -> SB
<*> SA
z)

       -- x <+> e == e <*> x
       unit :: SBool
unit  = (Forall "x" A -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool ((Forall "x" A -> SBool) -> SBool)
-> (Forall "x" A -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \(Forall @"x" SA
x) -> SA
x SA -> SB -> SB
<+> SB
e SB -> SB -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SB
e SB -> SA -> SB
<*> SA
x

   -- Helper: x <+> foldl (<*>) y xs == foldl (<*>) (x <+> y) xs
   helper <-
      String
-> (Forall "xs" [A] -> Forall "x" A -> Forall "y" B -> SBool)
-> (Proof -> SA -> SList A -> SA -> SB -> (SBool, [ProofStep SB]))
-> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
String -> a -> (Proof -> steps) -> KD Proof
induct String
"foldl over <*>/<+>"
             (\(Forall @"xs" SList A
xs) (Forall @"x" SA
x) (Forall @"y" SB
y) -> SBool
assoc SBool -> SBool -> SBool
.=> SA
x SA -> SB -> SB
<+> (SB -> SA -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SB -> SA -> SB
(<*>) SB
y SList A
xs SB -> SB -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SB -> SA -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SB -> SA -> SB
(<*>) (SA
x SA -> SB -> SB
<+> SB
y) SList A
xs) ((Proof -> SA -> SList A -> SA -> SB -> (SBool, [ProofStep SB]))
 -> KD Proof)
-> (Proof -> SA -> SList A -> SA -> SB -> (SBool, [ProofStep SB]))
-> KD Proof
forall a b. (a -> b) -> a -> b
$
             -- Using z to avoid confusion with the variable x already present, following Bird.
             -- z3 can figure out the proper instantiation of ih so the at call is unnecessary, but being explicit is helpful.
             \Proof
ih SA
z SList A
xs SA
x SB
y -> [SBool
assoc] [SBool] -> [ProofStep SB] -> (SBool, [ProofStep SB])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- SA
x SA -> SB -> SB
<+> (SB -> SA -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SB -> SA -> SB
(<*>) SB
y (SA
z SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs)
                                     SB -> ChainsTo SB -> ChainsTo SB
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SA
x SA -> SB -> SB
<+> (SB -> SA -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SB -> SA -> SB
(<*>) (SB
y SB -> SA -> SB
<*> SA
z) SList A
xs    SB -> [Helper] -> ProofStep SB
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [SBool -> Helper
hyp SBool
assoc, Proof -> Helper
hprf (Proof
ih Proof -> (Inst "x" A, Inst "y" B) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SA
x, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"y" (SB
y SB -> SA -> SB
<*> SA
z)))]
                                     ProofStep SB -> ChainsTo (ProofStep SB) -> ChainsTo (ProofStep SB)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SB -> SA -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SB -> SA -> SB
(<*>) (SA
x SA -> SB -> SB
<+> (SB
y SB -> SA -> SB
<*> SA
z)) SList A
xs  SB -> SBool -> ProofStep SB
forall a b. ProofHint a b => a -> b -> ProofStep a
?? SBool
assoc
                                     ProofStep SB -> ChainsTo (ProofStep SB) -> ChainsTo (ProofStep SB)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SB -> SA -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SB -> SA -> SB
(<*>) ((SA
x SA -> SB -> SB
<+> SB
y) SB -> SA -> SB
<*> SA
z) SList A
xs
                                     SB -> ChainsTo SB -> ChainsTo SB
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SB -> SA -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SB -> SA -> SB
(<*>) (SA
x SA -> SB -> SB
<+> SB
y) (SA
z SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs)
                                     SB -> ChainsTo SB -> ChainsTo SB
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep SB]
ChainsTo SB
forall a. [ProofStep a]
qed

   -- Final proof:
   induct "foldrFoldl"
          (\(Forall @"xs" SList A
xs) -> SBool
assoc SBool -> SBool -> SBool
.&& SBool
unit SBool -> SBool -> SBool
.=> (SA -> SB -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SB -> SB
(<+>) SB
e SList A
xs SB -> SB -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SB -> SA -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SB -> SA -> SB
(<*>) SB
e SList A
xs) $
          \Proof
ih SA
x SList A
xs -> [SBool
assoc, SBool
unit] [SBool] -> [ProofStep SB] -> (SBool, [ProofStep SB])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- (SA -> SB -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SB -> SB
(<+>) SB
e (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs)
                                    SB -> ChainsTo SB -> ChainsTo SB
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SA
x SA -> SB -> SB
<+> (SA -> SB -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SB -> SB
(<+>) SB
e SList A
xs    SB -> [Helper] -> ProofStep SB
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [SBool -> Helper
hyp SBool
assoc, SBool -> Helper
hyp SBool
unit, Proof -> Helper
hprf Proof
ih]
                                    ProofStep SB -> ChainsTo (ProofStep SB) -> ChainsTo (ProofStep SB)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SA
x SA -> SB -> SB
<+> (SB -> SA -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SB -> SA -> SB
(<*>) SB
e SList A
xs    SB -> [Helper] -> ProofStep SB
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [SBool -> Helper
hyp SBool
assoc, Proof -> Helper
hprf Proof
helper]
                                    ProofStep SB -> ChainsTo (ProofStep SB) -> ChainsTo (ProofStep SB)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SB -> SA -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SB -> SA -> SB
(<*>) (SA
x SA -> SB -> SB
<+> SB
e) SList A
xs  SB -> SBool -> ProofStep SB
forall a b. ProofHint a b => a -> b -> ProofStep a
?? SBool
unit
                                    ProofStep SB -> ChainsTo (ProofStep SB) -> ChainsTo (ProofStep SB)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SB -> SA -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SB -> SA -> SB
(<*>) (SB
e SB -> SA -> SB
<*> SA
x) SList A
xs
                                    SB -> ChainsTo SB -> ChainsTo SB
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SB -> SA -> SB) -> SB -> SList A -> SB
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SB -> SA -> SB
(<*>) SB
e (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs)
                                    SB -> ChainsTo SB -> ChainsTo SB
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep SB]
ChainsTo SB
forall a. [ProofStep a]
qed

-- * Bookkeeping law

-- | Provided @f@ is associative and @a@ is its both left and right-unit:
--
-- @foldr f a . concat == foldr f a . map (foldr f a)@
--
-- We have:
--
-- >>> bookKeeping
-- Inductive lemma: foldBase
--   Base: foldBase.Base                   Q.E.D.
--   Step: 1                               Q.E.D.
--   Asms: 2                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Asms: 3                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Step: foldBase.Step                   Q.E.D.
-- Inductive lemma: foldrOverAppend
--   Base: foldrOverAppend.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: foldrOverAppend.Step            Q.E.D.
-- Inductive lemma: bookKeeping
--   Base: bookKeeping.Base                Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Asms: 3                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Asms: 4                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Step: 5                               Q.E.D.
--   Step: 6                               Q.E.D.
--   Step: bookKeeping.Step                Q.E.D.
-- [Proven] bookKeeping
--
-- NB. As of early 2025, we cannot express the above theorem in SBV directly, since it involves nested lambdas.
-- (On the right hand side map has an argument that is represented as a foldr, which itself has a lambda.) As
-- SMTLib moves to a higher-order logic, we intend to make such expressions readily expressable. In the mean time,
-- we use an equivalent (albeit roundabout) version, where we define map-foldr combo as a recursive function ourselves.
--
-- NB. This theorem does not hold if @f@ does not have a left-unit! Consider the input @[[], [x]]@. Left hand side reduces to
-- @x@, while the right hand side reduces to: @f a x@. And unless @f@ is commutative or @a@ is not also a left-unit,
-- then one can find a counter-example. (Aside: if both left and right units exist for a binary operator, then they
-- are necessarily the same element, since @l = f l r = r@. So, an equivalent statement could simply say @f@ has
-- both left and right units.) A concrete counter-example is:
--
-- @
--   data T = A | B | C
--
--   f :: T -> T -> T
--   f C A = A
--   f C B = A
--   f x _ = x
-- @
--
-- You can verify @f@ is associative. Also note that @C@ is the right-unit for @f@, but it isn't the left-unit.
-- In fact, @f@ has no-left unit by the above argument. In this case, the bookkeeping law produces @B@ for
-- the left-hand-side, and @A@ for the right-hand-side for the input @[[], [B]]@.
bookKeeping :: IO Proof
bookKeeping :: IO Proof
bookKeeping = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do
   let a :: SA
       a :: SA
a = String -> SA
forall a. SMTDefinable a => String -> a
uninterpret String
"a"

       f :: SA -> SA -> SA
       f :: SA -> SA -> SA
f = String -> SA -> SA -> SA
forall a. SMTDefinable a => String -> a
uninterpret String
"f"

       -- Fuse map (foldr f a) in the theorem into one call to avoid nested lambdas. See above note.
       mapFoldr :: SA -> SList [A] -> SList A
       mapFoldr :: SA -> SList [A] -> SList A
mapFoldr = String
-> (SA -> SList [A] -> SList A) -> SA -> SList [A] -> SList A
forall a. (SMTDefinable a, Lambda Symbolic a) => String -> a -> a
smtFunction String
"mapFoldr" ((SA -> SList [A] -> SList A) -> SA -> SList [A] -> SList A)
-> (SA -> SList [A] -> SList A) -> SA -> SList [A] -> SList A
forall a b. (a -> b) -> a -> b
$ \SA
e SList [A]
xss -> 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]
xss)
                                                         SList A
forall a. SymVal a => SList a
nil
                                                         ((SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f SA
e (SList [A] -> SList A
forall a. SymVal a => SList a -> SBV a
head SList [A]
xss) SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SA -> SList [A] -> SList A
mapFoldr SA
e (SList [A] -> SList [A]
forall a. SymVal a => SList a -> SList a
tail SList [A]
xss))

   -- Assumptions about f
   let assoc :: SBool
assoc = (Forall "x" A -> Forall "y" A -> Forall "z" A -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool ((Forall "x" A -> Forall "y" A -> Forall "z" A -> SBool) -> SBool)
-> (Forall "x" A -> Forall "y" A -> Forall "z" A -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \(Forall @"x" SA
x) (Forall @"y" SA
y) (Forall @"z" SA
z) -> SA
x SA -> SA -> SA
`f` (SA
y SA -> SA -> SA
`f` SA
z) SA -> SA -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SA
x SA -> SA -> SA
`f` SA
y) SA -> SA -> SA
`f` SA
z
       rUnit :: SBool
rUnit = (Forall "x" A -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool ((Forall "x" A -> SBool) -> SBool)
-> (Forall "x" A -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \(Forall @"x" SA
x) -> SA
x SA -> SA -> SA
`f` SA
a SA -> SA -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SA
x
       lUnit :: SBool
lUnit = (Forall "x" A -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool ((Forall "x" A -> SBool) -> SBool)
-> (Forall "x" A -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \(Forall @"x" SA
x) -> SA
a SA -> SA -> SA
`f` SA
x SA -> SA -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SA
x

   -- Helper:
   --   foldr f y xs = foldr f a xs `f` y
   helper <- String
-> (Forall "xs" [A] -> Forall "y" A -> SBool)
-> (Proof -> SA -> SList A -> SA -> (SBool, [ProofStep SA]))
-> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
String -> a -> (Proof -> steps) -> KD Proof
induct String
"foldBase"
                    (\(Forall @"xs" SList A
xs) (Forall @"y" SA
y) -> SBool
lUnit SBool -> SBool -> SBool
.&& SBool
assoc SBool -> SBool -> SBool
.=> (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f SA
y SList A
xs SA -> SA -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f SA
a SList A
xs SA -> SA -> SA
`f` SA
y) ((Proof -> SA -> SList A -> SA -> (SBool, [ProofStep SA]))
 -> KD Proof)
-> (Proof -> SA -> SList A -> SA -> (SBool, [ProofStep SA]))
-> KD Proof
forall a b. (a -> b) -> a -> b
$
                    \Proof
ih SA
x SList A
xs SA
y -> [SBool
lUnit, SBool
assoc] [SBool] -> [ProofStep SA] -> (SBool, [ProofStep SA])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f SA
y (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs)
                                                 SA -> ChainsTo SA -> ChainsTo SA
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SA
x SA -> SA -> SA
`f` (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f SA
y SList A
xs          SA -> [Helper] -> ProofStep SA
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [SBool -> Helper
hyp SBool
lUnit, SBool -> Helper
hyp SBool
assoc, Proof -> Helper
hprf Proof
ih]
                                                 ProofStep SA -> ChainsTo (ProofStep SA) -> ChainsTo (ProofStep SA)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SA
x SA -> SA -> SA
`f` ((SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f SA
a SList A
xs SA -> SA -> SA
`f` SA
y)  SA -> SBool -> ProofStep SA
forall a b. ProofHint a b => a -> b -> ProofStep a
?? SBool
assoc
                                                 ProofStep SA -> ChainsTo (ProofStep SA) -> ChainsTo (ProofStep SA)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA
x SA -> SA -> SA
`f` (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f SA
a SList A
xs) SA -> SA -> SA
`f` SA
y
                                                 SA -> ChainsTo SA -> ChainsTo SA
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f SA
a (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs) SA -> SA -> SA
`f` SA
y
                                                 SA -> ChainsTo SA -> ChainsTo SA
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep SA]
ChainsTo SA
forall a. [ProofStep a]
qed

   foa <- use foldrOverAppend

   induct "bookKeeping"
          (\(Forall @"xss" SList [A]
xss) -> SBool
assoc SBool -> SBool -> SBool
.&& SBool
rUnit SBool -> SBool -> SBool
.&& SBool
lUnit SBool -> SBool -> SBool
.=> (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f SA
a (SList [A] -> SList A
forall a. SymVal a => SList [a] -> SList a
concat SList [A]
xss) SA -> SA -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f SA
a (SA -> SList [A] -> SList A
mapFoldr SA
a SList [A]
xss)) $
          \Proof
ih SList A
xs SList [A]
xss -> [SBool
assoc, SBool
rUnit, SBool
lUnit] [SBool] -> [ProofStep SA] -> (SBool, [ProofStep SA])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f SA
a (SList [A] -> SList A
forall a. SymVal a => SList [a] -> SList a
concat (SList A
xs SList A -> SList [A] -> SList [A]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList [A]
xss))
                                              SA -> ChainsTo SA -> ChainsTo SA
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f SA
a (SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList [A] -> SList A
forall a. SymVal a => SList [a] -> SList a
concat SList [A]
xss)                 SA -> Proof -> ProofStep SA
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
foa
                                              ProofStep SA -> ChainsTo (ProofStep SA) -> ChainsTo (ProofStep SA)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f ((SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f SA
a (SList [A] -> SList A
forall a. SymVal a => SList [a] -> SList a
concat SList [A]
xss)) SList A
xs          SA -> [Helper] -> ProofStep SA
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [SBool -> Helper
hyp SBool
assoc, SBool -> Helper
hyp SBool
rUnit, SBool -> Helper
hyp SBool
lUnit, Proof -> Helper
hprf Proof
ih]
                                              ProofStep SA -> ChainsTo (ProofStep SA) -> ChainsTo (ProofStep SA)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f ((SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f SA
a (SA -> SList [A] -> SList A
mapFoldr SA
a SList [A]
xss)) SList A
xs      SA -> [Helper] -> ProofStep SA
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [SBool -> Helper
hyp SBool
lUnit, SBool -> Helper
hyp SBool
assoc, Proof -> Helper
hprf (Proof
helper Proof -> (Inst "xs" [A], Inst "y" A) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList A
xs, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"y" ((SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f SA
a (SA -> SList [A] -> SList A
mapFoldr SA
a SList [A]
xss))))]
                                              ProofStep SA -> ChainsTo (ProofStep SA) -> ChainsTo (ProofStep SA)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f SA
a SList A
xs SA -> SA -> SA
`f` (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f SA
a (SA -> SList [A] -> SList A
mapFoldr SA
a SList [A]
xss)
                                              SA -> ChainsTo SA -> ChainsTo SA
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f SA
a ((SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f SA
a SList A
xs SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SA -> SList [A] -> SList A
mapFoldr SA
a SList [A]
xss)
                                              SA -> ChainsTo SA -> ChainsTo SA
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SA -> SA) -> SA -> SList A -> SA
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SA -> SA -> SA
f SA
a (SA -> SList [A] -> SList A
mapFoldr SA
a (SList A
xs SList A -> SList [A] -> SList [A]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList [A]
xss))
                                              SA -> ChainsTo SA -> ChainsTo SA
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep SA]
ChainsTo SA
forall a. [ProofStep a]
qed

-- * Filter-append

-- | @filter p (xs ++ ys) == filter p xs ++ filter p ys@
--
-- We have:
--
-- >>> filterAppend (uninterpret "p")
-- Inductive lemma: filterAppend
--   Base: filterAppend.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.
--   Step: filterAppend.Step               Q.E.D.
-- [Proven] filterAppend
filterAppend :: (SA -> SBool) -> IO Proof
filterAppend :: (SA -> SBool) -> IO Proof
filterAppend SA -> SBool
p = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$
   String
-> (Forall "xs" [A] -> Forall "ys" [A] -> SBool)
-> (Proof
    -> SA -> SList A -> SList A -> (SBool, [ProofStep (SList A)]))
-> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
String -> a -> (Proof -> steps) -> KD Proof
induct String
"filterAppend"
          (\(Forall @"xs" SList A
xs) (Forall @"ys" SList A
ys) -> (SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
p SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ (SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
p SList A
ys SList A -> SList A -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
p (SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys)) ((Proof
  -> SA -> SList A -> SList A -> (SBool, [ProofStep (SList A)]))
 -> KD Proof)
-> (Proof
    -> SA -> SList A -> SList A -> (SBool, [ProofStep (SList A)]))
-> KD Proof
forall a b. (a -> b) -> a -> b
$
          \Proof
ih SA
x SList A
xs SList A
ys -> [] [SBool] -> [ProofStep (SList A)] -> (SBool, [ProofStep (SList A)])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- (SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
p (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs) SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ (SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
p SList A
ys
                            SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SList A -> SList A -> SList A
forall a. Mergeable a => SBool -> a -> a -> a
ite (SA -> SBool
p SA
x) (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
p SList A
xs) ((SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
p SList A
xs) SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ (SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
p SList A
ys
                            SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SList A -> SList A -> SList A
forall a. Mergeable a => SBool -> a -> a -> a
ite (SA -> SBool
p SA
x) (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
p SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ (SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
p SList A
ys) ((SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
p SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ (SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
p SList A
ys)  SList A -> Proof -> ProofStep (SList A)
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
ih
                            ProofStep (SList A)
-> ChainsTo (ProofStep (SList A)) -> ChainsTo (ProofStep (SList A))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SList A -> SList A -> SList A
forall a. Mergeable a => SBool -> a -> a -> a
ite (SA -> SBool
p SA
x) (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
p (SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys)) ((SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
p (SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys))
                            SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
p (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys))
                            SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
p ((SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs) SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys)
                            SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep (SList A)]
ChainsTo (SList A)
forall a. [ProofStep a]
qed

-- | @filter p (concat xss) == concatMap (filter p xss)@
--
-- Similar to the book-keeping law, we cannot express this in SBV directly, since it involves a nested lambda.
-- @concatMap (filter p)@ maps a higher-order function @filter p@, which itself has a nested lambda. So, we use
-- our own merged definition. Hopefully we'll relax this as SMTLib gains more higher order features.
--
-- We have:
--
-- >>> filterConcat
-- Inductive lemma: filterAppend
--   Base: filterAppend.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.
--   Step: filterAppend.Step               Q.E.D.
-- Inductive lemma: filterConcat
--   Base: filterConcat.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: filterConcat.Step               Q.E.D.
-- [Proven] filterConcat
filterConcat :: IO Proof
filterConcat :: IO Proof
filterConcat = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do
  let -- For an arbitrary uninterpreted prediate 'p':
      p :: SA -> SBool
      p :: SA -> SBool
p = String -> SA -> SBool
forall a. SMTDefinable a => String -> a
uninterpret String
"p"

      -- Fuse concatMap (filter p) in the theorem to avoid nested lambdas. See above note
      concatMapFilter :: (SA -> SBool) -> SList [A] -> SList A
      concatMapFilter :: (SA -> SBool) -> SList [A] -> SList A
concatMapFilter SA -> SBool
pred = String -> (SList [A] -> SList A) -> SList [A] -> SList A
forall a. (SMTDefinable a, Lambda Symbolic a) => String -> a -> a
smtFunction String
"concatMapFilter" ((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)
                                                                        SList A
forall a. SymVal a => SList a
nil
                                                                        ((SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
pred (SList [A] -> SList A
forall a. SymVal a => SList a -> SBV a
head SList [A]
xs) SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ (SA -> SBool) -> SList [A] -> SList A
concatMapFilter SA -> SBool
pred (SList [A] -> SList [A]
forall a. SymVal a => SList a -> SList a
tail SList [A]
xs))


  fa <- IO Proof -> KD Proof
use (IO Proof -> KD Proof) -> IO Proof -> KD Proof
forall a b. (a -> b) -> a -> b
$ (SA -> SBool) -> IO Proof
filterAppend SA -> SBool
p

  induct "filterConcat"
         (\(Forall @"xss" SList [A]
xss) -> (SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
p (SList [A] -> SList A
forall a. SymVal a => SList [a] -> SList a
concat SList [A]
xss) SList A -> SList A -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SA -> SBool) -> SList [A] -> SList A
concatMapFilter SA -> SBool
p SList [A]
xss) $
         \Proof
ih SList A
xs SList [A]
xss -> [] [SBool] -> [ProofStep (SList A)] -> (SBool, [ProofStep (SList A)])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- (SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
p (SList [A] -> SList A
forall a. SymVal a => SList [a] -> SList a
concat (SList A
xs SList A -> SList [A] -> SList [A]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList [A]
xss))
                          SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
p (SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList [A] -> SList A
forall a. SymVal a => SList [a] -> SList a
concat SList [A]
xss)           SList A -> Proof -> ProofStep (SList A)
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
fa
                          ProofStep (SList A)
-> ChainsTo (ProofStep (SList A)) -> ChainsTo (ProofStep (SList A))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
p SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ (SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
p (SList [A] -> SList A
forall a. SymVal a => SList [a] -> SList a
concat SList [A]
xss)  SList A -> Proof -> ProofStep (SList A)
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
ih
                          ProofStep (SList A)
-> ChainsTo (ProofStep (SList A)) -> ChainsTo (ProofStep (SList A))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
p SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ (SA -> SBool) -> SList [A] -> SList A
concatMapFilter SA -> SBool
p SList [A]
xss
                          SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SBool) -> SList [A] -> SList A
concatMapFilter SA -> SBool
p (SList A
xs SList A -> SList [A] -> SList [A]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList [A]
xss)
                          SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep (SList A)]
ChainsTo (SList A)
forall a. [ProofStep a]
qed

-- * Map and filter don't commute

-- | In general, mapping and filtering operations do not commute. We'll see the kind of counter-example we get from SBV if
-- we attempt to prove:
--
-- >>> mapFilter `catch` (\(_ :: SomeException) -> pure ())
-- Lemma: badMapFilter
-- *** Failed to prove badMapFilter.
-- Falsifiable. Counter-example:
--   xs  = [A_3] :: [A]
--   lhs = [A_0] :: [A]
--   rhs =    [] :: [A]
-- <BLANKLINE>
--   f :: A -> A
--   f _ = A_0
-- <BLANKLINE>
--   p :: A -> Bool
--   p A_3 = True
--   p _   = False
--
-- As expected, the function @f@ maps everything to @A_0@, and the predicate @p@ only lets @A_3@ through. As shown in the
-- counter-example, for the input @[A_3]@, left-hand-side filters nothing and the result is the singleton @A_0@. But the
-- map on the right-hand side maps everything to @[A_0]@ and the filter gets rid of the elements, resulting in an empty list.
mapFilter :: IO ()
mapFilter :: IO ()
mapFilter = KD () -> IO ()
forall a. KD a -> IO a
runKD (KD () -> IO ()) -> KD () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
   let f :: SA -> SA
       f :: SA -> SA
f = String -> SA -> SA
forall a. SMTDefinable a => String -> a
uninterpret String
"f"

       p :: SA -> SBool
       p :: SA -> SBool
p = String -> SA -> SBool
forall a. SMTDefinable a => String -> a
uninterpret String
"p"

   KD Proof -> KD ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (KD Proof -> KD ()) -> KD Proof -> KD ()
forall a b. (a -> b) -> a -> b
$ String -> (Forall "xs" [A] -> SBool) -> [Proof] -> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"badMapFilter"
                (\(Forall @"xs" SList A
xs) -> String -> SList A -> SList A
forall a. SymVal a => String -> SBV a -> SBV a
observe String
"lhs" ((SA -> SA) -> SList A -> SList A
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SA
f ((SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
p SList A
xs)) SList A -> SList A -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== String -> SList A -> SList A
forall a. SymVal a => String -> SBV a -> SBV a
observe String
"rhs" ((SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
p ((SA -> SA) -> SList A -> SList A
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SA
f SList A
xs)))
                []

-- * Partition

-- | @fst (partition f xs) == filter f xs@
--
-- >>> partition1
-- Inductive lemma: partition1
--   Base: partition1.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: partition1.Step                 Q.E.D.
-- [Proven] partition1
partition1 :: IO Proof
partition1 :: IO Proof
partition1 = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do
   let f :: SA -> SBool
       f :: SA -> SBool
f = String -> SA -> SBool
forall a. SMTDefinable a => String -> a
uninterpret String
"f"

   String
-> (Forall "xs" [A] -> SBool)
-> (Proof -> SA -> SList A -> (SBool, [ProofStep (SList A)]))
-> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
String -> a -> (Proof -> steps) -> KD Proof
induct String
"partition1"
          (\(Forall @"xs" SList A
xs) -> STuple [A] [A] -> SList A
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst ((SA -> SBool) -> SList A -> STuple [A] [A]
forall a. SymVal a => (SBV a -> SBool) -> SList a -> STuple [a] [a]
partition SA -> SBool
f SList A
xs) SList A -> SList A -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
f SList A
xs) ((Proof -> SA -> SList A -> (SBool, [ProofStep (SList A)]))
 -> KD Proof)
-> (Proof -> SA -> SList A -> (SBool, [ProofStep (SList A)]))
-> KD Proof
forall a b. (a -> b) -> a -> b
$
          \Proof
ih SA
x SList A
xs -> [] [SBool] -> [ProofStep (SList A)] -> (SBool, [ProofStep (SList A)])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- STuple [A] [A] -> SList A
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst ((SA -> SBool) -> SList A -> STuple [A] [A]
forall a. SymVal a => (SBV a -> SBool) -> SList a -> STuple [a] [a]
partition SA -> SBool
f (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs))
                         SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: STuple [A] [A] -> SList A
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst (let res :: STuple [A] [A]
res = (SA -> SBool) -> SList A -> STuple [A] [A]
forall a. SymVal a => (SBV a -> SBool) -> SList a -> STuple [a] [a]
partition SA -> SBool
f SList A
xs
                                 in SBool -> STuple [A] [A] -> STuple [A] [A] -> STuple [A] [A]
forall a. Mergeable a => SBool -> a -> a -> a
ite (SA -> SBool
f SA
x)
                                        ((SList A, SList A) -> STuple [A] [A]
forall tup a. Tuple tup a => a -> SBV tup
tuple (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: STuple [A] [A] -> SList A
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst STuple [A] [A]
res, STuple [A] [A] -> SList A
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd STuple [A] [A]
res))
                                        ((SList A, SList A) -> STuple [A] [A]
forall tup a. Tuple tup a => a -> SBV tup
tuple (STuple [A] [A] -> SList A
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst STuple [A] [A]
res, SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: STuple [A] [A] -> SList A
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd STuple [A] [A]
res)))
                         SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SList A -> SList A -> SList A
forall a. Mergeable a => SBool -> a -> a -> a
ite (SA -> SBool
f SA
x) (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: STuple [A] [A] -> SList A
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst ((SA -> SBool) -> SList A -> STuple [A] [A]
forall a. SymVal a => (SBV a -> SBool) -> SList a -> STuple [a] [a]
partition SA -> SBool
f SList A
xs)) (STuple [A] [A] -> SList A
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst ((SA -> SBool) -> SList A -> STuple [A] [A]
forall a. SymVal a => (SBV a -> SBool) -> SList a -> STuple [a] [a]
partition SA -> SBool
f SList A
xs)) SList A -> Proof -> ProofStep (SList A)
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
ih
                         ProofStep (SList A)
-> ChainsTo (ProofStep (SList A)) -> ChainsTo (ProofStep (SList A))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SList A -> SList A -> SList A
forall a. Mergeable a => SBool -> a -> a -> a
ite (SA -> SBool
f SA
x) (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
f SList A
xs) ((SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
f SList A
xs)
                         SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SA -> SBool
f (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs)
                         SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep (SList A)]
ChainsTo (SList A)
forall a. [ProofStep a]
qed

-- | @snd (partition f xs) == filter (not . f) xs@
--
-- >>> partition2
-- Inductive lemma: partition2
--   Base: partition2.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: partition2.Step                 Q.E.D.
-- [Proven] partition2
partition2 :: IO Proof
partition2 :: IO Proof
partition2 = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do
   let f :: SA -> SBool
       f :: SA -> SBool
f = String -> SA -> SBool
forall a. SMTDefinable a => String -> a
uninterpret String
"f"

   String
-> (Forall "xs" [A] -> SBool)
-> (Proof -> SA -> SList A -> (SBool, [ProofStep (SList A)]))
-> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
String -> a -> (Proof -> steps) -> KD Proof
induct String
"partition2"
          (\(Forall @"xs" SList A
xs) -> STuple [A] [A] -> SList A
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd ((SA -> SBool) -> SList A -> STuple [A] [A]
forall a. SymVal a => (SBV a -> SBool) -> SList a -> STuple [a] [a]
partition SA -> SBool
f SList A
xs) SList A -> SList A -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter (SBool -> SBool
sNot (SBool -> SBool) -> (SA -> SBool) -> SA -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SA -> SBool
f) SList A
xs) ((Proof -> SA -> SList A -> (SBool, [ProofStep (SList A)]))
 -> KD Proof)
-> (Proof -> SA -> SList A -> (SBool, [ProofStep (SList A)]))
-> KD Proof
forall a b. (a -> b) -> a -> b
$
          \Proof
ih SA
x SList A
xs -> [] [SBool] -> [ProofStep (SList A)] -> (SBool, [ProofStep (SList A)])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- STuple [A] [A] -> SList A
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd ((SA -> SBool) -> SList A -> STuple [A] [A]
forall a. SymVal a => (SBV a -> SBool) -> SList a -> STuple [a] [a]
partition SA -> SBool
f (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs))
                         SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: STuple [A] [A] -> SList A
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd (let res :: STuple [A] [A]
res = (SA -> SBool) -> SList A -> STuple [A] [A]
forall a. SymVal a => (SBV a -> SBool) -> SList a -> STuple [a] [a]
partition SA -> SBool
f SList A
xs
                                 in SBool -> STuple [A] [A] -> STuple [A] [A] -> STuple [A] [A]
forall a. Mergeable a => SBool -> a -> a -> a
ite (SA -> SBool
f SA
x)
                                        ((SList A, SList A) -> STuple [A] [A]
forall tup a. Tuple tup a => a -> SBV tup
tuple (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: STuple [A] [A] -> SList A
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst STuple [A] [A]
res, STuple [A] [A] -> SList A
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd STuple [A] [A]
res))
                                        ((SList A, SList A) -> STuple [A] [A]
forall tup a. Tuple tup a => a -> SBV tup
tuple (STuple [A] [A] -> SList A
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst STuple [A] [A]
res, SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: STuple [A] [A] -> SList A
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd STuple [A] [A]
res)))
                         SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SList A -> SList A -> SList A
forall a. Mergeable a => SBool -> a -> a -> a
ite (SA -> SBool
f SA
x) (STuple [A] [A] -> SList A
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd ((SA -> SBool) -> SList A -> STuple [A] [A]
forall a. SymVal a => (SBV a -> SBool) -> SList a -> STuple [a] [a]
partition SA -> SBool
f SList A
xs)) (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: STuple [A] [A] -> SList A
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd ((SA -> SBool) -> SList A -> STuple [A] [A]
forall a. SymVal a => (SBV a -> SBool) -> SList a -> STuple [a] [a]
partition SA -> SBool
f SList A
xs)) SList A -> Proof -> ProofStep (SList A)
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
ih
                         ProofStep (SList A)
-> ChainsTo (ProofStep (SList A)) -> ChainsTo (ProofStep (SList A))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SList A -> SList A -> SList A
forall a. Mergeable a => SBool -> a -> a -> a
ite (SA -> SBool
f SA
x) ((SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter (SBool -> SBool
sNot (SBool -> SBool) -> (SA -> SBool) -> SA -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SA -> SBool
f) SList A
xs) (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter (SBool -> SBool
sNot (SBool -> SBool) -> (SA -> SBool) -> SA -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SA -> SBool
f) SList A
xs)
                         SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SBool) -> SList A -> SList A
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter (SBool -> SBool
sNot (SBool -> SBool) -> (SA -> SBool) -> SA -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SA -> SBool
f) (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs)
                         SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep (SList A)]
ChainsTo (SList A)
forall a. [ProofStep a]
qed

-- * Take and drop

-- | @take n (take m xs) = take (n `smin` m) xs@
--
-- >>> take_take
-- Lemma: take_take                        Q.E.D.
-- [Proven] take_take
take_take :: IO Proof
take_take :: IO Proof
take_take = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$
   String
-> (Forall "xs" [A]
    -> Forall "m" Integer -> Forall "n" Integer -> SBool)
-> [Proof]
-> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"take_take"
         (\(Forall @"xs" (SList A
xs :: SList A)) (Forall @"m" SInteger
m) (Forall @"n" SInteger
n) -> SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
n (SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
m SList A
xs) SList A -> SList A -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
take (SInteger
n SInteger -> SInteger -> SInteger
forall a. OrdSymbolic a => a -> a -> a
`smin` SInteger
m) SList A
xs)
         []


-- | @n >= 0 && m >= 0 => drop n (drop m xs) = drop (n + m) xs@
--
-- >>> drop_drop
-- Lemma: drop_drop                        Q.E.D.
-- [Proven] drop_drop
drop_drop :: IO Proof
drop_drop :: IO Proof
drop_drop = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$
   String
-> (Forall "n" Integer
    -> Forall "m" Integer -> Forall "xs" [A] -> SBool)
-> [Proof]
-> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"drop_drop"
          (\(Forall @"n" SInteger
n) (Forall @"m" SInteger
m) (Forall @"xs" (SList A
xs :: SList A)) ->
                SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.&& SInteger
m SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
n (SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
m SList A
xs) SList A -> SList A -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
drop (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
m) SList A
xs)
          []

-- | @take n xs ++ drop n xs == xs@
--
-- >>> take_drop
-- Lemma: take_drop                        Q.E.D.
-- [Proven] take_drop
take_drop :: IO Proof
take_drop :: IO Proof
take_drop = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$
    String
-> (Forall "n" Integer -> Forall "xs" [A] -> SBool)
-> [Proof]
-> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"take_drop"
           (\(Forall @"n" SInteger
n) (Forall @"xs" (SList A
xs :: SList A)) -> SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
n SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
n SList A
xs SList A -> SList A -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList A
xs)
           []

-- | @n .> 0 => take n (x .: xs) = x .: take (n - 1) xs@
--
-- >>> take_cons
-- Lemma: take_cons                        Q.E.D.
-- [Proven] take_cons
take_cons :: IO Proof
take_cons :: IO Proof
take_cons = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$
   String
-> (Forall "n" Integer -> Forall "x" A -> Forall "xs" [A] -> SBool)
-> [Proof]
-> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"take_cons"
         (\(Forall @"n" SInteger
n) (Forall @"x" SA
x) (Forall @"xs" (SList A
xs :: SList A)) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
n (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs) SList A -> SList A -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
take (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) SList A
xs)
         []

-- | @take n (map f xs) == map f (take n xs)@
--
-- >>> take_map
-- Lemma: take_cons                        Q.E.D.
-- Lemma: map1                             Q.E.D.
-- Lemma: take_map.n <= 0                  Q.E.D.
-- Inductive lemma: take_map.n > 0
--   Base: take_map.n > 0.Base             Q.E.D.
--   Step: 1                               Q.E.D.
--   Asms: 2                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Asms: 5                               Q.E.D.
--   Step: 5                               Q.E.D.
--   Step: take_map.n > 0.Step             Q.E.D.
-- Lemma: take_map                         Q.E.D.
-- [Proven] take_map
take_map :: IO Proof
take_map :: IO Proof
take_map = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do
    let f :: SA -> SB
        f :: SA -> SB
f = String -> SA -> SB
forall a. SMTDefinable a => String -> a
uninterpret String
"f"

    tc   <- IO Proof -> KD Proof
use IO Proof
take_cons
    map1 <- lemma "map1" (\(Forall @"x" SA
x) (Forall @"xs" SList A
xs) -> (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs) SList B -> SList B -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SA -> SB
f SA
x SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f SList A
xs) []

    h1 <- lemma "take_map.n <= 0"
                 (\(Forall @"xs" SList A
xs) (Forall @"n" SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SList B -> SList B
forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
n ((SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f SList A
xs) SList B -> SList B -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
n SList A
xs))
                 []

    h2 <- induct "take_map.n > 0"
                 (\(Forall @"xs" SList A
xs) (Forall @"n" SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SList B -> SList B
forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
n ((SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f SList A
xs) SList B -> SList B -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
n SList A
xs)) $
                 \Proof
ih SA
x SList A
xs SInteger
n -> [SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0] [SBool] -> [ProofStep (SList B)] -> (SBool, [ProofStep (SList B)])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- SInteger -> SList B -> SList B
forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
n ((SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs))
                                        SList B -> ChainsTo (SList B) -> ChainsTo (SList B)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SList B -> SList B
forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
n (SA -> SB
f SA
x SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f SList A
xs)       SList B -> SBool -> ProofStep (SList B)
forall a b. ProofHint a b => a -> b -> ProofStep a
?? SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0
                                        ProofStep (SList B)
-> ChainsTo (ProofStep (SList B)) -> ChainsTo (ProofStep (SList B))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SA -> SB
f SA
x SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger -> SList B -> SList B
forall a. SymVal a => SInteger -> SList a -> SList a
take (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) ((SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f SList A
xs) SList B -> Proof -> ProofStep (SList B)
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
ih   Proof -> Inst "n" Integer -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1)
                                        ProofStep (SList B)
-> ChainsTo (ProofStep (SList B)) -> ChainsTo (ProofStep (SList B))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SA -> SB
f SA
x SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
take (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) SList A
xs) SList B -> Proof -> ProofStep (SList B)
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
map1 Proof -> (Inst "x" A, Inst "xs" [A]) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SA
x, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" (SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
take (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) SList A
xs))
                                        ProofStep (SList B)
-> ChainsTo (ProofStep (SList B)) -> ChainsTo (ProofStep (SList B))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
take (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) SList A
xs)   SList B -> [Helper] -> ProofStep (SList B)
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [SBool -> Helper
hyp (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0), Proof -> Helper
hprf Proof
tc]
                                        ProofStep (SList B)
-> ChainsTo (ProofStep (SList B)) -> ChainsTo (ProofStep (SList B))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
n (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs))
                                        SList B -> ChainsTo (SList B) -> ChainsTo (SList B)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep (SList B)]
ChainsTo (SList B)
forall a. [ProofStep a]
qed

    lemma "take_map" (\(Forall @"xs" SList A
xs) (Forall @"n" SInteger
n) -> SInteger -> SList B -> SList B
forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
n ((SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f SList A
xs) SList B -> SList B -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
n SList A
xs)) [h1, h2]

-- | @n .> 0 => drop n (x .: xs) = drop (n - 1) xs@
--
-- >>> drop_cons (Proxy @A)
-- Lemma: drop_cons                        Q.E.D.
-- [Proven] drop_cons
drop_cons :: forall elt. SymVal elt => Proxy elt -> IO Proof
drop_cons :: forall elt. SymVal elt => Proxy elt -> IO Proof
drop_cons Proxy elt
_ = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$
   String
-> (Forall "n" Integer
    -> Forall "x" elt -> Forall "xs" [elt] -> SBool)
-> [Proof]
-> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"drop_cons"
         (\(Forall @"n" SInteger
n) (Forall @"x" SBV elt
x) (Forall @"xs" (SList elt
xs :: SList elt)) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SList elt -> SList elt
forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
n (SBV elt
x SBV elt -> SList elt -> SList elt
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList elt
xs) SList elt -> SList elt -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SList elt -> SList elt
forall a. SymVal a => SInteger -> SList a -> SList a
drop (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) SList elt
xs)
         []

-- | @drop n (map f xs) == map f (drop n xs)@
--
-- >>> drop_map
-- Lemma: drop_cons                        Q.E.D.
-- Lemma: drop_cons                        Q.E.D.
-- Lemma: drop_map.n <= 0                  Q.E.D.
-- Inductive lemma: drop_map.n > 0
--   Base: drop_map.n > 0.Base             Q.E.D.
--   Step: 1                               Q.E.D.
--   Asms: 2                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Asms: 3                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Asms: 4                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Step: drop_map.n > 0.Step             Q.E.D.
-- Lemma: drop_map
--   Step  : 1                             Q.E.D.
--   Step  : 2                             Q.E.D.
--   Step  : 3                             Q.E.D.
--   Step  : 4                             Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] drop_map
drop_map :: IO Proof
drop_map :: IO Proof
drop_map = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do
   let f :: SA -> SB
       f :: SA -> SB
f = String -> SA -> SB
forall a. SMTDefinable a => String -> a
uninterpret String
"f"

   dcA <- IO Proof -> KD Proof
use (IO Proof -> KD Proof) -> IO Proof -> KD Proof
forall a b. (a -> b) -> a -> b
$ Proxy A -> IO Proof
forall elt. SymVal elt => Proxy elt -> IO Proof
drop_cons (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @A)
   dcB <- use $ drop_cons (Proxy @B)

   h1 <- lemma "drop_map.n <= 0"
               (\(Forall @"xs" SList A
xs) (Forall @"n" SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SList B -> SList B
forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
n ((SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f SList A
xs) SList B -> SList B -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
n SList A
xs))
               []

   h2 <- induct "drop_map.n > 0"
                (\(Forall @"xs" SList A
xs) (Forall @"n" SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SList B -> SList B
forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
n ((SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f SList A
xs) SList B -> SList B -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
n SList A
xs)) $
                \Proof
ih SA
x SList A
xs SInteger
n -> [SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0] [SBool] -> [ProofStep (SList B)] -> (SBool, [ProofStep (SList B)])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- SInteger -> SList B -> SList B
forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
n ((SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs))
                                       SList B -> ChainsTo (SList B) -> ChainsTo (SList B)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SList B -> SList B
forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
n (SA -> SB
f SA
x SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f SList A
xs)
                                       SList B -> [Helper] -> ProofStep (SList B)
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [SBool -> Helper
hyp (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0), Proof -> Helper
hprf (Proof
dcB Proof -> (Inst "n" Integer, Inst "x" B, Inst "xs" [B]) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SInteger
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" (SA -> SB
f SA
x), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" ((SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f SList A
xs)))]
                                       ProofStep (SList B)
-> ChainsTo (ProofStep (SList B)) -> ChainsTo (ProofStep (SList B))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SList B -> SList B
forall a. SymVal a => SInteger -> SList a -> SList a
drop (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) ((SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f SList A
xs)
                                       SList B -> [Helper] -> ProofStep (SList B)
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [SBool -> Helper
hyp (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0), Proof -> Helper
hprf (Proof
ih Proof -> Inst "n" Integer -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1))]
                                       ProofStep (SList B)
-> ChainsTo (ProofStep (SList B)) -> ChainsTo (ProofStep (SList B))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
drop (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) SList A
xs)
                                       SList B -> [Helper] -> ProofStep (SList B)
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [SBool -> Helper
hyp (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0), Proof -> Helper
hprf (Proof
dcA Proof -> (Inst "n" Integer, Inst "x" A, Inst "xs" [A]) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SInteger
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SA
x, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList A
xs))]
                                       ProofStep (SList B)
-> ChainsTo (ProofStep (SList B)) -> ChainsTo (ProofStep (SList B))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
n (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs))
                                       SList B -> ChainsTo (SList B) -> ChainsTo (SList B)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep (SList B)]
ChainsTo (SList B)
forall a. [ProofStep a]
qed

   -- I'm a bit surprised that z3 can't deduce the following with a simple-lemma, which is essentially a simple case-split.
   -- But the good thing about calc is that it lets us direct the tool in precise ways that we'd like.
   calc "drop_map"
        (\(Forall @"xs" SList A
xs) (Forall @"n" SInteger
n) -> SInteger -> SList B -> SList B
forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
n ((SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f SList A
xs) SList B -> SList B -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
n SList A
xs)) $
        \SList A
xs SInteger
n -> [] [SBool] -> [ProofStep SBool] -> (SBool, [ProofStep SBool])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- let result :: SBool
result = SInteger -> SList B -> SList B
forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
n ((SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f SList A
xs) SList B -> SList B -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SA -> SB) -> SList A -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SA -> SB
f (SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
n SList A
xs)
                    in SBool
result
                    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 (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0) (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0 SBool -> SBool -> SBool
.=> SBool
result) (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0 SBool -> SBool -> SBool
.=> SBool
result) SBool -> Proof -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
h1
                    ProofStep SBool
-> ChainsTo (ProofStep SBool) -> ChainsTo (ProofStep 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 (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0) SBool
sTrue                (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0 SBool -> SBool -> SBool
.=> SBool
result) SBool -> Proof -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
h2
                    ProofStep SBool
-> ChainsTo (ProofStep SBool) -> ChainsTo (ProofStep 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 (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0) SBool
sTrue                SBool
sTrue
                    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
=: [ProofStep SBool]
ChainsTo SBool
forall a. [ProofStep a]
qed

-- | @n >= 0 ==> length (take n xs) = length xs \`min\` n@
--
-- >>> length_take
-- Lemma: length_take                      Q.E.D.
-- [Proven] length_take
length_take :: IO Proof
length_take :: IO Proof
length_take = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$
     String
-> (Forall "n" Integer -> Forall "xs" [A] -> SBool)
-> [Proof]
-> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"length_take"
           (\(Forall @"n" SInteger
n) (Forall @"xs" (SList A
xs :: SList A)) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
n SList A
xs) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList A
xs SInteger -> SInteger -> SInteger
forall a. OrdSymbolic a => a -> a -> a
`smin` SInteger
n)
           []

-- | @n >= 0 ==> length (drop n xs) = (length xs - n) \`max\` 0@
--
-- >>> length_drop
-- Lemma: length_drop                      Q.E.D.
-- [Proven] length_drop
length_drop :: IO Proof
length_drop :: IO Proof
length_drop = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$
     String
-> (Forall "n" Integer -> Forall "xs" [A] -> SBool)
-> [Proof]
-> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"length_drop"
           (\(Forall @"n" SInteger
n) (Forall @"xs" (SList A
xs :: SList A)) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
n SList A
xs) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList A
xs SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
n) SInteger -> SInteger -> SInteger
forall a. OrdSymbolic a => a -> a -> a
`smax` SInteger
0)
           []

-- | @length xs \<= n ==\> take n xs == xs@
--
-- >>> take_all
-- Lemma: take_all                         Q.E.D.
-- [Proven] take_all
take_all :: IO Proof
take_all :: IO Proof
take_all = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$
    String
-> (Forall "n" Integer -> Forall "xs" [A] -> SBool)
-> [Proof]
-> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"take_all"
          (\(Forall @"n" SInteger
n) (Forall @"xs" (SList A
xs :: SList A)) -> SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList A
xs SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
n SBool -> SBool -> SBool
.=> SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
n SList A
xs SList A -> SList A -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList A
xs)
          []

-- | @length xs \<= n ==\> drop n xs == nil@
--
-- >>> drop_all
-- Lemma: drop_all                         Q.E.D.
-- [Proven] drop_all
drop_all :: IO Proof
drop_all :: IO Proof
drop_all = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$
    String
-> (Forall "n" Integer -> Forall "xs" [A] -> SBool)
-> [Proof]
-> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"drop_all"
          (\(Forall @"n" SInteger
n) (Forall @"xs" (SList A
xs :: SList A)) -> SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList A
xs SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
n SBool -> SBool -> SBool
.=> SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
n SList A
xs SList A -> SList A -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList A
forall a. SymVal a => SList a
nil)
          []

-- | @take n (xs ++ ys) = (take n xs ++ take (n - length xs) ys)@
--
-- >>> take_append
-- Lemma: take_append
--   Step  : 1                             Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] take_append
take_append :: IO Proof
take_append :: IO Proof
take_append = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$
    String
-> (Forall "n" Integer
    -> Forall "xs" [A] -> Forall "ys" [A] -> SBool)
-> (SInteger
    -> SList A -> SList A -> (SBool, [ProofStep (SList A)]))
-> KD Proof
forall a steps.
(CalcLemma a steps, Proposition a) =>
String -> a -> steps -> KD Proof
calc String
"take_append"
         (\(Forall @"n" SInteger
n) (Forall @"xs" (SList A
xs :: SList A)) (Forall @"ys" SList A
ys) -> SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
n (SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys) SList A -> SList A -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
n SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
take (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList A
xs) SList A
ys) ((SInteger -> SList A -> SList A -> (SBool, [ProofStep (SList A)]))
 -> KD Proof)
-> (SInteger
    -> SList A -> SList A -> (SBool, [ProofStep (SList A)]))
-> KD Proof
forall a b. (a -> b) -> a -> b
$

         -- z3 requires an explicit split here on xs. cvc5 actually proves this out-of-the-box without any helping steps.
         \SInteger
n (SList A
xs :: SList A) SList A
ys -> [] [SBool] -> [ProofStep (SList A)] -> (SBool, [ProofStep (SList A)])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
n (SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys)
                                     SList A -> String -> ProofStep (SList A)
forall a b. ProofHint a b => a -> b -> ProofStep a
?? String
"case split on xs"
                                     ProofStep (SList A)
-> ChainsTo (ProofStep (SList A)) -> ChainsTo (ProofStep (SList A))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: 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)
                                            (SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
n SList A
ys)
                                            (SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
n (SList A -> SA
forall a. SymVal a => SList a -> SBV a
head SList A
xs SA -> 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
tail SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys)))
                                     SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep (SList A)]
ChainsTo (SList A)
forall a. [ProofStep a]
qed

-- | @drop n (xs ++ ys) = drop n xs ++ drop (n - length xs) ys@
--
-- NB. As of Feb 2025, z3 struggles to prove this, but cvc5 gets it out-of-the-box.
--
-- >>> drop_append
-- Lemma: drop_append                      Q.E.D.
-- [Proven] drop_append
drop_append :: IO Proof
drop_append :: IO Proof
drop_append = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$
    SMTConfig
-> String
-> (Forall "n" Integer
    -> Forall "xs" [A] -> Forall "ys" [A] -> SBool)
-> [Proof]
-> KD Proof
forall a.
Proposition a =>
SMTConfig -> String -> a -> [Proof] -> KD Proof
lemmaWith SMTConfig
cvc5 String
"drop_append"
                   (\(Forall @"n" SInteger
n) (Forall @"xs" (SList A
xs :: SList A)) (Forall @"ys" SList A
ys) -> SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
n (SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SList A
ys) SList A -> SList A -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
n SList A
xs SList A -> SList A -> SList A
forall a. SymVal a => SList a -> SList a -> SList a
++ SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
drop (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList A
xs) SList A
ys)
                   []

-- * Summing via halving

-- | We prove that summing a list can be done by halving the list, summing parts, and adding the results. The proof uses
-- strong induction. We have:
--
-- >>> sumHalves
-- Inductive lemma: sumAppend
--   Base: sumAppend.Base                  Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: sumAppend.Step                  Q.E.D.
-- Inductive lemma (strong): sumHalves
--   Base: sumHalves.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.
--   Step: sumHalves.Step                  Q.E.D.
-- [Proven] sumHalves
sumHalves :: IO Proof
sumHalves :: IO Proof
sumHalves = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do

    let halvingSum :: SList Integer -> SInteger
        halvingSum :: SList Integer -> SInteger
halvingSum = String -> (SList Integer -> SInteger) -> SList Integer -> SInteger
forall a. (SMTDefinable a, Lambda Symbolic a) => String -> a -> a
smtFunction String
"halvingSum" ((SList Integer -> SInteger) -> SList Integer -> SInteger)
-> (SList Integer -> SInteger) -> SList Integer -> SInteger
forall a b. (a -> b) -> a -> b
$ \SList Integer
xs -> SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList Integer -> SBool
forall a. SymVal a => SList a -> SBool
null SList Integer
xs SBool -> SBool -> SBool
.|| SList Integer -> SBool
forall a. SymVal a => SList a -> SBool
null (SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a
tail SList Integer
xs))
                                                           (SList Integer -> SInteger
sum SList Integer
xs)
                                                           (let (SList Integer
f, SList Integer
s) = SInteger -> SList Integer -> (SList Integer, SList Integer)
forall a. SymVal a => SInteger -> SList a -> (SList a, SList a)
splitAt (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
xs SInteger -> SInteger -> SInteger
forall a. SDivisible a => a -> a -> a
`sDiv` SInteger
2) SList Integer
xs
                                                            in SList Integer -> SInteger
halvingSum SList Integer
f SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
halvingSum SList Integer
s)

        sum :: SList Integer -> SInteger
        sum :: SList Integer -> SInteger
sum = String -> (SList Integer -> SInteger) -> SList Integer -> SInteger
forall a. (SMTDefinable a, Lambda Symbolic a) => String -> a -> a
smtFunction String
"sum" ((SList Integer -> SInteger) -> SList Integer -> SInteger)
-> (SList Integer -> SInteger) -> SList Integer -> SInteger
forall a b. (a -> b) -> a -> b
$ \SList Integer
xs -> SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList Integer -> SBool
forall a. SymVal a => SList a -> SBool
null SList Integer
xs) SInteger
0 (SList Integer -> SInteger
forall a. SymVal a => SList a -> SBV a
head SList Integer
xs SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
sum (SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a
tail SList Integer
xs))

    helper <- String
-> (Forall "xs" [Integer] -> Forall "ys" [Integer] -> SBool)
-> (Proof
    -> SInteger
    -> SList Integer
    -> SList Integer
    -> (SBool, [ProofStep SInteger]))
-> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
String -> a -> (Proof -> steps) -> KD Proof
induct String
"sumAppend"
                     (\(Forall @"xs" SList Integer
xs) (Forall @"ys" SList Integer
ys) -> SList Integer -> SInteger
sum (SList Integer
xs SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
ys) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList Integer -> SInteger
sum SList Integer
xs SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
sum SList Integer
ys) ((Proof
  -> SInteger
  -> SList Integer
  -> SList Integer
  -> (SBool, [ProofStep SInteger]))
 -> KD Proof)
-> (Proof
    -> SInteger
    -> SList Integer
    -> SList Integer
    -> (SBool, [ProofStep SInteger]))
-> KD Proof
forall a b. (a -> b) -> a -> b
$
                     \Proof
ih SInteger
x SList Integer
xs SList Integer
ys -> [] [SBool] -> [ProofStep SInteger] -> (SBool, [ProofStep SInteger])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- SList Integer -> SInteger
sum (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
ys)
                                       SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
sum (SList Integer
xs SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
ys)
                                       SInteger -> Proof -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
ih
                                       ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
sum SList Integer
xs SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
sum SList Integer
ys
                                       SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer -> SInteger
sum (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
sum SList Integer
ys
                                       SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep SInteger]
ChainsTo SInteger
forall a. [ProofStep a]
qed

    -- Use strong induction to prove the theorem. CVC5 solves this with ease, but z3 struggles.
    sInductWith cvc5 "sumHalves"
                (\(Forall @"xs" SList Integer
xs) -> SList Integer -> SInteger
halvingSum SList Integer
xs SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList Integer -> SInteger
sum SList Integer
xs) $
                \Proof
ih SInteger
x SList Integer
xs -> [] [SBool] -> [ProofStep SInteger] -> (SBool, [ProofStep SInteger])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- SList Integer -> SInteger
halvingSum (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs)
                               SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let (SList Integer
f, SList Integer
s) = SInteger -> SList Integer -> (SList Integer, SList Integer)
forall a. SymVal a => SInteger -> SList a -> (SList a, SList a)
splitAt (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) SInteger -> SInteger -> SInteger
forall a. SDivisible a => a -> a -> a
`sDiv` SInteger
2) (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs)
                                  in SList Integer -> SInteger
halvingSum SList Integer
f SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
halvingSum SList Integer
s
                               SInteger -> Proof -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
ih Proof -> Inst "xs" [Integer] -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
f
                               ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer -> SInteger
sum SList Integer
f SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
halvingSum SList Integer
s
                               SInteger -> Proof -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
ih Proof -> Inst "xs" [Integer] -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
s
                               ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer -> SInteger
sum SList Integer
f SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
sum SList Integer
s
                               SInteger -> Proof -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
helper Proof -> (Inst "xs" [Integer], Inst "ys" [Integer]) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
f, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList Integer
s)
                               ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer -> SInteger
sum (SList Integer
f SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
s)
                               SInteger -> String -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? String
"simplify"
                               ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer -> SInteger
sum (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs)
                               SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep SInteger]
ChainsTo SInteger
forall a. [ProofStep a]
qed

-- * Zip

-- | @length xs = length ys ⟹ map fst (zip xs ys) = xs@
--
-- >>> map_fst_zip
-- Inductive lemma: map_fst_zip
--   Base: map_fst_zip.Base                Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Asms: 4                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Step: map_fst_zip.Step                Q.E.D.
-- [Proven] map_fst_zip
map_fst_zip :: IO Proof
map_fst_zip :: IO Proof
map_fst_zip = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$
   String
-> (Forall "xs" [A] -> Forall "ys" [B] -> SBool)
-> (Proof
    -> SA
    -> SList A
    -> SB
    -> SList B
    -> (SBool, [ProofStep (SList A)]))
-> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
String -> a -> (Proof -> steps) -> KD Proof
induct String
"map_fst_zip"
          (\(Forall @"xs" (SList A
xs :: SList A)) (Forall @"ys" (SList B
ys :: SList B)) -> SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList A
xs SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList B -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList B
ys SBool -> SBool -> SBool
.=> (SBV (A, B) -> SA) -> SList (A, B) -> SList A
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SBV (A, B) -> SA
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst (SList A -> SList B -> SList (A, B)
forall a b.
(SymVal a, SymVal b) =>
SList a -> SList b -> SList (a, b)
zip SList A
xs SList B
ys) SList A -> SList A -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList A
xs) ((Proof
  -> SA
  -> SList A
  -> SB
  -> SList B
  -> (SBool, [ProofStep (SList A)]))
 -> KD Proof)
-> (Proof
    -> SA
    -> SList A
    -> SB
    -> SList B
    -> (SBool, [ProofStep (SList A)]))
-> KD Proof
forall a b. (a -> b) -> a -> b
$
          \Proof
ih (SA
x :: SA) SList A
xs (SB
y :: SB) SList B
ys -> [SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList B -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SB
y SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList B
ys)]
                                        [SBool] -> [ProofStep (SList A)] -> (SBool, [ProofStep (SList A)])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- (SBV (A, B) -> SA) -> SList (A, B) -> SList A
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SBV (A, B) -> SA
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst (SList A -> SList B -> SList (A, B)
forall a b.
(SymVal a, SymVal b) =>
SList a -> SList b -> SList (a, b)
zip (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs) (SB
y SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList B
ys))
                                        SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV (A, B) -> SA) -> SList (A, B) -> SList A
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SBV (A, B) -> SA
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst ((SA, SB) -> SBV (A, B)
forall tup a. Tuple tup a => a -> SBV tup
tuple (SA
x, SB
y) SBV (A, B) -> SList (A, B) -> SList (A, B)
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A -> SList B -> SList (A, B)
forall a b.
(SymVal a, SymVal b) =>
SList a -> SList b -> SList (a, b)
zip SList A
xs SList B
ys)
                                        SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV (A, B) -> SA
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst ((SA, SB) -> SBV (A, B)
forall tup a. Tuple tup a => a -> SBV tup
tuple (SA
x, SB
y)) SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SBV (A, B) -> SA) -> SList (A, B) -> SList A
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SBV (A, B) -> SA
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst (SList A -> SList B -> SList (A, B)
forall a b.
(SymVal a, SymVal b) =>
SList a -> SList b -> SList (a, b)
zip SList A
xs SList B
ys)
                                        SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SBV (A, B) -> SA) -> SList (A, B) -> SList A
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SBV (A, B) -> SA
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst (SList A -> SList B -> SList (A, B)
forall a b.
(SymVal a, SymVal b) =>
SList a -> SList b -> SList (a, b)
zip SList A
xs SList B
ys)
                                        SList A -> [Helper] -> ProofStep (SList A)
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [Proof -> Helper
hprf Proof
ih, SBool -> Helper
hyp (SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList A
xs SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList B -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList B
ys)]
                                        ProofStep (SList A)
-> ChainsTo (ProofStep (SList A)) -> ChainsTo (ProofStep (SList A))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs
                                        SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep (SList A)]
ChainsTo (SList A)
forall a. [ProofStep a]
qed

-- | @length xs = length ys ⟹ map snd (zip xs ys) = xs@
--
-- >>> map_snd_zip
-- Inductive lemma: map_snd_zip
--   Base: map_snd_zip.Base                Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Asms: 4                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Step: map_snd_zip.Step                Q.E.D.
-- [Proven] map_snd_zip
map_snd_zip :: IO Proof
map_snd_zip :: IO Proof
map_snd_zip = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$
   String
-> (Forall "xs" [A] -> Forall "ys" [B] -> SBool)
-> (Proof
    -> SA
    -> SList A
    -> SB
    -> SList B
    -> (SBool, [ProofStep (SList B)]))
-> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
String -> a -> (Proof -> steps) -> KD Proof
induct String
"map_snd_zip"
          (\(Forall @"xs" (SList A
xs :: SList A)) (Forall @"ys" (SList B
ys :: SList B)) -> SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList A
xs SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList B -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList B
ys SBool -> SBool -> SBool
.=> (SBV (A, B) -> SB) -> SList (A, B) -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SBV (A, B) -> SB
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd (SList A -> SList B -> SList (A, B)
forall a b.
(SymVal a, SymVal b) =>
SList a -> SList b -> SList (a, b)
zip SList A
xs SList B
ys) SList B -> SList B -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList B
ys) ((Proof
  -> SA
  -> SList A
  -> SB
  -> SList B
  -> (SBool, [ProofStep (SList B)]))
 -> KD Proof)
-> (Proof
    -> SA
    -> SList A
    -> SB
    -> SList B
    -> (SBool, [ProofStep (SList B)]))
-> KD Proof
forall a b. (a -> b) -> a -> b
$
          \Proof
ih (SA
x :: SA) SList A
xs (SB
y :: SB) SList B
ys -> [SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList B -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SB
y SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList B
ys)]
                                        [SBool] -> [ProofStep (SList B)] -> (SBool, [ProofStep (SList B)])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- (SBV (A, B) -> SB) -> SList (A, B) -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SBV (A, B) -> SB
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd (SList A -> SList B -> SList (A, B)
forall a b.
(SymVal a, SymVal b) =>
SList a -> SList b -> SList (a, b)
zip (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs) (SB
y SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList B
ys))
                                        SList B -> ChainsTo (SList B) -> ChainsTo (SList B)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV (A, B) -> SB) -> SList (A, B) -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SBV (A, B) -> SB
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd ((SA, SB) -> SBV (A, B)
forall tup a. Tuple tup a => a -> SBV tup
tuple (SA
x, SB
y) SBV (A, B) -> SList (A, B) -> SList (A, B)
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A -> SList B -> SList (A, B)
forall a b.
(SymVal a, SymVal b) =>
SList a -> SList b -> SList (a, b)
zip SList A
xs SList B
ys)
                                        SList B -> ChainsTo (SList B) -> ChainsTo (SList B)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV (A, B) -> SB
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd ((SA, SB) -> SBV (A, B)
forall tup a. Tuple tup a => a -> SBV tup
tuple (SA
x, SB
y)) SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SBV (A, B) -> SB) -> SList (A, B) -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SBV (A, B) -> SB
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd (SList A -> SList B -> SList (A, B)
forall a b.
(SymVal a, SymVal b) =>
SList a -> SList b -> SList (a, b)
zip SList A
xs SList B
ys)
                                        SList B -> ChainsTo (SList B) -> ChainsTo (SList B)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SB
y SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SBV (A, B) -> SB) -> SList (A, B) -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SBV (A, B) -> SB
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd (SList A -> SList B -> SList (A, B)
forall a b.
(SymVal a, SymVal b) =>
SList a -> SList b -> SList (a, b)
zip SList A
xs SList B
ys)
                                        SList B -> [Helper] -> ProofStep (SList B)
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [Proof -> Helper
hprf Proof
ih, SBool -> Helper
hyp (SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList A
xs SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList B -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList B
ys)]
                                        ProofStep (SList B)
-> ChainsTo (ProofStep (SList B)) -> ChainsTo (ProofStep (SList B))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SB
y SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList B
ys
                                        SList B -> ChainsTo (SList B) -> ChainsTo (SList B)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep (SList B)]
ChainsTo (SList B)
forall a. [ProofStep a]
qed

-- | @map fst (zip xs ys) = take (min (length xs) (length ys)) xs@
--
-- >>> map_fst_zip_take
-- Lemma: take_cons                        Q.E.D.
-- Inductive lemma: map_fst_zip_take
--   Base: map_fst_zip_take.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.
--   Step: map_fst_zip_take.Step           Q.E.D.
-- [Proven] map_fst_zip_take
map_fst_zip_take :: IO Proof
map_fst_zip_take :: IO Proof
map_fst_zip_take = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do
   tc <- IO Proof -> KD Proof
use IO Proof
take_cons

   induct "map_fst_zip_take"
          (\(Forall @"xs" (SList A
xs :: SList A)) (Forall @"ys" (SList B
ys :: SList B)) -> (SBV (A, B) -> SA) -> SList (A, B) -> SList A
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SBV (A, B) -> SA
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst (SList A -> SList B -> SList (A, B)
forall a b.
(SymVal a, SymVal b) =>
SList a -> SList b -> SList (a, b)
zip SList A
xs SList B
ys) SList A -> SList A -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
take (SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList A
xs SInteger -> SInteger -> SInteger
forall a. OrdSymbolic a => a -> a -> a
`smin` SList B -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList B
ys) SList A
xs) $
          \Proof
ih (SA
x :: SA) SList A
xs (SB
y :: SB) SList B
ys -> []
                                        [SBool] -> [ProofStep (SList A)] -> (SBool, [ProofStep (SList A)])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- (SBV (A, B) -> SA) -> SList (A, B) -> SList A
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SBV (A, B) -> SA
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst (SList A -> SList B -> SList (A, B)
forall a b.
(SymVal a, SymVal b) =>
SList a -> SList b -> SList (a, b)
zip (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs) (SB
y SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList B
ys))
                                        SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV (A, B) -> SA) -> SList (A, B) -> SList A
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SBV (A, B) -> SA
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst ((SA, SB) -> SBV (A, B)
forall tup a. Tuple tup a => a -> SBV tup
tuple (SA
x, SB
y) SBV (A, B) -> SList (A, B) -> SList (A, B)
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A -> SList B -> SList (A, B)
forall a b.
(SymVal a, SymVal b) =>
SList a -> SList b -> SList (a, b)
zip SList A
xs SList B
ys)
                                        SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SBV (A, B) -> SA) -> SList (A, B) -> SList A
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SBV (A, B) -> SA
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst (SList A -> SList B -> SList (A, B)
forall a b.
(SymVal a, SymVal b) =>
SList a -> SList b -> SList (a, b)
zip SList A
xs SList B
ys)
                                        SList A -> Proof -> ProofStep (SList A)
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
ih
                                        ProofStep (SList A)
-> ChainsTo (ProofStep (SList A)) -> ChainsTo (ProofStep (SList A))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
take (SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList A
xs SInteger -> SInteger -> SInteger
forall a. OrdSymbolic a => a -> a -> a
`smin` SList B -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList B
ys) SList A
xs
                                        SList A -> Proof -> ProofStep (SList A)
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
tc
                                        ProofStep (SList A)
-> ChainsTo (ProofStep (SList A)) -> ChainsTo (ProofStep (SList A))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
take (SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ (SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList A
xs SInteger -> SInteger -> SInteger
forall a. OrdSymbolic a => a -> a -> a
`smin` SList B -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList B
ys)) (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs)
                                        SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SList A -> SList A
forall a. SymVal a => SInteger -> SList a -> SList a
take (SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs) SInteger -> SInteger -> SInteger
forall a. OrdSymbolic a => a -> a -> a
`smin` SList B -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SB
y SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList B
ys)) (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs)
                                        SList A -> ChainsTo (SList A) -> ChainsTo (SList A)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep (SList A)]
ChainsTo (SList A)
forall a. [ProofStep a]
qed

-- | @map snd (zip xs ys) = take (min (length xs) (length ys)) xs@
--
-- >>> map_snd_zip_take
-- Lemma: take_cons                        Q.E.D.
-- Inductive lemma: map_snd_zip_take
--   Base: map_snd_zip_take.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.
--   Step: map_snd_zip_take.Step           Q.E.D.
-- [Proven] map_snd_zip_take
map_snd_zip_take :: IO Proof
map_snd_zip_take :: IO Proof
map_snd_zip_take = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do
   tc <- IO Proof -> KD Proof
use IO Proof
take_cons

   induct "map_snd_zip_take"
          (\(Forall @"xs" (SList A
xs :: SList A)) (Forall @"ys" (SList B
ys :: SList B)) -> (SBV (A, B) -> SB) -> SList (A, B) -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SBV (A, B) -> SB
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd (SList A -> SList B -> SList (A, B)
forall a b.
(SymVal a, SymVal b) =>
SList a -> SList b -> SList (a, b)
zip SList A
xs SList B
ys) SList B -> SList B -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SList B -> SList B
forall a. SymVal a => SInteger -> SList a -> SList a
take (SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList A
xs SInteger -> SInteger -> SInteger
forall a. OrdSymbolic a => a -> a -> a
`smin` SList B -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList B
ys) SList B
ys) $
          \Proof
ih (SA
x :: SA) SList A
xs (SB
y :: SB) SList B
ys -> []
                                        [SBool] -> [ProofStep (SList B)] -> (SBool, [ProofStep (SList B)])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- (SBV (A, B) -> SB) -> SList (A, B) -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SBV (A, B) -> SB
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd (SList A -> SList B -> SList (A, B)
forall a b.
(SymVal a, SymVal b) =>
SList a -> SList b -> SList (a, b)
zip (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs) (SB
y SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList B
ys))
                                        SList B -> ChainsTo (SList B) -> ChainsTo (SList B)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV (A, B) -> SB) -> SList (A, B) -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SBV (A, B) -> SB
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd ((SA, SB) -> SBV (A, B)
forall tup a. Tuple tup a => a -> SBV tup
tuple (SA
x, SB
y) SBV (A, B) -> SList (A, B) -> SList (A, B)
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A -> SList B -> SList (A, B)
forall a b.
(SymVal a, SymVal b) =>
SList a -> SList b -> SList (a, b)
zip SList A
xs SList B
ys)
                                        SList B -> ChainsTo (SList B) -> ChainsTo (SList B)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SB
y SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SBV (A, B) -> SB) -> SList (A, B) -> SList B
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SBV (A, B) -> SB
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd (SList A -> SList B -> SList (A, B)
forall a b.
(SymVal a, SymVal b) =>
SList a -> SList b -> SList (a, b)
zip SList A
xs SList B
ys)
                                        SList B -> Proof -> ProofStep (SList B)
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
ih
                                        ProofStep (SList B)
-> ChainsTo (ProofStep (SList B)) -> ChainsTo (ProofStep (SList B))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SB
y SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger -> SList B -> SList B
forall a. SymVal a => SInteger -> SList a -> SList a
take (SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList A
xs SInteger -> SInteger -> SInteger
forall a. OrdSymbolic a => a -> a -> a
`smin` SList B -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList B
ys) SList B
ys
                                        SList B -> Proof -> ProofStep (SList B)
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
tc
                                        ProofStep (SList B)
-> ChainsTo (ProofStep (SList B)) -> ChainsTo (ProofStep (SList B))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SList B -> SList B
forall a. SymVal a => SInteger -> SList a -> SList a
take (SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ (SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList A
xs SInteger -> SInteger -> SInteger
forall a. OrdSymbolic a => a -> a -> a
`smin` SList B -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList B
ys)) (SB
y SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList B
ys)
                                        SList B -> ChainsTo (SList B) -> ChainsTo (SList B)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SList B -> SList B
forall a. SymVal a => SInteger -> SList a -> SList a
take (SList A -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SA
x SA -> SList A -> SList A
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList A
xs) SInteger -> SInteger -> SInteger
forall a. OrdSymbolic a => a -> a -> a
`smin` SList B -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SB
y SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList B
ys)) (SB
y SB -> SList B -> SList B
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList B
ys)
                                        SList B -> ChainsTo (SList B) -> ChainsTo (SList B)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep (SList B)]
ChainsTo (SList B)
forall a. [ProofStep a]
qed

{- HLint ignore reverseReverse "Redundant reverse" -}
{- HLint ignore allAny         "Use and"           -}
{- HLint ignore foldrMapFusion "Fuse foldr/map"    -}
{- HLint ignore filterConcat   "Move filter"       -}
{- HLint ignore module         "Use camelCase"     -}
{- HLint ignore module         "Use first"         -}
{- HLint ignore module         "Use second"        -}
{- HLint ignore module         "Use zipWith"       -}