content: {-# LANGUAGE ExplicitNamespaces    #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE RankNTypes            #-}
  {-# LANGUAGE TypeOperators         #-}
  {-# LANGUAGE PolyKinds             #-}
  
  {-|
    Module      :  Logic.Propositional
    Copyright   :  (c) Matt Noonan 2018
    License     :  BSD-style
    Maintainer  :  matt.noonan@gmail.com
    Portability :  portable
  -}
  
  module Logic.Propositional
    ( -- * First-order Logic
  
    -- ** Logical symbols
      TRUE, FALSE
  
    , And,     type (&&), type (∧), type (/\)
    , Or,      type (||), type (∨), type (\/)
    , Implies, type (-->)
    , Not
    , ForAll
    , Exists
  
    -- ** Natural deduction
  
    -- *** Tautologies
    , true
    , noncontra
  
    -- *** Introduction rules
  
    -- | Introduction rules give the elementary building blocks
    --   for creating a formula from simpler ones.
    , introAnd
    , introAnd'
  
    , introOrL
    , introOrR
  
    , introImpl
    , introNot
  
    , contrapositive
    , contradicts
    , contradicts'
    , introUniv
    , introEx
  
    -- *** Elimination rules
  
    -- | Elimination rules give the elementary building blocks for
    --   decomposing a complex formula into simpler ones.
    , elimAndL
    , elimAndR
  
    , elimOr
    , elimOrL
    , elimOrR
  
    , elimImpl
    , modusPonens
    , modusTollens
    , absurd
    , elimUniv
    , elimEx
  
    -- *** Classical logic and the Law of the Excluded Middle
    , Classical
    , classically
    , lem
    , contradiction
    , elimNot
    , elimNotNot
  
    , deMorganNor
    , deMorganAndNots
    , deMorganNand
    , deMorganOrNots
  
    -- *** Mapping over conjunctions and disjunctions.
  
    -- | These function names mimic the ones for
    -- (@Functor@/@Bifunctor@/@Profunctor@).
    , firstAnd
    , secondAnd
    , bimapAnd
  
    , firstOr
    , secondOr
    , bimapOr
  
    , lmapImpl
    , rmapImpl
    , dimapImpl
  
    , mapNot
  
    ) where
  
  import Logic.Classes
  import Logic.Proof
  
  {--------------------------------------------------
    Logical constants
  --------------------------------------------------}
  
  -- | The constant "true".
  data TRUE
  
  -- | The constant "false".
  data FALSE
  
  -- | The conjunction of @p@ and @q@.
  data And p q
  
  -- | The disjunction of @p@ and @q@.
  data Or p q
  
  -- | The negation of @p@.
  data Not p
  
  -- | The implication "@p@ implies @q@".
  data Implies p q
  
  -- | Existential quantifiation.
  data Exists x p
  
  -- | Universal quantification.
  data ForAll x p
  
  -- | An infix alias for @Or@.
  type p || q   = p `Or` q
  
  -- | An infix alias for @Or@.
  type p ∨ q   = p `Or` q
  
  -- | An infix alias for @Or@.
  type p \/ q  = p `Or` q
  
  -- | An infix alias for @And@.
  type p && q  = p `And` q
  
  -- | An infix alias for @And@.
  type p ∧ q   = p `And` q
  
  -- | An infix alias for @And@.
  type p /\ q  = p `And` q
  
  -- | An infix alias for @Implies@.
  type p --> q = p `Implies` q
  
  infixl 2 `Or`
  infixl 2 ||
  infixl 2 ∨
  infixl 2 \/
  
  infixl 3 `And`
  infixl 3 &&
  infixl 3 ∧
  infixl 3 /\
  
  infixr 1 `Implies`
  infixr 1 -->
  
  {--------------------------------------------------
    Mapping over conjunctions and disjunctions
  --------------------------------------------------}
  
  -- | Apply a derivation to the left side of a conjunction.
  firstAnd :: (Proof p -> Proof p') -> Proof (p && q) -> Proof (p' && q)
  firstAnd = flip bimapAnd id
  
  -- | Apply a derivation to the right side of a conjunction.
  secondAnd :: (Proof q -> Proof q') -> Proof (p && q) -> Proof (p && q')
  secondAnd = bimapAnd id
  
  -- | Apply derivations to the left and right sides of a conjunction.
  bimapAnd :: (Proof p -> Proof p') -> (Proof q -> Proof q') -> Proof (p && q) -> Proof (p' && q')
  bimapAnd implP implQ conj = let
    (lhs, rhs) = elimAnd conj
    lhs' = implP lhs
    rhs' = implQ rhs
    in introAnd lhs' rhs'
  
  -- | Apply a derivation to the left side of a disjunction.
  firstOr :: (Proof p -> Proof p') -> Proof (p || q) -> Proof (p' || q)
  firstOr = flip bimapOr id
  
  -- | Apply a derivation to the right side of a disjunction.
  secondOr :: (Proof q -> Proof q') -> Proof (p || q) -> Proof (p || q')
  secondOr = bimapOr id
  
  -- | Apply derivations to the left and right sides of a disjunction.
  bimapOr :: (Proof p -> Proof p') -> (Proof q -> Proof q') -> Proof (p || q) -> Proof (p' || q')
  bimapOr implP implQ = elimOr (introOrL . implP) (introOrR . implQ)
  
  -- | Apply a derivation to the left side of an implication.
  lmapImpl :: (Proof p' -> Proof p) -> Proof (p --> q) -> Proof (p' --> q)
  lmapImpl = flip dimapImpl id
  
  -- | Apply a derivation to the right side of an implication.
  rmapImpl :: (Proof q -> Proof q') -> Proof (p --> q) -> Proof (p --> q')
  rmapImpl = dimapImpl id
  
  -- | Apply derivations to the left and right sides of an implication.
  dimapImpl :: (Proof p' -> Proof p) -> (Proof q -> Proof q') -> Proof (p --> q) -> Proof (p' --> q')
  dimapImpl dervL dervR impl = introImpl (dervR . modusPonens impl . dervL)
  
  -- | Apply a derivation inside of a negation.
  mapNot :: (Proof p' -> Proof p) -> Proof (Not p) -> Proof (Not p')
  mapNot impl notP = introNot (absurd . contradicts' notP . impl)
  
  {--------------------------------------------------
    Tautologies
  --------------------------------------------------}
  
  -- | @TRUE@ is always true, and can be introduced into a proof at any time.
  true :: Proof TRUE
  true = axiom
  
  -- | The Law of Noncontradiction: for any proposition P, "P and not-P" is false.
  noncontra :: Proof (Not (p && Not p))
  noncontra = axiom
  
  {--------------------------------------------------
    Introduction rules
  --------------------------------------------------}
  
  -- | Prove "P and Q" from P and Q.
  introAnd :: Proof p -> Proof q -> Proof (p && q)
  introAnd _ _ = axiom
  
  -- | Prove "P and Q" from Q and P.
  introAnd' :: Proof q -> Proof p -> Proof (p && q)
  introAnd' _ _ = axiom
  
  -- | Prove "P or Q" from  P.
  introOrL :: Proof p -> Proof (p || q)
  introOrL _ = axiom
  
  -- | Prove "P or Q" from Q.
  introOrR :: Proof q -> Proof (p || q)
  introOrR _ = axiom
  
  -- | Prove "P implies Q" by demonstrating that,
  --   from the assumption P, you can prove Q.
  introImpl :: (Proof p -> Proof q) -> Proof (p --> q)
  introImpl _ = axiom
  
  -- | Prove "not P" by demonstrating that,
  --   from the assumption P, you can derive a false conclusion.
  introNot :: (Proof p -> Proof FALSE) -> Proof (Not p)
  introNot _ = axiom
  
  -- | `contrapositive` is an alias for `introNot`, with
  --   a somewhat more suggestive name. Not-introduction
  --   corresponds to the proof technique "proof by contrapositive".
  contrapositive :: (Proof p -> Proof FALSE) -> Proof (Not p)
  contrapositive = introNot
  
  -- | Prove a contradiction from "P" and "not P".
  contradicts :: Proof p -> Proof (Not p) -> Proof FALSE
  contradicts _ _ = axiom
  
  -- | `contradicts'` is `contradicts` with the arguments
  --   flipped. It is useful when you want to partially
  --   apply `contradicts` to a negation.
  contradicts' :: Proof (Not p) -> Proof p -> Proof FALSE
  contradicts' = flip contradicts
  
  -- | Prove "For all x, P(x)" from a proof of P(*c*) with
  --   *c* indeterminate.
  introUniv :: (forall c. Proof (p c)) -> Proof (ForAll x (p x))
  introUniv _ = axiom
  
  -- | Prove "There exists an x such that P(x)" from a specific
  --   instance of P(c).
  introEx :: Proof (p c) -> Proof (Exists x (p x))
  introEx _ = axiom
  
  {--------------------------------------------------
    Elimination rules
  --------------------------------------------------}
  
  -- | From the assumption "P and Q", produce a proof of P.
  elimAndL :: Proof (p && q) -> Proof p
  elimAndL _ = axiom
  
  -- | From the assumption "P and Q", produce a proof of Q.
  elimAndR :: Proof (p && q) -> Proof q
  elimAndR _ = axiom
  
  -- | From the assumption "P and Q", produce both a proof
  --   of P, and a proof of Q.
  elimAnd :: Proof (p && q) -> (Proof p, Proof q)
  elimAnd c = (elimAndL c, elimAndR c)
  
  -- | If you have a proof of R from P, and a proof of R from Q, then
  --   convert "P or Q" into a proof of R.
  elimOr :: (Proof p -> Proof r) -> (Proof q -> Proof r) -> Proof (p || q) -> Proof r
  elimOr _ _ _ = axiom
  
  -- | elimOrL is elimOr with the disjunction in the middle.
  elimOrL :: (Proof p -> Proof r) -> Proof (p || q) -> (Proof q -> Proof r) -> Proof r
  elimOrL case1 disj case2 = elimOr case1 case2 disj
  
  -- | elimOrR is elimOr with the disjunction in the middle and the implications
  --   swapped.
  elimOrR :: (Proof q -> Proof r) -> Proof (p || q) -> (Proof p -> Proof r) -> Proof r
  elimOrR case2 disj case1 = elimOr case1 case2 disj
  
  -- | Given "P imples Q" and P, produce a proof of Q.
  --   (modus ponens)
  elimImpl :: Proof p -> Proof (p --> q) -> Proof q
  elimImpl _ _ = axiom
  
  -- | @modusPonens@ is just `elimImpl` with the arguments
  --   flipped. In this form, it is useful for partially
  --   applying an implication.
  modusPonens :: Proof (p --> q) -> Proof p -> Proof q
  modusPonens = flip elimImpl
  
  {-| Modus tollens lets you prove "Not P" from
      "P implies Q" and "Not Q".
  
      Modus tollens is not fundamental, and can be derived from
      other rules:
  
  @
                                    -----         (assumption)
                          p --> q,    p
                         ---------------------    (modus ponens)
                 Not q,            q
                --------------------------        (contradicts')
                        FALSE
            ------------------------------------- (not-intro)
                               Not p
  @
  
  We can encode this proof tree as a @Proof@ to implement
  @modus_tollens@:
  
  @
  modusTollens :: Proof (p --> q) -> Proof (Not q) -> Proof (Not p)
  modusTollens impl q' = introNot $ \p -> contradicts' q' (modusPonens impl p)
  @
  -}
  
  modusTollens :: Proof (p --> q) -> Proof (Not q) -> Proof (Not p)
  modusTollens impl q' = introNot $ \p -> contradicts' q' (modusPonens impl p)
  
  -- | From a falsity, prove anything.
  absurd :: Proof FALSE -> Proof p
  absurd _ = axiom
  
  -- | Given "For all x, P(x)" and any c, prove the proposition
  --   "P(c)".
  elimUniv :: Proof (ForAll x (p x)) -> Proof (p c)
  elimUniv _ = axiom
  
  -- | Given a proof of Q from P(c) with c generic, and the
  --   statement "There exists an x such that P(x)", produce
  --   a proof of Q.
  elimEx :: (forall c. Proof (p c) -> Proof q) -> Proof (Exists x (p x)) -> Proof q
  elimEx _ _ = axiom
  
  {--------------------------------------------------
    Classical logic
  --------------------------------------------------}
  
  -- | The inference rules so far have all been valid in
  --   constructive logic. Proofs in classical logic are
  --   also allowed, but will be constrained by the
  --   `Classical` typeclass.
  class Classical
  
  -- | Discharge a @Classical@ constraint, by saying
  --   "I am going to allow a classical argument here."
  --
  --   NOTE: The existence of this function means that a proof
  --   should only be considered constructive if it
  --   does not have a @Classical@ constraint, *and*
  --   it does not invoke @classically@.
  classically :: (Classical => Proof p) -> Proof p
  classically _ = axiom
  
  -- | The Law of the Excluded Middle: for any proposition
  --   P, assert that either P is true, or Not P is true.
  lem :: Classical => Proof (p || Not p)
  lem = axiom
  
  {-| Proof by contradiction: this proof technique allows
       you to prove P by showing that, from "Not P", you
       can prove a falsehood.
  
       Proof by contradiction is not a theorem of
       constructive logic, so it requires the @Classical@
       constraint. But note that the similar technique
       of proof by contrapositive (not-introduction) /is/
       valid in constructive logic! For comparison, the two types are:
  
  @
  contradiction  :: Classical => (Proof (Not p) -> Proof FALSE) -> Proof p
  introNot       ::              (Proof      p  -> Proof FALSE) -> Proof (Not p)
  @
  
  The derivation of proof by contradiction from the law of the excluded
  middle goes like this: first, use the law of the excluded middle to
  prove @p || Not p@. Then use or-elimination to prove @p@ for each
  alternative. The first alternative is immediate; for the second
  alternative, use the provided implication to get a proof of falsehood,
  from which the desired conclusion is derived.
  
  @
  contradiction impl = elimOr id (absurd . impl) lem
  @
  -}
  contradiction :: Classical => (Proof (Not p) -> Proof FALSE) -> Proof p
  contradiction impl = elimOr id (absurd . impl) lem
  
  -- | Alias for 'contradiction', to complete the patterns.
  elimNot :: Classical => (Proof (Not p) -> Proof FALSE) -> Proof p
  elimNot = contradiction
  
  {-| Double-negation elimination. This is another non-constructive
      proof technique, so it requires the @Classical@ constraint.
  
      The derivation of double-negation elimination follows from
      proof by contradiction, since "Not (Not p)" contradicts "Not p".
  @
  elimNotNot p'' = contradiction (contradicts' p'')
  @
  -}
  
  elimNotNot :: Classical => Proof (Not (Not p)) -> Proof p
  elimNotNot p'' = contradiction (contradicts' p'')
  
  -- | De Morgan for Nor: If (P or Q) is False, then both P and Q are False.
  deMorganNor :: Proof (Not (p || q)) -> Proof (Not p && Not q)
  deMorganNor npq = introAnd (mapNot introOrL npq) (mapNot introOrR npq)
  
  -- | De Morgan for And of Nots :: If both P and Q are False, then (P or Q) is False.
  deMorganAndNots :: Proof (Not p && Not q) -> Proof (Not (p || q))
  deMorganAndNots npnq = introNot $ \pq -> elimOr (contradicts' (elimAndL npnq)) (contradicts' (elimAndR npnq)) pq
  
  -- | De Morgan for Nand :: If (P and Q) is False, then either P or Q are False.
  --   Need to step into the realm of classical logic for this proof.
  deMorganNand :: Classical => Proof (Not (p && q)) -> Proof (Not p || Not q)
  deMorganNand npq = elimNot (\nnpnq -> contradicts (bimapAnd elimNotNot elimNotNot (deMorganNor nnpnq)) npq)
  
  -- | De Morgan for Or of Nots: If either P or Q are False, then (P and Q) is False.
  deMorganOrNots :: Proof (Not p || Not q) -> Proof (Not (p && q))
  deMorganOrNots npnq = introNot $ \pq -> elimOr (contradicts (elimAndL pq)) (contradicts (elimAndR pq)) npnq
  
  {--------------------------------------------------
    Algebraic properties
  --------------------------------------------------}
  
  instance Symmetric And
  instance Symmetric Or
  
  instance Associative And
  instance Associative Or
  
  instance DistributiveR And And
  instance DistributiveR And Or
  instance DistributiveR Or  And
  instance DistributiveR Or  Or
  
  instance DistributiveL And And
  instance DistributiveL And Or
  instance DistributiveL Or  And
  instance DistributiveL Or  Or
  