-- |
-- Module      : AutoProof.Internal.Intuitionistic.Proof.Search.Statman
-- Copyright   : (c) Artem Mavrin, 2021
-- License     : BSD3
-- Maintainer  : artemvmavrin@gmail.com
-- Stability   : experimental
-- Portability : POSIX
--
-- Check provability of general propositional formulas using an algorithm
-- derived from
--
-- *  Richard Statman (1979)
--    "Intuitionistic propositional logic is polynomial-space complete."
--    Theoretical Computer Science, Volume 9, Issue 1, pp. 67–72.
--    <https://doi.org/10.1016/0304-3975(79)90006-9 DOI>.
module AutoProof.Internal.Intuitionistic.Proof.Search.Statman
  ( proveStatman,
    toImp,
  )
where

import AutoProof.Internal.AST (AST (root))
import AutoProof.Internal.Formula
  ( Formula (And, Iff, Imp, Lit, Not, Or, Var),
    subformulas,
  )
import AutoProof.Internal.Intuitionistic.Proof.Search.Implication (proveImp)
import AutoProof.Internal.Judgement
  ( Judgement
      ( Judgement,
        antecedents,
        succedent
      ),
    (|-),
  )
import AutoProof.Internal.Proof.Structural (strengthenProof)
import AutoProof.Internal.Proof.Types
  ( Proof
      ( AndElimL,
        AndElimR,
        AndIntr,
        Axiom,
        FalseElim,
        IffElimL,
        IffElimR,
        IffIntr,
        ImpElim,
        ImpIntr,
        NotElim,
        NotIntr,
        OrElim,
        OrIntrL,
        OrIntrR,
        TrueIntr
      ),
  )
import qualified AutoProof.Internal.Utils.DList as DList
  ( cons,
    empty,
    fromList,
    toSet,
  )
import qualified Data.Set as Set

-- | Convert a general propositional judgement into an implicational judgement
-- which is intuitionistically provable if and only if the original judgement is
-- intuitionistically provable.
--
-- This construction is due to
--
-- *  Richard Statman (1979)
--    "Intuitionistic propositional logic is polynomial-space complete."
--    Theoretical Computer Science, Volume 9, Issue 1, pp. 67–72.
--    <https://doi.org/10.1016/0304-3975(79)90006-9 DOI>.
--
-- ==== __Details__
--
-- This algorithm turns a judgement \(g \vdash a\) in full propositional logic
-- into a judgement \(g^* \vdash a^*\) in just the implicational fragment of
-- propositional logic such that \(g \vdash a\) is provable if and only if the
-- judgement \(g^* \vdash a^*\) is provable. The latter judgement's provability
-- can then be checked using 'AutoProof.Proof.Search.Implication.proveImp'.
--
-- The transformation from \(g \vdash a\) to \(g^* \vdash a^*\) involves two
-- steps:
--
-- 1. For each propositional formula \(b\), introduce a new propositional
--    variable \(x_b\). Take \(a^* = x_a\).
-- 2. Construct the set \(g^*\) as follows.
--
--     1. For each formula \(b \in g\), add \(x_b\) to \(g^*\).
--     2. (Truth)
--        Add \(x_\top\) to  \(g^*\).
--     3. For each subformula \(b\) of either \(a\) or a formula in \(g\), do
--        the following.
--
--         1. (Falsity elimination and truth introduction)
--            Add the following formulas to \(g^*\).
--            \[
--              \begin{gathered}
--                x_\bot \rightarrow x_b \\
--                x_b \rightarrow x_\top
--              \end{gathered}
--            \]
--         2. (Negation introduction and elimination)
--            If \(b = \lnot c\), then add the following formulas to \(g^*\).
--            \[
--              \begin{gathered}
--                (x_c \rightarrow x_\bot) \rightarrow x_{\lnot c} \\
--                x_{\lnot c} \rightarrow (x_c \rightarrow x_\bot)
--              \end{gathered}
--            \]
--         3. (Implication introduction and elimination)
--            If \(b = c \rightarrow d\), then add the following formulas to
--            \(g^*\).
--            \[
--              \begin{gathered}
--                (x_c \rightarrow x_d) \rightarrow x_{c \rightarrow d} \\
--                x_{c \rightarrow d} \rightarrow (x_c \rightarrow x_d)
--              \end{gathered}
--            \]
--         4. (Disjunction introduction and elimination)
--            If \(b = c \lor d\), then for each additional subformula \(e\) of
--            \(a\), add the following formulas to \(g^*\).
--            \[
--              \begin{gathered}
--                x_c \rightarrow x_{c \lor d} \\
--                x_d \rightarrow x_{c \lor d} \\
--                x_{c \lor d} \rightarrow ((x_c \rightarrow x_e) \rightarrow ((x_d \rightarrow x_e) \rightarrow x_e))
--              \end{gathered}
--            \]
--         5. (Conjunction introduction and elimination)
--            If \(b = c \land d\), then add the following formulas to \(g^*\).
--            \[
--              \begin{gathered}
--                x_c \rightarrow (x_d \rightarrow x_{c \land d}) \\
--                x_{c \land d} \rightarrow x_c \\
--                x_{c \land d} \rightarrow x_d
--              \end{gathered}
--            \]
--         6. (Equivalence introduction and elimination)
--            If \(b = c \leftrightarrow d\), then add the following formulas to
--            \(g^*\).
--            \[
--              \begin{gathered}
--                (x_c \rightarrow x_d) \rightarrow ((x_d \rightarrow x_c) \rightarrow x_{c \leftrightarrow d}) \\
--                x_{c \leftrightarrow d} \rightarrow (x_c \rightarrow x_d) \\
--                x_{c \leftrightarrow d} \rightarrow (x_d \rightarrow x_c)
--              \end{gathered}
--            \]
toImp :: Ord a => Judgement a -> Judgement (Formula a)
toImp :: Judgement a -> Judgement (Formula a)
toImp (Judgement g :: Context a
g a :: Formula a
a) = Context (Formula a) -> Formula (Formula a) -> Judgement (Formula a)
forall a. Context a -> Formula a -> Judgement a
Judgement Context (Formula a)
gStar (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
a)
  where
    -- Initial implicational context (vacuous truth introduction)
    g0 :: DList (Formula (Formula a))
