Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Documentation.SBV.Examples.KnuckleDragger.ShefferStroke

Contents

Generalized Boolean Algebras
The sheffer stroke
Sheffer's stroke defines a boolean algebra

Description

Inspired by https://www.philipzucker.com/cody_sheffer/, proving that the axioms of sheffer stroke (i.e., nand in traditional boolean logic), imply it is a boolean algebra.

Synopsis

class BooleanAlgebra α where
- ﬧ :: α -> α
- (⨆) :: α -> α -> α
- (⨅) :: α -> α -> α
- (≤) :: α -> α -> SBool
- (<) :: α -> α -> SBool
- (\\) :: α -> α -> α
- (⇨) :: α -> α -> α
- ⲳ :: α
- т :: α
data BooleanAlgebraProof = BooleanAlgebraProof {
- le_refl :: Proof
- le_trans :: Proof
- lt_iff_le_not_le :: Proof
- le_antisymm :: Proof
- le_sup_left :: Proof
- le_sup_right :: Proof
- sup_le :: Proof
- inf_le_left :: Proof
- inf_le_right :: Proof
- le_inf :: Proof
- le_sup_inf :: Proof
- inf_compl_le_bot :: Proof
- top_le_sup_compl :: Proof
- le_top :: Proof
- bot_le :: Proof
- sdiff_eq :: Proof
- himp_eq :: Proof
}
data Stroke
type SStroke = SBV Stroke
(⏐) :: SStroke -> SStroke -> SStroke
ﬧﬧ :: BooleanAlgebra a => a -> a
sheffer1 :: KD Proof
sheffer2 :: KD Proof
sheffer3 :: KD Proof
shefferBooleanAlgebra :: IO BooleanAlgebraProof

Generalized Boolean Algebras

class BooleanAlgebra α where Source #

Capture what it means to be a boolean algebra. We follow Lean's definition, as much as we can: https://leanprover-community.github.io/mathlib_docs/order/boolean_algebra.html. Since there's no way in Haskell to capture properties together with a class, we'll represent the properties separately.

Methods

ﬧ :: α -> α Source #

(⨆) :: α -> α -> α infixl 6 Source #

(⨅) :: α -> α -> α infixl 7 Source #

(≤) :: α -> α -> SBool infix 4 Source #

(<) :: α -> α -> SBool Source #

(\\) :: α -> α -> α Source #

(⇨) :: α -> α -> α Source #

ⲳ :: α Source #

т :: α Source #

Instances

Instances details

BooleanAlgebra SStroke Source #

The boolean algebra of the sheffer stroke.

Instance details

Defined in Documentation.SBV.Examples.KnuckleDragger.ShefferStroke

Methods

ﬧ :: SStroke -> SStroke Source #

(⨆) :: SStroke -> SStroke -> SStroke Source #

(⨅) :: SStroke -> SStroke -> SStroke Source #

(≤) :: SStroke -> SStroke -> SBool Source #

(<) :: SStroke -> SStroke -> SBool Source #

(\\) :: SStroke -> SStroke -> SStroke Source #

(⇨) :: SStroke -> SStroke -> SStroke Source #

ⲳ :: SStroke Source #

т :: SStroke Source #

data BooleanAlgebraProof Source #

Proofs needed for a boolean-algebra. Again, we follow Lean's definition here. Since we cannot put these in the class definition above, we will keep them in a simple data-structure.

Constructors

BooleanAlgebraProof
Fields le_refl :: Proof le_trans :: Proof lt_iff_le_not_le :: Proof le_antisymm :: Proof le_sup_left :: Proof le_sup_right :: Proof sup_le :: Proof inf_le_left :: Proof inf_le_right :: Proof le_inf :: Proof le_sup_inf :: Proof inf_compl_le_bot :: Proof top_le_sup_compl :: Proof le_top :: Proof bot_le :: Proof sdiff_eq :: Proof himp_eq :: Proof

Instances

Instances details

Show BooleanAlgebraProof Source #	A somewhat prettier printer for a BooleanAlgebra proof
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.ShefferStroke Methods showsPrec :: Int -> BooleanAlgebraProof -> ShowS # show :: BooleanAlgebraProof -> String # showList :: [BooleanAlgebraProof] -> ShowS #

The sheffer stroke

data Stroke Source #

The abstract type for the domain.

Instances

