-- |
-- Module      : AutoProof.Internal.Intuitionistic.Proof.Search.Implication
-- Copyright   : (c) Artem Mavrin, 2021
-- License     : BSD3
-- Maintainer  : artemvmavrin@gmail.com
-- Stability   : experimental
-- Portability : POSIX
--
-- Intuitionistic proofs in the implicational fragment of propositional logic.
module AutoProof.Internal.Intuitionistic.Proof.Search.Implication
  ( proveImp,
  )
where

import AutoProof.Internal.Formula (Formula (Imp, Var))
import AutoProof.Internal.Judgement (Judgement (Judgement))
import AutoProof.Internal.Proof.Types (Proof (Axiom, ImpElim, ImpIntr))
import Control.Applicative ((<|>))
import qualified Data.Set as Set

-- | @('proveImp' (g 'AutoProof.Judgement.|-' a))@ finds an intuitionistic proof
-- of a judgement \(g \vdash a\) in the implicational fragment of propositional
-- logic, if such a proof exists.
--
-- The algorithm is adapted from section 2.4 of
--
-- *  Samuel Mimram (2020)
--    /PROGRAM = PROOF/.
--
-- ==== __Examples__
--
-- >>> proveImp $ [Var 'a', Imp (Var 'a') (Var 'b')] |- Var 'b'
-- Just (ImpElim ([Var 'a',Imp (Var 'a') (Var 'b')] |- Var 'b') (Axiom ([Var 'a',Imp (Var 'a') (Var 'b')] |- Imp (Var 'a') (Var 'b'))) (Axiom ([Var 'a',Imp (Var 'a') (Var 'b')] |- Var 'a')))
--
-- >>> proveImp $ [Imp (Var 'a') (Var 'b'), Imp (Var 'b') (Var 'a')] |- Var 'a'
-- Nothing
proveImp :: Ord a => Judgement a -> Maybe (Proof a)
proveImp :: Judgement a -> Maybe (Proof a)
proveImp = Set (Judgement a) -> Judgement a -> Maybe (Proof a)
forall a.
Ord a =>
Set (Judgement a) -> Judgement a -> Maybe (Proof a)
search Set (Judgement a)
forall a. Set a
Set.empty
  where
    -- We search for a proof while maintaining a set s of previously seen
    -- judgements of the form g ⊢ x, for x a variable, to avoid cycles

    -- Easy case: if there is a proof of g ⊢ a → b, then there must be a proof
    -- proof of g ⊢ a → b that ends with an inference of the form
    --
    --  g,a ⊢ b
    -- --------- (→I)
    -- g ⊢ a → b
    --
    -- so it suffices to look for a proof of g,a ⊢ b
    search :: Set (Judgement a) -> Judgement a -> Maybe (Proof a)
search s :: Set (Judgement a)
s j :: Judgement a
j@(Judgement g :: Context a
g i :: Formula a
i@(Imp a :: Formula a
a b :: Formula a
b)) =
      if Formula a -> Context a -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Formula a
i Context a
g
        then Proof a -> Maybe (Proof a)
forall a. a -> Maybe a
Just (Judgement a -> Proof a
forall a. Judgement a -> Proof a
Axiom Judgement a
j)
        else Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