g0 = [Formula (Formula a)] -> DList (Formula (Formula a))
forall a. [a] -> DList a
DList.fromList [Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var (Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
True)]

    -- Intermediate implicational context: add all formulas derived from the
    -- succedent a
    g1 :: [Formula (Formula a)] -> [Formula (Formula a)]
g1 = ([Formula (Formula a)] -> [Formula (Formula a)])
-> Formula a -> [Formula (Formula a)] -> [Formula (Formula a)]
forall c.
([Formula (Formula a)] -> c)
-> Formula a -> [Formula (Formula a)] -> c
addFormulas [Formula (Formula a)] -> [Formula (Formula a)]
forall a. DList (Formula (Formula a))
g0 Formula a
a

    -- Final implicational context g^*, created by recursing over subformulas of
    -- formulas in the original context g
    gStar :: Context (Formula a)
gStar = ([Formula (Formula a)] -> [Formula (Formula a)])
-> Context (Formula a)
forall a. Ord a => DList a -> Set a
DList.toSet (([Formula (Formula a)] -> [Formula (Formula a)])
 -> Context (Formula a))
-> ([Formula (Formula a)] -> [Formula (Formula a)])
-> Context (Formula a)
forall a b. (a -> b) -> a -> b
$ (([Formula (Formula a)] -> [Formula (Formula a)])
 -> Formula a -> [Formula (Formula a)] -> [Formula (Formula a)])
-> ([Formula (Formula a)] -> [Formula (Formula a)])
-> Context a
-> [Formula (Formula a)]
-> [Formula (Formula a)]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ([Formula (Formula a)] -> [Formula (Formula a)])
-> Formula a -> [Formula (Formula a)] -> [Formula (Formula a)]
addFormulas' [Formula (Formula a)] -> [Formula (Formula a)]
g1 Context a
g

    -- Add formulas derived from a given formula b into the growing context g'
    addFormulas :: ([Formula (Formula a)] -> c)
-> Formula a -> [Formula (Formula a)] -> c
addFormulas g' :: [Formula (Formula a)] -> c
g' b :: Formula a
b = ([Formula (Formula a)] -> c)
-> Formula a -> [Formula (Formula a)] -> c
addFormulasByPattern ([Formula (Formula a)] -> c
g' ([Formula (Formula a)] -> c)
-> ([Formula (Formula a)] -> [Formula (Formula a)])
-> [Formula (Formula a)]
-> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula a -> [Formula (Formula a)] -> [Formula (Formula a)]
forall a. Formula a -> DList (Formula (Formula a))
common Formula a
b) Formula a
b

    -- Add formulas derived from a given formula b into the growing context g',
    -- but also add x_b (the new propositional variable obtained from b)
    addFormulas' :: ([Formula (Formula a)] -> [Formula (Formula a)])
-> Formula a -> [Formula (Formula a)] -> [Formula (Formula a)]
addFormulas' g' :: [Formula (Formula a)] -> [Formula (Formula a)]
g' b :: Formula a
b = Formula (Formula a)
-> ([Formula (Formula a)] -> [Formula (Formula a)])
-> [Formula (Formula a)]
-> [Formula (Formula a)]
forall a. a -> DList a -> DList a
DList.cons (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
b) (([Formula (Formula a)] -> [Formula (Formula a)])
-> Formula a -> [Formula (Formula a)] -> [Formula (Formula a)]
forall c.
([Formula (Formula a)] -> c)
-> Formula a -> [Formula (Formula a)] -> c
addFormulas [Formula (Formula a)] -> [Formula (Formula a)]
g' Formula a
b)

    -- Add formulas that depend on the form of b into the growing context g'
    addFormulasByPattern :: ([Formula (Formula a)] -> c)
-> Formula a -> [Formula (Formula a)] -> c
addFormulasByPattern g' :: [Formula (Formula a)] -> c
g' b :: Formula a
b@(Lit _) = [Formula (Formula a)] -> c
g' ([Formula (Formula a)] -> c)
-> ([Formula (Formula a)] -> [Formula (Formula a)])
-> [Formula (Formula a)]
-> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula a -> [Formula (Formula a)] -> [Formula (Formula a)]
unique Formula a
b
    addFormulasByPattern g' :: [Formula (Formula a)] -> c
