;; 2023-04-26.

(load "~/git/minlog/init.scm")

;; 1.1.1.  Natural deduction
;; =========================

(add-predconst-name "A" "B" "C" (make-arity))

(set-goal "(A -> B -> C) -> (A -> B) -> A -> C")
(assume "u" "v" "w")
(use "u")
(use "w")
(use "v")
(use "w")

(add-var-name "x" (py "alpha"))
(add-predconst-name "P" "Q" (make-arity (py "alpha")))

(set-goal "all x(A -> P x) -> A -> all x P x")
(assume "u" "v" "x")
(use "u")
(use "v")

;; 1.1.2.  Properties of negation
;; ==============================

(set-goal "(((A -> B) -> F) -> F) -> ((A -> F) -> F) -> (B -> F) -> F")
(assume "u" "v" "w")
(use "u")
(assume "u1")
(use "v")
(assume "u2")
(use "w")
(use "u1")
(use "u2")

(set-goal "(F -> B) ->
 (((A -> F) -> F) -> (B -> F) -> F) -> ((A -> B) -> F) -> F")
(assume "u" "v" "w")
(use "v")
(assume "v1")
(use "w")
(assume "v2")
(use "u")
(use "v1")
(use "v2")
(assume "v3")
(use "w")
(assume "v4")
(use "v3")

(set-goal "((all x P x -> F) -> F) -> all x((P x -> F) -> F)")
(assume "u" "x" "v")
(use "u")
(assume "w")
(use "v")
(use "w")

;; 1.1.3.  Intuitionistic and classical derivability
;; =================================================

;; Stability theorem (a)
(set-goal "(((B -> F) -> F) -> B) -> (((A -> B) -> F) -> F) -> A -> B")
(assume "u" "v" "w")
(use "u")
(assume "u1")
(use "v")
(assume "v1")
(use "u1")
(use "v1")
(use "w")

;; Stability theorem (b) corollary
(set-goal
 "all x(((P x -> F) -> F) -> P x) -> ((all x P x -> F) -> F) -> all x P x")
(assume "u" "v" "x")
(use "u")
(assume "w")
(use "v")
(assume "v1")
(use "w")
(use "v1")

(pp (fold-formula (pf "(all x(P x -> F)) -> F")))

(add-var-name "y" (py "alpha"))

;; ;; Lemma (1)
;; (set-goal "(exca x P x -> A) -> all x(P x -> A)")

;; ;; Lemma (2)
;; (set-goal "(((A -> F) -> F) -> A) -> all x(P x -> A) -> exca x P x -> A")

;; Lemma (3)
(set-goal "all y(F -> P y) -> (A -> exca x P x) -> exca x(A -> P x)")
(assume "u" "v" "w")
(use "w" (pt "y"))
(assume "u2")
(use "u")
(use "v")
(use "u2")
(assume "x" "u1")
(use "w" (pt "x"))
(assume "u3")
(use "u1")

;; ;; Lemma (4)
;; (set-goal "exca x(A -> P x) -> A -> exca x P x")

;; Lemma (5)
(set-goal "(((A -> F) -> F) -> A) -> exca x(P x -> A) -> all x P x -> A")
(assume "u" "v" "w")
(use "u")
(assume "u2")
(use "v")
(assume "x" "u1")
(use "u2")
(use "u1")
(use "w")

;; An axiliary Lemma for Lemma (6)
;; L6Aux
(set-goal
 "all x(all x(F -> P x) -> (all x P x -> A) -> all x((P x -> A) -> F) ->
 (P x -> F) -> F)")
(assume "x" "EfP" "u" "v" "w")
(use "v" (pt "x"))
(assume "u1")
(use "u")
(assume "y")
(use "EfP")
(use "w")
(use "u1")
;; Proof finished.
(save "L6Aux")

;; Lemma (6)
(set-goal
 "all x(((P x -> F) -> F) -> P x) -> (all x P x -> A) -> exca x(P x -> A)")
(assume "StabP" "u" "v")
(use "v" (pt "x"))
(assume "w")
(use "u")
(assume "y")
(use "StabP")
(use "L6Aux")
;; 8-10
(assume "x0" "Absurd")
(use "StabP")
(assume "Useless")
(use "Absurd")
;; 9
(use "u")
;; 10
(use "v")

;; Drinker (special case of (6) with all x P x for A)

;; DrinkerAux
(set-goal "all x(all x(F -> P x) -> all x((P x -> all x P x) -> F) ->
 (P x -> F) -> F)")

;; Drinker
(set-goal "all x(((P x -> F) -> F) -> P x) -> exca x(P x -> all x P x)")

;; 1.2.  Derivation terms, normalization
;; =====================================

;; 1.2.1.  The Curry-Howard correspondence
;; =======================================

;; We display the proof terms some derivations.

(set-goal "(A -> B -> C) -> (A -> B) -> A -> C")
(assume "u" "v" "w")
(use "u")
(use "w")
(use "v")
(use "w")

(define proof (current-proof))
(proof-to-expr-with-formulas proof)

;; u: A -> B -> C
;; v: A -> B
;; w: A

;; (lambda (u) (lambda (v) (lambda (w) ((u w) (v w)))))

(set-goal "all x(A -> P x) -> A -> all x P x")
(assume "u" "v" "x")
(use "u")
(use "v")

(define proof (current-proof))
(proof-to-expr-with-formulas proof)

;; u: all x(A -> P x)
;; v: A

;; (lambda (u) (lambda (v) (lambda (x) ((u x) v))))

;; Drinker (special case of (6) with all x P x for A)

;; DrinkerAux
(set-goal "all x(all x(F -> P x) -> all x((P x -> all x P x) -> F) ->
 (P x -> F) -> F)")
(assume "x" "EfP" "v" "w")
(use "v" (pt "x"))
(assume "u1")
(assume "y")
(use "EfP")
(use "w")
(use "u1")
;; Proof finished.
(save "DrinkerAux")

(define proof (current-proof))
(proof-to-expr-with-formulas proof)

;; all x((P x -> all x0 P x0) -> F)
;; w: P x -> F
;; u1: P x

;; (lambda (x)
;;   (lambda (EfP)
;;     (lambda (v)
;;       (lambda (w)
;;         ((v x) (lambda (u1) (lambda (y) ((EfP y) (w u1)))))))))

;; Drinker
(set-goal
 "all x(((P x -> F) -> F) -> P x) -> exca x(P x -> all x P x)")
(assume "StabP" "v")
(use "v" (pt "x"))
(assume "w")
(assume "x1")
(use "StabP")
(use "DrinkerAux")
;; 7,8
(assume "y" "Absurd")
(use "StabP")
(assume "Useless")
(use "Absurd")
;; 8
(use "v")

(define proof (current-proof))
(proof-to-expr-with-formulas proof)

;; DrinkerAux: all x(
;;  all x0(F -> P x0) -> all x0((P x0 -> all x1 P x1) -> F) -> (P x -> F) -> F)
;; StabP: all x(((P x -> F) -> F) -> P x)
;; v: all x((P x -> all x0 P x0) -> F)
;; w: P x
;; Absurd: F
;; Useless: P y -> F

;; (lambda (StabP)
;;   (lambda (v)
;;     ((v x)
;;       (lambda (w)
;;         (lambda (x1)
;;           ((StabP x1)
;;             (((DrinkerAux x1)
;;                (lambda (y)
;;                  (lambda (Absurd) ((StabP y) (lambda (Useless) Absurd)))))
;;               v)))))))

;; Proof search

;; Minlog has tools search and prop for proof search.  If prop is applied
;; to a propositional formula, it first checks whether it is derivable
;; in minimal logic.  If not, prop tries first Ex-Falso axioms and then
;; stability axioms.

;; We show by an example that search and prop may return different proofs,
;; which are both longer than proof done by hand:

(set-goal "(F -> B) ->
 (((A -> F) -> F) -> (B -> F) -> F) -> ((A -> B) -> F) -> F")
(assume "u" "v" "w")
(use "v")
(assume "v1")
(use "w")
(assume "w1")
(use "u")
(use "v1")
(use "w1")
(assume "u1")
(use "w")
(assume "u2")
(use "u1")

(define proof (current-proof))
(proof-to-expr-with-formulas proof)

(set-goal "(F -> B) ->
 (((A -> F) -> F) -> (B -> F) -> F) -> ((A -> B) -> F) -> F")
(search)
;; ok, ?_1 is proved by minimal quantifier logic.  Proof finished.

(define proof (current-proof))
(proof-to-expr-with-formulas proof)

(set-goal "(F -> B) ->
 (((A -> F) -> F) -> (B -> F) -> F) -> ((A -> B) -> F) -> F")
(prop)
;; ok, ?_1 is proved in minimal propositional logic.  Proof finished.

(define proof (current-proof))
(proof-to-expr-with-formulas proof)

(set-goal "(((A -> F) -> F) -> (B -> F) -> F) -> ((A -> B) -> F) -> F")
(prop)

(define proof (current-proof))
(proof-to-expr-with-formulas proof)

;; 1.2.2.  Normalization
;; =====================

;; SKK

(set-goal "(A -> (B -> A) -> A) -> (A -> B -> A) -> A -> A")
(assume "u" "v" "w")
(use "u")
(use "w")
(assume "u1")
(use "v")
(use "w")
(use "u1")

(define S (current-proof))
(proof-to-expr-with-formulas S)

(set-goal "A -> (B -> A) -> A")
(assume "u" "v")
(use "u")

(define K1 (current-proof))
(proof-to-expr-with-formulas K1)

(set-goal "A -> B -> A")
(assume "u" "v1")
(use "u")
;; Proof finished.

(define K2 (current-proof))
(proof-to-expr-with-formulas K2)

(define SKK (mk-proof-in-elim-form S K1 K2))
(proof-to-expr-with-formulas SKK)

(define SKK1 (proof-to-one-step-reduct SKK))
(proof-to-expr-with-formulas SKK1)

(define SKK2 (proof-to-one-step-reduct SKK1))
(proof-to-expr-with-formulas SKK2)

(define SKK3 (proof-to-one-step-reduct SKK2))
(proof-to-expr-with-formulas SKK3)

(define SKK4 (proof-to-one-step-reduct SKK3))
(proof-to-expr-with-formulas SKK4)

(define nSKK (np SKK))
(proof-to-expr-with-formulas nSKK)