Proof Logic extensions

Terms of Proof Logic are proofs. A proof x proves an equality a = b, where a = left(x) and b = right(x), and a and b are also proofs. The basic operators of the initial version of Proof Logic are defined by the left and right sides of the equality proved by a proof built with these operators :

If x is a symbol or the variable "*", then left(x) = x and right(x) = x, which means that x proves x = x.
left('x) = 'left(x) ; right('x) = 'right(x)
left([x]) = [left(x)] ; right([x]) = [right(x)]
left(x y) = left(x) left(y) ; right(x y) = right(x) right(y), which means that if x proves a = b and y proves c = d then x y proves a c = b d.
left({x,y}) = right(x) and right({x,y}) = right(y) if left(x) and left(y) reduce to a same term, otherwise left({x,y}) = right({x,y}) = {x,y}
left(a=b) = a ; right(a=b) = b

These operators (except the last one which expresses the axiom a=b) can be seen as logical rules, where x proves a = b and y proves c = d :

s : |- s = s ; * : |- * = *
' : a = b |- 'a = 'b
[] : a = b |- [a] = [b]
() : a = b, c = d |- a c = b d
{,} : a = b, c = d, red(a) = red(c) |- b = d

The operator {,} introduces a dissymetry between left and right sides of equalities. We can extend the theory by adding the symmetric operator written <|> and defined by :

left(<x|y>) = left(x) and right(<x,y>) = left(y) if right(x) and right(y) reduce to the same term, otherwise left(<x|y>) = right(<x|y>) = <x|y>

It corresponds to the logical rule :

<|> : a = b, c = d, red(b) = red(d) |- a = c

It can be defined from {,} : <x|y> = { {x,left(x)}, {y,left(y)} }.
Suppose we have x proves a = b, y proves c = d, red(b) = red(d). Then left(x) proves a = a, {x,left(x)} proves b = a. And left(y) proves c = c, {y,left(y)} proves d = c. Then { {x,left(x)}, {y,left(y)} } proves a = c since red(b) = red(d).

The operator "@" can also be introduced to implement definitions of the form "let name = definition in proof". It is not necessary but useful to write proofs more easily. It is defined by :

left(@x) = left(red(x)) ; right(@x) = right(red(x))

The operator "@" is more difficult to express in terms of logical rules because the definition of left(@x) and right(@x) does not involve left(x) and right(x). Perhaps we could write something like :

@ : x |- left(red(x)) = right(red(x))

These basic operators can be composed to define new operators. For example, we can define operators LFT and RGT by :

left(LFT x) = left x ; right(LFT x) = left x
left(RGT x) = right(x) ; right(RGT x) = right x

corresponding to the logical rules :

LFT : a = b |- a = a
RGT : a = b |- b = b

These operators can obviously be defined by :

LFT x = <x|x>
RGT x = {x,x}

We can define an operator associated to the symmetry rule :

SYM : a = b |- b = a

This operator is defined by :

left(SYM x) = right(x)
right(SYM x) = left(x)

It can be defined by a combination of {,} and LFT, or of <|> and RGT :

SYM x = {x,LFT x} = <RGT x|x>

The transitivity rule is :

TRN : a = b, b = c |- a = c

The corresponding operator is defined by :

if right(x) = left(y) then left(TRN x y) = left(x) and right(TRN x y) = right(y)

It can be defined by a combination of {,} or <|>, and SYM :

TRN x y = {SYM x,y} = <x|SYM y>

We can say that if a = b, then red(a) = b. This is formalized by the RDL rule :

RDL : a = b |- red(a) = b

The corresponding operator is defined by :

left(RDL x) = red(left(x))
right(RDL x) = right(x)

It can also be defined by a combination of {,}, @ and LFT :

RDL x = {@(LFT x),x}

The symmetric rule is :

RDR : a = b |- a = red(b)

The corresponding operator is defined by :

left(RDR x) = left(x)
right(RDR x) = red(right(x))

It can also be defined by a combination of <|>, @ and RGT :

RDR x = <x|@(RGT x)>

RDL can also be defined from RDR and reciprocally :

RDL x = SYM (RDR (SYM x))
RDR x = SYM (RDL (SYM x))

We can also reduce both left and right sides :

RDB : a = b |- red(a) = red(b)

The corresponding operator is defined by :

left(RDB x) = red(left(x))
right(RDB x) = red(right(x))

It can be defined by a combination of RDL or RDR, and SYM :

RDB x = SYM (RDL (SYM (RDL x)))
RDB x = RDL (SYM (RDL (SYM x)))
RDB x = SYM (RDR (SYM (RDR x)))
RDB x = RDR (SYM (RDR (SYM x)))

A rule can also be introduced to do the substitution in application of a function to an argument :

SUB : a = b, c = d |- [a] c = subst(*,b,d)

The corresponding operator is defined by :

left(SUB x y) = [left(x)] left(y)
right(SUB x y) = subst(*,right(x),right(y))

Definitions of extensions with Haskell program

The definitions of new operators as combinations of basic operators look like the definition of new combinators as combination of basic combinators (K, S) in combinatory logic. But here we are at some kind of "meta" level. However, it seems that such definitions at "normal" level works if we use the @ operator. For example, we have seen that LFT x = <x|x>. With lambda calculus-like notation it gives "LFT = ^x <x|x>". If we apply it to a proof, for example the axiom a = b, we get :

PL> proves $ pl "^x <x|x> (a=b)"

The proof
  [< * |
     * >] (a = b) 
proves
  [*] a
= [*] b

We would like to obtain that it proves a = a. But with the @ operator, we get :

PL> proves $ pl "@ (^x <x|x> (a=b))"

The proof
  @([< * |
       * >] (a = b)) 
proves
  a
= a

Remember that the @ operator is defined by :

left(@x) = left(red(x)) ; right(@x) = right(red(x))

The reduction of its operand gives :

PL> red $ pl "(^x <x|x> (a=b))"
< (a = b) |
  (a = b) >

which proves a = a :

PL> proves $ red $ pl "(^x <x|x> (a=b))"

The proof
  < (a = b) |
    (a = b) >
proves
  a
= a

We can also use the notation "! x y z" (equivalent of "let x = y in z" in Haskell) since the definition of ! embeds the @ operator (RED in Haskell code) :

 pl1 ('!' : s) = let (x, t) = pl1 s in case x of SMB x1 -> let (y, u) = pl1 t in let (z, v) = pl1 u in (RED (APL (lambda x1 z) y), v)

Here is the result with LFT defined by ! :

PL> proves $ pl "! LFT ^x <x|x> (LFT (a=b))"

The proof
  @([* (a = b)] [< * |
                   * >]) 
proves
  a
= a

This definition does not give exactly the same result than the operator we want to define, because the operator we obtain by this method also reduces the terms of the conclusion, for example :

PL> proves $ pl "! LFT ^x <x|x> (LFT ([*]a=b))"

The proof
  @([* ([*] a = b)] [< * |
                       * >]) 
proves
  a
= a

We obtain a = a instead of [*]a = [*]a.

Here are some other examples of such definitions :

PL> proves $ pl "! RGT ^x {x,x} (RGT (a=b))"

The proof
  @([* (a = b)] [{ * ,
                   * }])
proves
  b
= b

PL> proves $ pl "! LFT ^x <x|x> ! SYM ^x {x,(LFT x)} (SYM(a=b))"

The proof
  @([@([* (a = b)] [{ * ,
                      '* * }])] [< * |
                                   * >])
proves
  b
= a

PL> proves $ pl "! LFT ^x <x|x> ! SYM ^x {x,(LFT x)} ! TRN ^x ^y {(SYM x),y} (TRN (a=b) (b=c)"

The proof
  @([@([@([* (a = b) (b = c)] [[{ ''* '* ,
                                  * }]])] [{ * ,
                                             '* * }])] [< * |
                                                          * >])
proves
  a
= c

Haskell code

module PL where
 
 import Data.List

 data Proof = SMB String
            | VAR 
            | NXV Proof
            | FNC Proof
            | RED Proof
            | APL Proof Proof
            | LTR Proof Proof
			| RTR Proof Proof
            | EQU Proof Proof			
	deriving (Eq)
	
 data Side = LeftSide | RightSide
	deriving (Eq, Show)

 data Context = Function | Argument | Other
	deriving (Eq, Show)


 -- shift u x increases all variables greater than u in x
 shift :: Proof -> Proof -> Proof
 shift _ (SMB s) = SMB s
 shift VAR VAR = NXV VAR
 shift _ VAR = VAR
 shift (NXV u) (NXV x) = NXV (shift u x)
 shift u (NXV x) = NXV (shift u x)
 shift u (FNC x) = FNC (shift (NXV u) x)
 shift u (RED x) = RED (shift u x)
 shift u (APL x y) = APL (shift u x) (shift u y)
 shift u (LTR x y) = LTR (shift u x) (shift u y)
 shift u (RTR x y) = RTR (shift u x) (shift u y)
 shift u (EQU x y) = EQU (shift u x) (shift u y)

 -- subst u a b (approximatively) replaces u in a by b (a little more complex in fact)
 subst :: Proof -> Proof -> Proof -> Proof
 subst1 :: Proof -> Proof -> Proof -> Proof
 subst u a b = if u == a then b else (if NXV u == a then u else subst1 u a b)
 subst1 _ (SMB s) _ = SMB s
 subst1 _ VAR _ = VAR
 subst1 u (NXV x) b = NXV (subst u x b)
 subst1 u (FNC x) b = FNC (subst (NXV u) x (shift VAR b))
 subst1 u (RED x) b = RED (subst u x b)
 subst1 u (APL x y) b = APL (subst u x b) (subst u y b)
 subst1 u (LTR x y) b = LTR (subst u x b) (subst u y b)
 subst1 u (RTR x y) b = RTR (subst u x b) (subst u y b) 
 subst1 u (EQU x y) b = EQU (subst u x b) (subst u y b)

 -- cont x y tests if x contains y 
 cont :: Proof -> Proof -> Bool
 cont1 :: Proof -> Proof -> Bool
 cont x y = if x == y then True else cont1 x y
 cont1 (SMB s) _ = False
 cont1 VAR _ = False
 cont1 (NXV x) y = cont x y
 cont1 (FNC x) y = cont x y
 cont1 (RED x) y = cont x y
 cont1 (APL x y) z = (cont x z) || (cont y z)
 cont1 (LTR x y) z = (cont x z) || (cont y z)
 cont1 (RTR x y) z = (cont x z) || (cont y z)
 cont1 (EQU x y) z = (cont x z) || (cont y z)

 -- red1 does one step of reduction
 red1 :: Proof -> Proof
 red1 (SMB s) = SMB s
 red1 VAR = VAR
 red1 (NXV x) = NXV (red1 x)
 red1 (FNC x) = FNC (red1 x)
 red1 (RED x) = RED (red1 x)
 red1 (APL (FNC x) y) = subst VAR x y
 red1 (APL x y) = APL (red1 x) (red1 y)
 red1 (LTR x y) = LTR (red1 x) (red1 y)
 red1 (RTR x y) = RTR (red1 x) (red1 y) 
 red1 (EQU x y) = EQU (red1 x) (red1 y)

 red2 :: [Proof] -> [Proof]
 red2 [] = []
 red2 (x : l) = (red1 x) : (x : l)

 red3 :: [Proof] -> [Proof]
 red3 [] = []
 red3 (x : l) = case find (\y -> cont x y) l of
	Nothing -> red3 (red2 (x : l))
	Just _ -> x : l

 -- red : reduction
 red :: Proof -> Proof
 red x = case red3 (x : []) of
		[] -> x
		y : m -> y

 side :: Side -> Proof -> Proof
 side _ (SMB s) = SMB s
 side _ VAR = VAR
 side s (NXV x) = NXV (side s x)
 side s (FNC x) = FNC (side s x)
 side s (RED x) = side s (red x)
 side s (APL x y) = APL (side s x) (side s y)
 side s (LTR x y) = if red (side LeftSide x) == red (side LeftSide y) then (side RightSide (if s == LeftSide then x else y)) else LTR x y
 side s (RTR x y) = if red (side RightSide x) == red (side RightSide y) then (side LeftSide (if s == LeftSide then x else y)) else RTR x y
 side LeftSide (EQU x y) = x
 side RightSide (EQU x y) = y

 left = side LeftSide 
 right = side RightSide 


 contSmb :: Proof -> String -> Bool
 contSmb x s = cont x (SMB s)
 
 abstr :: Proof -> String -> Proof -> Proof
 abstr1 :: Proof -> String -> Proof -> Proof
 abstr d v x = if (contSmb x v) then (abstr1 d v x) else x
 abstr1 d v (EQU x y) = EQU (abstr d v x) (abstr d v y)
 abstr1 d v (SMB s) = if v == s then d else (SMB s)
 abstr1 d v VAR = VAR
 abstr1 d v (NXV x) = NXV (abstr d v x)
 abstr1 d v (FNC x) = FNC (abstr (NXV d) v x)
 abstr1 d v (RED x) = RED (abstr d v x)
 abstr1 d v (APL x y) = APL (abstr d v x) (abstr d v y)
 abstr1 d v (LTR x y) = LTR (abstr d v x) (abstr d v y)
 abstr1 d v (RTR x y) = RTR (abstr d v x) (abstr d v y)
 
 lambda :: String -> Proof -> Proof
 lambda v x = FNC (abstr VAR v x)


 proves x = do
  putStr ("\nThe proof\n  " ++ showproof1 Other 2 x ++ " \nproves\n  " ++ showproof1 Other 2 (left x) ++ "\n= " ++ showproof1 Other 2 (right x) ++ "\n")

 reducesTo x = do
  putStr ("\n  " ++ show x ++ "\nreduces to\n  " ++ show (red x) ++ "\n")

 ident = FNC VAR

 -- Multiple application
 apl2 f x y = APL (APL f x) y
 apl3 f x y z = APL (APL (APL f x) y) z
 
 -- Application with reduction
 apr r x = LTR (LTR (APL r x) (red (left (APL r x)))) (red (right (APL r x)))
 apr2 r x y = apr (apr r x) y
 apr3 r x y z = apr (apr (apr r x) y) z 
					   
 column col s = let l = length (lines s) in if l > 1 then length $ last $ lines s else col + length s 
 
 -- showproof1 ctx col x : user readable representation of x in context ctx at column col
 showproof1 :: Context -> Int -> Proof -> String
 showproof1 _ _ (SMB s) = s
 showproof1 _ _ VAR = "*"
 showproof1 _ col (NXV x) = "'" ++ showproof1 Argument (col+1) x
 showproof1 _ col (FNC x) = "[" ++ showproof1 Other (col+1) x ++ "]"
 showproof1 _ col (RED x) = "@" ++ showproof1 Argument (col+1) x
 showproof1 Argument col (APL x y) = "(" ++ showproof1 Other (col+1) (APL x y) ++ ")"
 showproof1 _ col (APL x y) = let s = showproof1 Function col x in s ++ " " ++ showproof1 Argument (column col s + 1) y 
 -- showproof1 _ (LTR x y) = "{ " ++ showproof1 Other x ++ " , " ++ showproof1 Other y ++ " }"
 showproof1 _ col (LTR x y) = "{ " ++ showproof1 Other (col+2) x ++ " ,\n" ++ concat (replicate (col+2) " ") ++ showproof1 Other (col+2) y ++ " }"
 showproof1 _ col (RTR x y) = "< " ++ showproof1 Other (col+2) x ++ " |\n" ++ concat (replicate (col+2) " ") ++ showproof1 Other (col+2) y ++ " >"
 -- showproof1 Other col (EQU x y) = let s = showproof1 Other col x in s ++ " = " ++ showproof1 Other (col + (length s) + 3) y 
 -- showproof1 _ col (EQU x y) = "(" ++ showproof1 Other (col+1) (EQU x y) ++ ")"
 showproof1 _ col (EQU x y) = let s = showproof1 Other (col+1) x in "(" ++ s ++ " = " ++ showproof1 Other (column (col+1) s + 3) y ++ ")" 
  
 -- showproof x = user readable representation of proof x
 showproof = showproof1 Other 0
 
 instance Show Proof where
  show x = showproof x
 

 -- Convert string to proof
 
 pl1 (' ' : s) = pl1 s
 pl1 ('\t' : s) = pl1 s
 pl1 ('\n' : s) = pl1 s
 pl1 ('\r' : s) = pl1 s
 pl1 ('#' : s) = pl1 $ concat $ map (\l -> l ++ "\n") $ tail $ lines s
 pl1 ('(' : s) = pl3 ')' Nothing Nothing s
 pl1 ('*' : s) = (VAR, s)
 pl1 ('\'' : s) = let (x, t) = pl1 s in (NXV x, t)
 pl1 ('[' : s) = let (x, t) = pl3 ']' Nothing Nothing s in (FNC x, t)
 pl1 ('@' : s) = let (x, t) = pl1 s in (RED x, t)
 pl1 ('-' : s) = let (x, t) = pl1 s in let (y, u) = pl1 t in (apr x y, u)
 pl1 ('{' : s) = let (x, t) = pl3 ',' Nothing Nothing s in let (y, u) = pl3 '}' Nothing Nothing t in (LTR x y, u)
 pl1 ('<' : s) = let (x, t) = pl3 '|' Nothing Nothing s in let (y, u) = pl3 '>' Nothing Nothing t in (RTR x y, u)
 pl1 ('^' : s) = let (x, t) = pl1 s in case x of SMB v -> let (y, u) = pl1 t in (lambda v y, u)
 pl1 ('!' : s) = let (x, t) = pl1 s in case x of SMB x1 -> let (y, u) = pl1 t in let (z, v) = pl1 u in (RED (APL (lambda x1 z) y), v)
 pl1 (c : s) = pl4 [c] s
 
 pl4 s "" = (SMB s, "")
 pl4 s (' ' : t) = (SMB s, t)
 pl4 s ('\t' : t) = (SMB s, t)
 pl4 s ('\n' : t) = (SMB s, t)
 pl4 s ('\r' : t) = (SMB s, t)
 pl4 s (c : t) = if (any.(==)) c " \t\n()*'\\[]-%{,}<|>#=" then (SMB s, (c : t)) else pl4 (s ++ [c]) t
 
 pl2 e (' ' : s) = pl2 e s
 pl2 e ('\t' : s) = pl2 e s
 pl2 e ('\n' : s) = pl2 e s
 pl2 e ('\r' : s) = pl2 e s
 pl2 e "" = (False, Nothing, "")
 pl2 e (c : s) = if c == e then (False, Nothing, s) else if c == '=' then (True, Nothing, s) else let (x, t) = pl1 (c : s) in (False, Just x, t)
 
 pl3 e l Nothing (':' : s) = let (y, t) = pl3 e l Nothing s in (y, t)
 pl3 e l (Just x) (':' : s) = let (y, t) = pl3 e l Nothing s in (APL x y, t)
 pl3 e l x1 s = let x = case x1 of { Nothing -> FNC VAR; Just x2 -> x2 } in case pl2 e s of
	(False, Nothing, t) -> case l of 
	                           Nothing -> (x, t)
	                           Just l -> (EQU l x, t)
	(True, Nothing, t) -> case l of 
	                          Nothing -> pl3 e (Just x) Nothing t
	                          Just l -> pl3 e (Just (EQU l x)) Nothing t		
	(False, Just y, t) -> case x1 of 
	                          Nothing -> pl3 e l (Just y) t
	                          _ -> pl3 e l (Just (APL x y)) t	
							  
 pl s = let (x, t) = pl3 '.' Nothing Nothing s in x
 
 run filename = do
  readFile filename >>= \s -> proves $ pl s


 -- Example of theory
 
 parent = apl2 (SMB "parent")
 grandparent = apl2 (SMB "grandparent")
 allan = SMB "allan"
 brenda = SMB "brenda"
 charles = SMB "charles"

 gpRule1 = lambda "x" $ lambda "y" $ lambda "z" $ 
  EQU (APL (parent (SMB "x") (SMB "y")) $
       APL (parent (SMB "y") (SMB "z")) $
       grandparent (SMB "x") (SMB "z"))
      ident
 gpAxiom1 = EQU (parent allan brenda) ident
 gpAxiom2 = EQU (parent brenda charles) ident
 
 gpTheorem1 = LTR (apr gpAxiom2 (grandparent allan charles))
                  (LTR (apr gpAxiom1 (APL (parent brenda charles) (grandparent allan charles)))
                       (apr3 gpRule1 allan brenda charles))

				
 gpRule1b = pl "^x ^y ^z ( (parent x y : parent y z : grandparent x z) = [*] )"
 gpAxiom1b = pl "parent allan brenda = [*]"
 gpAxiom2b = pl "parent brenda charles = [*]"
 
 gpTheorem1b = LTR (apr gpAxiom2b (grandparent allan charles))
                   (LTR (apr gpAxiom1b (APL (parent brenda charles) (grandparent allan charles)))
                        (apr3 gpRule1b allan brenda charles))
								  
 gpTheorem1c = pl "\
  \ ! gpRule1  ^x ^y ^z ( (parent x y : parent y z : grandparent x z) = [*] ) \
  \ ! gpAxiom1 (parent allan brenda = [*]) \
  \ ! gpAxiom2 (parent brenda charles = [*]) \
  \ ! gpLemma1c (gpRule1 allan brenda charles) \
  \ ! gpLemma2c (gpAxiom1 (parent brenda charles (grandparent allan charles))) \
  \ ! gpLemma3c1 { gpLemma2c , gpLemma1c } \
  \ ! gpLemma3c { { gpLemma3c1 , (parent brenda charles (grandparent allan charles)) } , [*] } \
  \ ! gpLemma4c (gpAxiom2 (grandparent allan charles)) \
  \ ! gpLemma5c { gpLemma4c , gpLemma3c } \
  \ ! gpTheorem1c { grandparent allan charles , gpLemma5c } \
  \ gpTheorem1c "
		
 test = do
  proves gpTheorem1
  proves gpTheorem1b
  proves gpTheorem1c