g' b :: Formula a
b@(Var _) = [Formula (Formula a)] -> c
g' ([Formula (Formula a)] -> c)
-> ([Formula (Formula a)] -> [Formula (Formula a)])
-> [Formula (Formula a)]
-> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula a -> [Formula (Formula a)] -> [Formula (Formula a)]
unique Formula a
b
    addFormulasByPattern g' :: [Formula (Formula a)] -> c
g' b :: Formula a
b@(Not c :: Formula a
c) = ([Formula (Formula a)] -> c)
-> Formula a -> [Formula (Formula a)] -> c
addFormulas ([Formula (Formula a)] -> c
g' ([Formula (Formula a)] -> c)
-> ([Formula (Formula a)] -> [Formula (Formula a)])
-> [Formula (Formula a)]
-> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula a -> [Formula (Formula a)] -> [Formula (Formula a)]
unique Formula a
b) Formula a
c
    addFormulasByPattern g' :: [Formula (Formula a)] -> c
g' b :: Formula a
b@(Imp c :: Formula a
c d :: Formula a
d) = ([Formula (Formula a)] -> c)
-> Formula a -> [Formula (Formula a)] -> c
addFormulas (([Formula (Formula a)] -> c)
-> Formula a -> [Formula (Formula a)] -> c
addFormulas ([Formula (Formula a)] -> c
g' ([Formula (Formula a)] -> c)
-> ([Formula (Formula a)] -> [Formula (Formula a)])
-> [Formula (Formula a)]
-> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula a -> [Formula (Formula a)] -> [Formula (Formula a)]
unique Formula a
b) Formula a
c) Formula a
d
    addFormulasByPattern g' :: [Formula (Formula a)] -> c
g' b :: Formula a
b@(Or c :: Formula a
c d :: Formula a
d) = ([Formula (Formula a)] -> c)
-> Formula a -> [Formula (Formula a)] -> c
addFormulas (([Formula (Formula a)] -> c)
-> Formula a -> [Formula (Formula a)] -> c
addFormulas ([Formula (Formula a)] -> c
g' ([Formula (Formula a)] -> c)
-> ([Formula (Formula a)] -> [Formula (Formula a)])
-> [Formula (Formula a)]
-> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula a -> [Formula (Formula a)] -> [Formula (Formula a)]
unique Formula a
b) Formula a
c) Formula a
d
    addFormulasByPattern g' :: [Formula (Formula a)] -> c
g' b :: Formula a
b@(And c :: Formula a
c d :: Formula a
d) = ([Formula (Formula a)] -> c)
-> Formula a -> [Formula (Formula a)] -> c
addFormulas (([Formula (Formula a)] -> c)
-> Formula a -> [Formula (Formula a)] -> c
addFormulas ([Formula (Formula a)] -> c
g' ([Formula (Formula a)] -> c)
-> ([Formula (Formula a)] -> [Formula (Formula a)])
-> [Formula (Formula a)]
-> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula a -> [Formula (Formula a)] -> [Formula (Formula a)]
unique Formula a
b) Formula a
c) Formula a
d
    addFormulasByPattern g' :: [Formula (Formula a)] -> c
g' b :: Formula a
b@(Iff c :: Formula a
c d :: Formula a
d) = ([Formula (Formula a)] -> c)
-> Formula a -> [Formula (Formula a)] -> c
addFormulas (([Formula (Formula a)] -> c)
-> Formula a -> [Formula (Formula a)] -> c
addFormulas ([Formula (Formula a)] -> c
g' ([Formula (Formula a)] -> c)
-> ([Formula (Formula a)] -> [Formula (Formula a)])
-> [Formula (Formula a)]
-> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula a -> [Formula (Formula a)] -> [Formula (Formula a)]
unique Formula a
b) Formula a
c) Formula a
d

    -- Formulas that get created for every subformula b
    common :: Formula a -> DList (Formula (Formula a))
common b :: Formula a
b =
      [Formula (Formula a)] -> DList (Formula (Formula a))
forall a. [a] -> DList a
DList.fromList
        [ Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var (Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
False)) (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
b), -- Falsity elimination
          Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
b) (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var (Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
True)) -- Truth introduction
        ]

    -- Formulas that get created depending on the form of a subformula b
    unique :: Formula a -> [Formula (Formula a)] -> [Formula (Formula a)]
unique (Lit _) = [Formula (Formula a)] -> [Formula (Formula a)]
forall a. DList a
DList.empty
    unique (Var _) = [Formula (Formula a)] -> [Formula (Formula a)]
forall a. DList a
DList.empty
    unique b :: Formula a
b@(Not c :: Formula a
c) =
      [Formula (Formula a)]
-> [Formula (Formula a)] -> [Formula (Formula a)]
forall a. [a] -> DList a
DList.fromList
        [ Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
b) (Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
c) (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var (Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
False))), -- Negation elimination
          Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
c) (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var (Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
False))) (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
b) -- Negation introduction
        ]
    unique b :: Formula a
b@(Imp c :: Formula a
c d :: Formula a
d) =
      [Formula (Formula a)]
-> [Formula (Formula a)] -> [Formula (Formula a)]
forall a. [a] -> DList a
DList.fromList
        [ Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
b) (Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
c) (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
d)), -- Implication elimination
          Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
c) (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
d)) (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
b) -- Implication introduction
        ]
    unique b :: Formula a
b@(Or c :: Formula a
c d :: Formula a
d) =
      [Formula (Formula a)]
