-----------------------------------------------------------------------------
-- |
-- 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 DeriveAnyClass       #-}
{-# LANGUAGE DeriveDataTypeable   #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE StandaloneDeriving   #-}
{-# 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
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 (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 :: IO ()
kleeneProofs = TP () -> IO ()
forall a. TP a -> IO a
runTP (TP () -> IO ()) -> TP () -> IO ()
forall a b. (a -> b) -> a -> b
$ do

  -- Kozen axioms
  Proof
  (Forall "x" Kleene
   -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
par_assoc <- String
-> (Forall "x" Kleene
    -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
-> TP
     (Proof
        (Forall "x" Kleene
         -> Forall "y" Kleene -> Forall "z" Kleene -> SBool))
forall a. Proposition a => String -> a -> TP (Proof a)
axiom String
"par_assoc" ((Forall "x" Kleene
  -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
 -> TP
      (Proof
         (Forall "x" Kleene
          -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)))
-> (Forall "x" Kleene
    -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
-> TP
     (Proof
        (Forall "x" Kleene
         -> Forall "y" Kleene -> Forall "z" Kleene -> SBool))
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
  Proof (Forall "x" Kleene -> Forall "y" Kleene -> SBool)
par_comm  <- String
-> (Forall "x" Kleene -> Forall "y" Kleene -> SBool)
-> TP (Proof (Forall "x" Kleene -> Forall "y" Kleene -> SBool))
forall a. Proposition a => String -> a -> TP (Proof a)
axiom String
"par_comm"  ((Forall "x" Kleene -> Forall "y" Kleene -> SBool)
 -> TP (Proof (Forall "x" Kleene -> Forall "y" Kleene -> SBool)))
-> (Forall "x" Kleene -> Forall "y" Kleene -> SBool)
-> TP (Proof (Forall "x" Kleene -> Forall "y" Kleene -> SBool))
forall a b. (a -> b) -> a -> b
$ \(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
  Proof (Forall "x" Kleene -> SBool)
par_idem  <- String
-> (Forall "x" Kleene -> SBool)
-> TP (Proof (Forall "x" Kleene -> SBool))
forall a. Proposition a => String -> a -> TP (Proof a)
axiom String
"par_idem"  ((Forall "x" Kleene -> SBool)
 -> TP (Proof (Forall "x" Kleene -> SBool)))
-> (Forall "x" Kleene -> SBool)
-> TP (Proof (Forall "x" Kleene -> SBool))
forall a b. (a -> b) -> a -> b
$ \(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
  Proof (Forall "x" Kleene -> SBool)
par_zero  <- String
-> (Forall "x" Kleene -> SBool)
-> TP (Proof (Forall "x" Kleene -> SBool))
forall a. Proposition a => String -> a -> TP (Proof a)
axiom String
"par_zero"  ((Forall "x" Kleene -> SBool)
 -> TP (Proof (Forall "x" Kleene -> SBool)))
-> (Forall "x" Kleene -> SBool)
-> TP (Proof (Forall "x" Kleene -> SBool))
forall a b. (a -> b) -> a -> b
$ \(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

  Proof
  (Forall "x" Kleene
   -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
seq_assoc <- String
-> (Forall "x" Kleene
    -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
-> TP
     (Proof
        (Forall "x" Kleene
         -> Forall "y" Kleene -> Forall "z" Kleene -> SBool))
forall a. Proposition a => String -> a -> TP (Proof a)
axiom String
"seq_assoc" ((Forall "x" Kleene
  -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
 -> TP
      (Proof
         (Forall "x" Kleene
          -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)))
-> (Forall "x" Kleene
    -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
-> TP
     (Proof
        (Forall "x" Kleene
         -> Forall "y" Kleene -> Forall "z" Kleene -> SBool))
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
  Proof (Forall "x" Kleene -> SBool)
seq_zero  <- String
-> (Forall "x" Kleene -> SBool)
-> TP (Proof (Forall "x" Kleene -> SBool))
forall a. Proposition a => String -> a -> TP (Proof a)
axiom String
"seq_zero"  ((Forall "x" Kleene -> SBool)
 -> TP (Proof (Forall "x" Kleene -> SBool)))
-> (Forall "x" Kleene -> SBool)
-> TP (Proof (Forall "x" Kleene -> SBool))
forall a b. (a -> b) -> a -> b
$ \(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
  Proof (Forall "x" Kleene -> SBool)
seq_one   <- String
-> (Forall "x" Kleene -> SBool)
-> TP (Proof (Forall "x" Kleene -> SBool))
forall a. Proposition a => String -> a -> TP (Proof a)
axiom String
"seq_one"   ((Forall "x" Kleene -> SBool)
 -> TP (Proof (Forall "x" Kleene -> SBool)))
-> (Forall "x" Kleene -> SBool)
-> TP (Proof (Forall "x" Kleene -> SBool))
forall a b. (a -> b) -> a -> b
$ \(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

  Proof
  (Forall "x" Kleene
   -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
rdistrib  <- String
-> (Forall "x" Kleene
    -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
-> TP
     (Proof
        (Forall "x" Kleene
         -> Forall "y" Kleene -> Forall "z" Kleene -> SBool))
forall a. Proposition a => String -> a -> TP (Proof a)
axiom String
"rdistrib"  ((Forall "x" Kleene
  -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
 -> TP
      (Proof
         (Forall "x" Kleene
          -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)))
-> (Forall "x" Kleene
    -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
-> TP
     (Proof
        (Forall "x" Kleene
         -> Forall "y" Kleene -> Forall "z" Kleene -> SBool))
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
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene
z
  Proof
  (Forall "x" Kleene
   -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
ldistrib  <- String
-> (Forall "x" Kleene
    -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
-> TP
     (Proof
        (Forall "x" Kleene
         -> Forall "y" Kleene -> Forall "z" Kleene -> SBool))
forall a. Proposition a => String -> a -> TP (Proof a)
axiom String
"ldistrib"  ((Forall "x" Kleene
  -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
 -> TP
      (Proof
         (Forall "x" Kleene
          -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)))
-> (Forall "x" Kleene
    -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
-> TP
     (Proof
        (Forall "x" Kleene
         -> Forall "y" Kleene -> Forall "z" Kleene -> SBool))
forall a b. (a -> b) -> a -> b
$ \(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

  Proof (Forall "e" Kleene -> SBool)
unfold    <- String
-> (Forall "e" Kleene -> SBool)
-> TP (Proof (Forall "e" Kleene -> SBool))
forall a. Proposition a => String -> a -> TP (Proof a)
axiom String
"unfold"    ((Forall "e" Kleene -> SBool)
 -> TP (Proof (Forall "e" Kleene -> SBool)))
-> (Forall "e" Kleene -> SBool)
-> TP (Proof (Forall "e" Kleene -> SBool))
forall a b. (a -> b) -> a -> b
$ \(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

  Proof
  (Forall "x" Kleene
   -> Forall "e" Kleene -> Forall "f" Kleene -> SBool)
least_fix <- String
-> (Forall "x" Kleene
    -> Forall "e" Kleene -> Forall "f" Kleene -> SBool)
-> TP
     (Proof
        (Forall "x" Kleene
         -> Forall "e" Kleene -> Forall "f" Kleene -> SBool))
forall a. Proposition a => String -> a -> TP (Proof a)
axiom String
"least_fix" ((Forall "x" Kleene
  -> Forall "e" Kleene -> Forall "f" Kleene -> SBool)
 -> TP
      (Proof
         (Forall "x" Kleene
          -> Forall "e" Kleene -> Forall "f" Kleene -> SBool)))
-> (Forall "x" Kleene
    -> Forall "e" Kleene -> Forall "f" Kleene -> SBool)
-> TP
     (Proof
        (Forall "x" Kleene
         -> Forall "e" Kleene -> Forall "f" Kleene -> SBool))
forall a b. (a -> b) -> a -> b
$ \(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 :: [ProofObj]
kleene = [ Proof
  (Forall "x" Kleene
   -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof
  (Forall "x" Kleene
   -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
par_assoc,  Proof (Forall "x" Kleene -> Forall "y" Kleene -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "x" Kleene -> Forall "y" Kleene -> SBool)
par_comm, Proof (Forall "x" Kleene -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "x" Kleene -> SBool)
par_idem, Proof (Forall "x" Kleene -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "x" Kleene -> SBool)
par_zero
               , Proof
  (Forall "x" Kleene
   -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof
  (Forall "x" Kleene
   -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
seq_assoc,  Proof (Forall "x" Kleene -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "x" Kleene -> SBool)
seq_zero, Proof (Forall "x" Kleene -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "x" Kleene -> SBool)
seq_one
               , Proof
  (Forall "x" Kleene
   -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof
  (Forall "x" Kleene
   -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
ldistrib,   Proof
  (Forall "x" Kleene
   -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof
  (Forall "x" Kleene
   -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
rdistrib
               , Proof (Forall "e" Kleene -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "e" Kleene -> SBool)
unfold
               , Proof
  (Forall "x" Kleene
   -> Forall "e" Kleene -> Forall "f" Kleene -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof
  (Forall "x" Kleene
   -> Forall "e" Kleene -> Forall "f" Kleene -> SBool)
least_fix
               ]

  -- Various proofs:
  Proof (Forall "x" Kleene -> SBool)
par_lzero    <- String
-> (Forall "x" Kleene -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "x" Kleene -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"par_lzero"    (\(Forall @"x" SKleene
x) -> (SKleene
0 :: SKleene) SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
x SKleene -> SKleene -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SKleene
x)                                        [ProofObj]
kleene
  Proof
  (Forall "x" Kleene
   -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
par_monotone <- String
-> (Forall "x" Kleene
    -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "x" Kleene
         -> Forall "y" Kleene -> Forall "z" Kleene -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"par_monotone" (\(Forall @"x" SKleene
x) (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))) [ProofObj]
kleene
  Proof
  (Forall "x" Kleene
   -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
seq_monotone <- String
-> (Forall "x" Kleene
    -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "x" Kleene
         -> Forall "y" Kleene -> Forall "z" Kleene -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"seq_monotone" (\(Forall @"x" SKleene
x) (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))) [ProofObj]
kleene

  -- This one requires a chain of reasoning: x* x* == x*
  Proof (Forall "x" Kleene -> SBool)
star_star_1  <- String
-> (Forall "x" Kleene -> SBool)
-> StepArgs (Forall "x" Kleene -> SBool) Kleene
-> TP (Proof (Forall "x" Kleene -> SBool))
forall t.
(Proposition (Forall "x" Kleene -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "x" Kleene -> SBool)
-> StepArgs (Forall "x" Kleene -> SBool) t
-> TP (Proof (Forall "x" Kleene -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"star_star_1"
                       (\(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 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SKleene -> SKleene
star SKleene
x) (StepArgs (Forall "x" Kleene -> SBool) Kleene
 -> TP (Proof (Forall "x" Kleene -> SBool)))
-> StepArgs (Forall "x" Kleene -> SBool) Kleene
-> TP (Proof (Forall "x" Kleene -> SBool))
forall a b. (a -> b) -> a -> b
$
                       \SKleene
x -> [] [SBool] -> TPProofRaw SKleene -> (SBool, TPProofRaw SKleene)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SKleene -> SKleene
star SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene -> SKleene
star SKleene
x                     SKleene -> Proof (Forall "e" Kleene -> SBool) -> Hinted SKleene
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "e" Kleene -> SBool)
unfold
                                TPProofRaw SKleene
-> ChainsTo (TPProofRaw SKleene) -> ChainsTo (TPProofRaw 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 -> String -> Hinted SKleene
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"factor out x * star x"
                                TPProofRaw SKleene -> [ProofObj] -> Hinted (TPProofRaw SKleene)
forall a b. HintsTo a b => a -> b -> Hinted a
?? [ProofObj]
kleene
                                Hinted (TPProofRaw SKleene)
-> ChainsTo (Hinted (TPProofRaw SKleene))
-> ChainsTo (Hinted (TPProofRaw 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 (Forall "x" Kleene -> SBool) -> Hinted SKleene
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "x" Kleene -> SBool)
par_idem
                                TPProofRaw SKleene
-> ChainsTo (TPProofRaw SKleene) -> ChainsTo (TPProofRaw 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 (Forall "e" Kleene -> SBool) -> Hinted SKleene
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "e" Kleene -> SBool)
unfold
                                TPProofRaw SKleene
-> ChainsTo (TPProofRaw SKleene) -> ChainsTo (TPProofRaw 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
=: ChainsTo SKleene
TPProofRaw SKleene
forall a. TPProofRaw a
qed

  Proof (Forall "x" Kleene -> Forall "y" Kleene -> SBool)
subset_eq   <- String
-> (Forall "x" Kleene -> Forall "y" Kleene -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "x" Kleene -> Forall "y" Kleene -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"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)) [ProofObj]
kleene

  -- Prove: x** = x*
  Proof (Forall "x" Kleene -> SBool)
star_star_2 <- do Proof (Forall "x" Kleene -> SBool)
_1 <- String
-> (Forall "x" Kleene -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "x" Kleene -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"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) [ProofObj]
kleene
                    Proof (Forall "x" Kleene -> SBool)
_2 <- String
-> (Forall "x" Kleene -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "x" Kleene -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"star_star_2_3" (\(Forall @"x" SKleene
x) -> SKleene -> SKleene
star (SKleene -> SKleene
star SKleene
x) SKleene -> SKleene -> SBool
<= SKleene -> SKleene
star SKleene
x)                                       ([ProofObj]
kleene [ProofObj] -> [ProofObj] -> [ProofObj]
forall a. [a] -> [a] -> [a]
++ [Proof (Forall "x" Kleene -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "x" Kleene -> SBool)
_1])
                    Proof (Forall "x" Kleene -> SBool)
_3 <- String
-> (Forall "x" Kleene -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "x" Kleene -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"star_star_2_1" (\(Forall @"x" SKleene
x) -> SKleene -> SKleene
star SKleene
x        SKleene -> SKleene -> SBool
<= SKleene -> SKleene
star (SKleene -> SKleene
star SKleene
x))                                [ProofObj]
kleene

                    String
-> (Forall "x" Kleene -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "x" Kleene -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"star_star_2" (\(Forall @"x" SKleene
x) -> SKleene -> SKleene
star (SKleene -> SKleene
star SKleene
x) SKleene -> SKleene -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SKleene -> SKleene
star SKleene
x) [Proof (Forall "x" Kleene -> Forall "y" Kleene -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "x" Kleene -> Forall "y" Kleene -> SBool)
subset_eq, Proof (Forall "x" Kleene -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "x" Kleene -> SBool)
_2, Proof (Forall "x" Kleene -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "x" Kleene -> SBool)
_3]

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