-- |
-- Module      : AutoProof.Internal.Intuitionistic.Proof.Correctness
-- Copyright   : (c) Artem Mavrin, 2021
-- License     : BSD3
-- Maintainer  : artemvmavrin@gmail.com
-- Stability   : experimental
-- Portability : POSIX
--
-- Check proof correctness in intuitionistic logic.
module AutoProof.Internal.Intuitionistic.Proof.Correctness
  ( correct,
    valid,
    debug,
  )
where

import AutoProof.Internal.AST (AST (root))
import AutoProof.Internal.Formula (Formula (And, Iff, Imp, Lit, Not, Or))
import AutoProof.Internal.Judgement (Judgement (Judgement))
import AutoProof.Internal.Proof.Types
  ( Proof
      ( AndElimL,
        AndElimR,
        AndIntr,
        Axiom,
        FalseElim,
        IffElimL,
        IffElimR,
        IffIntr,
        ImpElim,
        ImpIntr,
        NotElim,
        NotIntr,
        OrElim,
        OrIntrL,
        OrIntrR,
        TrueIntr
      ),
  )
import Data.Either (isRight)
import qualified Data.Set as Set

-- | Return an invalid inference node (on the 'Left'), if there is one.
-- Otherwise, return @'Right' ()@.
debug :: Ord a => Proof a -> Either (Proof a) ()
-- Axiom rule: if a belongs to g, then
--
-- ----- (Axiom)
-- g ⊢ a
debug :: Proof a -> Either (Proof a) ()
debug x :: Proof a
x@(Axiom (Judgement g :: Context a
g a :: Formula a
a)) = if Formula a -> Context a -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Formula a
a Context a
g then () -> Either (Proof a) ()
forall (m :: * -> *) a. Monad m => a -> m a
return () else Proof a -> Either (Proof a) ()
forall a b. a -> Either a b
Left Proof a
x
-- Falsity elimination:
--
--   p
-- -----
-- g ⊢ ⊥
-- ----- (⊥E)
-- g ⊢ a
debug x :: Proof a
x@(FalseElim (Judgement g :: Context a
g _) p :: Proof a
p) =
  let Judgement g' :: Context a
g' f :: Formula a
f = Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
p
   in if Formula a
f Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
False Bool -> Bool -> Bool
&& Context a
g' Context a -> Context a -> Bool
forall a. Eq a => a -> a -> Bool
== Context a
g
        then Proof a -> Either (Proof a) ()
forall a. Ord a => Proof a -> Either (Proof a) ()
debug Proof a
p
        else Proof a -> Either (Proof a) ()
forall a b. a -> Either a b
Left Proof a
x
-- Truth introduction:
--
-- ----- (⊤I)
-- g ⊢ ⊤
debug (TrueIntr (Judgement _ (Lit True))) = () -> Either (Proof a) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
-- Negation elimination: if g is the union of g1 and g2, then
--
--    p          q
-- -------    ------
-- g1 ⊢ ¬a    g2 ⊢ a
-- ----------------- (¬E)
--        g ⊢ ⊥
debug x :: Proof a
x@(NotElim (Judgement g :: Context a
g (Lit False)) p :: Proof a
p q :: Proof a
q) =
  let Judgement g1 :: Context a
g1 na :: Formula a
na = Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
p
      Judgement g2 :: Context a
g2 a :: Formula a
a = Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
q
   in case Formula a
na of
        Not b :: Formula a
b | Formula a
b Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
a Bool -> Bool -> Bool
&& Context a
g Context a -> Context a -> Bool
forall a. Eq a => a -> a -> Bool
== Context a -> Context a -> Context a
forall a. Ord a => Set a -> Set a -> Set a
Set.union Context a
g1 Context a
g2 -> do
          Proof a -> Either (Proof a) ()
forall a. Ord a => Proof a -> Either (Proof a) ()
debug Proof a
p
          Proof a -> Either (Proof a) ()
forall a. Ord a => Proof a -> Either (Proof a) ()
debug Proof a
q
        _ -> Proof a -> Either (Proof a) ()
forall a b. a -> Either a b
Left Proof a
x
-- Negation introduction:
--
--     p
-- --------
-- g, a ⊢ ⊥
-- -------- (¬I)
--  g ⊢ ¬a
debug x :: Proof a
x@(NotIntr (Judgement g :: Context a
g (Not a :: Formula a
a)) p :: Proof a
p) =
  let (Judgement g' :: Context a
g' f :: Formula a
f) = Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
p
   in case Formula a
f of
        Lit False | Context a