-> [Formula (Formula a)] -> [Formula (Formula a)]
forall a. [a] -> DList a
DList.fromList ([Formula (Formula a)]
 -> [Formula (Formula a)] -> [Formula (Formula a)])
-> [Formula (Formula a)]
-> [Formula (Formula a)]
-> [Formula (Formula a)]
forall a b. (a -> b) -> a -> b
$
        let introductions :: [Formula (Formula a)]
introductions =
              [ Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
c) (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
b), -- Left disjunction introduction
                Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
d) (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
b) -- Right disjunction introduction
              ]
            -- Disjunction elimination schema
            elimination :: Formula a -> Formula (Formula a)
elimination e :: Formula a
e = Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
b) (Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
c) (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
e)) (Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
d) (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
e)) (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
e)))
         in (Formula a -> [Formula (Formula a)] -> [Formula (Formula a)])
-> [Formula (Formula a)] -> Context a -> [Formula (Formula a)]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((:) (Formula (Formula a)
 -> [Formula (Formula a)] -> [Formula (Formula a)])
-> (Formula a -> Formula (Formula a))
-> Formula a
-> [Formula (Formula a)]
-> [Formula (Formula a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula a -> Formula (Formula a)
elimination) [Formula (Formula a)]
introductions (Formula a -> Context a
forall a. Ord a => Formula a -> Set (Formula a)
subformulas Formula a
a)
    -- TODO: is it sufficient to consider only subformulas of a above?
    unique b :: Formula a
b@(And c :: Formula a
c d :: Formula a
d) =
      [Formula (Formula a)]
-> [Formula (Formula a)] -> [Formula (Formula a)]
forall a. [a] -> DList a
DList.fromList
        [ Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
c) (Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
d) (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
b)), -- Conjunction introduction
          Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
b) (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
c), -- Left conjunction elimination
          Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
b) (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
d) -- Right conjunction elimination
        ]
    unique b :: Formula a
b@(Iff c :: Formula a
c d :: Formula a
d) =
      [Formula (Formula a)]
-> [Formula (Formula a)] -> [Formula (Formula a)]
forall a. [a] -> DList a
DList.fromList
        [ Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
c) (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
d)) (Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
d) (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
c)) (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
b)), -- Equivalence introduction
          Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
b) (Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
c) (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
d)), -- Left equivalence elimination
          Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
b) (Formula (Formula a) -> Formula (Formula a) -> Formula (Formula a)
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
d) (Formula a -> Formula (Formula a)
forall a. a -> Formula a
Var Formula a
c)) -- Right equivalence elimination
        ]

-- | Find an intuitionistic proof of a judgement, if one exists, using Statman's
-- algorithm.
--
-- *  Richard Statman (1979)
--    "Intuitionistic propositional logic is polynomial-space complete."
--    Theoretical Computer Science, Volume 9, Issue 1, pp. 67–72.
--    <https://doi.org/10.1016/0304-3975(79)90006-9 DOI>.
--
-- The judgement to be proved is converted to an implicational judgement as
-- described in 'toImp' and proved (if possible) using 'proveImp'. The resulting
-- proof is then converted into a proof of the original judgement.
proveStatman :: Ord a => Judgement a -> Maybe (Proof a)
proveStatman :: Judgement a -> Maybe (Proof a)
proveStatman j :: Judgement a
j@(Judgement g :: Context a
g _) = do
  -- Strengthening the proof here lets us remove some redundant hypotheses
  -- created by toImp.
  Proof (Formula a)
