sbv-14.1: Documentation/SBV/Examples/TP/ShefferStroke.hs
-----------------------------------------------------------------------------
-- |
-- Module : Documentation.SBV.Examples.TP.ShefferStroke
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- 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.
-----------------------------------------------------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeAbstractions #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.TP.ShefferStroke where
import Prelude hiding ((<))
import Data.List (intercalate)
import Data.SBV
import Data.SBV.TP
-- * Generalized Boolean Algebras
-- | 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.
class BooleanAlgebra α where
ﬧ :: α -> α
(⨆) :: α -> α -> α
(⨅) :: α -> α -> α
(≤) :: α -> α -> SBool
(<) :: α -> α -> SBool
(\\) :: α -> α -> α
(⇨) :: α -> α -> α
ⲳ :: α
т :: α
infix 4 ≤
infixl 6 ⨆
infixl 7 ⨅
-- | 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.
data BooleanAlgebraProof = BooleanAlgebraProof {
le_refl {- ∀ (a : α), a ≤ a -} :: Proof (Forall "a" Stroke -> SBool)
, le_trans {- ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c -} :: Proof (Forall "a" Stroke -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
, lt_iff_le_not_le {- (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) -} :: Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
, le_antisymm {- ∀ (a b : α), a ≤ b → b ≤ a → a = b -} :: Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
, le_sup_left {- ∀ (a b : α), a ≤ a ⊔ b -} :: Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
, le_sup_right {- ∀ (a b : α), b ≤ a ⊔ b -} :: Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
, sup_le {- ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c -} :: Proof (Forall "a" Stroke -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
, inf_le_left {- ∀ (a b : α), a ⊓ b ≤ a -} :: Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
, inf_le_right {- ∀ (a b : α), a ⊓ b ≤ b -} :: Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
, le_inf {- ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c -} :: Proof (Forall "a" Stroke -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
, le_sup_inf {- ∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z -} :: Proof (Forall "x" Stroke -> Forall "y" Stroke -> Forall "z" Stroke -> SBool)
, inf_compl_le_bot {- ∀ (x : α), x ⊓ xᶜ ≤ ⊥ -} :: Proof (Forall "x" Stroke -> SBool)
, top_le_sup_compl {- ∀ (x : α), ⊤ ≤ x ⊔ xᶜ -} :: Proof (Forall "x" Stroke -> SBool)
, le_top {- ∀ (a : α), a ≤ ⊤ -} :: Proof (Forall "a" Stroke -> SBool)
, bot_le {- ∀ (a : α), ⊥ ≤ a -} :: Proof (Forall "a" Stroke -> SBool)
, sdiff_eq {- (∀ (x y : α), x \ y = x ⊓ yᶜ) -} :: Proof (Forall "x" Stroke -> Forall "y" Stroke -> SBool)
, himp_eq {- (∀ (x y : α), x ⇨ y = y ⊔ xᶜ) -} :: Proof (Forall "x" Stroke -> Forall "y" Stroke -> SBool)
}
-- | A somewhat prettier printer for a BooleanAlgebra proof
instance Show BooleanAlgebraProof where
show p = intercalate "\n" [ "BooleanAlgebraProof {"
, " le_refl : " ++ show (le_refl p)
, " le_trans : " ++ show (le_trans p)
, " lt_iff_le_not_le: " ++ show (lt_iff_le_not_le p)
, " le_antisymm : " ++ show (le_antisymm p)
, " le_sup_left : " ++ show (le_sup_left p)
, " le_sup_right : " ++ show (le_sup_right p)
, " sup_le : " ++ show (sup_le p)
, " inf_le_left : " ++ show (inf_le_left p)
, " inf_le_right : " ++ show (inf_le_right p)
, " le_inf : " ++ show (le_inf p)
, " le_sup_inf : " ++ show (le_sup_inf p)
, " inf_compl_le_bot: " ++ show (inf_compl_le_bot p)
, " top_le_sup_compl: " ++ show (top_le_sup_compl p)
, " le_top : " ++ show (le_top p)
, " bot_le : " ++ show (bot_le p)
, " sdiff_eq : " ++ show (sdiff_eq p)
, " himp_eq : " ++ show (himp_eq p)
, "}"
]
-- * The sheffer stroke
-- | The abstract type for the domain.
data Stroke
mkSymbolic [''Stroke]
-- | The sheffer stroke operator.
(⏐) :: SStroke -> SStroke -> SStroke
(⏐) = uninterpret "⏐"
infixl 7 ⏐
-- | The boolean algebra of the sheffer stroke.
instance BooleanAlgebra SStroke where
ﬧ x = x ⏐ x
a ⨆ b = ﬧ(a ⏐ b)
a ⨅ b = ﬧ a ⏐ ﬧ b
a ≤ b = a .== b ⨅ a
a < b = a ≤ b .&& a ./= b
a \\ b = a ⨅ ﬧ b
a ⇨ b = b ⨆ ﬧ a
ⲳ = arb ⏐ ﬧ arb where arb = some "ⲳ" (const sTrue)
т = ﬧ ⲳ
-- | Double-negation
ﬧﬧ :: BooleanAlgebra a => a -> a
ﬧﬧ = ﬧ . ﬧ
-- | First Sheffer axiom: @ﬧﬧa == a@
sheffer1 :: TP (Proof (Forall "a" Stroke -> SBool))
sheffer1 = axiom "ﬧﬧa == a" $ \(Forall a) -> ﬧﬧ a .== a
-- | Second Sheffer axiom: @a ⏐ (b ⏐ ﬧb) == ﬧa@
sheffer2 :: TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
sheffer2 = axiom "a ⏐ (b ⏐ ﬧb) == ﬧa" $ \(Forall a) (Forall b) -> a ⏐ (b ⏐ ﬧ b) .== ﬧ a
-- | Third Sheffer axiom: @ﬧ(a ⏐ (b ⏐ c)) == (ﬧb ⏐ a) ⏐ (ﬧc ⏐ a)@
sheffer3 :: TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
sheffer3 = axiom "ﬧ(a ⏐ (b ⏐ c)) == (ﬧb ⏐ a) ⏐ (ﬧc ⏐ a)" $ \(Forall a) (Forall b) (Forall c) -> ﬧ(a ⏐ (b ⏐ c)) .== (ﬧ b ⏐ a) ⏐ (ﬧ c ⏐ a)
-- * Sheffer's stroke defines a boolean algebra
-- | 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 (ﬧﬧa == a) Q.E.D.
-- Step: 2 (ﬧﬧa == a) Q.E.D.
-- Step: 3 Q.E.D.
-- Step: 4 (ﬧ(a ⏐ (b ⏐ c)) == (ﬧb ⏐ a) ⏐ (ﬧc ⏐ a)) Q.E.D.
-- Step: 5 Q.E.D.
-- Step: 6 (ﬧﬧa == a) Q.E.D.
-- Step: 7 (ﬧﬧa == a) Q.E.D.
-- Result: Q.E.D.
-- Lemma: a | a′ = b | b′
-- Step: 1 (ﬧﬧa == a) Q.E.D.
-- Step: 2 (a ⏐ (b ⏐ ﬧb) == ﬧa) Q.E.D.
-- Step: 3 Q.E.D.
-- Step: 4 (a ⏐ (b ⏐ ﬧb) == ﬧa) Q.E.D.
-- Step: 5 (ﬧﬧa == a) 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.
-- 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.
-- 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
-- Step: 1 Q.E.D.
-- Step: 2 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
-- 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: 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
-- 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
-- Step: 1 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 :: Ɐa ∷ Stroke → Bool
-- le_trans : [Proven] a ≤ b → b ≤ c → a ≤ c :: Ɐa ∷ Stroke → Ɐb ∷ Stroke → Ɐc ∷ Stroke → Bool
-- lt_iff_le_not_le: [Proven] a < b ↔ a ≤ b ∧ ¬b ≤ a :: Ɐa ∷ Stroke → Ɐb ∷ Stroke → Bool
-- le_antisymm : [Proven] a ≤ b → b ≤ a → a = b :: Ɐa ∷ Stroke → Ɐb ∷ Stroke → Bool
-- le_sup_left : [Proven] a ≤ a ⊔ b :: Ɐa ∷ Stroke → Ɐb ∷ Stroke → Bool
-- le_sup_right : [Proven] b ≤ a ⊔ b :: Ɐa ∷ Stroke → Ɐb ∷ Stroke → Bool
-- sup_le : [Proven] a ≤ c → b ≤ c → a ⊔ b ≤ c :: Ɐa ∷ Stroke → Ɐb ∷ Stroke → Ɐc ∷ Stroke → Bool
-- inf_le_left : [Proven] a ⊓ b ≤ a :: Ɐa ∷ Stroke → Ɐb ∷ Stroke → Bool
-- inf_le_right : [Proven] a ⊓ b ≤ b :: Ɐa ∷ Stroke → Ɐb ∷ Stroke → Bool
-- le_inf : [Proven] a ≤ b → a ≤ c → a ≤ b ⊓ c :: Ɐa ∷ Stroke → Ɐb ∷ Stroke → Ɐc ∷ Stroke → Bool
-- le_sup_inf : [Proven] (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z :: Ɐx ∷ Stroke → Ɐy ∷ Stroke → Ɐz ∷ Stroke → Bool
-- inf_compl_le_bot: [Proven] x ⊓ xᶜ ≤ ⊥ :: Ɐx ∷ Stroke → Bool
-- top_le_sup_compl: [Proven] ⊤ ≤ x ⊔ xᶜ :: Ɐx ∷ Stroke → Bool
-- le_top : [Proven] a ≤ ⊤ :: Ɐa ∷ Stroke → Bool
-- bot_le : [Proven] ⊥ ≤ a :: Ɐa ∷ Stroke → Bool
-- sdiff_eq : [Proven] x \ y = x ⊓ yᶜ :: Ɐx ∷ Stroke → Ɐy ∷ Stroke → Bool
-- himp_eq : [Proven] x ⇨ y = y ⊔ xᶜ :: Ɐx ∷ Stroke → Ɐy ∷ Stroke → Bool
-- }
shefferBooleanAlgebra :: IO BooleanAlgebraProof
shefferBooleanAlgebra = runTP $ do
-- shorthand
let p = proofOf
-- Get the axioms
sh1 <- sheffer1
sh2 <- sheffer2
sh3 <- sheffer3
commut <- calc "a | b = b | a" (\(Forall @"a" a) (Forall @"b" b) -> a ⏐ b .== b ⏐ a) $
\a b -> [] ⊢ a ⏐ b ∵ sh1
≡ ﬧﬧ(a ⏐ b) ∵ sh1
≡ ﬧﬧ(a ⏐ ﬧﬧ b)
≡ ﬧﬧ(a ⏐ (ﬧ b ⏐ ﬧ b)) ∵ sh3
≡ ﬧ ((ﬧﬧ b ⏐ a) ⏐ (ﬧﬧ b ⏐ a))
≡ ﬧﬧ(ﬧﬧ b ⏐ a) ∵ sh1
≡ ﬧﬧ b ⏐ a ∵ sh1
≡ b ⏐ a
≡ qed
all_bot <- calc "a | a′ = b | b′" (\(Forall @"a" a) (Forall @"b" b) -> a ⏐ ﬧ a .== b ⏐ ﬧ b) $
\a b -> [] ⊢ a ⏐ ﬧ a ∵ sh1
≡ ﬧﬧ(a ⏐ ﬧ a) ∵ sh2
≡ ﬧ((a ⏐ ﬧ a) ⏐ (b ⏐ ﬧ b)) ∵ commut
≡ ﬧ((b ⏐ ﬧ b) ⏐ (a ⏐ ﬧ a)) ∵ sh2
≡ ﬧﬧ (b ⏐ ﬧ b) ∵ sh1
≡ b ⏐ ﬧ b
≡ qed
commut1 <- lemma "a ⊔ b = b ⊔ a" (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) -> a ⨆ b .== b ⨆ a) [p commut]
commut2 <- lemma "a ⊓ b = b ⊓ a" (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) -> a ⨅ b .== b ⨅ a) [p commut]
ident1 <- lemma "a ⊔ ⲳ = a" (\(Forall @"a" (a :: SStroke)) -> a ⨆ ⲳ .== a) [p sh1, p sh2]
ident2 <- lemma "a ⊓ т = a" (\(Forall @"a" (a :: SStroke)) -> a ⨅ т .== a) [p sh1, p sh2]
distrib1 <- lemma "a ⊔ (b ⊓ c) = (a ⊔ b) ⊓ (a ⊔ c)"
(\(Forall @"a" (a :: SStroke)) (Forall @"b" b) (Forall @"c" c) -> a ⨆ (b ⨅ c) .== (a ⨆ b) ⨅ (a ⨆ c))
[p sh1, p sh3, p commut]
distrib2 <- lemma "a ⊓ (b ⊔ c) = (a ⊓ b) ⊔ (a ⊓ c)"
(\(Forall @"a" (a :: SStroke)) (Forall @"b" b) (Forall @"c" c) -> a ⨅ (b ⨆ c) .== (a ⨅ b) ⨆ (a ⨅ c))
[p sh1, p sh3, p commut]
compl1 <- lemma "a ⊔ aᶜ = т" (\(Forall @"a" (a :: SStroke)) -> a ⨆ ﬧ a .== т) [p sh1, p sh2, p sh3, p all_bot]
compl2 <- lemma "a ⊓ aᶜ = ⲳ" (\(Forall @"a" (a :: SStroke)) -> a ⨅ ﬧ a .== ⲳ) [p sh1, p commut, p all_bot]
bound1 <- calc "a ⊔ т = т" (\(Forall @"a" a) -> a ⨆ т .== т) $
\a -> [] ⊢ a ⨆ т ∵ ident2
≡ (a ⨆ т) ⨅ т ∵ commut2
≡ т ⨅ (a ⨆ т) ∵ compl1
≡ (a ⨆ ﬧ a) ⨅ (a ⨆ т) ∵ distrib1
≡ a ⨆ (ﬧ a ⨅ т) ∵ ident2
≡ a ⨆ ﬧ a ∵ compl1
≡ (т :: SStroke)
≡ qed
bound2 <- calc "a ⊓ ⲳ = ⲳ" (\(Forall @"a" a) -> a ⨅ ⲳ .== ⲳ) $
\a -> [] ⊢ a ⨅ ⲳ ∵ ident1
≡ (a ⨅ ⲳ) ⨆ ⲳ ∵ commut1
≡ ⲳ ⨆ (a ⨅ ⲳ) ∵ compl2
≡ (a ⨅ ﬧ a) ⨆ (a ⨅ ⲳ) ∵ distrib2
≡ a ⨅ (ﬧ a ⨆ ⲳ) ∵ ident1
≡ a ⨅ ﬧ a ∵ compl2
≡ (ⲳ :: SStroke)
≡ qed
absorb1 <- calc "a ⊔ (a ⊓ b) = a" (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) -> a ⨆ (a ⨅ b) .== a) $
\a b -> [] ⊢ a ⨆ (a ⨅ b) ∵ ident2
≡ (a ⨅ т) ⨆ (a ⨅ b) ∵ distrib2
≡ a ⨅ (т ⨆ b) ∵ commut1
≡ a ⨅ (b ⨆ т) ∵ bound1
≡ a ⨅ т ∵ ident2
≡ a
≡ qed
absorb2 <- calc "a ⊓ (a ⊔ b) = a" (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) -> a ⨅ (a ⨆ b) .== a) $
\a b -> [] ⊢ a ⨅ (a ⨆ b) ∵ ident1
≡ (a ⨆ ⲳ) ⨅ (a ⨆ b) ∵ distrib1
≡ a ⨆ (ⲳ ⨅ b) ∵ commut2
≡ a ⨆ (b ⨅ ⲳ) ∵ bound2
≡ a ⨆ ⲳ ∵ ident1
≡ a
≡ qed
idemp2 <- calc "a ⊓ a = a" (\(Forall @"a" (a :: SStroke)) -> a ⨅ a .== a) $
\a -> [] ⊢ a ⨅ a ∵ ident1
≡ a ⨅ (a ⨆ ⲳ) ∵ absorb2
≡ a
≡ qed
inv <- calc "a ⊔ a' = т → a ⊓ a' = ⲳ → a' = aᶜ"
(\(Forall @"a" (a :: SStroke)) (Forall @"a'" a') -> a ⨆ a' .== т .=> a ⨅ a' .== ⲳ .=> a' .== ﬧ a) $
\a a' -> [a ⨆ a' .== т, a ⨅ a' .== ⲳ] ⊢ a' ∵ ident2
≡ a' ⨅ т ∵ compl1
≡ a' ⨅ (a ⨆ ﬧ a) ∵ distrib2
≡ (a' ⨅ a) ⨆ (a' ⨅ ﬧ a) ∵ commut2
≡ (a' ⨅ a) ⨆ (ﬧ a ⨅ a') ∵ commut2
≡ (a ⨅ a') ⨆ (ﬧ a ⨅ a') ∵ a ⨅ a' .== ⲳ
≡ ⲳ ⨆ (ﬧ a ⨅ a') ∵ compl2
≡ (a ⨅ ﬧ a) ⨆ (ﬧ a ⨅ a') ∵ commut2
≡ (ﬧ a ⨅ a) ⨆ (ﬧ a ⨅ a') ∵ distrib2
≡ ﬧ a ⨅ (a ⨆ a') ∵ a ⨆ a' .== т
≡ ﬧ a ⨅ т ∵ ident2
≡ ﬧ a
≡ qed
dne <- lemma "aᶜᶜ = a"
(\(Forall @"a" (a :: SStroke)) -> ﬧﬧ a .== a)
[p inv, p compl1, p compl2, p commut1, p commut2]
inv_elim <- lemma "aᶜ = bᶜ → a = b"
(\(Forall @"a" (a :: SStroke)) (Forall @"b" b) -> ﬧ a .== ﬧ b .=> a .== b)
[p dne]
cancel <- lemma "a ⊔ bᶜ = т → a ⊓ bᶜ = ⲳ → a = b"
(\(Forall @"a" (a :: SStroke)) (Forall @"b" b) -> a ⨆ ﬧ b .== т .=> a ⨅ ﬧ b .== ⲳ .=> a .== b)
[p inv, p inv_elim]
a1 <- calc "a ⊔ (aᶜ ⊔ b) = т" (\(Forall @"a" a) (Forall @"b" b) -> a ⨆ (ﬧ a ⨆ b) .== т) $
\a b -> [] ⊢ a ⨆ (ﬧ a ⨆ b) ∵ ident2
≡ (a ⨆ (ﬧ a ⨆ b)) ⨅ т ∵ commut2
≡ т ⨅ (a ⨆ (ﬧ a ⨆ b)) ∵ compl1
≡ (a ⨆ ﬧ a) ⨅ (a ⨆ (ﬧ a ⨆ b)) ∵ distrib1
≡ a ⨆ (ﬧ a ⨅ (ﬧ a ⨆ b)) ∵ absorb2
≡ a ⨆ ﬧ a ∵ compl1
≡ (т :: SStroke)
≡ qed
a2 <- calc "a ⊓ (aᶜ ⊓ b) = ⲳ" (\(Forall @"a" a) (Forall @"b" b) -> a ⨅ (ﬧ a ⨅ b) .== ⲳ) $
\a b -> [] ⊢ a ⨅ (ﬧ a ⨅ b) ∵ ident1
≡ (a ⨅ (ﬧ a ⨅ b)) ⨆ ⲳ ∵ commut1
≡ ⲳ ⨆ (a ⨅ (ﬧ a ⨅ b)) ∵ compl2
≡ (a ⨅ ﬧ a) ⨆ (a ⨅ (ﬧ a ⨅ b)) ∵ distrib2
≡ a ⨅ (ﬧ a ⨆ (ﬧ a ⨅ b)) ∵ absorb1
≡ a ⨅ ﬧ a ∵ compl2
≡ (ⲳ :: SStroke)
≡ qed
dm1 <- lemma "(a ⊔ b)ᶜ = aᶜ ⊓ bᶜ"
(\(Forall @"a" (a :: SStroke)) (Forall @"b" b) -> ﬧ(a ⨆ b) .== ﬧ a ⨅ ﬧ b)
[p a1, p a2, p dne, p commut1, p commut2, p ident1, p ident2, p distrib1, p distrib2]
dm2 <- lemma "(a ⨅ b)ᶜ = aᶜ ⨆ bᶜ"
(\(Forall @"a" (a :: SStroke)) (Forall @"b" b) -> ﬧ(a ⨅ b) .== ﬧ a ⨆ ﬧ b)
[p a1, p a2, p dne, p commut1, p commut2, p ident1, p ident2, p distrib1, p distrib2]
d1 <- lemma "(a ⊔ (b ⊔ c)) ⊔ aᶜ = т"
(\(Forall @"a" (a :: SStroke)) (Forall @"b" b) (Forall @"c" c) -> (a ⨆ (b ⨆ c)) ⨆ ﬧ a .== т)
[p a1, p a2, p commut1, p ident1, p ident2, p distrib1, p compl1, p compl2, p dm1, p dm2, p idemp2]
e1 <- lemma "b ⊓ (a ⊔ (b ⊔ c)) = b"
(\(Forall @"a" (a :: SStroke)) (Forall @"b" b) (Forall @"c" c) -> b ⨅ (a ⨆ (b ⨆ c)) .== b)
[p distrib2, p absorb1, p absorb2, p commut1]
e2 <- lemma "b ⊔ (a ⊓ (b ⊓ c)) = b" (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) (Forall @"c" c) -> b ⨆ (a ⨅ (b ⨅ c)) .== b) [p distrib1, p absorb1, p absorb2, p commut2]
f1 <- calc "(a ⊔ (b ⊔ c)) ⊔ bᶜ = т" (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) (Forall @"c" c) -> (a ⨆ (b ⨆ c)) ⨆ ﬧ b .== т) $
\a b c -> [] ⊢ (a ⨆ (b ⨆ c)) ⨆ ﬧ b ∵ commut1
≡ ﬧ b ⨆ (a ⨆ (b ⨆ c)) ∵ ident2
≡ (ﬧ b ⨆ (a ⨆ (b ⨆ c))) ⨅ т ∵ commut2
≡ т ⨅ (ﬧ b ⨆ (a ⨆ (b ⨆ c))) ∵ compl1
≡ (b ⨆ ﬧ b) ⨅ (ﬧ b ⨆ (a ⨆ (b ⨆ c))) ∵ commut1
≡ (ﬧ b ⨆ b) ⨅ (ﬧ b ⨆ (a ⨆ (b ⨆ c))) ∵ distrib1
≡ ﬧ b ⨆ (b ⨅ (a ⨆ (b ⨆ c))) ∵ e1
≡ ﬧ b ⨆ b ∵ commut1
≡ b ⨆ ﬧ b ∵ compl1
≡ (т :: SStroke)
≡ qed
g1 <- lemma "(a ⊔ (b ⊔ c)) ⊔ cᶜ = т"
(\(Forall @"a" (a :: SStroke)) (Forall @"b" b) (Forall @"c" c) -> (a ⨆ (b ⨆ c)) ⨆ ﬧ c .== т)
[p commut1, p f1]
h1 <- calc "(a ⊔ b ⊔ c)ᶜ ⊓ a = ⲳ"
(\(Forall @"a" (a :: SStroke)) (Forall @"b" b) (Forall @"c" c) -> ﬧ(a ⨆ b ⨆ c) ⨅ a .== ⲳ) $
\a b c -> [] ⊢ ﬧ(a ⨆ b ⨆ c) ⨅ a ∵ commut2
≡ a ⨅ ﬧ (a ⨆ b ⨆ c) ∵ dm1
≡ a ⨅ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c) ∵ ident1
≡ (a ⨅ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c)) ⨆ ⲳ ∵ commut1
≡ ⲳ ⨆ (a ⨅ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c)) ∵ compl2
≡ (a ⨅ ﬧ a) ⨆ (a ⨅ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c)) ∵ distrib2
≡ a ⨅ (ﬧ a ⨆ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c)) ∵ commut2
≡ a ⨅ (ﬧ a ⨆ (ﬧ c ⨅ (ﬧ a ⨅ ﬧ b))) ∵ e2
≡ a ⨅ ﬧ a ∵ compl2
≡ (ⲳ :: SStroke)
≡ qed
i1 <- lemma "(a ⊔ b ⊔ c)ᶜ ⊓ b = ⲳ"
(\(Forall @"a" (a :: SStroke)) (Forall @"b" b) (Forall @"c" c) -> ﬧ(a ⨆ b ⨆ c) ⨅ b .== ⲳ)
[p commut1, p h1]
j1 <- lemma "(a ⊔ b ⊔ c)ᶜ ⊓ c = ⲳ"
(\(Forall @"a" (a :: SStroke)) (Forall @"b" b) (Forall @"c" c) -> ﬧ(a ⨆ b ⨆ c) ⨅ c .== ⲳ)
[p a2, p dne, p commut2]
assoc1 <- do
c1 <- calc "(a ⊔ (b ⊔ c)) ⊔ ((a ⊔ b) ⊔ c)ᶜ = т"
(\(Forall @"a" (a :: SStroke)) (Forall @"b" b) (Forall @"c" c) -> (a ⨆ (b ⨆ c)) ⨆ ﬧ((a ⨆ b) ⨆ c) .== т) $
\a b c -> [] ⊢ (a ⨆ (b ⨆ c)) ⨆ ﬧ((a ⨆ b) ⨆ c) ∵ dm1
≡ (a ⨆ (b ⨆ c)) ⨆ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c) ∵ distrib1
≡ ((a ⨆ (b ⨆ c)) ⨆ (ﬧ a ⨅ ﬧ b)) ⨅ ((a ⨆ (b ⨆ c)) ⨆ ﬧ c) ∵ g1
≡ ((a ⨆ (b ⨆ c)) ⨆ (ﬧ a ⨅ ﬧ b)) ⨅ т ∵ ident2
≡ (a ⨆ (b ⨆ c)) ⨆ (ﬧ a ⨅ ﬧ b) ∵ distrib1
≡ ((a ⨆ (b ⨆ c)) ⨆ ﬧ a) ⨅ ((a ⨆ (b ⨆ c)) ⨆ ﬧ b) ∵ d1
≡ т ⨅ ((a ⨆ (b ⨆ c)) ⨆ ﬧ b) ∵ f1
≡ (т ⨅ т :: SStroke) ∵ idemp2
≡ (т :: SStroke)
≡ qed
c2 <- calc "(a ⊔ (b ⊔ c)) ⊓ ((a ⊔ b) ⊔ c)ᶜ = ⲳ"
(\(Forall @"a" (a :: SStroke)) (Forall @"b" b) (Forall @"c" c) -> (a ⨆ (b ⨆ c)) ⨅ ﬧ((a ⨆ b) ⨆ c) .== ⲳ) $
\a b c -> [] ⊢ (a ⨆ (b ⨆ c)) ⨅ ﬧ((a ⨆ b) ⨆ c) ∵ commut2
≡ ﬧ((a ⨆ b) ⨆ c) ⨅ (a ⨆ (b ⨆ c)) ∵ distrib2
≡ (ﬧ((a ⨆ b) ⨆ c) ⨅ a) ⨆ (ﬧ((a ⨆ b) ⨆ c) ⨅ (b ⨆ c)) ∵ commut2
≡ (a ⨅ ﬧ((a ⨆ b) ⨆ c)) ⨆ ((b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c)) ∵ commut2
≡ (ﬧ((a ⨆ b) ⨆ c) ⨅ a) ⨆ ((b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c)) ∵ h1
≡ ⲳ ⨆ ((b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c)) ∵ commut1
≡ ((b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c)) ⨆ ⲳ ∵ ident1
≡ (b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c) ∵ commut2
≡ ﬧ((a ⨆ b) ⨆ c) ⨅ (b ⨆ c) ∵ distrib2
≡ (ﬧ((a ⨆ b) ⨆ c) ⨅ b) ⨆ (ﬧ((a ⨆ b) ⨆ c) ⨅ c) ∵ j1
≡ (ﬧ((a ⨆ b) ⨆ c) ⨅ b) ⨆ ⲳ ∵ i1
≡ (ⲳ ⨆ ⲳ :: SStroke) ∵ ident1
≡ (ⲳ :: SStroke)
≡ qed
lemma "a ⊔ (b ⊔ c) = (a ⊔ b) ⊔ c"
(\(Forall @"a" (a :: SStroke)) (Forall @"b" b) (Forall @"c" c) -> a ⨆ (b ⨆ c) .== (a ⨆ b) ⨆ c)
[p c1, p c2, p cancel]
assoc2 <- calc "a ⊓ (b ⊓ c) = (a ⊓ b) ⊓ c"
(\(Forall @"a" (a :: SStroke)) (Forall @"b" b) (Forall @"c" c) -> a ⨅ (b ⨅ c) .== (a ⨅ b) ⨅ c) $
\a b c -> [] ⊢ a ⨅ (b ⨅ c) ∵ dne
≡ ﬧﬧ(a ⨅ (b ⨅ c)) ∵ assoc1
≡ ﬧﬧ((a ⨅ b) ⨅ c) ∵ dne
≡ ((a ⨅ b) ⨅ c)
≡ qed
le_antisymm <- calc "a ≤ b → b ≤ a → a = b"
(\(Forall @"a" a) (Forall @"b" b) -> a ≤ b .=> b ≤ a .=> a .== b) $
\a b -> [a ≤ b, b ≤ a] ⊢ a ∵ a ≤ b
≡ b ⨅ a ∵ commut2
≡ a ⨅ b ∵ b ≤ a
≡ b
≡ qed
le_refl <- lemma "a ≤ a" (\(Forall @"a" a) -> a ≤ a) [p idemp2]
le_trans <- calc "a ≤ b → b ≤ c → a ≤ c" (\(Forall a) (Forall b) (Forall c) -> a ≤ b .=> b ≤ c .=> a ≤ c) $
\a b c -> [a ≤ b, b ≤ c] ⊢ a ∵ a ≤ b
≡ b ⨅ a ∵ b ≤ c
≡ (c ⨅ b) ⨅ a ∵ assoc2
≡ c ⨅ (b ⨅ a) ∵ a ≤ b
≡ (c ⨅ a)
≡ qed
lt_iff_le_not_le <- lemma "a < b ↔ a ≤ b ∧ ¬b ≤ a"
(\(Forall @"a" (a :: SStroke)) (Forall @"b" b) -> (a < b) .<=> a ≤ b .&& sNot (b ≤ a))
[p sh3]
le_sup_left <- lemma "a ≤ a ⊔ b"
(\(Forall @"a" (a :: SStroke)) (Forall @"b" b) -> a ≤ a ⨆ b)
[p commut1, p commut2, p absorb2]
le_sup_right <- lemma "b ≤ a ⊔ b"
(\(Forall @"a" (a :: SStroke)) (Forall @"b" b) -> a ≤ a ⨆ b)
[p commut1, p commut2, p absorb2]
sup_le <- calc "a ≤ c → b ≤ c → a ⊔ b ≤ c"
(\(Forall a) (Forall b) (Forall c) -> a ≤ c .=> b ≤ c .=> a ⨆ b ≤ c) $
\a b c -> [a ≤ c, b ≤ c] ⊢ a ⨆ b ∵ [a ≤ c, b ≤ c]
≡ (c ⨅ a) ⨆ (c ⨅ b) ∵ distrib2
≡ c ⨅ (a ⨆ b)
≡ qed
inf_le_left <- lemma "a ⊓ b ≤ a"
(\(Forall @"a" (a :: SStroke)) (Forall @"b" b) -> a ⨅ b ≤ a)
[p assoc2, p idemp2]
inf_le_right <- lemma "a ⊓ b ≤ b"
(\(Forall @"a" (a :: SStroke)) (Forall @"b" b) -> a ⨅ b ≤ b)
[p commut2, p inf_le_left]
le_inf <- calc "a ≤ b → a ≤ c → a ≤ b ⊓ c"
(\(Forall a) (Forall b) (Forall c) -> a ≤ b .=> a ≤ c .=> a ≤ b ⨅ c) $
\a b c -> [a ≤ b, a ≤ c] ⊢ a ∵ a ≤ b
≡ b ⨅ a ∵ a ≤ c
≡ b ⨅ (c ⨅ a) ∵ assoc2
≡ (b ⨅ c ⨅ a)
≡ qed
le_sup_inf <- lemma "(x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z"
(\(Forall x) (Forall y) (Forall z) -> (x ⨆ y) ⨅ (x ⨆ z) ≤ x ⨆ y ⨅ z)
[p distrib1, p le_refl]
inf_compl_le_bot <- lemma "x ⊓ xᶜ ≤ ⊥" (\(Forall x) -> x ⨅ ﬧ x ≤ ⲳ) [p compl2, p le_refl]
top_le_sup_compl <- lemma "⊤ ≤ x ⊔ xᶜ" (\(Forall x) -> т ≤ x ⨆ ﬧ x) [p compl1, p le_refl]
le_top <- calc "a ≤ ⊤" (\(Forall @"a" a) -> a ≤ т) $
\a -> [] ⊢ a ≤ т
≡ a .== т ⨅ a ∵ commut2
≡ a .== a ⨅ т ∵ ident2
≡ a .== a
≡ qed
bot_le <- calc "⊥ ≤ a" (\(Forall @"a" a) -> ⲳ ≤ a) $
\a -> [] ⊢ ⲳ ≤ a
≡ ⲳ .== a ⨅ ⲳ ∵ bound2
≡ ⲳ .== (ⲳ :: SStroke)
≡ qed
sdiff_eq <- lemma "x \\ y = x ⊓ yᶜ" (\(Forall x) (Forall y) -> x \\ y .== x ⨅ ﬧ y) []
himp_eq <- lemma "x ⇨ y = y ⊔ xᶜ" (\(Forall x) (Forall y) -> x ⇨ y .== y ⨆ ﬧ x) []
pure BooleanAlgebraProof {
le_refl {- ∀ (a : α), a ≤ a -} = le_refl
, le_trans {- ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c -} = le_trans
, lt_iff_le_not_le {- (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) -} = lt_iff_le_not_le
, le_antisymm {- ∀ (a b : α), a ≤ b → b ≤ a → a = b -} = le_antisymm
, le_sup_left {- ∀ (a b : α), a ≤ a ⊔ b -} = le_sup_left
, le_sup_right {- ∀ (a b : α), b ≤ a ⊔ b -} = le_sup_right
, sup_le {- ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c -} = sup_le
, inf_le_left {- ∀ (a b : α), a ⊓ b ≤ a -} = inf_le_left
, inf_le_right {- ∀ (a b : α), a ⊓ b ≤ b -} = inf_le_right
, le_inf {- ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c -} = le_inf
, le_sup_inf {- ∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z -} = le_sup_inf
, inf_compl_le_bot {- ∀ (x : α), x ⊓ xᶜ ≤ ⊥ -} = inf_compl_le_bot
, top_le_sup_compl {- ∀ (x : α), ⊤ ≤ x ⊔ xᶜ -} = top_le_sup_compl
, le_top {- ∀ (a : α), a ≤ ⊤ -} = le_top
, bot_le {- ∀ (a : α), ⊥ ≤ a -} = bot_le
, sdiff_eq {- (∀ (x y : α), x \ y = x ⊓ yᶜ) -} = sdiff_eq
, himp_eq {- (∀ (x y : α), x ⇨ y = y ⊔ xᶜ) -} = himp_eq
}