Instances details

Data Stroke Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.ShefferStroke Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Stroke -> c Stroke # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Stroke # toConstr :: Stroke -> Constr # dataTypeOf :: Stroke -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Stroke) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Stroke) # gmapT :: (forall b. Data b => b -> b) -> Stroke -> Stroke # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Stroke -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Stroke -> r # gmapQ :: (forall d. Data d => d -> u) -> Stroke -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Stroke -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Stroke -> m Stroke # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Stroke -> m Stroke # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Stroke -> m Stroke #
Read Stroke Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.ShefferStroke Methods readsPrec :: Int -> ReadS Stroke # readList :: ReadS [Stroke] # readPrec :: ReadPrec Stroke # readListPrec :: ReadPrec [Stroke] #
Show Stroke Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.ShefferStroke Methods showsPrec :: Int -> Stroke -> ShowS # show :: Stroke -> String # showList :: [Stroke] -> ShowS #
SymVal Stroke Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.ShefferStroke Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Stroke) Source # literal :: Stroke -> SBV Stroke Source # fromCV :: CV -> Stroke Source # isConcretely :: SBV Stroke -> (Stroke -> Bool) -> Bool Source # free :: MonadSymbolic m => String -> m (SBV Stroke) Source # free_ :: MonadSymbolic m => m (SBV Stroke) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV Stroke] Source # symbolic :: MonadSymbolic m => String -> m (SBV Stroke) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV Stroke] Source # unliteral :: SBV Stroke -> Maybe Stroke Source # isConcrete :: SBV Stroke -> Bool Source # isSymbolic :: SBV Stroke -> Bool Source #
HasKind Stroke Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.ShefferStroke Methods kindOf :: Stroke -> Kind Source # hasSign :: Stroke -> Bool Source # intSizeOf :: Stroke -> Int Source # isBoolean :: Stroke -> Bool Source # isBounded :: Stroke -> Bool Source # isReal :: Stroke -> Bool Source # isFloat :: Stroke -> Bool Source # isDouble :: Stroke -> Bool Source # isRational :: Stroke -> Bool Source # isFP :: Stroke -> Bool Source # isUnbounded :: Stroke -> Bool Source # isUserSort :: Stroke -> Bool Source # isChar :: Stroke -> Bool Source # isString :: Stroke -> Bool Source # isList :: Stroke -> Bool Source # isSet :: Stroke -> Bool Source # isTuple :: Stroke -> Bool Source # isMaybe :: Stroke -> Bool Source # isEither :: Stroke -> Bool Source # isArray :: Stroke -> Bool Source # showType :: Stroke -> String Source #
SatModel Stroke Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.ShefferStroke Methods parseCVs :: [CV] -> Maybe (Stroke, [CV]) Source # cvtModel :: (Stroke -> Maybe b) -> Maybe (Stroke, [CV]) -> Maybe (b, [CV]) Source #
BooleanAlgebra SStroke Source #	The boolean algebra of the sheffer stroke.
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.ShefferStroke Methods ﬧ :: SStroke -> SStroke Source # (⨆) :: SStroke -> SStroke -> SStroke Source # (⨅) :: SStroke -> SStroke -> SStroke Source # (≤) :: SStroke -> SStroke -> SBool Source # (<) :: SStroke -> SStroke -> SBool Source # (\\) :: SStroke -> SStroke -> SStroke Source # (⇨) :: SStroke -> SStroke -> SStroke Source # ⲳ :: SStroke Source # т :: SStroke Source #

type SStroke = SBV Stroke Source #

Symbolic version of the type Stroke.

(⏐) :: SStroke -> SStroke -> SStroke infixl 7 Source #

The sheffer stroke operator.

ﬧﬧ :: BooleanAlgebra a => a -> a Source #

Double-negation

sheffer1 :: KD Proof Source #

First Sheffer axiom: ﬧﬧa == a

sheffer2 :: KD Proof Source #

Second Sheffer axiom: a ⏐ (b ⏐ ﬧb) == ﬧa

sheffer3 :: KD Proof Source #

Third Sheffer axiom: ﬧ(a ⏐ (b ⏐ c)) == (ﬧb ⏐ a) ⏐ (ﬧc ⏐ a)

Sheffer's stroke defines a boolean algebra

shefferBooleanAlgebra :: IO BooleanAlgebraProof Source #

