;; temp20231113.scm.  

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

;; Interactive generation of proofs with a "proof assistent", here Minlog

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

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

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

(cdp)

(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")
(assume "v")
(assume "x")
(use "u")
(use "v")

(cdp)

(set-goal "all x(A -> P x) -> A -> all x P x")
(assume 1 2 "x")
(assume 3)

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

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

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

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

;; As an example we prove the drinker formula
;; all x(((P x -> F) -> F) -> P x) -> exca x(P x -> all x P x)

;; 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" "x0")
(use "EfP")
(use "w")
(use "u1")
;; Proof finished.
(save "DrinkerAux")

;; 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" "x0")
(use "StabP")
(use "DrinkerAux")
;; 6,7
(assume "x1" "Absurd")
(use "StabP")
(assume "Useless")
(use "Absurd")
;; 7
(use "v")
;; Proof finished.
(save "Drinker")

(cp)

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

(define daux-proof (theorem-name-to-proof "DrinkerAux"))

(proof-to-expr-with-formulas daux-proof)

EfP: all x(F -> P x)
v: 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 (x0) ((EfP x0) (w u1)))))))))

(define d-proof (theorem-name-to-proof "Drinker"))

(proof-to-expr-with-formulas d-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 x1 -> F

(lambda (StabP)
  (lambda (v)
    ((v x)
      (lambda (w)
        (lambda (x0)
          ((StabP x0)
            (((DrinkerAux x0)
               (lambda (x1)
                 (lambda (Absurd) ((StabP x1) (lambda (Useless) Absurd)))))
	     v)))))))

;; We expand the d-proof by insering the daux-proof.

(define e-proof
  (expand-theorems d-proof (lambda (name) (string=? name "DrinkerAux"))))

(proof-to-expr-with-formulas e-proof)

StabP: all x(((P x -> F) -> F) -> P x)
v: all x((P x -> all x0 P x0) -> F)
w: P x
EfP: all x(F -> P x)
v0: all x((P x -> all x0 P x0) -> F)
w0: P x -> F
u1: P x
Absurd: F
Useless: P x1 -> F

(lambda (StabP)
  (lambda (v)
    ((v x)
      (lambda (w)
        (lambda (x0)
          ((StabP x0)
            ((((lambda (x)
                 (lambda (EfP)
                   (lambda (v0)
                     (lambda (w0)
                       ((v0 x)
                         (lambda (u1)
                           (lambda (x0) ((EfP x0) (w0 u1)))))))))
                x0)
               (lambda (x1)
                 (lambda (Absurd) ((StabP x1) (lambda (Useless) Absurd)))))
	     v)))))))

;; This proof is not normal, since it contains a redex ((lambda (x) ...)x0).
;; np means normalize-proof.

(define ne-proof (np e-proof))

(proof-to-expr-with-formulas ne-proof)

u: all x(((P x -> F) -> F) -> P x)
u0: all x((P x -> all x0 P x0) -> F)
u1: P x
u2: P x1592 -> F
u3: P x1592
u4: P x1593 -> F

(lambda (u)
  (lambda (u0)
    ((u0 x)
      (lambda (u1)
        (lambda (x1592)
          ((u x1592)
            (lambda (u2)
              ((u0 x1592)
                (lambda (u3)
                  (lambda (x1593)
                    ((u x1593) (lambda (u4) (u2 u3)))))))))))))