-- |
-- Module      : AutoProof.Internal.Proof.Structural
-- Copyright   : (c) Artem Mavrin, 2021
-- License     : BSD3
-- Maintainer  : artemvmavrin@gmail.com
-- Stability   : experimental
-- Portability : POSIX
--
-- Structural rules to transform proofs.
module AutoProof.Internal.Proof.Structural
  ( weakenProof,
    strengthenProof,
  )
where

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

-- | The /weakening/ structural rule. @('weakenProof' p a)@ modifies the proof
-- @p@ to include @a@ as an additional hypothesis.
weakenProof :: Ord a => Proof a -> Formula a -> Proof a
weakenProof :: Proof a -> Formula a -> Proof a
weakenProof (Axiom j :: Judgement a
j) a :: Formula a
a = (Judgement a -> Proof a) -> Formula a -> Judgement a -> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a) -> Formula a -> Judgement a -> Proof a
weakenNullary Judgement a -> Proof a
forall a. Judgement a -> Proof a
Axiom Formula a
a Judgement a
j
weakenProof x :: Proof a
x@(FalseElim j :: Judgement a
j p :: Proof a
p) a :: Formula a
a = (Judgement a -> Proof a -> Proof a)
-> Proof a -> Formula a -> Judgement a -> Proof a -> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a -> Proof a)
-> Proof a -> Formula a -> Judgement a -> Proof a -> Proof a
weakenUnary Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
FalseElim Proof a
x Formula a
a Judgement a
j Proof a
p
weakenProof (TrueIntr j :: Judgement a
j) a :: Formula a
a = (Judgement a -> Proof a) -> Formula a -> Judgement a -> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a) -> Formula a -> Judgement a -> Proof a
weakenNullary Judgement a -> Proof a
forall a. Judgement a -> Proof a
TrueIntr Formula a
a Judgement a
j
weakenProof x :: Proof a
x@(NotElim j :: Judgement a
j p :: Proof a
p q :: Proof a
q) a :: Formula a
a = (Judgement a -> Proof a -> Proof a -> Proof a)
-> Proof a
-> Formula a
-> Judgement a
-> Proof a
-> Proof a
-> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a -> Proof a -> Proof a)
-> Proof a
-> Formula a
-> Judgement a
-> Proof a
-> Proof a
-> Proof a
weakenBinary Judgement a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a
NotElim Proof a
x Formula a
a Judgement a
j Proof a
p Proof a
q
weakenProof x :: Proof a
x@(NotIntr j :: Judgement a
j p :: Proof a
p) a :: Formula a
a = (Judgement a -> Proof a -> Proof a)
-> Proof a -> Formula a -> Judgement a -> Proof a -> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a -> Proof a)
-> Proof a -> Formula a -> Judgement a -> Proof a -> Proof a
weakenUnary Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
NotIntr Proof a
x Formula a
a Judgement a
j Proof a
p
weakenProof x :: Proof a
x@(ImpElim j :: Judgement a
j p :: Proof a
p q :: Proof a
q) a :: Formula a
a = (Judgement a -> Proof a -> Proof a -> Proof a)
-> Proof a
-> Formula a
-> Judgement a
-> Proof a
-> Proof a
-> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a -> Proof a -> Proof a)
-> Proof a
-> Formula a
-> Judgement a
-> Proof a
-> Proof a
-> Proof a
weakenBinary Judgement a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a
ImpElim Proof a
x Formula a
a Judgement a
j Proof a
p Proof a
q
weakenProof x :: Proof a
x@(ImpIntr j :: Judgement a
j p :: Proof a
p) a :: Formula a
a = (Judgement a -> Proof a -> Proof a)
-> Proof a -> Formula a -> Judgement a -> Proof a -> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a -> Proof a)
-> Proof a -> Formula a -> Judgement a -> Proof a -> Proof a
weakenUnary Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
ImpIntr Proof a
x Formula a
a Judgement a
j Proof a
p
weakenProof x :: Proof a
x@(OrElim j :: Judgement a
j p :: Proof a
p q :: Proof a
q r :: Proof a
r) a :: Formula a
a = (Judgement a -> Proof a -> Proof a -> Proof a -> Proof a)
-> Proof a
-> Formula a
-> Judgement a
-> Proof a
-> Proof a
-> Proof a
-> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a -> Proof a -> Proof a -> Proof a)
-> Proof a
-> Formula a
-> Judgement a
-> Proof a
-> Proof a
-> Proof a
-> Proof a
weakenTernary Judgement a -> Proof a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a -> Proof a
OrElim Proof a
x Formula a
a Judgement a
j Proof a
p Proof a
q Proof a
r
weakenProof x :: Proof a
x@(OrIntrL j :: Judgement a
j p :: Proof a
p) a :: Formula a
a = (Judgement a -> Proof a -> Proof a)
-> Proof a -> Formula a -> Judgement a -> Proof a -> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a -> Proof a)
-> Proof a -> Formula a -> Judgement a -> Proof a -> Proof a
weakenUnary Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
OrIntrL Proof a
x Formula a
a Judgement a
j Proof a
p
weakenProof x :: Proof a
x@(OrIntrR j :: Judgement a
j p :: Proof a
p) a :: Formula a
a = (Judgement a -> Proof a -> Proof a)
-> Proof a -> Formula a -> Judgement a -> Proof a -> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a -> Proof a)
-> Proof a -> Formula a -> Judgement a -> Proof a -> Proof a
weakenUnary Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
OrIntrR Proof a
x Formula a
a Judgement a
j Proof a
p
weakenProof x :: Proof a
x@(AndElimL j :: Judgement a
j p :: Proof a
p) a :: Formula a
a = (Judgement a -> Proof a -> Proof a)
-> Proof a -> Formula a -> Judgement a -> Proof a -> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a -> Proof a)
-> Proof a -> Formula a -> Judgement a -> Proof a -> Proof a
weakenUnary Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
AndElimL Proof a
x Formula a
a Judgement a
j Proof a
p
weakenProof x :: Proof a
x@(AndElimR j :: Judgement a
j p :: Proof a
p) a :: Formula a
a = (Judgement a -> Proof a -> Proof a)
-> Proof a -> Formula a -> Judgement a -> Proof a -> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a -> Proof a)
-> Proof a -> Formula a -> Judgement a -> Proof a -> Proof a
weakenUnary Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
AndElimR Proof a
x Formula a
a Judgement a
j Proof a
p
weakenProof x :: Proof a
x@(AndIntr j :: Judgement a
j p :: Proof a
p q :: Proof a
q) a :: Formula a
a = (Judgement a -> Proof a -> Proof a -> Proof a)
-> Proof a
-> Formula a
-> Judgement a
-> Proof a
-> Proof a
-> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a -> Proof a -> Proof a)
-> Proof a
-> Formula a
-> Judgement a
-> Proof a
-> Proof a
-> Proof a
weakenBinary Judgement a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a
AndIntr Proof a
x Formula a
a Judgement a
j Proof a
p Proof a
q
weakenProof x :: Proof a
x@(IffElimL j :: Judgement a
j p :: Proof a
p) a :: Formula a
a = (Judgement a -> Proof a -> Proof a)
-> Proof a -> Formula a -> Judgement a -> Proof a -> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a -> Proof a)
-> Proof a -> Formula a -> Judgement a -> Proof a -> Proof a
weakenUnary Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
IffElimL Proof a
x Formula a
a Judgement a
j Proof a
p
weakenProof x :: Proof a
x@(IffElimR j :: Judgement a
j p :: Proof a
p) a :: Formula a
a = (Judgement a -> Proof a -> Proof a)
-> Proof a -> Formula a -> Judgement a -> Proof a -> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a -> Proof a)
-> Proof a -> Formula a -> Judgement a -> Proof a -> Proof a
weakenUnary Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
IffElimR Proof a
x Formula a
a Judgement a
j Proof a
p
weakenProof x :: Proof a
x@(IffIntr j :: Judgement a
j p :: Proof a
p q :: Proof a
q) a :: Formula a
a = (Judgement a -> Proof a -> Proof a -> Proof a)
-> Proof a
-> Formula a
-> Judgement a
-> Proof a
-> Proof a
-> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a -> Proof a -> Proof a)
-> Proof a
-> Formula a
-> Judgement a
-> Proof a
-> Proof a
-> Proof a
weakenBinary Judgement a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a
IffIntr Proof a
x Formula a
a Judgement a
j Proof a
p Proof a
q

