-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.TP.Kleene
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Example use of the TP layer, proving some Kleene algebra theorems.
--
-- Based on <http://www.philipzucker.com/bryzzowski_kat/>
-----------------------------------------------------------------------------

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell     #-}
{-# LANGUAGE TypeAbstractions    #-}

{-# OPTIONS_GHC -Wall -Werror -Wno-unused-matches #-}

module Documentation.SBV.Examples.TP.Kleene where

import Prelude hiding((<=))

import Data.SBV
import Data.SBV.TP

-- | An uninterpreted sort, corresponding to the type of Kleene algebra strings.
data Kleene
mkSymbolic [''Kleene]

-- | Star operator over kleene algebras. We're leaving this uninterpreted.
star :: SKleene -> SKleene
star = uninterpret "STAR"

-- | The 'Num' instance for Kleene makes it easy to write regular expressions
-- in the more familiar form.
instance Num SKleene where
  (+) = uninterpret "PAR"
  (*) = uninterpret "SEQ"

  abs    = error "SKleene: not defined: abs"
  signum = error "SKleene: not defined: signum"
  negate = error "SKleene: not defined: signum"

  fromInteger 0 = uninterpret "zero"
  fromInteger 1 = uninterpret "one"
  fromInteger n = error $ "SKleene: not defined: fromInteger " ++ show n

-- | The set of strings matched by one regular expression is a subset of the second,
-- if adding it to the second doesn't change the second set.
(<=) :: SKleene -> SKleene -> SBool
x <= y = x + y .== y

-- | A sequence of Kleene algebra proofs. See <http://www.cs.cornell.edu/~kozen/Papers/ka.pdf>
--
-- We have:
--
-- >>> kleeneProofs
-- Axiom: par_assoc
-- Axiom: par_comm
-- Axiom: par_idem
-- Axiom: par_zero
-- Axiom: seq_assoc
-- Axiom: seq_zero
-- Axiom: seq_one
-- Axiom: rdistrib
-- Axiom: ldistrib
-- Axiom: unfold
-- Axiom: least_fix
-- Lemma: par_lzero                        Q.E.D.
-- Lemma: par_monotone                     Q.E.D.
-- Lemma: seq_monotone                     Q.E.D.
-- Lemma: star_star_1
--   Step: 1 (unfold)                      Q.E.D.
--   Step: 2 (factor out x * star x)       Q.E.D.
--   Step: 3 (par_idem)                    Q.E.D.
--   Step: 4 (unfold)                      Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: subset_eq                        Q.E.D.
-- Lemma: star_star_2_2                    Q.E.D.
-- Lemma: star_star_2_3                    Q.E.D.
-- Lemma: star_star_2_1                    Q.E.D.
-- Lemma: star_star_2                      Q.E.D.
kleeneProofs :: IO ()
kleeneProofs = runTP $ do

  -- Kozen axioms
  par_assoc <- axiom "par_assoc" $ \(Forall @"x" (x :: SKleene)) (Forall @"y" y) (Forall @"z" z) -> x + (y + z) .== (x + y) + z
  par_comm  <- axiom "par_comm"  $ \(Forall @"x" (x :: SKleene)) (Forall @"y" y)                 -> x + y       .== y + x
  par_idem  <- axiom "par_idem"  $ \(Forall @"x" (x :: SKleene))                                 -> x + x       .== x
  par_zero  <- axiom "par_zero"  $ \(Forall @"x" (x :: SKleene))                                 -> x + 0       .== x

  seq_assoc <- axiom "seq_assoc" $ \(Forall @"x" (x :: SKleene)) (Forall @"y" y) (Forall @"z" z) -> x * (y * z) .== (x * y) * z
  seq_zero  <- axiom "seq_zero"  $ \(Forall @"x" (x :: SKleene))                                 -> x * 0       .== 0
  seq_one   <- axiom "seq_one"   $ \(Forall @"x" (x :: SKleene))                                 -> x * 1       .== x

  rdistrib  <- axiom "rdistrib"  $ \(Forall @"x" (x :: SKleene)) (Forall @"y" y) (Forall @"z" z) -> x * (y + z) .== x * y + x * z
  ldistrib  <- axiom "ldistrib"  $ \(Forall @"x" (x :: SKleene)) (Forall @"y" y) (Forall @"z" z) -> (y + z) * x .== y * x + z * x

  unfold    <- axiom "unfold"    $ \(Forall @"e" e) -> star e .== 1 + e * star e

  least_fix <- axiom "least_fix" $ \(Forall @"x" x) (Forall @"e" e) (Forall @"f" f) -> ((f + e * x) <= x) .=> ((star e * f) <= x)

  -- Collect the basic axioms in a list for easy reference
  let kleene = [ proofOf par_assoc,  proofOf par_comm, proofOf par_idem, proofOf par_zero
               , proofOf seq_assoc,  proofOf seq_zero, proofOf seq_one
               , proofOf ldistrib,   proofOf rdistrib
               , proofOf unfold
               , proofOf least_fix
               ]

  -- Various proofs:
  par_lzero    <- lemma "par_lzero"    (\(Forall @"x" x) -> (0 :: SKleene) + x .== x)                                        kleene
  par_monotone <- lemma "par_monotone" (\(Forall @"x" x) (Forall @"y" y) (Forall @"z" z) -> x <= y .=> ((x + z) <= (y + z))) kleene
  seq_monotone <- lemma "seq_monotone" (\(Forall @"x" x) (Forall @"y" y) (Forall @"z" z) -> x <= y .=> ((x * z) <= (y * z))) kleene

  -- This one requires a chain of reasoning: x* x* == x*
  star_star_1  <- calc "star_star_1"
                       (\(Forall @"x" x) -> star x * star x .== star x) $
                       \x -> [] |- star x * star x                     ?? unfold
                                =: (1 + x * star x) * (1 + x * star x)
                                ?? "factor out x * star x"
                                ?? kleene
                                =: (1 + 1) + (x * star x + x * star x) ?? par_idem
                                =: 1 + x * star x                      ?? unfold
                                =: star x
                                =: qed

  subset_eq   <- lemma "subset_eq" (\(Forall @"x" x) (Forall @"y" y) -> (x .== y) .== (x <= y .&& y <= x)) kleene

  -- Prove: x** = x*
  star_star_2 <- do _1 <- lemma "star_star_2_2" (\(Forall @"x" x) -> ((star x * star x + 1) <= star x) .=> star (star x) <= star x) kleene
                    _2 <- lemma "star_star_2_3" (\(Forall @"x" x) -> star (star x) <= star x)                                       (kleene ++ [proofOf _1])
                    _3 <- lemma "star_star_2_1" (\(Forall @"x" x) -> star x        <= star (star x))                                kleene

                    lemma "star_star_2" (\(Forall @"x" x) -> star (star x) .== star x) [proofOf subset_eq, proofOf _2, proofOf _3]

  pure ()