; This short Minlog tutorial contains some of the examples of the Tutorial
; for Minlog version 4.0
; To evaluate an expression place the cursor at the end of the expression
; and press Ctrl-x-e
; PROPOSITIONAL LOGIC
(add-predconst-name "P" "Q" "R" (make-arity))
; Implication
(set-goal (pf "(P -> Q -> R) -> (P -> Q) -> P -> R"))
(assume "u")
(assume "v")
(assume "w")
; alternatively: (assume "u" "v" "w")
(use-with "u" "w" "?")
(use-with "v" "w")
(display-proof)
(display-proof-expr)
; Now try this one:
(set-goal (pf "(P -> Q) -> (Q -> R) -> P -> R"))
; Pierce's law
(set-goal (pf "((P -> Q) -> P) -> P"))
(assume "u")
(raa)
(assume "v")
(use-with "v" "?")
(use-with "u" "?")
(assume "w")
(efq)
(use-with "v" "w")
(cdp)
; Conjunction
(set-goal (pf "(P & Q) -> (Q & P)"))
(assume "u")
(split)
(use "u" 'right)
(use "u" 'left)
; PREDICATE LOGIC
(add-pvar-name "A" "B" (make-arity (py "alpha")))
(add-var-name "x" (py "alpha"))
(add-var-name "f" (py "alpha => alpha"))
(set-goal
(pf
"all f.(all x. A x -> B x) ->
all x A(f x) ->
all x B(f x)"))
(assume "f" "u" "v" "x")
(use-with "u" (pt "f x") "?")
(use-with "v" (pt "x"))
; Automated proof search
(add-tvar-name "real")
(add-tvar-name "open")
(add-var-name "r" "s" (py "real"))
(add-var-name "U" "V" (py "open"))
(add-predconst-name
"in" (make-arity (py "real") (py "open")))
(add-var-name "g" (py "real=>real"))
; If g is continuous, so is g o g
(set-goal
(pf
"all g.(all r,V.in(g r)V -> excl U.in r U
& all s.in s U -> in(g s)V) ->
all r,V.in(g(g r))V -> excl U.in r U
& all s.in s U -> in(g(g s))V"))
(search)
(dpe)
(cdp)
;Program extraction: Quotient and remainder
(mload "../lib/nat.scm")
(remove-var-name "r")
(add-var-name "a" "b" "q" "r" (py "nat"))
(set-goal (pf "all b. 0** all a ex q,r. a=b*q+r & r**** F
(assume "w")
; Now try to find the right terms in place of ...
(ex-intro (pt "..."))
(ex-intro (pt "..."))
; We do the rest in one go:
(begin
(ng)
(inst-with "kernel" 'left)
(inst-with "kernel" 'right)
(aga "lemma" (pf "all r,m.(r F) -> r m=r"))
(inst-with "lemma" (pt "r+1")(pt "b"))
(ng)
(inst-with 8 "w" 7)
(simp 6)
(simp 9)
(ng)
(prop)
)
; block (begin ...) finished
(check-and-display-proof)
(define program
(nt (proof-to-extracted-term (current-proof))))
(term-to-expr program)
;133 divided by 15
(term-to-string
(nt (mk-term-in-app-form program (pt "15") (pt "133"))))
**