content: -- | An example showing the usage of the What4 backend in copilot-theorem for
  -- propositional logic on boolean streams.
  
  module Main where
  
  import qualified Prelude as P
  import Control.Monad (void, forM_)
  
  import Language.Copilot
  import Copilot.Theorem.What4
  
  spec :: Spec
  spec = do
    -- * Non-inductive propositions
  
    -- The constant value true, which is translated as the corresponding SMT
    -- boolean literal (and is therefore provable).
    void $ prop "Example 1" (forAll true)
  
    -- The constant value false, which is translated as the corresponding SMT
    -- boolean literal (and is therefore not provable).
    void $ prop "Example 2" (forAll false)
  
    -- An "a or not a" proposition which does not require any sort of inductive
    -- argument (but see examples 5 and 6 below for versions that do require
    -- induction to solve). This is easily proven.
    let a = [False] ++ b
        b = not a
    void $ prop "Example 3" (forAll (a || b))
  
    -- An "a or not a" proposition using external streams, which is also provable.
    let a = extern "a" Nothing
    void $ prop "Example 4" (forAll (a || not a))
  
    -- * Simple inductive propositions
    --
    -- While Copilot.Theorem.What4 is not able to solve all inductive propositions
    -- in general (see the "Complex inductive propositions" section below), the
    -- following inductive propositions are simple enough that the heuristics in
    -- Copilot.Theorem.What4 can solve them without issue.
  
    -- An inductively defined flavor of true.
    let a = [True] ++ a
    void $ prop "Example 5" (forAll a)
  
    -- An inductively defined "a or not a" proposition (i.e., a more complex
    -- version of example 3 above).
    let a = [False] ++ b
        b = [True] ++ a
    void $ prop "Example 6" (forAll (a || b))
  
    -- A bit more convoluted version of example 6.
    let a = [True, False] ++ b
        b = [False] ++ not (drop 1 a)
    void $ prop "Example 7" (forAll (a || b))
  
    -- * Complex induction propositions
    --
    -- The heuristics in Copilot.Theorem.What4 are not able to prove these
    -- inductive propositions, so these will be reported as unprovable, even
    -- though each proposition is actually provable.
  
    -- An inductively defined flavor of true (i.e., a more complex version of
    -- example 5 above).
    let a = [True] ++ ([True] ++ ([True] ++ a))
    void $ prop "Example 8" (forAll a)
  
    -- An inductively defined "a or not a" proposition (i.e., a more complex
    -- version of example 6 above).
    let a = [False] ++ ([False] ++ ([False] ++ b))
        b = [True] ++ ([True] ++ ([True] ++ a))
    void $ prop "Example 9" (forAll (a || b))
  
  main :: IO ()
  main = do
    spec' <- reify spec
  
    -- Use Z3 to prove the properties.
    results <- prove Z3 spec'
  
    -- Print the results.
    forM_ results $ \(nm, res) -> do
      putStr $ nm <> ": "
      case res of
        Valid   -> putStrLn "valid"
        Invalid -> putStrLn "invalid"
        Unknown -> putStrLn "unknown"
  