;; 2025-10-27.  drinker.scm

;; We work with a concrete type which has a total inhabitant, for
;; instance nat

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

(add-alg "nat" '("Zero" "nat") '("Succ" "nat=>nat"))
(add-var-name "n" "m" "l" (py "nat"))

(add-pvar-name "A" (make-arity (py "nat")))
(add-pvar-name "B" (make-arity))

;; Lemma6
(set-goal
 "all n(((A^ n -> F) -> F) -> A^ n) ->
 (all n A^ n -> B^) ->
 exca n(A^ n -> B^)")
(assume "StabA")

(assert "all n(F -> A^ n)")
(assume "n" "Absurd")
(use "StabA")
(assume "Useless")
(use "Absurd")
;; Assertion proved.
(assume "EfA")

(assume "u" "v")
(use "v" (pt "Zero"))
(assume "Useless")
(use "u")
(assume "n")
(use "StabA")
;; Now the auxiliary dervation starts
(assume "u1")
(use "v" (pt "n"))
(assume "u2")
(use "u")
(assume "m")
(use "EfA")
(use "u1")
(use "u2")
;; Proof finished.
;; (cp)
(save "Lemma6")

(proof-to-expr-with-formulas)

;; Let B^ := all n A^ n

(set-goal
 "all n(((A^ n -> F) -> F) -> A^ n) ->
 (all n A^ n -> all n A^ n) ->
 exca n(A^ n -> all n A^ n)")
(use "Lemma6")
;; Proof finished.
;; (cp)
(save "Lemma6Inst")

;; Drinker
(set-goal
 "all n(((A^ n -> F) -> F) -> A^ n) ->
 exca n(A^ n -> all n A^ n)")
(assume "StabA")
(use "Lemma6Inst")
(use "StabA")
(assume "u")
(use "u")
;; Proof finished.
;; (cp)
(save "Drinker")