ImpIntr Judgement a
j (Proof a -> Proof a) -> Maybe (Proof a) -> Maybe (Proof a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (Judgement a) -> Judgement a -> Maybe (Proof a)
search Set (Judgement a)
s (Context a -> Formula a -> Judgement a
forall a. Context a -> Formula a -> Judgement a
Judgement (Formula a -> Context a -> Context a
forall a. Ord a => a -> Set a -> Set a
Set.insert Formula a
a Context a
g) Formula a
b)
    -- Trickier case: if there is a proof of g ⊢ x, where x is a variable, then
    -- either
    --
    -- (1) x belongs to g, so g ⊢ x is proved via
    --
    -- ----- (Axiom)
    -- g ⊢ x
    --
    -- or
    --
    -- (2) there is a sequence a1,...,an of propositional formulas such that
    -- a1 → (a2 → (... an → x)...) belongs to g, and g ⊢ ai for all i=1,...,n.
    -- In this case, one proof of g ⊢ x is
    --
    --                                          p1
    -- ------------------------------- (Ax.)  ------
    -- g ⊢ a1 → (a2 → (... an → x)...)        g ⊢ a1         p2
    -- --------------------------------------------- (→E)  ------
    --        g ⊢ a2 → (... an → x)                        g ⊢ a2
    --                                 ...                            pn
    -- ------------------------------------------------------ (→E)  ------
    --                             g ⊢ an → x                       g ⊢ an
    -- ------------------------------------------------------------------- (→E)
    --                                g ⊢ x
    --
    -- Actually, case (1) is the n=0 case of case (2).
    --
    -- The implementation:
    search s :: Set (Judgement a)
s j :: Judgement a
j@(Judgement g :: Context a
g v :: Formula a
v@(Var x :: a
x)) =
      if Judgement a -> Set (Judgement a) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Judgement a
j Set (Judgement a)
s
        then Maybe (Proof a)
forall a. Maybe a
Nothing -- Already visited current judgement; skip to avoid cycles
        else (Formula a -> Maybe (Proof a) -> Maybe (Proof a))
-> Maybe (Proof a) -> Context a -> Maybe (Proof a)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Maybe (Proof a) -> Maybe (Proof a) -> Maybe (Proof a)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) (Maybe (Proof a) -> Maybe (Proof a) -> Maybe (Proof a))
-> (Formula a -> Maybe (Proof a))
-> Formula a
-> Maybe (Proof a)
-> Maybe (Proof a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula a -> Maybe (Proof a)
findImp) Maybe (Proof a)
forall a. Maybe a
Nothing Context a
g -- Scan context looking for proof
      where
        -- findImp searches each formula in the context for implications ending
        -- in the variable x. When encountering a formula of the form
        -- a1 → (a2 → (... an → x)...), ensure each ai is provable, and, if so,
        -- construct a proof
        findImp :: Formula a -> Maybe (Proof a)
findImp a :: Formula a
a = do
          [Formula a]
as <- Formula a -> Maybe [Formula a]
splitImp Formula a
a
          [Formula a] -> Formula a -> Maybe (Proof a)
construct [Formula a]
as Formula a
v

        -- Given a formula of the form a1 → (a2 → (... an → x)...), extract the
        -- list [an, ..., a2, a1] (note the reverse order)
        splitImp :: Formula a -> Maybe [Formula a]
splitImp = [Formula a] -> Formula a -> Maybe [Formula a]
go []
          where
            go :: [Formula a] -> Formula a -> Maybe [Formula a]
go l :: [Formula a]
l (Var y :: a
y) = if a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y then [Formula a] -> Maybe [Formula a]
forall a. a -> Maybe a
Just [Formula a]
l else Maybe [Formula a]
forall a. Maybe a
Nothing
            go l :: [Formula a]
l (Imp a :: Formula a
a b :: Formula a
b) = [Formula a] -> Formula a -> Maybe [Formula a]
go (Formula a
a Formula a -> [Formula a] -> [Formula a]
forall a. a -> [a] -> [a]
: [Formula a]
l) Formula a
b
            go _ _ = Maybe [Formula a]
forall a. Maybe a
Nothing -- non-implicational case

        -- Given a list of formulas [an, ..., a2, a1] from an implication of the
        -- form a1 → (a2 → (... an → x)...), try to prove the ai's, and use the
        -- resulting proofs to construct a proof of x using nested implication
        -- eliminations
        construct :: [Formula a] -> Formula a -> Maybe (Proof a)
construct [] b :: Formula a
b = Proof a -> Maybe (Proof a)
forall a. a -> Maybe a
Just (Judgement a -> Proof a
forall a. Judgement a -> Proof a
Axiom (Context a -> Formula a -> Judgement a
forall a. Context a -> Formula a -> Judgement a
Judgement Context a
g Formula a
b))
        construct (a :: Formula a
a : as :: [Formula a]
as) b :: Formula a
b = do
          Proof a
q <- Set (Judgement a) -> Judgement a -> Maybe (Proof a)
search (Judgement a -> Set (Judgement a) -> Set (Judgement a)
forall a. Ord a => a -> Set a -> Set a
Set.insert Judgement a
j Set (Judgement a)
s) (Context a -> Formula a -> Judgement a
forall a. Context a -> Formula a -> Judgement a
Judgement Context a
g Formula a
a)
          Proof a
p <- [Formula a] -> Formula a -> Maybe (Proof a)
construct [Formula a]
as (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
a Formula a
b)
          Proof a -> Maybe (Proof a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Judgement a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a
ImpElim (Context a -> Formula a -> Judgement a
forall a. Context a -> Formula a -> Judgement a
Judgement Context a
g Formula a
b) Proof a
p Proof a
q)

    -- Non-implicational case
    search _ _ = Maybe (Proof a)
forall a. Maybe a
Nothing