p <- Proof (Formula a) -> Proof (Formula a)
forall a. Ord a => Proof a -> Proof a
strengthenProof (Proof (Formula a) -> Proof (Formula a))
-> Maybe (Proof (Formula a)) -> Maybe (Proof (Formula a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Judgement (Formula a) -> Maybe (Proof (Formula a))
forall a. Ord a => Judgement a -> Maybe (Proof a)
proveImp (Judgement a -> Judgement (Formula a)
forall a. Ord a => Judgement a -> Judgement (Formula a)
toImp Judgement a
j)
  let g' :: Context (Formula a)
g' = Judgement (Formula a) -> Context (Formula a)
forall a. Judgement a -> Context a
antecedents (Proof (Formula a) -> Root (Proof (Formula a))
forall t. AST t => t -> Root t
root Proof (Formula a)
p)
  let proveImpAxiom :: Proof a -> Formula (Formula a) -> Proof a
proveImpAxiom q :: Proof a
q (Var c :: Formula a
c) | Formula a
c Formula a -> Context a -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Context a
g = Proof a
q
      proveImpAxiom q :: Proof a
q b :: Formula (Formula a)
b = Proof a -> Proof a -> Proof a
forall a. Eq a => Proof a -> Proof a -> Proof a
subAxiom Proof a
q (Formula (Formula a) -> Proof a
forall a. Ord a => Formula (Formula a) -> Proof a
proveToImpHypothesis Formula (Formula a)
b)
  Proof a -> Maybe (Proof a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Proof a -> Proof a
forall a. Ord a => Proof a -> Proof a
strengthenProof ((Proof a -> Formula (Formula a) -> Proof a)
-> Proof a -> Context (Formula a) -> Proof a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Proof a -> Formula (Formula a) -> Proof a
proveImpAxiom (Proof (Formula a) -> Proof a
forall a. Ord a => Proof (Formula a) -> Proof a
fromImpProof Proof (Formula a)
p) Context (Formula a)
g'))
  where
    -- Substitute a proof for an axiom
    subAxiom :: Proof a -> Proof a -> Proof a
subAxiom p :: Proof a
p@(Axiom (Judgement _ b :: Formula a
b)) q :: Proof a
q = if Formula a
b Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Judgement a -> Formula a
forall a. Judgement a -> Formula a
succedent (Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
q) then Proof a
q else Proof a
p
    subAxiom (FalseElim j' :: Judgement a
j' p :: Proof a
p) q :: Proof a
q = Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
FalseElim Judgement a
j' (Proof a -> Proof a -> Proof a
subAxiom Proof a
p Proof a
q)
    subAxiom p :: Proof a
p@(TrueIntr _) _ = Proof a
p
    subAxiom (NotElim j' :: Judgement a
j' p :: Proof a
p q :: Proof a
q) r :: Proof a
r = Judgement a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a
NotElim Judgement a
j' (Proof a -> Proof a -> Proof a
subAxiom Proof a
p Proof a
r) (Proof a -> Proof a -> Proof a
subAxiom Proof a
q Proof a
r)
    subAxiom (NotIntr j' :: Judgement a
j' p :: Proof a
p) q :: Proof a
q = Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
NotIntr Judgement a
j' (Proof a -> Proof a -> Proof a
subAxiom Proof a
p Proof a
q)
    subAxiom (ImpElim j' :: Judgement a
j' p :: Proof a
p q :: Proof a
q) r :: Proof a
r = Judgement a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a
ImpElim Judgement a
j' (Proof a -> Proof a -> Proof a
subAxiom Proof a
p Proof a
r) (Proof a -> Proof a -> Proof a
subAxiom Proof a
q Proof a
r)
    subAxiom (ImpIntr j' :: Judgement a
j' p :: Proof a
p) q :: Proof a
q = Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
ImpIntr Judgement a
j' (Proof a -> Proof a -> Proof a
subAxiom Proof a
p Proof a
q)
    subAxiom (OrElim j' :: Judgement a
j' p :: Proof a
p q :: Proof a
q r :: Proof a
r) s :: Proof a
s = Judgement a -> Proof a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a -> Proof a
OrElim Judgement a
j' (Proof a -> Proof a -> Proof a
subAxiom Proof a
p Proof a
s) (Proof a -> Proof a -> Proof a
subAxiom Proof a
q Proof a
s) (Proof a -> Proof a -> Proof a
subAxiom Proof a
r Proof a
s)
    subAxiom (OrIntrL j' :: Judgement a
j' p :: Proof a
p) q :: Proof a
q = Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
OrIntrL Judgement a
j' (Proof a -> Proof a -> Proof a
subAxiom Proof a
p Proof a
q)
    subAxiom (OrIntrR j' :: Judgement a
j' p :: Proof a
p) q :: Proof a
q = Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
OrIntrR Judgement a
j' (Proof a -> Proof a -> Proof a
subAxiom Proof a
p Proof a
q)
    subAxiom (AndElimL j' :: Judgement a
j' p :: Proof a
p) q :: Proof a
q = Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
AndElimL Judgement a
j' (Proof a -> Proof a -> Proof a
subAxiom Proof a
p Proof a
q)
    subAxiom (AndElimR j' :: Judgement a
j' p :: Proof a
p) q :: Proof a
q = Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
AndElimR Judgement a
j' (Proof a -> Proof a -> Proof a
subAxiom Proof a
p Proof a
q)
    subAxiom (AndIntr j' :: Judgement a
j' p :: Proof a
p q :: Proof a
q) r :: Proof a
r = Judgement a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a
AndIntr Judgement a
j' (Proof a -> Proof a -> Proof a
subAxiom Proof a
p Proof a
r) (Proof a -> Proof a -> Proof a
subAxiom Proof a
q Proof a
r)
    subAxiom (IffElimL j' :: Judgement a
j' p :: Proof a
p) q :: Proof a
q = Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
IffElimL Judgement a
j' (Proof a -> Proof a -> Proof a
subAxiom Proof a
p Proof a
q)
    subAxiom (IffElimR j' :: Judgement a
j' p :: Proof a
p) q :: Proof a
q = Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
IffElimR Judgement a
j' (Proof a -> Proof a -> Proof a
subAxiom Proof a
p Proof a
q)
    subAxiom (IffIntr j' :: Judgement a
j' p :: Proof a
p q :: Proof a
q) r :: Proof a
r = Judgement a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a
IffIntr Judgement a
j' (Proof a -> Proof a -> Proof a
subAxiom Proof a
p Proof a
r) (Proof a -> Proof a -> Proof a
subAxiom Proof a
q Proof a
r)

-- The stuff below is a tedious conversion from an implicational proof
-- (obtained from proveImp . toImp) to a "regular" proof of the original
-- judgement

-- Convert a formula with extra variables x_a (as described in toImp) back to an
-- ordinary formula
fromImpFormula :: Formula (Formula a) -> Formula a
fromImpFormula :: Formula (Formula a) -> Formula a
fromImpFormula (Lit b :: Bool
b) = Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
b
fromImpFormula (Var a :: Formula a
a) = Formula a
a
fromImpFormula (Imp a :: Formula (Formula a)
a b :: Formula (Formula a)
b) = Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp (Formula (Formula a) -> Formula a
forall a. Formula (Formula a) -> Formula a
fromImpFormula Formula (Formula a)
a) (Formula (Formula a) -> Formula a
forall a. Formula (Formula a) -> Formula a
fromImpFormula Formula (Formula a)
b)
-- This should be unreachable in intended use cases.
fromImpFormula _ = Formula a
forall a. HasCallStack => a
undefined

