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

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

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

module Documentation.SBV.Examples.KnuckleDragger.Kleene where

import Prelude hiding((<=))

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

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

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

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

  abs :: SKleene -> SKleene
abs    = String -> SKleene -> SKleene
forall a. HasCallStack => String -> a
error String
"SKleene: not defined: abs"
  signum :: SKleene -> SKleene
signum = String -> SKleene -> SKleene
forall a. HasCallStack => String -> a
error String
"SKleene: not defined: signum"
  negate :: SKleene -> SKleene
negate = String -> SKleene -> SKleene
forall a. HasCallStack => String -> a
error String
"SKleene: not defined: signum"

  fromInteger :: Integer -> SKleene
fromInteger Integer
0 = String -> SKleene
forall a. SMTDefinable a => String -> a
uninterpret String
"zero"
  fromInteger Integer
1 = String -> SKleene
forall a. SMTDefinable a => String -> a
uninterpret String
"one"
  fromInteger Integer
n = String -> SKleene
forall a. HasCallStack => String -> a
error (String -> SKleene) -> String -> SKleene
forall a b. (a -> b) -> a -> b
$ String
"SKleene: not defined: fromInteger " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
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
SKleene
x <= :: SKleene -> SKleene -> SBool
<= SKleene
y = SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
y SKleene -> SKleene -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SKleene
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                             Q.E.D.
--   Step  : 2                             Q.E.D.
--   Step  : 3                             Q.E.D.
--   Step  : 4                             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 :: IO ()
kleeneProofs = KD () -> IO ()
forall a. KD a -> IO a
runKD (KD () -> IO ()) -> KD () -> IO ()
forall a b. (a -> b) -> a -> b
$ do

  -- Kozen axioms
  par_assoc <- String
-> (Forall "x" Kleene
    -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
-> KD Proof
forall a. Proposition a => String -> a -> KD Proof
axiom String
"par_assoc" ((Forall "x" Kleene
  -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
 -> KD Proof)
-> (Forall "x" Kleene
    -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
-> KD Proof
forall a b. (a -> b) -> a -> b
$ \(Forall @"x" (SKleene
x :: SKleene)) (Forall @"y" SKleene
y) (Forall @"z" SKleene
z) -> SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ (SKleene
y SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
z) SKleene -> SKleene -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
y) SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
z
  par_comm  <- axiom "par_comm"  $ \(Forall @"x" (SKleene
x :: SKleene)) (Forall @"y" SKleene
y)                 -> SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
y       SKleene -> SKleene -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SKleene
y SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
x
  par_idem  <- axiom "par_idem"  $ \(Forall @"x" (SKleene
x :: SKleene))                                 -> SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
x       SKleene -> SKleene -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SKleene
x
  par_zero  <- axiom "par_zero"  $ \(Forall @"x" (SKleene
x :: SKleene))                                 -> SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
0       SKleene -> SKleene -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SKleene
x

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

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

  unfold    <- axiom "unfold"    $ \(Forall @"e" SKleene
e) -> SKleene -> SKleene
star SKleene
e SKleene -> SKleene -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SKleene
1 SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
e SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene -> SKleene
star SKleene
e

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

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

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

  -- This one requires a chain of reasoning: x* x* == x*
  star_star_1  <- calc "star_star_1"
                       (\(Forall @"x" (SKleene
x :: SKleene)) -> SKleene -> SKleene
star SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene -> SKleene
star SKleene
x SKleene -> SKleene -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SKleene -> SKleene
star SKleene
x) $
                       \SKleene
x -> [] [SBool] -> [ProofStep SKleene] -> (SBool, [ProofStep SKleene])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- SKleene -> SKleene
star SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene -> SKleene
star SKleene
x                     SKleene -> Proof -> ProofStep SKleene
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
unfold
                                ProofStep SKleene
-> ChainsTo (ProofStep SKleene) -> ChainsTo (ProofStep SKleene)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SKleene
1 SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene -> SKleene
star SKleene
x) SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* (SKleene
1 SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene -> SKleene
star SKleene
x) SKleene -> [Proof] -> ProofStep SKleene
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [Proof]
kleene
                                ProofStep SKleene
-> ChainsTo (ProofStep SKleene) -> ChainsTo (ProofStep SKleene)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SKleene
1 SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
1) SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ (SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene -> SKleene
star SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene -> SKleene
star SKleene
x) SKleene -> Proof -> ProofStep SKleene
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
par_idem
                                ProofStep SKleene
-> ChainsTo (ProofStep SKleene) -> ChainsTo (ProofStep SKleene)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SKleene
1 SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene -> SKleene
star SKleene
x                      SKleene -> Proof -> ProofStep SKleene
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
unfold
                                ProofStep SKleene
-> ChainsTo (ProofStep SKleene) -> ChainsTo (ProofStep SKleene)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SKleene -> SKleene
star SKleene
x
                                SKleene -> ChainsTo SKleene -> ChainsTo SKleene
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep SKleene]
ChainsTo SKleene
forall a. [ProofStep a]
qed

  subset_eq   <- lemma "subset_eq" (\(Forall @"x" SKleene
x) (Forall @"y" SKleene
y) -> (SKleene
x SKleene -> SKleene -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SKleene
y) SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SKleene
x SKleene -> SKleene -> SBool
<= SKleene
y SBool -> SBool -> SBool
.&& SKleene
y SKleene -> SKleene -> SBool
<= SKleene
x)) kleene

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

                    lemma "star_star_2" (\(Forall @"x" (SKleene
x :: SKleene)) -> SKleene -> SKleene
star (SKleene -> SKleene
star SKleene
x) SKleene -> SKleene -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SKleene -> SKleene
star SKleene
x) [subset_eq, _2, _3]

  pure ()