Prove that Sheffer stroke axioms imply it is a boolean algebra. We have:

>>> shefferBooleanAlgebra
Axiom: ﬧﬧa == a
Axiom: a ⏐ (b ⏐ ﬧb) == ﬧa
Axiom: ﬧ(a ⏐ (b ⏐ c)) == (ﬧb ⏐ a) ⏐ (ﬧc ⏐ a)
Lemma: a | b = b | a
  Step  : 1                                                 Q.E.D.
  Step  : 2                                                 Q.E.D.
  Step  : 3                                                 Q.E.D.
  Step  : 4                                                 Q.E.D.
  Step  : 5                                                 Q.E.D.
  Step  : 6                                                 Q.E.D.
  Step  : 7                                                 Q.E.D.
  Result:                                                   Q.E.D.
Lemma: a | a′ = b | b′
  Step  : 1                                                 Q.E.D.
  Step  : 2                                                 Q.E.D.
  Step  : 3                                                 Q.E.D.
  Step  : 4                                                 Q.E.D.
  Step  : 5                                                 Q.E.D.
  Result:                                                   Q.E.D.
Lemma: a ⊔ b = b ⊔ a                                        Q.E.D.
Lemma: a ⊓ b = b ⊓ a                                        Q.E.D.
Lemma: a ⊔ ⲳ = a                                            Q.E.D.
Lemma: a ⊓ т = a                                            Q.E.D.
Lemma: a ⊔ (b ⊓ c) = (a ⊔ b) ⊓ (a ⊔ c)                      Q.E.D.
Lemma: a ⊓ (b ⊔ c) = (a ⊓ b) ⊔ (a ⊓ c)                      Q.E.D.
Lemma: a ⊔ aᶜ = т                                           Q.E.D.
Lemma: a ⊓ aᶜ = ⲳ                                           Q.E.D.
Lemma: a ⊔ т = т
  Step  : 1                                                 Q.E.D.
  Step  : 2                                                 Q.E.D.
  Step  : 3                                                 Q.E.D.
  Step  : 4                                                 Q.E.D.
  Step  : 5                                                 Q.E.D.
  Step  : 6                                                 Q.E.D.
  Result:                                                   Q.E.D.
Lemma: a ⊓ ⲳ = ⲳ
  Step  : 1                                                 Q.E.D.
  Step  : 2                                                 Q.E.D.
  Step  : 3                                                 Q.E.D.
  Step  : 4                                                 Q.E.D.
  Step  : 5                                                 Q.E.D.
  Step  : 6                                                 Q.E.D.
  Result:                                                   Q.E.D.
Lemma: a ⊔ (a ⊓ b) = a
  Step  : 1                                                 Q.E.D.
  Step  : 2                                                 Q.E.D.
  Step  : 3                                                 Q.E.D.
  Step  : 4                                                 Q.E.D.
  Step  : 5                                                 Q.E.D.
  Result:                                                   Q.E.D.
Lemma: a ⊓ (a ⊔ b) = a
  Step  : 1                                                 Q.E.D.
  Step  : 2                                                 Q.E.D.
  Step  : 3                                                 Q.E.D.
  Step  : 4                                                 Q.E.D.
  Step  : 5                                                 Q.E.D.
  Result:                                                   Q.E.D.
Lemma: a ⊓ a = a
  Step  : 1                                                 Q.E.D.
  Step  : 2                                                 Q.E.D.
  Result:                                                   Q.E.D.
Lemma: a ⊔ a' = т → a ⊓ a' = ⲳ → a' = aᶜ
  Step  : 1                                                 Q.E.D.
  Step  : 2                                                 Q.E.D.
  Step  : 3                                                 Q.E.D.
  Step  : 4                                                 Q.E.D.
  Step  : 5                                                 Q.E.D.
  Asms  : 6                                                 Q.E.D.
  Step  : 6                                                 Q.E.D.
  Step  : 7                                                 Q.E.D.
  Step  : 8                                                 Q.E.D.
  Step  : 9                                                 Q.E.D.
  Asms  : 10                                                Q.E.D.
  Step  : 10                                                Q.E.D.
  Step  : 11                                                Q.E.D.
  Result:                                                   Q.E.D.