-- Helper functions for weakenProof

weakenNullary ::
  Ord a =>
  (Judgement a -> Proof a) ->
  Formula a ->
  Judgement a ->
  Proof a
weakenNullary :: (Judgement a -> Proof a) -> Formula a -> Judgement a -> Proof a
weakenNullary c :: Judgement a -> Proof a
c a :: Formula a
a j :: Judgement a
j = Judgement a -> Proof a
c (Judgement a -> Formula a -> Judgement a
forall a. Ord a => Judgement a -> Formula a -> Judgement a
weakenJudgement Judgement a
j Formula a
a)

weakenUnary ::
  Ord a =>
  (Judgement a -> Proof a -> Proof a) ->
  Proof a ->
  Formula a ->
  Judgement a ->
  Proof a ->
  Proof a
weakenUnary :: (Judgement a -> Proof a -> Proof a)
-> Proof a -> Formula a -> Judgement a -> Proof a -> Proof a
weakenUnary c :: Judgement a -> Proof a -> Proof a
c x :: Proof a
x a :: Formula a
a j :: Judgement a
j@(Judgement g :: Context a
g _) p :: Proof a
p
  | Formula a
a Formula a -> Context a -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Context a
g = Proof a
x
  | Bool
otherwise = Judgement a -> Proof a -> Proof a
c (Judgement a -> Formula a -> Judgement a
forall a. Ord a => Judgement a -> Formula a -> Judgement a
weakenJudgement Judgement a
j Formula a
a) (Proof a -> Formula a -> Proof a
forall a. Ord a => Proof a -> Formula a -> Proof a
weakenProof Proof a
p Formula a
a)

