;; ;; 2024-04-16.  ueb00.scm (by Nils Koepp and Valentin Herrmann)

;; We assume that minlog, scheme and emacs is installed.

;; Everything after ';;' are comments

;; Open this file using the minlog or emacs command.  (For more info
;; see MINLOG-FOLDER/doc/tutor.pdf and for even more info
;; MINLOG-FOLDER/doc/ref.pdf)
;; In the minlogpad you can open those files from the Help menu

;; It is recommended to use two windows.  If your window is not split
;; then these may help:

;; Ctrl-x 2, or
;; Ctrl-x 3, to split your window
;; Ctrl-x o, to switch between windows
;; Ctrl-x b, (then type name of the buffer and enter) to change buffer,
;; e.g. to *scheme* or ueb00.scm

;; For emacs see https://www.gnu.org/software/emacs/refcards/pdf/refcard.pdf

;; Your *scheme* buffer should look similar to this:

;; Chez Scheme Version 9.6.4
;; Copyright 1984-2023 Cisco Systems, Inc.

;; > 

;; If the *scheme* buffer does not exist then scheme is not running,
;; do: Alt-x, type run-scheme, press enter

;; If run-scheme doesn't exist, you didn't install scheme properly.

;; You can evaluate commands by placing the cursor behind the closing
;; parantheses and pressing Ctrl-x Ctlr-e.  To run minlog evaluate

;; Evaluate this (pp for 'pretty print', pf for 'parse formula')
(pp (pf "Pvar"))

;; If this throws an error, then minlog is not loaded, in that case, eval:

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

;; (your path to the init.scm might be different)

;; You can also mark a whole bunch of commands and eval them all by
;; using Ctrl-c Ctrl-r

;; Some Propositional Logic
;; ========================

;; We add some names for propositionss (predicate variables with empty arity)
(add-pvar-name "A" "B" "C" (make-arity))

;; We can formulate some statements (the arrow is written -(minus)>(greater))

(pp (pf "A -> B"))
(pp (pf "(A -> B -> C) -> (A -> B) -> A -> C"))

;; We can prove some things ('set-goal' sets a new target to prove)

(set-goal "(A -> B -> C) -> (A -> B) -> A -> C")

;; -----------------------------------------------------------------------------
;; ?_1:(A -> B -> C) -> (A -> B) -> A -> C

;; Minlog tells you the current goal: ?_1:(A -> B -> C) -> (A -> B) -> A -> C
;; Proofs are backwards, we use 'assume' which corresponds to imp-intro

(assume 1)
(assume 2)
(assume 3)

;; You can undo the last n commands by '(undo n)'

(undo 3)

;; In the minlogpad you can also just press C-c C-u to undo one statement

;; You can assume all things at once and also use proper names

(assume "u" "v" "w")

;; We need to prove '?_2:C'.  We use the 'use' command which
;; corresponds to imp-elim.  We need to provide somethings which ends
;; in the goal formula.  The only thing is 'u:A -> B -> C'

(use "u")

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

(use "w")
(use "v")
(use "w")
;; done

;; We can check proofs for correctness with the 'cdp' (check and
;; display proof) command

(cdp)

;; We can display the proof as a lambda-term with the
;; 'proof-to-expr-with-formulas' command

(proof-to-expr-with-formulas)

;; Falsity is written 'bot'

(set-goal "A -> (A -> bot) -> bot")
(assume "u" "v")
(use "v")
(use "u")
(proof-to-expr-with-formulas)

;; That was just an instance of imp-elim ...

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

;; 'save' saves a proven theorem under the name given.  Can 'use' it
;; to prove other things

(save "ModusPonens")

(set-goal "A -> (A -> bot) -> bot")
(use "ModusPonens")

;; More examples
(set-goal "A -> B -> A")

(set-goal "(A -> B -> C) -> B -> A -> C")

(set-goal "(A -> B) -> (B -> C) -> A -> C")

(set-goal "(((A -> B) -> bot) -> bot) -> ((A -> bot) -> bot) -> (B -> bot) -> bot")

(set-goal "(bot -> B) -> (((A -> bot) -> bot) -> (B -> bot) -> bot) -> (((A -> B) -> bot) -> bot) ")