# Based on Vladimir Lifschitz, "On Calculational Proofs"

# An attempt to create a set of axioms for creating calculational proofs within
# Ghilbert.  The system here is that which Lifschitz calls DS.  Numbering
# matches his article.

import (CALCPROP pax/calcprop () "")


var (wff F G H)



thm (inf-<->comm () ((hyp (<-> G H))) (<-> H G)
	(
		hyp
		# (<-> G H)
			G H ax-4
			# (<-> (<-> G H) (<-> H G))
		mpbi
		# (<-> H G)
	)
)

def ((-. F) (<-> F (false)))
def ((true) (-. (false)))


# Here are the proofs of some sample theorems from Lifschitz's article.  In all
# proofs given here, the indentation of a statement represents the number of
# expressions on the stack after that statement.  Also, for most statements the
# expression on top of the stack is given just below that statement.  This
# automatically gives us a layout is such that it is similar in format to a
# calculational proof.
#
# Best viewed with syntax highlighting that gives comment lines a different
# color.


thm (th-12 () () (<-> F F)
	(
		F ax-9
		# (<-> (\/ F (false)) F)
			F ax-9
			# (<-> (\/ F (false)) F)
			F leibniz-<->l
			# "in left hand side of <->"
		mpbi
		# (<-> F F)
	)
)

thm (df-not () ()
	(<-> (-. F) (<-> F (false)))
	(
		(<-> F (false)) th-12
	)
)

thm (th-14 () ()
	(true)
	(
		(false) th-12
	)
)

thm (df-true () ()
	(<-> (true) (-. (false)))
	(
		(-. (false)) th-12
	)
)

thm (th-15 () ()
	(<-> (<-> F (true)) F)
	(
		(<-> F (false)) th-12
		# (<-> (<-> F (false)) (<-> F (false)))
			F (false) ax-4
			# "symmetry of <->"
			(<-> F (false)) leibniz-<->r
			# "in right hand side of <->"
		mpbi
		# (<-> (<-> F (false)) (<-> (false) F))
			(<-> F (false)) (false) F ax-5
			# ...
		mpbi
		# (<-> (<-> (<-> F (false)) (false)) F)
			F (false) (false) ax-5
			inf-<->comm
			F leibniz-<->l
		mpbi
		# (<-> (<-> F (<-> (false) (false))) F)
			# "by abbreviations (-. F) and (true)"
		# (<-> (<-> F (true)) F)
	)
)

# Note how the proof of (17) in Lifschitz just has one step saying
# "commutativity and associativity of <->"...
#
# Now you see why I'd like to have a tool that supports calculational proofs
# :-)

thm (th-17 () ()
	(<-> (<-> F F) (true))
	(
		(<-> F (false)) th-12
		# (<-> (<-> F (false)) (<-> F (false)))
			F (false) (<-> F (false)) ax-5
			# "associativity of <->"
			inf-<->comm
			# "right to left"
		mpbi
		# (<-> F (<-> (false) (<-> F (false))))
			(false) F (false) ax-5
			# "associativity of <->"
			F leibniz-<->r
			# "in right hand side of <->"
		mpbi
		# (<-> F (<-> (<-> (false) F) (false)))
			(false) F ax-4
			# "symmetry of <->"
			(false) leibniz-<->l
			F leibniz-<->r
			# "in right hand side of <->, in left hand side of <->"
		mpbi
		# (<-> F (<-> (<-> F (false)) (false)))
			F (false) (false) ax-5
			# "associativity of <->"
			inf-<->comm
			F leibniz-<->r
			# "in right hand side of <->, right to left"
		mpbi
		# (<-> F (<-> F (<-> (false) (false))))
			F F (<-> (false) (false)) ax-5
			# "associativity of <->"
		mpbi
		# (<-> (<-> F F) (<-> (false) (false)))
			# "by abbreviations (-. F) and (true)"
		# (<-> (<-> F F) (true))
	)
)

# This is a different (and simpler) proof than Lifschitz'.

thm (th-19 () ()
	(<-> (\/ F (true)) (true))
	(
		# all intermediate results below have the form
		# (<-> (\/ F (true)) ...)
		
		(\/ F (true)) th-12
		# ...(\/ F (true))...
			df-true
			# "expand definition of (true)"
			F leibniz-\/r
			# "in right hand side of \/"
			(\/ F (true)) leibniz-<->r
		mpbi
		# ...(\/ F (-. (false)))...
			(false) df-not
			# "expand definition of -."
			F leibniz-\/r
			# "in right hand side of \/"
			(\/ F (true)) leibniz-<->r
		mpbi
		# ...(\/ F (<-> (false) (false)))...
			F (false) (false) ax-10
			# "\/ distributes over <->"
			(\/ F (true)) leibniz-<->r
		mpbi
		# ...(<-> (\/ F (false)) (\/ F (false)))...
			(\/ F (false)) th-17
			#...
			(\/ F (true)) leibniz-<->r
		mpbi
		# ...(true)...
	)
)

