src/Logic/Theory/Bool.hs

   1 {-# LANGUAGE Safe #-}
   2 -- For `axiom`
   3 {-# OPTIONS_GHC -Wno-deprecations #-}
   4 {-# OPTIONS_GHC -Wno-orphans #-}
   5 {-# OPTIONS_GHC -Wno-unused-top-binds #-}
   6
   7 module Logic.Theory.Bool (
   8   true,
   9   implies,
  10   unImplies,
  11   type True,
  12   type False,
  13   type (&&),
  14   andL,
  15   andR,
  16   unAnd,
  17   type (||),
  18   type UnOr,
  19   runOr,
  20   leftOr,
  21   rightOr,
  22   unOr,
  23   unOrL,
  24   unOrR,
  25   type Not (),
  26   type NotAsNonExistent,
  27   modusTollens,
  28   absurd,
  29   and,
  30   not,
  31   type NonContradiction,
  32   contradicts,
  33   type ExcludedMiddle,
  34 )
  35 where
  36
  37 import Control.Applicative (Applicative (..), liftA3)
  38 import Control.Monad (Monad (..))
  39 import Data.Either (Either (..), either)
  40 import Data.Function (id, (.))
  41 import Data.Functor ((<$>))
  42 import Data.Tuple (fst, snd)
  43 import Data.Void (Void)
  44 import Data.Void qualified as Void
  45
  46 import Logic.Kernel
  47
  48 true :: Proof True
  49 true = pure ()
  50 {-# INLINE true #-}
  51
  52 type False = Void
  53
  54 -- | From a falsity, prove anything.
  55 -- (aka. ex falso quodlibet).
  56 absurd :: False -> p
  57 absurd = Void.absurd
  58 {-# INLINE absurd #-}
  59
  60 type True = ()
  61
  62 -- The conjunction in the logic side,
  63 -- is the product type in the programming side.
  64 type (&&) = (,)
  65 infixl 3 &&
  66
  67 and :: Proof p -> Proof q -> Proof (p && q)
  68 and = liftA2 (,)
  69 {-# INLINE and #-}
  70
  71 andL :: Proof (p && q) -> Proof p
  72 andL = (<$>) fst
  73
  74 andR :: Proof (p && q) -> Proof q
  75 andR = (<$>) snd
  76
  77 unAnd :: Proof (p && q) -> (Proof p, Proof q)
  78 unAnd c = (andL c, andR c)
  79
  80 -- The disjunction in the logic side,
  81 -- is the sum type in the programming side.
  82 type (||) = Either
  83 infixl 2 ||
  84
  85 leftOr :: Proof p -> Proof (p || q)
  86 leftOr = (<$>) Left
  87
  88 rightOr :: Proof q -> Proof (p || q)
  89 rightOr = (<$>) Right
  90
  91 type UnOr p q r = (p -> r) -> (q -> r) -> (p || q) -> r
  92 instance Lemma (UnOr p q r) where
  93   lemma = pure runOr
  94
  95 runOr :: UnOr p q r
  96 runOr = either
  97
  98 unOr :: (Proof p -> Proof r) -> (Proof q -> Proof r) -> Proof (p || q) -> Proof r
  99 unOr p2r q2r = (>>= either (p2r . pure) (q2r . pure))
 100
 101 unOrL :: (Proof p -> Proof r) -> Proof (p || q) -> (Proof q -> Proof r) -> Proof r
 102 unOrL p2r poq q2r = unOr p2r q2r poq
 103
 104 unOrR :: (Proof q -> Proof r) -> Proof (p || q) -> (Proof p -> Proof r) -> Proof r
 105 unOrR q2r poq p2r = unOr p2r q2r poq
 106
 107 -- | CorrectnessNote: the existence of a construction of @(`Not` p)@ is much stronger
 108 -- than the non-existence of a construction of @(p)@.
 109 newtype Not p = Not ()
 110
 111 -- | A construction of @(`Not` p)@, treated like @(p `->` `False`)@,
 112 -- is an algorithm that, from a (hypothetical) construction of @(p)@
 113 -- produces a non-existent object.
 114 type NotAsNonExistent p = Not p <-> (p -> False)
 115
 116 instance Axiom (NotAsNonExistent p)
 117
 118 -- | contraprositive
 119 not :: (Proof p -> Proof False) -> Proof (Not p)
 120 not f = liftA2 (<--) (axiom @(NotAsNonExistent _)) (implies f)
 121 {-# INLINE not #-}
 122
 123 modusTollens :: Proof (p -> q) -> Proof (Not q) -> Proof (Not p)
 124 modusTollens p2qP nqP = not (contradicts nqP . unImplies p2qP)
 125 {-# INLINE modusTollens #-}
 126
 127 -- | Non contradiction
 128 type NonContradiction p = Not (p && Not p)
 129
 130 instance Axiom (NonContradiction p)
 131
 132 contradicts :: Proof (Not p) -> Proof p -> Proof False
 133 contradicts = liftA3 (-->) (axiom @(NotAsNonExistent _))
 134 {-# INLINE contradicts #-}
 135
 136 -- `RefHoTTBook`:
 137 -- > It has been known for a long time, however, that principles such as AC and LEM are fundamentally
 138 -- > antithetical to computability, since they assert baldly that certain things exist without giving any
 139 -- > way to compute them. Thus, avoiding them is necessary to maintain the character of type theory
 140 -- > as a theory of computation.
 141
 142 -- Intuitionistic logic rejects excluded middle (and the many equivalent rules)
 143 type ExcludedMiddle p = p || Not p
 144
 145 type Contradiction p = (Not p -> False) -> p
 146 instance Axiom (ExcludedMiddle p) => Lemma (Contradiction p) where
 147   lemma = (\em np2f -> runOr id (absurd . np2f) em) <$> axiom @(ExcludedMiddle p)