g' Context a -> Context a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a -> Context a -> Context a
forall a. Ord a => a -> Set a -> Set a
Set.insert Formula a
a Context a
g -> Proof a -> Either (Proof a) ()
forall a. Ord a => Proof a -> Either (Proof a) ()
debug Proof a
p
        _ -> Proof a -> Either (Proof a) ()
forall a b. a -> Either a b
Left Proof a
x
-- Implication elimination: if g is the union of g1 and g2, then
--
--     p           q
-- ----------    ------
-- g1 ⊢ a → b    g2 ⊢ a
-- -------------------- (→E)
--        g ⊢ b
debug x :: Proof a
x@(ImpElim (Judgement g :: Context a
g b :: Formula a
b) p :: Proof a
p q :: Proof a
q) =
  let Judgement g1 :: Context a
g1 c :: Formula a
c = Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
p
      Judgement g2 :: Context a
g2 a :: Formula a
a = Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
q
   in if Formula a
c Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
a Formula a
b Bool -> Bool -> Bool
&& Context a
g Context a -> Context a -> Bool
forall a. Eq a => a -> a -> Bool
== Context a
g1 Context a -> Context a -> Context a
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Context a
g2
        then do
          Proof a -> Either (Proof a) ()
forall a. Ord a => Proof a -> Either (Proof a) ()
debug Proof a
p
          Proof a -> Either (Proof a) ()
forall a. Ord a => Proof a -> Either (Proof a) ()
debug Proof a
q
        else Proof a -> Either (Proof a) ()
forall a b. a -> Either a b
Left Proof a
x
-- Implication introduction:
--
--     p
--  -------
--  g,a ⊢ b
-- --------- (→I)
-- g ⊢ a → b
debug x :: Proof a
x@(ImpIntr (Judgement g :: Context a
g (Imp a :: Formula a
a b :: Formula a
b)) p :: Proof a
p) =
  let Judgement g' :: Context a
g' b' :: Formula a
b' = Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
p
   in if Formula a
b' Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
b Bool -> Bool -> Bool
&& Context a
g' Context a -> Context a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a -> Context a -> Context a
forall a. Ord a => a -> Set a -> Set a
Set.insert Formula a
a Context a
g
        then Proof a -> Either (Proof a) ()
forall a. Ord a => Proof a -> Either (Proof a) ()
debug Proof a
p
        else Proof a -> Either (Proof a) ()
forall a b. a -> Either a b
Left Proof a
x
-- Disjunction elimination: if g is the union of g1, g2, and g3, then
--
--      p            q            r
-- ----------    ---------    ---------
-- g1 ⊢ a ∨ b    g2, a ⊢ c    g3, b ⊢ c
-- ------------------------------------ (∨E)
--                g ⊢ c
debug x :: Proof a
x@(OrElim (Judgement g :: Context a
g c :: Formula a
c) p :: Proof a
p q :: Proof a
q r :: Proof a
r) =
  let Judgement g1 :: Context a
g1 ab :: Formula a
ab = Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
p
      Judgement g2 :: Context a
g2 c2 :: Formula a
c2 = Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
q
      Judgement g3 :: Context a
g3 c3 :: Formula a
c3 = Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
r
   in case Formula a
ab of
        Or a :: Formula a
a b :: Formula a
b | Formula a
c2 Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
c
                   Bool -> Bool -> Bool
&& Formula a
c3 Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
c
                   Bool -> Bool -> Bool
&& Formula a
a Formula a -> Context a -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Context a
g2
                   Bool -> Bool -> Bool
&& Formula a
b Formula a -> Context a -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Context a
g3
                   Bool -> Bool -> Bool
&& Formula a -> Context a -> Context a
forall a. Ord a => a -> Set a -> Set a
Set.insert Formula a
a (Formula a -> Context a -> Context a
forall a. Ord a => a -> Set a -> Set a
Set.insert Formula a
b Context a
g) Context a -> Context a -> Bool
forall a. Eq a => a -> a -> Bool
== Context a -> Context a -> Context a
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Context a -> Context a -> Context a
forall a. Ord a => Set a -> Set a -> Set a
Set.union Context a
g1 Context a
g2) Context a
g3 ->
          do
            Proof a -> Either (Proof a) ()
forall a. Ord a => Proof a -> Either (Proof a) ()
debug Proof a
p
            Proof a -> Either (Proof a) ()
forall a. Ord a => Proof a -> Either (Proof a) ()
debug Proof a
q
            Proof a -> Either (Proof a) ()
forall a. Ord a => Proof a -> Either (Proof a) ()
debug Proof a
r
        _ -> Proof a -> Either (Proof a) ()
