-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.KnuckleDragger.AppendRev
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Example use of the KnuckleDragger, on list append and reverses.
-----------------------------------------------------------------------------

{-# 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.AppendRev where

import Prelude hiding (reverse, (++))

import Data.SBV
import Data.SBV.Tools.KnuckleDragger

import Data.SBV.List ((.:), (++), reverse)
import qualified Data.SBV.List as SL

-- | Use an uninterpreted type for the elements
data Elt
mkUninterpretedSort ''Elt

-- | @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" [Elt] -> SBool) -> [Proof] -> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"appendNull"
                           (\(Forall @"xs" (SList Elt
xs :: SList Elt)) -> SList Elt
xs SList Elt -> SList Elt -> SList Elt
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Elt
forall a. SymVal a => SList a
SL.nil SList Elt -> SList Elt -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList Elt
xs)
                           []

-- | @(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" Elt
    -> Forall "xs" [Elt] -> Forall "ys" [Elt] -> SBool)
-> [Proof]
-> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"consApp"
                        (\(Forall @"x" (SBV Elt
x :: SElt)) (Forall @"xs" SList Elt
xs) (Forall @"ys" SList Elt
ys) -> (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 -> SList Elt
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Elt
ys SList Elt -> SList Elt -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== 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 -> SList Elt
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Elt
ys))
                        []

-- | @(xs ++ ys) ++ zs == xs ++ (ys ++ zs)@
--
-- We have:
--
-- >>> appendAssoc
-- Lemma: appendAssoc                      Q.E.D.
-- [Proven] appendAssoc
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
$ do
   let p :: SymVal a => SList a -> SList a -> SList a -> SBool
       p :: forall a. SymVal a => SList a -> SList a -> SList a -> SBool
p SList a
xs SList a
ys 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

   String
-> (Forall "xs" [Elt]
    -> Forall "ys" [Elt] -> Forall "zs" [Elt] -> SBool)
-> [Proof]
-> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"appendAssoc"
         (\(Forall @"xs" (SList Elt
xs :: SList Elt)) (Forall @"ys" SList Elt
ys) (Forall @"zs" SList Elt
zs) -> SList Elt -> SList Elt -> SList Elt -> SBool
forall a. SymVal a => SList a -> SList a -> SList a -> SBool
p SList Elt
xs SList Elt
ys SList Elt
zs)
         []

-- | @reverse (reverse xs) == xs@
--
-- We have:
--
-- >>> reverseReverse
-- Lemma: revApp                           Q.E.D.
-- Lemma: reverseReverse                   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

   -- Helper lemma: @reverse (xs ++ ys) .== reverse ys ++ reverse xs@
   let ra :: SymVal a => SList a -> SList a -> SBool
       ra :: forall a. SymVal a => SList a -> SList a -> SBool
ra SList a
xs 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

   revApp <- String
-> (Forall "xs" [Elt] -> Forall "ys" [Elt] -> SBool)
-> [Proof]
-> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"revApp" (\(Forall @"xs" (SList Elt
xs :: SList Elt)) (Forall @"ys" SList Elt
ys) -> SList Elt -> SList Elt -> SBool
forall a. SymVal a => SList a -> SList a -> SBool
ra SList Elt
xs SList Elt
ys)
                   -- induction is always done on the last argument, so flip to make sure we induct on xs
                   [(SList Elt -> SList Elt -> SBool) -> Proof
forall a. Induction a => a -> Proof
induct ((SList Elt -> SList Elt -> SBool)
-> SList Elt -> SList Elt -> SBool
forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall a. SymVal a => SList a -> SList a -> SBool
ra @Elt))]

   let p :: SymVal a => SList a -> SBool
       p SList a
xs = 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

   lemma "reverseReverse"
         (\(Forall @"xs" (SList Elt
xs :: SList Elt)) -> SList Elt -> SBool
forall a. SymVal a => SList a -> SBool
p SList Elt
xs)
         [induct (p @Elt), revApp]