weakenBinary ::
  Ord a =>
  (Judgement a -> Proof a -> Proof a -> Proof a) ->
  Proof a ->
  Formula a ->
  Judgement a ->
  Proof a ->
  Proof a ->
  Proof a
weakenBinary :: (Judgement a -> Proof a -> Proof a -> Proof a)
-> Proof a
-> Formula a
-> Judgement a
-> Proof a
-> Proof a
-> Proof a
weakenBinary c :: Judgement a -> Proof a -> Proof a -> Proof a
c x :: Proof a
x a :: Formula a
a j :: Judgement a
j@(Judgement g :: Context a
g _) p :: Proof a
p q :: Proof a
q
  | Formula a
a Formula a -> Context a -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Context a
g = Proof a
x
  | Formula a
a Formula a -> Context a -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Judgement a -> Context a
forall a. Judgement a -> Context a
antecedents (Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
p) = Judgement a -> Proof a -> Proof a -> Proof a
c (Judgement a -> Formula a -> Judgement a
forall a. Ord a => Judgement a -> Formula a -> Judgement a
weakenJudgement Judgement a
j Formula a
a) Proof a
p Proof a
q
  | Formula a
a Formula a -> Context a -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Judgement a -> Context a
forall a. Judgement a -> Context a
antecedents (Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
q) = Judgement a -> Proof a -> Proof a -> Proof a
c (Judgement a -> Formula a -> Judgement a
forall a. Ord a => Judgement a -> Formula a -> Judgement a
weakenJudgement Judgement a
j Formula a
a) Proof a
p Proof a
q
  | Proof a -> Int