Lemma: aᶜᶜ = a                                              Q.E.D.
Lemma: aᶜ = bᶜ → a = b                                      Q.E.D.
Lemma: a ⊔ bᶜ = т → a ⊓ bᶜ = ⲳ → a = b                      Q.E.D.
Lemma: a ⊔ (aᶜ ⊔ b) = т
  Step  : 1                                                 Q.E.D.
  Step  : 2                                                 Q.E.D.
  Step  : 3                                                 Q.E.D.
  Step  : 4                                                 Q.E.D.
  Step  : 5                                                 Q.E.D.
  Step  : 6                                                 Q.E.D.
  Result:                                                   Q.E.D.
Lemma: a ⊓ (aᶜ ⊓ b) = ⲳ
  Step  : 1                                                 Q.E.D.
  Step  : 2                                                 Q.E.D.
  Step  : 3                                                 Q.E.D.
  Step  : 4                                                 Q.E.D.
  Step  : 5                                                 Q.E.D.
  Step  : 6                                                 Q.E.D.
  Result:                                                   Q.E.D.
Lemma: (a ⊔ b)ᶜ = aᶜ ⊓ bᶜ                                   Q.E.D.
Lemma: (a ⨅ b)ᶜ = aᶜ ⨆ bᶜ                                   Q.E.D.
Lemma: (a ⊔ (b ⊔ c)) ⊔ aᶜ = т                               Q.E.D.
Lemma: b ⊓ (a ⊔ (b ⊔ c)) = b                                Q.E.D.
Lemma: b ⊔ (a ⊓ (b ⊓ c)) = b                                Q.E.D.
Lemma: (a ⊔ (b ⊔ c)) ⊔ bᶜ = т
  Step  : 1                                                 Q.E.D.
  Step  : 2                                                 Q.E.D.
  Step  : 3                                                 Q.E.D.
  Step  : 4                                                 Q.E.D.
  Step  : 5                                                 Q.E.D.
  Step  : 6                                                 Q.E.D.
  Step  : 7                                                 Q.E.D.
  Step  : 8                                                 Q.E.D.
  Step  : 9                                                 Q.E.D.
  Result:                                                   Q.E.D.
Lemma: (a ⊔ (b ⊔ c)) ⊔ cᶜ = т                               Q.E.D.
Lemma: (a ⊔ b ⊔ c)ᶜ ⊓ a = ⲳ
  Step  : 1                                                 Q.E.D.
  Step  : 2                                                 Q.E.D.
  Step  : 3                                                 Q.E.D.
  Step  : 4                                                 Q.E.D.
  Step  : 5                                                 Q.E.D.
  Step  : 6                                                 Q.E.D.
  Step  : 7                                                 Q.E.D.
  Step  : 8                                                 Q.E.D.
  Step  : 9                                                 Q.E.D.
  Result:                                                   Q.E.D.
Lemma: (a ⊔ b ⊔ c)ᶜ ⊓ b = ⲳ                                 Q.E.D.
Lemma: (a ⊔ b ⊔ c)ᶜ ⊓ c = ⲳ                                 Q.E.D.
Lemma: (a ⊔ (b ⊔ c)) ⊔ ((a ⊔ b) ⊔ c)ᶜ = т
  Step  : 1                                                 Q.E.D.
  Step  : 2                                                 Q.E.D.
  Step  : 3                                                 Q.E.D.
  Step  : 4                                                 Q.E.D.
  Step  : 5                                                 Q.E.D.
  Step  : 6                                                 Q.E.D.
  Step  : 7                                                 Q.E.D.
  Step  : 8                                                 Q.E.D.
  Result:                                                   Q.E.D.
Lemma: (a ⊔ (b ⊔ c)) ⊓ ((a ⊔ b) ⊔ c)ᶜ = ⲳ
  Step  : 1                                                 Q.E.D.
  Step  : 2                                                 Q.E.D.
  Step  : 3                                                 Q.E.D.
  Step  : 4                                                 Q.E.D.
  Step  : 5                                                 Q.E.D.
  Step  : 6                                                 Q.E.D.
  Step  : 7                                                 Q.E.D.
  Step  : 8                                                 Q.E.D.
  Step  : 9                                                 Q.E.D.
  Step  : 10                                                Q.E.D.
  Step  : 11                                                Q.E.D.
  Step  : 12                                                Q.E.D.
  Result:                                                   Q.E.D.