-- Convert a judgement with extra variables x_a (as described in toImp) back to
-- an ordinary judgement
fromImpJudgement :: Ord a => Judgement (Formula a) -> Judgement a
fromImpJudgement :: Judgement (Formula a) -> Judgement a
fromImpJudgement (Judgement g :: Context (Formula a)
g a :: Formula (Formula a)
a) = (Formula (Formula a) -> Formula a)
-> [Formula (Formula a)] -> [Formula a]
forall a b. (a -> b) -> [a] -> [b]
map Formula (Formula a) -> Formula a
forall a. Formula (Formula a) -> Formula a
fromImpFormula (Context (Formula a) -> [Formula (Formula a)]
forall a. Set a -> [a]
Set.toList Context (Formula a)
g) [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula (Formula a) -> Formula a
forall a. Formula (Formula a) -> Formula a
fromImpFormula Formula (Formula a)
a

-- Convert a proof with extra variables x_a (as described in toImp) back to an
-- ordinary proof
fromImpProof :: Ord a => Proof (Formula a) -> Proof a
fromImpProof :: Proof (Formula a) -> Proof a
fromImpProof (Axiom j :: Judgement (Formula a)
j) = Judgement a -> Proof a
forall a. Judgement a -> Proof a
Axiom (Judgement (Formula a) -> Judgement a
forall a. Ord a => Judgement (Formula a) -> Judgement a
fromImpJudgement Judgement (Formula a)
j)
fromImpProof (ImpElim j :: Judgement (Formula a)
j p :: Proof (Formula a)
p q :: Proof (Formula a)
q) = Judgement a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a
ImpElim (Judgement (Formula a) -> Judgement a
forall a. Ord a => Judgement (Formula a) -> Judgement a
fromImpJudgement Judgement (Formula a)
j) (Proof (Formula a) -> Proof a
forall a. Ord a => Proof (Formula a) -> Proof a
fromImpProof Proof (Formula a)
p) (Proof (Formula a) -> Proof a
forall a. Ord a => Proof (Formula a) -> Proof a
fromImpProof Proof (Formula a)
q)
fromImpProof (ImpIntr j :: Judgement (Formula a)
j p :: Proof (Formula a)
p) = Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
ImpIntr (Judgement (Formula a) -> Judgement a
forall a. Ord a => Judgement (Formula a) -> Judgement a
fromImpJudgement Judgement (Formula a)
j) (Proof (Formula a) -> Proof a
forall a. Ord a => Proof (Formula a) -> Proof a
fromImpProof Proof (Formula a)
p)
-- This should be uncreachable! This function is intended to operate on proofs
-- constructed using proveImp, which will only use the axiom, implication
-- introduction, And implication elimination rules.
fromImpProof _ = Proof a
forall a. HasCallStack => a
undefined

-- toImp will produce a set of hypotheses, all of which are intuitionistic
-- tautologies. This function performs a pattern-matching-based conversion of
-- each hypothesis into a proof. Each pattern matching case corresponds to a
-- specific inference rule.
--
-- Recall from toImp that a variable Var a, where a itself is a propositional
-- formula, represents a new propositional variable x_a.
proveToImpHypothesis :: Ord a => Formula (Formula a) -> Proof a
-- Axiom
proveToImpHypothesis :: Formula (Formula a) -> Proof a
proveToImpHypothesis (Imp (Var a :: Formula a
a) (Var a' :: Formula a
a'))
  | Formula a
a Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
a' =
    Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
ImpIntr
      ([] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
a Formula a
a)
      (Judgement a -> Proof a
forall a. Judgement a -> Proof a
Axiom ([Formula a
a] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a
a))
-- Falsity elimination
proveToImpHypothesis (Imp (Var (Lit False)) (Var b :: Formula a
b)) =
  Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
ImpIntr
    ([] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp (Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
False) Formula a
b)
    ( Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
FalseElim
        ([Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
False] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a
b)
        ( Judgement a -> Proof a
forall a. Judgement a -> Proof a
Axiom
            ( [Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
False] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
False
            )
        )
    )
-- Vacuous truth introduction (special case)
proveToImpHypothesis (Var (Lit True)) = Judgement a -> Proof a
forall a. Judgement a -> Proof a
TrueIntr ([] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
True)
-- Truth introduction
proveToImpHypothesis (Imp (Var b :: Formula a
b) (Var (Lit True))) =
  Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
ImpIntr
    ([] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
b (Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
True))
    (Judgement a -> Proof a
forall a. Judgement a -> Proof a
TrueIntr ([Formula a
b] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
True))
-- Negation elimination
proveToImpHypothesis (Imp (Var (Not c :: Formula a
c)) (Imp (Var c' :: Formula a
c') (Var (Lit False))))
  | Formula a
c Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
c' =
    Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
ImpIntr
      ([] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula a
forall a. Formula a -> Formula a
Not Formula a
c) (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c (Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
False)))
      ( Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
ImpIntr
          ([Formula a -> Formula a
forall a. Formula a -> Formula a
Not Formula a
c] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c (Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
False))
          ( Judgement a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a
NotElim
              ([Formula a -> Formula a
forall a. Formula a -> Formula a
Not Formula a
c, Formula a
c] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
False)
              (Judgement a -> Proof a
forall a. Judgement a -> Proof a
Axiom ([Formula a -> Formula a
forall a. Formula a -> Formula a
Not Formula a
c] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a
forall a. Formula a -> Formula a
Not Formula a
c))
              (Judgement a -> Proof a
forall a. Judgement a -> Proof a
Axiom ([Formula a
c] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a
c))
          )
      )
-- Negation introduction
proveToImpHypothesis (Imp (Imp (Var c :: Formula a
c) (Var (Lit False))) (Var (Not c' :: Formula a
c')))
  | Formula a
c Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
c' =
    Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
ImpIntr
      ([] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c (Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
False)) (Formula a -> Formula a
forall a. Formula a -> Formula a
Not Formula a
c))
      ( Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
NotIntr
          ([Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c (Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
False)] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a
forall a. Formula a -> Formula a
Not Formula a
c)
          ( Judgement a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a
ImpElim
              ([Formula a
c, Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c (Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
False)] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
False)
              (Judgement a -> Proof a
forall a. Judgement a -> Proof a
Axiom ([Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c (Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
False)] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c (Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
False)))
              (Judgement a -> Proof a
forall a. Judgement a -> Proof a
Axiom ([Formula a
c] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a
c))
          )
      )
-- Implication elimination
proveToImpHypothesis (Imp (Var (Imp c :: Formula a
c d :: Formula a
d)) (Imp (Var c' :: Formula a
c') (Var d' :: Formula a
d')))
  | Formula a
c Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
c' Bool -> Bool -> Bool
&& Formula a
d Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
d' =
    Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
ImpIntr
      ([] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c Formula a
d) (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c Formula a
d))
      (Judgement a -> Proof a
forall a. Judgement a -> Proof a
Axiom ([Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c Formula a
d] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c Formula a
d))
-- Implication introduction
proveToImpHypothesis (Imp (Imp (Var c :: Formula a
c) (Var d :: Formula a
d)) (Var (Imp c' :: Formula a
c' d' :: Formula a
d')))
  | Formula a
c Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
c' Bool -> Bool -> Bool
&& Formula a
d Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
d' =
    Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
ImpIntr
      ([] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c Formula a
d) (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c Formula a
d))
      (Judgement a -> Proof a
forall a. Judgement a -> Proof a
Axiom ([Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c Formula a
d] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c Formula a
d))
-- Left disjunction introduction
proveToImpHypothesis (Imp (Var c :: Formula a
c) (Var (Or c' :: Formula a
c' d :: Formula a
d)))
  | Formula a
c Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
c' =
    Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
ImpIntr
      ([] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Or Formula a
c Formula a
d))
      ( Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
OrIntrL
          ([Formula a
c] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Or Formula a
c Formula a
d)
          (Judgement a -> Proof a
forall a. Judgement a -> Proof a
Axiom ([Formula a
c] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a
c))
      )
-- Right disjunction introduction
proveToImpHypothesis (Imp (Var d :: Formula a
d) (Var (Or c :: Formula a
c d' :: Formula a
d')))
  | Formula a
d Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
d' =
    Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
ImpIntr
      ([] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
d (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Or Formula a
c Formula a
d))
      ( Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
OrIntrR
          ([Formula a
d] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Or Formula a
c Formula a
d)
          (Judgement a -> Proof a
forall a. Judgement a -> Proof a
Axiom ([Formula a
d] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a
d))
      )
-- Disjunction elimination
proveToImpHypothesis (Imp (Var (Or c :: Formula a
c d :: Formula a
d)) (Imp (Imp (Var c' :: Formula a
c') (Var e :: Formula a
e)) (Imp (Imp (Var d' :: Formula a
d') (Var e' :: Formula a
e')) (Var e'' :: Formula a
e''))))
  | Formula a
c Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
c' Bool -> Bool -> Bool
&& Formula a
d Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
d' Bool -> Bool -> Bool
&& Formula a
e Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
e' Bool -> Bool -> Bool
&& Formula a
e Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
e'' =
    Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
ImpIntr
      ([] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Or Formula a
c Formula a
d) (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c Formula a
e) (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
d Formula a
e) Formula a
e)))
      ( Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
ImpIntr
          ([Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Or Formula a
c Formula a
d] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c Formula a
e) (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
d Formula a
e) Formula a
e))
          ( Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
ImpIntr
              ([Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Or Formula a
c Formula a
d, Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c Formula a
e] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
d Formula a
e) Formula a
e)
              ( Judgement a -> Proof a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a -> Proof a
OrElim
                  ([Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Or Formula a
c Formula a
d, Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c Formula a
e, Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
d Formula a
e] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a
e)
                  (Judgement a -> Proof a
forall a. Judgement a -> Proof a
Axiom ([Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Or Formula a
c Formula a
d] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Or Formula a
c Formula a
d))
                  ( Judgement a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a
ImpElim
                      ([Formula a
c, Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c Formula a
e] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a
e)
                      (Judgement a -> Proof a
forall a. Judgement a -> Proof a
Axiom ([Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c Formula a
e] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c Formula a
e))
                      (Judgement a -> Proof a
forall a. Judgement a -> Proof a
Axiom ([Formula a
c] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a
c))
                  )
                  ( Judgement a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a
ImpElim
                      ([Formula a
d, Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
d Formula a
e] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a
e)
                      (Judgement a -> Proof a
forall a. Judgement a -> Proof a
Axiom ([Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
d Formula a
e] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
d Formula a
e))
                      (Judgement a -> Proof a
forall a. Judgement a -> Proof a
Axiom ([Formula a
d] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a
d))
                  )
              )
          )
      )
-- Conjunction introduction
proveToImpHypothesis (Imp (Var c :: Formula a
c) (Imp (Var d :: Formula a
d) (Var (And c' :: Formula a
c' d' :: Formula a
d'))))
  | Formula a
c Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
c' Bool -> Bool -> Bool
&& Formula a
d Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
d' =
    Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
ImpIntr
      ([] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
d (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
And Formula a
c Formula a
d)))
      ( Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
ImpIntr
          ([Formula a
c] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
d (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
And Formula a
c Formula a
d))
          ( Judgement a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a
AndIntr
              ([Formula a
c, Formula a
d] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
And Formula a
c Formula a
d)
              (Judgement a -> Proof a
forall a. Judgement a -> Proof a
Axiom ([Formula a
c] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a
c))
              (Judgement a -> Proof a
forall a. Judgement a -> Proof a
Axiom ([Formula a
d] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a
d))
          )
      )
-- Left conjunction elimination
proveToImpHypothesis (Imp (Var (And c :: Formula a
c d :: Formula a
d)) (Var c' :: Formula a
c'))
  | Formula a
c Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
c' =
    Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
ImpIntr
      ([] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
And Formula a
c Formula a
d) Formula a
c)
      ( Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
AndElimL
          ([Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
And Formula a
c Formula a
d] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a
c)
          (Judgement a -> Proof a
forall a. Judgement a -> Proof a
Axiom ([Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
And Formula a
c Formula a
d] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
And Formula a
c Formula a
d))
      )
-- Right conjunction elimination
proveToImpHypothesis (Imp (Var (And c :: Formula a
c d :: Formula a
d)) (Var d' :: Formula a
d'))
  | Formula a
d Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
d' =
    Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
ImpIntr
      ([] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
And Formula a
c Formula a
d) Formula a
d)
      ( Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
AndElimR
          ([Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
And Formula a
c Formula a
d] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a
d)
          (Judgement a -> Proof a
forall a. Judgement a -> Proof a
Axiom ([Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
And Formula a
c Formula a
d] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
And Formula a
c Formula a
d))
      )
-- Equivalence introduction
proveToImpHypothesis (Imp (Imp (Var c :: Formula a
c) (Var d :: Formula a
d)) (Imp (Imp (Var d' :: Formula a
d') (Var c' :: Formula a
c')) (Var (Iff c'' :: Formula a
c'' d'' :: Formula a
d''))))
  | Formula a
c Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
c' Bool -> Bool -> Bool
&& Formula a
c Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
c'' Bool -> Bool -> Bool
&& Formula a
d Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
d' Bool -> Bool -> Bool
&& Formula a
d Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
d'' =
    Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
ImpIntr
      ([] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c Formula a
d) (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
d Formula a
c) (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Iff Formula a
c Formula a
d)))
      ( Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
ImpIntr
          ([Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c Formula a
d] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
d Formula a
c) (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Iff Formula a
c Formula a
d))
          ( Judgement a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a
IffIntr
              ([Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c Formula a
d, Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
d Formula a
c] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Iff Formula a
c Formula a
d)
              (Judgement a -> Proof a
forall a. Judgement a -> Proof a
Axiom ([Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c Formula a
d] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c Formula a
d))
              (Judgement a -> Proof a
forall a. Judgement a -> Proof a
Axiom ([Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
d Formula a
c] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
d Formula a
c))
          )
      )
-- Left equivalence elimination
proveToImpHypothesis (Imp (Var (Iff c :: Formula a
c d :: Formula a
d)) (Imp (Var c' :: Formula a
c') (Var d' :: Formula a
d')))
  | Formula a
c Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
c' Bool -> Bool -> Bool
&& Formula a
d Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
d' =
    Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
ImpIntr
      ([] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Iff Formula a
c Formula a
d) (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c Formula a
d))
      ( Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
IffElimL
          ([Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Iff Formula a
c Formula a
d] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
c Formula a
d)
          (Judgement a -> Proof a
forall a. Judgement a -> Proof a
Axiom ([Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Iff Formula a
c Formula a
d] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Iff Formula a
c Formula a
d))
      )
-- Right equivalence elimination
proveToImpHypothesis (Imp (Var (Iff c :: Formula a
c d :: Formula a
d)) (Imp (Var d' :: Formula a
d') (Var c' :: Formula a
c')))
  | Formula a
c Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
c' Bool -> Bool -> Bool
&& Formula a
d Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
d' =
    Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
ImpIntr
      ([] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Iff Formula a
c Formula a
d) (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
d Formula a
c))
      ( Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
IffElimR
          ([Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Iff Formula a
c Formula a
d] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
d Formula a
c)
          (Judgement a -> Proof a
forall a. Judgement a -> Proof a
Axiom ([Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Iff Formula a
c Formula a
d] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Iff Formula a
c Formula a
d))
      )
-- This should never be reached! If it is, that means we're mishandling one of
-- the cases in the toImp translation
proveToImpHypothesis _ = Proof a
forall a. HasCallStack => a
undefined