forall t. AST t => t -> Int
height Proof a
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Proof a -> Int
forall t. AST t => t -> Int
height Proof a
q = Judgement a -> Proof a -> Proof a -> Proof a
c (Judgement a -> Formula a -> Judgement a
forall a. Ord a => Judgement a -> Formula a -> Judgement a
weakenJudgement Judgement a
j Formula a
a) (Proof a -> Formula a -> Proof a
forall a. Ord a => Proof a -> Formula a -> Proof a
weakenProof Proof a
p Formula a
a) Proof a
q
  | Bool
otherwise = Judgement a -> Proof a -> Proof a -> Proof a
c (Judgement a -> Formula a -> Judgement a
forall a. Ord a => Judgement a -> Formula a -> Judgement a
weakenJudgement Judgement a
j Formula a
a) Proof a
p (Proof a -> Formula a -> Proof a
forall a. Ord a => Proof a -> Formula a -> Proof a
weakenProof Proof a
q Formula a
a)

weakenTernary ::
  Ord a =>
  (Judgement a -> Proof a -> Proof a -> Proof a -> Proof a) ->
  Proof a ->
  Formula a ->
  Judgement a ->
  Proof a ->
  Proof a ->
  Proof a ->
  Proof a
weakenTernary :: (Judgement a -> Proof a -> Proof a -> Proof a -> Proof a)
-> Proof a
-> Formula a
-> Judgement a
-> Proof a
-> Proof a
-> Proof a
-> Proof a
weakenTernary c :: Judgement a -> Proof a -> Proof a -> Proof a -> Proof a
c x :: Proof a
x a :: Formula a
a j :: Judgement a
j@(Judgement g :: Context a
g _) p :: Proof a
p q :: Proof a
q r :: Proof a
r
  | Formula a
a Formula a -> Context a -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Context a
g = Proof a
x
  | Formula a
a Formula a -> Context a -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Judgement a -> Context a
forall a. Judgement a -> Context a
antecedents (Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
p) = Judgement a -> Proof a -> Proof a -> Proof a -> Proof a
c (Judgement a -> Formula a -> Judgement a
forall a. Ord a => Judgement a -> Formula a -> Judgement a
weakenJudgement Judgement a
j Formula a
a) Proof a
p Proof a
q Proof a
r
  | Formula a
a Formula a -> Context a -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Judgement a -> Context a
forall a. Judgement a -> Context a
antecedents (Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
q) = Judgement a -> Proof a -> Proof a -> Proof a -> Proof a
c (Judgement a -> Formula a -> Judgement a
forall a. Ord a => Judgement a -> Formula a -> Judgement a
weakenJudgement Judgement a
j Formula a
a) Proof a
p Proof a
q Proof a
r
  | Formula a
a Formula a -> Context a -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Judgement a -> Context a
forall a. Judgement a -> Context a
antecedents (Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
r) = Judgement a -> Proof a -> Proof a -> Proof a -> Proof a
c (Judgement a -> Formula a -> Judgement a
forall a. Ord a => Judgement a -> Formula a -> Judgement a
weakenJudgement Judgement a
j Formula a
a) Proof a
p Proof a
q Proof a
r
  | Proof a -> Int
forall t. AST t => t -> Int
height Proof a
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int -> Int -> Int
forall a. Ord a => a -> a -> a
min (Proof a -> Int
forall t. AST t => t -> Int
height Proof a
q) (Proof a -> Int
forall t. AST t => t -> Int
height Proof a
r) = Judgement a -> Proof a -> Proof a -> Proof a -> Proof a
c (Judgement a -> Formula a -> Judgement a
forall a. Ord a => Judgement a -> Formula a -> Judgement a
weakenJudgement Judgement a
j Formula a
a) (Proof a -> Formula a -> Proof a
forall a. Ord a => Proof a -> Formula a -> Proof a
weakenProof Proof a
p Formula a
a) Proof a
q Proof a
r
  | Proof a -> Int