Lemma: a ⊔ (b ⊔ c) = (a ⊔ b) ⊔ c                            Q.E.D.
Lemma: a ⊓ (b ⊓ c) = (a ⊓ b) ⊓ c
  Step  : 1                                                 Q.E.D.
  Step  : 2                                                 Q.E.D.
  Step  : 3                                                 Q.E.D.
  Result:                                                   Q.E.D.
Lemma: a ≤ b → b ≤ a → a = b
  Asms  : 1                                                 Q.E.D.
  Step  : 1                                                 Q.E.D.
  Step  : 2                                                 Q.E.D.
  Asms  : 3                                                 Q.E.D.
  Step  : 3                                                 Q.E.D.
  Result:                                                   Q.E.D.
Lemma: a ≤ a                                                Q.E.D.
Lemma: a ≤ b → b ≤ c → a ≤ c
  Asms  : 1                                                 Q.E.D.
  Step  : 1                                                 Q.E.D.
  Asms  : 2                                                 Q.E.D.
  Step  : 2                                                 Q.E.D.
  Step  : 3                                                 Q.E.D.
  Asms  : 4                                                 Q.E.D.
  Step  : 4                                                 Q.E.D.
  Result:                                                   Q.E.D.
Lemma: a < b ↔ a ≤ b ∧ ¬b ≤ a                               Q.E.D.
Lemma: a ≤ a ⊔ b                                            Q.E.D.
Lemma: b ≤ a ⊔ b                                            Q.E.D.
Lemma: a ≤ c → b ≤ c → a ⊔ b ≤ c
  Asms  : 1                                                 Q.E.D.
  Step  : 1                                                 Q.E.D.
  Step  : 2                                                 Q.E.D.
  Result:                                                   Q.E.D.
Lemma: a ⊓ b ≤ a                                            Q.E.D.
Lemma: a ⊓ b ≤ b                                            Q.E.D.
Lemma: a ≤ b → a ≤ c → a ≤ b ⊓ c
  Asms  : 1                                                 Q.E.D.
  Step  : 1                                                 Q.E.D.
  Asms  : 2                                                 Q.E.D.
  Step  : 2                                                 Q.E.D.
  Step  : 3                                                 Q.E.D.
  Result:                                                   Q.E.D.
Lemma: (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z                        Q.E.D.
Lemma: x ⊓ xᶜ ≤ ⊥                                           Q.E.D.
Lemma: ⊤ ≤ x ⊔ xᶜ                                           Q.E.D.
Lemma: a ≤ ⊤
  Step  : 1                                                 Q.E.D.
  Step  : 2                                                 Q.E.D.
  Step  : 3                                                 Q.E.D.
  Result:                                                   Q.E.D.
Lemma: ⊥ ≤ a
  Step  : 1                                                 Q.E.D.
  Step  : 2                                                 Q.E.D.
  Result:                                                   Q.E.D.
Lemma: x \ y = x ⊓ yᶜ                                       Q.E.D.
Lemma: x ⇨ y = y ⊔ xᶜ                                       Q.E.D.
BooleanAlgebraProof {
  le_refl         : [Proven] a ≤ a
  le_trans        : [Proven] a ≤ b → b ≤ c → a ≤ c
  lt_iff_le_not_le: [Proven] a < b ↔ a ≤ b ∧ ¬b ≤ a
  le_antisymm     : [Proven] a ≤ b → b ≤ a → a = b
  le_sup_left     : [Proven] a ≤ a ⊔ b
  le_sup_right    : [Proven] b ≤ a ⊔ b
  sup_le          : [Proven] a ≤ c → b ≤ c → a ⊔ b ≤ c
  inf_le_left     : [Proven] a ⊓ b ≤ a
  inf_le_right    : [Proven] a ⊓ b ≤ b
  le_inf          : [Proven] a ≤ b → a ≤ c → a ≤ b ⊓ c
  le_sup_inf      : [Proven] (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
  inf_compl_le_bot: [Proven] x ⊓ xᶜ ≤ ⊥
  top_le_sup_compl: [Proven] ⊤ ≤ x ⊔ xᶜ
  le_top          : [Proven] a ≤ ⊤
  bot_le          : [Proven] ⊥ ≤ a
  sdiff_eq        : [Proven] x \ y = x ⊓ yᶜ
  himp_eq         : [Proven] x ⇨ y = y ⊔ xᶜ
}