;; 2012-11-03.  Examples of proof representation.

;; Why?
;; -- Data bank for proofs.  Want an appropriate format.
;; -- Correctness: no forgotten cases, organization of subgoals.
;; -- Machine support for finding (routine) proofs (not for induction).
;; -- Proofs can be checked (independently of the proof assistant).
;; -- Proofs can be normalized (no detours).
;; -- Copmputational content of proofs can be extracted.

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

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

(set-goal "(A -> B -> C) -> (A -> B) -> A -> C")
(assume "u" "v" "w")
(use-with "u" "w" "?")
(use-with "v" "w")
(save "ExOne")

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

(set-goal "all x(P x -> Q x) -> all x P x -> all x Q x")
(assume "u" "v" "x")
(use "u")
(use "v")
(save "ExTwo")

(cdp "ExOne")
#|
.....A -> B -> C by assumption u78
.....A by assumption w80
....B -> C by imp elim
.....A -> B by assumption v79
.....A by assumption w80
....B by imp elim
...C by imp elim
..A -> C by imp intro w80
.(A -> B) -> A -> C by imp intro v79
(A -> B -> C) -> (A -> B) -> A -> C by imp intro u78
|#

(proof-to-expr-with-formulas "ExOne")
#|
u78: A -> B -> C
v79: A -> B
w80: A

(lambda (u78)
  (lambda (v79) (lambda (w80) ((u78 w80) (v79 w80)))))
|#

(cdp "ExTwo")
#|
.....all x(P x -> Q x) by assumption u87
.....x
....P x -> Q x by all elim
.....all x P x by assumption v88
.....x
....P x by all elim
...Q x by imp elim
..all x Q x by all intro
.all x P x -> all x Q x by imp intro v88
all x(P x -> Q x) -> all x P x -> all x Q x by imp intro u87
|#

(proof-to-expr-with-formulas "ExTwo")
#|
u87: all x(P x -> Q x)
v88: all x P x

(lambda (u87) (lambda (v88) (lambda (x) ((u87 x) (v88 x)))))
|#

(set-goal "all x(((Q x -> bot) -> bot) -> Q x) -> excl x(Q x -> all x Q x)")
(search)
(save "Drinker")

(cdp "Drinker")
#|
....all x((Q x -> all x Q x) -> bot) by assumption u101
....x
...(Q x -> all x Q x) -> bot by all elim
.......all x(((Q x -> bot) -> bot) -> Q x) by assumption u100
.......x154
......((Q x154 -> bot) -> bot) -> Q x154 by all elim
.........all x((Q x -> all x Q x) -> bot) by assumption u101
.........x154
........(Q x154 -> all x Q x) -> bot by all elim
............all x(((Q x -> bot) -> bot) -> Q x) by assumption u100
............x168
...........((Q x168 -> bot) -> bot) -> Q x168 by all elim
.............Q x154 -> bot by assumption u103
.............Q x154 by assumption u106
............bot by imp elim
...........(Q x168 -> bot) -> bot by imp intro u107
..........Q x168 by imp elim
.........all x168 Q x168 by all intro
........Q x154 -> all x168 Q x168 by imp intro u106
.......bot by imp elim
......(Q x154 -> bot) -> bot by imp intro u103
.....Q x154 by imp elim
....all x154 Q x154 by all intro
...Q x -> all x154 Q x154 by imp intro u102
..bot by imp elim
.excl x(Q x -> all x Q x) by imp intro u101
all x(((Q x -> bot) -> bot) -> Q x) -> excl x(Q x -> all x Q x) by imp intro u100
|#

(proof-to-expr-with-formulas "Drinker")

#|
u100: all x(((Q x -> bot) -> bot) -> Q x)
u101: all x((Q x -> all x0 Q x0) -> bot)
u102: Q x
u103: Q x154 -> bot
u106: Q x154
u107: Q x168 -> bot

(lambda (u100)
  (lambda (u101)
    ((u101 x)
      (lambda (u102)
        (lambda (x154)
          ((u100 x154)
            (lambda (u103)
              ((u101 x154)
                (lambda (u106)
                  (lambda (x168)
                    ((u100 x168) (lambda (u107) (u103 u106)))))))))))))
|#