-- |
-- Module      : AutoProof.Internal.Classical.Proof.Glivenko
-- Copyright   : (c) Artem Mavrin, 2021
-- License     : BSD3
-- Maintainer  : artemvmavrin@gmail.com
-- Stability   : experimental
-- Portability : POSIX
--
-- Glivenko translation.
module AutoProof.Internal.Classical.Proof.Glivenko
  ( glivenkoTranslate,
    isProvableGlivenko,
  )
where

import AutoProof.Internal.Formula (Formula (Lit, Not))
import qualified AutoProof.Internal.Intuitionistic.Proof as I (isProvable)
import AutoProof.Internal.Judgement (Judgement (Judgement))
import qualified Data.Set as Set (insert)

-- | Translate one judgement into another such that the first is classically
-- provable if and only if the second is intuitionistically provable.
-- Specifically, the Glivenko translation of a judgement \(g \vdash a\) is the
-- judgement \(g, \lnot a \vdash \bot\).
glivenkoTranslate :: Ord a => Judgement a -> Judgement a
glivenkoTranslate :: Judgement a -> Judgement a
glivenkoTranslate (Judgement g :: Context a
g a :: Formula a
a) = 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 -> Formula a
forall a. Formula a -> Formula a
Not Formula a
a) Context a
g) (Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
False)

-- | Determine whether a judgement is classically valid using Glivenko's
-- translation.
isProvableGlivenko :: Ord a => Judgement a -> Bool
isProvableGlivenko :: Judgement a -> Bool
isProvableGlivenko = Judgement a -> Bool
forall a. Ord a => Judgement a -> Bool
I.isProvable (Judgement a -> Bool)
-> (Judgement a -> Judgement a) -> Judgement a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement a -> Judgement a
forall a. Ord a => Judgement a -> Judgement a
glivenkoTranslate