forall a b. a -> Either a b
Left Proof a
x
-- Disjunction introduction (left):
--
--     p
--   -----
--   g ⊢ a
-- --------- (∨IL)
-- g ⊢ a ∨ b
debug x :: Proof a
x@(OrIntrL (Judgement g :: Context a
g (Or a :: Formula a
a _)) p :: Proof a
p) =
  let Judgement g' :: Context a
g' a' :: Formula a
a' = Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
p
   in if Formula a
a' Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
a Bool -> Bool -> Bool
&& Context a
g' Context a -> Context a -> Bool
forall a. Eq a => a -> a -> Bool
== Context a
g
        then Proof a -> Either (Proof a) ()
forall a. Ord a => Proof a -> Either (Proof a) ()
debug Proof a
p
        else Proof a -> Either (Proof a) ()
forall a b. a -> Either a b
Left Proof a
x
-- Disjunction introduction (right):
--
--     p
--   -----
--   g ⊢ b
-- --------- (∨IL)
-- g ⊢ a ∨ b
debug x :: Proof a
x@(OrIntrR (Judgement g :: Context a
g (Or _ b :: Formula a
b)) p :: Proof a
p) =
  let Judgement g' :: Context a
g' b' :: Formula a
b' = Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
p
   in if Formula a
b' Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
b Bool -> Bool -> Bool
&& Context a
g' Context a -> Context a -> Bool
forall a. Eq a => a -> a -> Bool
== Context a
g
        then Proof a -> Either (Proof a) ()
forall a. Ord a => Proof a -> Either (Proof a) ()
debug Proof a
p
        else Proof a -> Either (Proof a) ()
forall a b. a -> Either a b
Left Proof a
x
-- Conjunction elimination (left):
--
--     p
-- ---------
-- g ⊢ a ∧ b
-- --------- (∧EL)
--   g ⊢ a
debug x :: Proof a
x@(AndElimL (Judgement g :: Context a
g a :: Formula a
a) p :: Proof a
p) =
  let Judgement g' :: Context a
g' ab :: Formula a
ab = Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
p
   in case Formula a
ab of
        And a' :: Formula a
a' _ | Formula a
a' Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
a Bool -> Bool -> Bool
&& Context a
g' Context a -> Context a -> Bool
forall a. Eq a => a -> a -> Bool
== Context a
g -> Proof a -> Either (Proof a) ()
forall a. Ord a => Proof a -> Either (Proof a) ()
debug Proof a
p
        _ -> Proof a -> Either (Proof a) ()
forall a b. a -> Either a b
Left Proof a
x
-- Conjunction elimination (right):
--
--     p
-- ---------
-- g ⊢ a ∧ b
-- --------- (∧ER)
--   g ⊢ b
debug x :: Proof a
x@(AndElimR (Judgement g :: Context a
g b :: Formula a
b) p :: Proof a
p) =
  let Judgement g' :: Context a
g' ab :: Formula a
ab = Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
p
   in case Formula a
ab of
        And _ b' :: Formula a
b' | Formula a
b' Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
b Bool -> Bool -> Bool
&& Context a
g' Context a -> Context a -> Bool
forall a. Eq a => a -> a -> Bool
== Context a
g -> Proof a -> Either (Proof a) ()
forall a. Ord a => Proof a -> Either (Proof a) ()
debug Proof a
p
        _ -> Proof a -> Either (Proof a) ()
forall a b. a -> Either a b
Left Proof a
x
-- Conjunction introduction: if g is the union of g1 and g2, then
--
--    p          q
-- ------     ------
-- g1 ⊢ a     g2 ⊢ b
-- ----------------- (∧I)
--     g ⊢ a ∧ b
debug x :: Proof a
x@(AndIntr (Judgement g :: Context a
g (And a :: Formula a
a b :: Formula a
b)) p :: Proof a
p q :: Proof a
q) =
  let Judgement g1 :: Context a
g1 a' :: Formula a
a' = Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
p
      Judgement g2 :: Context a
g2 b' :: Formula a
b' = Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
q
   in if Formula a
a' Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
a Bool -> Bool -> Bool
&& Formula a
b' Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
b Bool -> Bool -> Bool
&& Context a
g Context a -> Context a -> Bool
forall a. Eq a => a -> a -> Bool
== Context a -> Context a -> Context a
forall a. Ord a => Set a -> Set a -> Set a
Set.union Context a
g1 Context a
g2
        then do
          Proof a -> Either (Proof a) ()
forall a. Ord a => Proof a -> Either (Proof a) ()
debug Proof a
p
          Proof a -> Either (Proof a) ()
forall a. Ord a => Proof a -> Either (Proof a) ()
debug Proof a
q
        else Proof a -> Either (Proof a) ()