thm (th-21 () ()
	(<-> (\/ F (-. F)) (true))
	(
		F th-17
		# (<-> (<-> F F) (true))
			F ax-8
			# (<-> (\/ F F) F)
			inf-<->comm
			F leibniz-<->l
			(true) leibniz-<->l
			# "in left hand side of <->, in left hand side of <->,
			# backward"
		mpbi
		# (<-> (<-> (\/ F F) F) (true))
			F ax-9
			# (<-> (\/ F (false)) F)
			inf-<->comm
			(\/ F F) leibniz-<->r
			(true) leibniz-<->l
			# "in left hand side of <->, in right hand side of \/,
			# backward"
		mpbi
		# (<-> (<-> (\/ F F) (\/ F (false)) (true)))
			F F (false) ax-10
			# "distribute F over <->"
			inf-<->comm
			(true) leibniz-<->l
			# "in left hand side of <->, backward"
		mpbi
		# (<-> (\/ F (<-> F (false))) (true))
			# "abbreviation -."
		# (<-> (\/ F (-. F)) (true))
	)
)

thm (th-24 () ()
	(<-> (\/ (-. F) G) (<-> (\/ F G) G))
	(
		# all intermediate results below have the form
		# (<-> (\/ (-. F) G) ...)

		(\/ (-. F) G) th-12
		# ...(\/ (-. F) G)...
			F df-not
			# "expand definition of -."
			G leibniz-\/l
			(\/ (-. F) G) leibniz-<->r
		mpbi
		# ...(\/ (<-> F (false)) G)...
			(<-> F (false)) G ax-6
			# "commutativity of \/"
			(\/ (-. F) G) leibniz-<->r
		mpbi
		# ...(\/ G (<-> F (false)))...
			G F (false) ax-10
			# "\/ distributes over <->"
			(\/ (-. F) G) leibniz-<->r
		mpbi
		# ...(<-> (\/ G F) (\/ G (false)))...
			G F ax-6
			# "commutativity of \/"
			(\/ G (false)) leibniz-<->l
			(\/ (-. F) G) leibniz-<->r
		mpbi
		# ...(<-> (\/ F G) (\/ G (false)))...
			G ax-9
			# "(false) is neutral element of \/"
			(\/ F G) leibniz-<->r
			(\/ (-. F) G) leibniz-<->r
		mpbi
		# ...(<-> (\/ F G) G)...
	)
)

thm (th-25 () ()
	(<-> (\/ (-. (\/ F G)) G) (\/ (-. F) G))
	(
		# all intermediate results below have the form
		# (<-> (\/ (-. (\/ F G)) G) ...)

		(\/ (-. (\/ F G)) G) th-12
		# ...(\/ (-. (\/ F G)) G)...
			(\/ F G) G th-24
			# "alternate representation of implication"
			(\/ (-. (\/ F G)) G) leibniz-<->r
		mpbi
		# ...(<-> (\/ (\/ F G) G) G)...
			F G G ax-7
			# "associativity of \/"
			inf-<->comm
			G leibniz-<->l
			# "in left hand side of <->, backward"
			(\/ (-. (\/ F G)) G) leibniz-<->r
		mpbi
		# ...(<-> (\/ F (\/ G G)) G)...
			G ax-8
			# "\/ is idempotent"
			F leibniz-\/r
			G leibniz-<->l
			# "in left hand side of <->, in right hand side of \/"
			(\/ (-. (\/ F G)) G) leibniz-<->r
		mpbi
		# ...(<-> (\/ F G) G)...
			F G th-24
			# "alternate representation of implication"
			inf-<->comm
			# "backward"
			(\/ (-. (\/ F G)) G) leibniz-<->r
		mpbi
		# ...(\/ (-. F) G)...
	)
)

def ((-> F G) (\/ (-. F) G))

thm (df-impl () ()
	(<-> (-> F G) (\/ (-. F) G))
	(
		(\/ (-. F) G) th-12
	)
)

thm (mp () ((hyp.1 F) (hyp.2 (-> F G)))
	G
	(
		hyp.2
		# (-> F G)
			F G df-impl
		mpbi
		# (\/ (-. F) G)
			F G th-24
		mpbi
		# (<-> (\/ F G) G)
			hyp.1
			# F
				F th-15
				# (<-> (<-> F (true)) F)
				inf-<->comm
			mpbi
			# (<-> F (true))
			G leibniz-\/l
			G leibniz-<->l
		mpbi
		# (<-> (\/ (true) G) G)
			(\/ (true) G) G ax-4
		mpbi
		# (<-> G (\/ (true) G))
			(true) G ax-6
			G leibniz-<->r
		mpbi
		# (<-> G (\/ G (true)))
			G th-19
			G leibniz-<->r
		mpbi
		# (<-> G (true))
			G th-15
		mpbi
	)
)

export (CALCPROP-THMS pax/calcprop-thms (CALCPROP) "")