-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.KnuckleDragger.RevLen
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Proof that reversing a list does not change its length.
-----------------------------------------------------------------------------

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

{-# OPTIONS_GHC -Wall -Werror -Wno-unused-do-bind #-}

module Documentation.SBV.Examples.KnuckleDragger.RevLen where

import Prelude hiding (length, reverse)

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

import Data.SBV.List (reverse, length)

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

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

-- | @length xs == length (reverse xs)@
--
-- We have:
--
-- >>> revLen
-- Lemma: revLen                           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
$ do
   let p :: SList Elt -> SBool
       p :: SList Elt -> SBool
p SList Elt
xs = SList Elt -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SList Elt -> SList Elt
forall a. SymVal a => SList a -> SList a
reverse SList Elt
xs) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList Elt -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Elt
xs

   String -> (Forall "xs" [Elt] -> SBool) -> [Proof] -> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"revLen"
         (\(Forall @"xs" SList Elt
xs) -> SList Elt -> SBool
p SList Elt
xs)
         [(SList Elt -> SBool) -> Proof
forall a. Induction a => a -> Proof
induct SList Elt -> SBool
p]

-- | 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 = [Elt_1,Elt_2,Elt_1] :: [Elt]
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
$ do
   let p :: SList Elt -> SBool
       p :: SList Elt -> SBool
p SList Elt
xs = SList Elt -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SList Elt -> SList Elt
forall a. SymVal a => SList a -> SList a
reverse SList Elt
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 Elt -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Elt
xs SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
3) SInteger
5 (SList Elt -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Elt
xs)

   String -> (Forall "xs" [Elt] -> SBool) -> [Proof] -> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"badRevLen"
         (\(Forall @"xs" SList Elt
xs) -> SList Elt -> SBool
p SList Elt
xs)
         [(SList Elt -> SBool) -> Proof
forall a. Induction a => a -> Proof
induct SList Elt -> SBool
p]

   () -> KD ()
forall a. a -> KD a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()