forall a b. a -> Either a b
Left Proof a
x
-- Equivalence elimination (left):
--
--     p
-- ---------
-- g ⊢ a ↔ b
-- --------- (↔EL)
-- g ⊢ a → b
debug x :: Proof a
x@(IffElimL (Judgement g :: Context a
g (Imp a :: Formula a
a b :: Formula a
b)) p :: Proof a
p) =
  let Judgement g' :: Context a
g' ab :: Formula a
ab = Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
p
   in case Formula a
ab of
        Iff a' :: Formula a
a' b' :: Formula a
b' | Formula a
a' Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
a Bool -> Bool -> Bool
&& Formula a
b' Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
b Bool -> Bool -> Bool
&& Context a
g' Context a -> Context a -> Bool
forall a. Eq a => a -> a -> Bool
== Context a
g -> Proof a -> Either (Proof a) ()
forall a. Ord a => Proof a -> Either (Proof a) ()
debug Proof a
p
        _ -> Proof a -> Either (Proof a) ()
forall a b. a -> Either a b
Left Proof a
x
-- Equivalence elimination (right):
--
--     p
-- ---------
-- g ⊢ a ↔ b
-- --------- (↔EL)
-- g ⊢ b → a
debug x :: Proof a
x@(IffElimR (Judgement g :: Context a
g (Imp b :: Formula a
b a :: Formula a
a)) p :: Proof a
p) =
  let Judgement g' :: Context a
g' ab :: Formula a
ab = Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
p
   in case Formula a
ab of
        Iff a' :: Formula a
a' b' :: Formula a
b' | Formula a
a' Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
a Bool -> Bool -> Bool
&& Formula a
b' Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
b Bool -> Bool -> Bool
&& Context a
g' Context a -> Context a -> Bool
forall a. Eq a => a -> a -> Bool
== Context a
g -> Proof a -> Either (Proof a) ()
forall a. Ord a => Proof a -> Either (Proof a) ()
debug Proof a
p
        _ -> Proof a -> Either (Proof a) ()
forall a b. a -> Either a b
Left Proof a
x
-- Equivalence introduction: if g is the union of g1 and g2, then
--
--      p              q
-- ----------     ----------
-- g1 ⊢ a → b     g2 ⊢ b → a
-- ------------------------- (↔I)
--         g ⊢ a ↔ b
debug x :: Proof a
x@(IffIntr (Judgement g :: Context a
g (Iff a :: Formula a
a b :: Formula a
b)) p :: Proof a
p q :: Proof a
q) =
  let Judgement g1 :: Context a
g1 ab :: Formula a
ab = Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
p
      Judgement g2 :: Context a
g2 ba :: Formula a
ba = Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
q
   in if Formula a
ab Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
a Formula a
b Bool -> Bool -> Bool
&& Formula a
ba Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
b Formula a
a Bool -> Bool -> Bool
&& Context a
g Context a -> Context a -> Bool
forall a. Eq a => a -> a -> Bool
== Context a -> Context a -> Context a
forall a. Ord a => Set a -> Set a -> Set a
Set.union Context a
g1 Context a
g2
        then do
          Proof a -> Either (Proof a) ()
forall a. Ord a => Proof a -> Either (Proof a) ()
debug Proof a
p
          Proof a -> Either (Proof a) ()
forall a. Ord a => Proof a -> Either (Proof a) ()
debug Proof a
q
        else Proof a -> Either (Proof a) ()
forall a b. a -> Either a b
Left Proof a
x
-- Pattern match failure:
debug x :: Proof a
x = Proof a -> Either (Proof a) ()
forall a b. a -> Either a b
Left Proof a
x

-- | Check whether a proof is valid.
valid :: Ord a => Proof a -> Bool
valid :: Proof a -> Bool
valid p :: Proof a
p = Either (Proof a) () -> Bool
forall a b. Either a b -> Bool
isRight (Proof a -> Either (Proof a) ()
forall a. Ord a => Proof a -> Either (Proof a) ()
debug Proof a
p)

-- | Check whether a proof is a correct proof of a given judgement
correct :: Ord a => Judgement a -> Proof a -> Bool
correct :: Judgement a -> Proof a -> Bool
correct (Judgement c :: Context a
c a :: Formula a
a) p :: Proof a
p =
  Proof a -> Bool
forall a. Ord a => Proof a -> Bool
valid Proof a
p
    Bool -> Bool -> Bool
&& ( let Judgement c' :: Context a
c' b :: Formula a
b = Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
p
          in Formula a
a Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
b Bool -> Bool -> Bool
&& Context a
c' Context a -> Context a -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Context a
c
       )