forall t. AST t => t -> Int
height Proof a
q Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int -> Int -> Int
forall a. Ord a => a -> a -> a
min (Proof a -> Int
forall t. AST t => t -> Int
height Proof a
p) (Proof a -> Int
forall t. AST t => t -> Int
height Proof a
r) = Judgement a -> Proof a -> Proof a -> Proof a -> Proof a
c (Judgement a -> Formula a -> Judgement a
forall a. Ord a => Judgement a -> Formula a -> Judgement a
weakenJudgement Judgement a
j Formula a
a) Proof a
p (Proof a -> Formula a -> Proof a
forall a. Ord a => Proof a -> Formula a -> Proof a
weakenProof Proof a
q Formula a
a) Proof a
r
  | Bool
otherwise = Judgement a -> Proof a -> Proof a -> Proof a -> Proof a
c (Judgement a -> Formula a -> Judgement a
forall a. Ord a => Judgement a -> Formula a -> Judgement a
weakenJudgement Judgement a
j Formula a
a) Proof a
p Proof a
q (Proof a -> Formula a -> Proof a
forall a. Ord a => Proof a -> Formula a -> Proof a
weakenProof Proof a
r Formula a
a)

-- | Strengthen a proof by preserving its structure but removing redundant
-- hypotheses where possible.
strengthenProof :: Ord a => Proof a -> Proof a
strengthenProof :: Proof a -> Proof a
strengthenProof (Axiom (Judgement _ a :: Formula a
a)) = 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 (Formula a -> Context a
forall a. a -> Set a
Set.singleton Formula a
a) Formula a
a)
strengthenProof (FalseElim j :: Judgement a
j p :: Proof a
p) = (Judgement a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a
strengthenUnary Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
FalseElim Judgement a
j Proof a
p
strengthenProof (TrueIntr (Judgement _ a :: Formula a
a)) = Judgement a -> Proof a
forall a. Judgement a -> Proof a
TrueIntr (Context a -> Formula a -> Judgement a
forall a. Context a -> Formula a -> Judgement a
Judgement Context a
forall a. Set a
Set.empty Formula a
a)
strengthenProof (NotElim j :: Judgement a
j p :: Proof a
p q :: Proof a
q) = (Judgement a -> Proof a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a -> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a -> Proof a
strengthenBinary Judgement a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a
NotElim Judgement a
j Proof a
p Proof a
q
strengthenProof (NotIntr (Judgement _ a :: Formula a
a@(Not b :: Formula a
b)) p :: Proof a
p) = (Judgement a -> Proof a -> Proof a)
-> Formula a -> Formula a -> Proof a -> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a -> Proof a)
-> Formula a -> Formula a -> Proof a -> Proof a
strengthenUnaryImp Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
NotIntr Formula a
a Formula a
b Proof a
p
strengthenProof (ImpElim j :: Judgement a
j p :: Proof a
p q :: Proof a
q) = (Judgement a -> Proof a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a -> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a -> Proof a
strengthenBinary Judgement a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a
ImpElim Judgement a
j Proof a
p Proof a
q
strengthenProof (ImpIntr (Judgement _ a :: Formula a
a@(Imp b :: Formula a
b _)) p :: Proof a
p) = (Judgement a -> Proof a -> Proof a)
-> Formula a -> Formula a -> Proof a -> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a -> Proof a)
-> Formula a -> Formula a -> Proof a -> Proof a
strengthenUnaryImp Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
ImpIntr Formula a
a Formula a
b Proof a
p
strengthenProof (OrElim j :: Judgement a
j p :: Proof a
p q :: Proof a
q r :: Proof a
r) = Judgement a -> Proof a -> Proof a -> Proof a -> Proof a
forall a.
Ord a =>
Judgement a -> Proof a -> Proof a -> Proof a -> Proof a
strengthenOrElim Judgement a
j Proof a
p Proof a
q Proof a
r
strengthenProof (OrIntrL j :: Judgement a
j p :: Proof a
p) = (Judgement a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a
strengthenUnary Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
OrIntrL Judgement a
j Proof a
p
strengthenProof (OrIntrR j :: Judgement a
j p :: Proof a
p) = (Judgement a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a
strengthenUnary Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
OrIntrR Judgement a
j Proof a
p
strengthenProof (AndElimL j :: Judgement a
j p :: Proof a
p) = (Judgement a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a
strengthenUnary Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
AndElimL Judgement a
j Proof a
p
strengthenProof (AndElimR j :: Judgement a
j p :: Proof a
p) = (Judgement a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a
strengthenUnary Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
AndElimR Judgement a
j Proof a
p
strengthenProof (AndIntr j :: Judgement a
j p :: Proof a
p q :: Proof a
q) = (Judgement a -> Proof a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a -> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a -> Proof a
strengthenBinary Judgement a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a
AndIntr Judgement a
j Proof a
p Proof a
q
strengthenProof (IffElimL j :: Judgement a
j p :: Proof a
p) = (Judgement a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a
strengthenUnary Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
IffElimL Judgement a
j Proof a
p
strengthenProof (IffElimR j :: Judgement a
j p :: Proof a
p) = (Judgement a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a
strengthenUnary Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
IffElimR Judgement a
j Proof a
p
strengthenProof (IffIntr j :: Judgement a
j p :: Proof a
p q :: Proof a
q) = (Judgement a -> Proof a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a -> Proof a
forall a.
Ord a =>
(Judgement a -> Proof a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a -> Proof a
strengthenBinary Judgement a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a
IffIntr Judgement a
j Proof a
p Proof a
q
-- If we're here, then there was a pattern match failure, and the proof is
-- invalid! Note that there are some invalid proofs that will nevertheless slip
-- through this function; its goal is not to check validity. However, a valid
-- input proof should yield a valid output proof.
strengthenProof p :: Proof a
p = Proof a
p

-- Helper functions for strengthenProof

strengthenUnary ::
  Ord a =>
  (Judgement a -> Proof a -> Proof a) ->
  Judgement a ->
  Proof a ->
  Proof a
strengthenUnary :: (Judgement a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a
strengthenUnary c :: Judgement a -> Proof a -> Proof a
c (Judgement _ a :: Formula a
a) p :: Proof a
p =
  let p' :: Proof a
p' = Proof a -> Proof a
forall a. Ord a => Proof a -> Proof a
strengthenProof Proof a
p
      g :: Context a
g = Judgement a -> Context a
forall a. Judgement a -> Context a
antecedents (Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
p')
   in Judgement a -> Proof a -> Proof a
c (Context a -> Formula a -> Judgement a
forall a. Context a -> Formula a -> Judgement a
Judgement Context a
g Formula a
a) Proof a
p'

strengthenBinary ::
  Ord a =>
  (Judgement a -> Proof a -> Proof a -> Proof a) ->
  Judgement a ->
  Proof a ->
  Proof a ->
  Proof a
strengthenBinary :: (Judgement a -> Proof a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a -> Proof a
strengthenBinary c :: Judgement a -> Proof a -> Proof a -> Proof a
c (Judgement _ a :: Formula a
a) p :: Proof a
p q :: Proof a
q =
  let p' :: Proof a
p' = Proof a -> Proof a
forall a. Ord a => Proof a -> Proof a
strengthenProof Proof a
p
      q' :: Proof a
q' = Proof a -> Proof a
forall a. Ord a => Proof a -> Proof a
strengthenProof Proof a
q
      gp :: Context a
gp = Judgement a -> Context a
forall a. Judgement a -> Context a
antecedents (Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
p')
      gq :: Context a
gq = Judgement a -> Context a
forall a. Judgement a -> Context a
antecedents (Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
q')
      g :: Context a
g = Context a -> Context a -> Context a
forall a. Ord a => Set a -> Set a -> Set a
Set.union Context a
gp Context a
gq
   in Judgement a -> Proof a -> Proof a -> Proof a
c (Context a -> Formula a -> Judgement a
forall a. Context a -> Formula a -> Judgement a
Judgement Context a
g Formula a
a) Proof a
p' Proof a
q'

-- Implication and negation introduction rules involve removing a hypothesis
-- and must be treated as a special case
strengthenUnaryImp ::
  Ord a =>
  (Judgement a -> Proof a -> Proof a) ->
  Formula a ->
  Formula a ->
  Proof a ->
  Proof a
strengthenUnaryImp :: (Judgement a -> Proof a -> Proof a)
-> Formula a -> Formula a -> Proof a -> Proof a
strengthenUnaryImp c :: Judgement a -> Proof a -> Proof a
c a :: Formula a
a b :: Formula a
b p :: Proof a
p =
  let p' :: Proof a
p' = Proof a -> Proof a
forall a. Ord a => Proof a -> Proof a
strengthenProof Proof a
p
      p'' :: Proof a
p'' = Proof a -> Formula a -> Proof a
forall a. Ord a => Proof a -> Formula a -> Proof a
weakenProof Proof a
p' Formula a
b -- b might not be needed in p'
      g :: Context a
g = Judgement a -> Context a
forall a. Judgement a -> Context a
antecedents (Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
p'')
      g' :: Context a
g' = Formula a -> Context a -> Context a
forall a. Ord a => a -> Set a -> Set a
Set.delete Formula a
b Context a
g
   in Judgement a -> Proof a -> Proof a
c (Context a -> Formula a -> Judgement a
forall a. Context a -> Formula a -> Judgement a
Judgement Context a
g' Formula a
a) Proof a
p''

strengthenOrElim ::
  Ord a =>
  Judgement a ->
  Proof a ->
  Proof a ->
  Proof a ->
  Proof a
strengthenOrElim :: Judgement a -> Proof a -> Proof a -> Proof a -> Proof a
strengthenOrElim j :: Judgement a
j@(Judgement _ c :: Formula a
c) p :: Proof a
p q :: Proof a
q r :: Proof a
r = case 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
p) of
  Or a :: Formula a
a b :: Formula a
b ->
    let p' :: Proof a
p' = Proof a -> Proof a
forall a. Ord a => Proof a -> Proof a
strengthenProof Proof a
p
        q' :: Proof a
q' = Proof a -> Proof a
forall a. Ord a => Proof a -> Proof a
strengthenProof Proof a
q
        r' :: Proof a
r' = Proof a -> Proof a
forall a. Ord a => Proof a -> Proof a
strengthenProof Proof a
r
        q'' :: Proof a
q'' = Proof a -> Formula a -> Proof a
forall a. Ord a => Proof a -> Formula a -> Proof a
weakenProof Proof a
q' Formula a
a -- a might not be needed in q'
        r'' :: Proof a
r'' = Proof a -> Formula a -> Proof a
forall a. Ord a => Proof a -> Formula a -> Proof a
weakenProof Proof a
r' Formula a
b -- b might not be needed in r'
        g1 :: Context a
g1 = Judgement a -> Context a
forall a. Judgement a -> Context a
antecedents (Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
p')
        g2 :: Context a
g2 = Formula a -> Context a -> Context a
forall a. Ord a => a -> Set a -> Set a
Set.delete Formula a
a (Judgement a -> Context a
forall a. Judgement a -> Context a
antecedents (Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
q''))
        g3 :: Context a
g3 = Formula a -> Context a -> Context a
forall a. Ord a => a -> Set a -> Set a
Set.delete Formula a
b (Judgement a -> Context a
forall a. Judgement a -> Context a
antecedents (Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
r''))
        g :: Context a
g = 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
     in Judgement a -> Proof a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a -> Proof a
OrElim (Context a -> Formula a -> Judgement a
forall a. Context a -> Formula a -> Judgement a
Judgement Context a
g Formula a
c) Proof a
p' Proof a
q'' Proof a
r''
  _ -> 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
p Proof a
q Proof a
r -- Wrong form of inference rule!