295 lines
7.1 KiB
Scheme
295 lines
7.1 KiB
Scheme
;; okay, i'll keep these procedures for the sake of nesting
|
||
|
||
(define (make-pand p q) `(∧ ,p ,q))
|
||
|
||
(define pand
|
||
(case-lambda
|
||
[() #t]
|
||
[(p) p]
|
||
[(p . qs) (make-pand p (apply pand qs))]))
|
||
|
||
(define (make-por p q) `(∨ ,p ,q))
|
||
|
||
(define por
|
||
(case-lambda
|
||
[() #f]
|
||
[(p) p]
|
||
[(p . qs) (make-por p (apply por qs))]))
|
||
|
||
;; iirc, or: (not p) or q
|
||
(define (make-p-> p q) `(→ ,p ,q))
|
||
|
||
;; could fold but laziness
|
||
(define p->
|
||
(case-lambda
|
||
[() #t]
|
||
[(p) p]
|
||
[(p . qs) (make-p-> p (apply p-> qs))]))
|
||
|
||
(define (p<-> p q) (pand (p-> p q) (p-> q p)))
|
||
;; maybe could have some pretty-printing logic? this definition is just 2 good 2 pass up
|
||
(define (pnot p) (p-> p #f))
|
||
(define ~ pnot)
|
||
|
||
;; maybe a var is just a sym? no forall lel
|
||
;; existence l8r
|
||
;; nah
|
||
;; valued vars? :o
|
||
|
||
;; (define-record-type forall
|
||
;; (fields vars p)
|
||
;; (nongenerative forall))
|
||
;; (define-syntax forall
|
||
;; (syntax-rules ()
|
||
;; [(forall (var* ...) p)
|
||
;; (make-forall
|
||
;; '(var* ...)
|
||
;; (let ([var* 'var*] ...) p))]
|
||
;; [(forall var p) (forall (var) p)]))
|
||
|
||
(define-record-type argument
|
||
(fields premises conclusions)
|
||
(nongenerative argument))
|
||
|
||
(define-syntax argument
|
||
(syntax-rules ()
|
||
[(_ (var* ...) (premise* ...) (conclusion* ...))
|
||
(lambda (var* ...)
|
||
(make-argument (list premise* ...) (list conclusion* ...)))]))
|
||
|
||
(define (argument->statement arg)
|
||
(apply p-> (append (argument-premises arg)
|
||
(list (apply pand (argument-conclusions arg))))))
|
||
|
||
(define (general-argument->statement arg)
|
||
(lambda ps (argument->statement (apply arg ps))))
|
||
|
||
;; (follows (P* ... (-> p q) p Q* ...) q modus-ponens) => #t
|
||
;; iterative argument
|
||
;; laws of inference are taken as fact
|
||
;; norm vars
|
||
;; order irrelevant
|
||
;; search for reqs?
|
||
|
||
(define (premises<=? p1 p2)
|
||
(and (andmap (lambda (prem) (member prem p2)) p1)
|
||
#t))
|
||
|
||
(define (follows? prems q by)
|
||
(and (member q (argument-conclusions by))
|
||
(premises<=? (argument-premises by) prems)))
|
||
|
||
(define-record-type step
|
||
(fields conclusion rule)
|
||
(nongenerative step))
|
||
|
||
(define-record-type proof
|
||
(fields argument steps)
|
||
(nongenerative proof))
|
||
|
||
(define-syntax proof
|
||
(syntax-rules ()
|
||
[(_ (var* ...) arg (conclusion* rule*) ...)
|
||
(lambda (var* ...)
|
||
(make-proof (arg var* ...)
|
||
(list (make-step conclusion* rule*) ...)))]))
|
||
|
||
;; bleh
|
||
;; huh, procedure-arity-mask can handle 1000+ no problem
|
||
;; returns the lowest arity
|
||
(define (procedure-arity proc)
|
||
(define mask (procedure-arity-mask proc))
|
||
(let loop ([i 0])
|
||
(if (logbit? i mask)
|
||
i
|
||
(loop (add1 i)))))
|
||
|
||
;; so over-general lel
|
||
(define proof-variable
|
||
(let* ([bases '#(p q r s t u)]
|
||
[bases-count (vector-length bases)])
|
||
(lambda (n)
|
||
(define base (vector-ref bases (mod n bases-count)))
|
||
(define num (floor (/ n bases-count)))
|
||
(string->symbol
|
||
(format "~a~a"
|
||
base
|
||
(if (zero? num) "" num))))))
|
||
|
||
(define (placeholder-saturate f)
|
||
;; map iota is bad but convenient (macro so needed)
|
||
(apply f (map proof-variable (iota (procedure-arity f)))))
|
||
|
||
;; i think i prefer the turnstile to therefore
|
||
(define (argument-pp arg port)
|
||
(define prems (argument-premises arg))
|
||
(define concls (argument-conclusions arg))
|
||
(format port "~{~a\n~}~{⊢ ~a\n~}"
|
||
prems concls))
|
||
|
||
(define (general-argument-pp arg port)
|
||
(argument-pp (placeholder-saturate arg) port))
|
||
|
||
(define (cartesian-exponent xs n)
|
||
(assert (and (integer? n) (>= n 0)))
|
||
(case n
|
||
[0 '()]
|
||
[1 (map list xs)]
|
||
[else
|
||
(let ([exp-1 (cartesian-exponent xs (sub1 n))])
|
||
(apply append
|
||
(map (lambda (xs2)
|
||
(map (lambda (x)
|
||
(cons x xs2))
|
||
xs))
|
||
exp-1)))]))
|
||
|
||
(define (gensyms n)
|
||
(let loop ([i 0]
|
||
[xs '()])
|
||
(if (>= i n)
|
||
(reverse xs)
|
||
(loop (add1 i)
|
||
(cons (gensym (symbol->string (proof-variable i))) xs)))))
|
||
|
||
(define (proof-valid? proof%)
|
||
(define proof (apply proof% (gensyms (procedure-arity proof%))))
|
||
(define arg (proof-argument proof))
|
||
;; reversing here lets us recover a nice order at the end
|
||
(define prems (reverse (argument-premises arg)))
|
||
(define goals (argument-conclusions arg))
|
||
|
||
(define (fail concl rule)
|
||
(printf "Failed to apply rule:\n")
|
||
(argument-pp rule #t)
|
||
(printf "Proof state:\n~{~a\n~}⊢ ~a\n"
|
||
(reverse prems) concl)
|
||
#f)
|
||
|
||
(define (handle-general-step concl rule)
|
||
(define base-targets (append prems goals))
|
||
(define targets
|
||
(apply append base-targets (map (lambda (p) (if (pair? p) (cdr p) '())) base-targets)))
|
||
(ormap
|
||
(lambda (ts) (follows? prems concl (apply rule ts)))
|
||
(cartesian-exponent targets (procedure-arity rule))))
|
||
|
||
(call/1cc
|
||
(lambda (return)
|
||
(for-each
|
||
(lambda (step)
|
||
(define concl (step-conclusion step))
|
||
(define rule (step-rule step))
|
||
(define ok?
|
||
(if (procedure? rule)
|
||
(handle-general-step concl rule)
|
||
(follows? prems concl rule)))
|
||
(if ok?
|
||
(set! prems (cons concl prems))
|
||
(begin
|
||
(fail concl (if (procedure? rule) (placeholder-saturate rule) rule))
|
||
(return #f))))
|
||
(proof-steps proof))
|
||
(when (or (member #f prems) (premises<=? goals prems))
|
||
(printf "Proof complete!\n")
|
||
(return #t))
|
||
(printf "Unsolved goals:\n~{~a\n~}~{⊢ ~a\n~}\n"
|
||
(reverse prems)
|
||
(filter (lambda (g) (not (member g prems))) goals))
|
||
#f)))
|
||
|
||
(define modus-ponens
|
||
(argument (p q)
|
||
[(p-> p q)
|
||
p]
|
||
[q]))
|
||
|
||
(define modus-tollens
|
||
(argument (p q)
|
||
[(p-> p q)
|
||
(~ q)]
|
||
[(~ p)]))
|
||
|
||
(define or.inl
|
||
(argument (p q)
|
||
[p]
|
||
[(por p q)]))
|
||
|
||
(define or.inr
|
||
(argument (p q)
|
||
[q]
|
||
[(por p q)]))
|
||
|
||
(define simplification
|
||
(argument (p q)
|
||
[(pand p q)]
|
||
[p q]))
|
||
|
||
(define or.eliml
|
||
(argument (p q)
|
||
[(por p q)
|
||
(~ p)]
|
||
[q]))
|
||
|
||
(define or.elimr
|
||
(argument (p q)
|
||
[(por p q)
|
||
(~ q)]
|
||
[p]))
|
||
|
||
(define conjunction
|
||
(argument (p q)
|
||
[p
|
||
q]
|
||
[(pand p q)]))
|
||
|
||
(define transitivity
|
||
(argument (p q r)
|
||
[(p-> p q)
|
||
(p-> q r)]
|
||
[(p-> p r)]))
|
||
|
||
(define cases
|
||
(argument (p q r)
|
||
[(por p q)
|
||
(p-> p r)
|
||
(p-> q r)]
|
||
[r]))
|
||
|
||
;; TODO: this really isn't far from the macroless version....
|
||
(define and-comm
|
||
(proof (p q)
|
||
(argument (p q)
|
||
[(pand p q)]
|
||
[(pand q p)])
|
||
[p (simplification p q)]
|
||
[q (simplification p q)]
|
||
[(pand q p) (conjunction q p)]))
|
||
|
||
(define and-comm-ez
|
||
(proof (p q)
|
||
(argument (p q)
|
||
[(pand p q)]
|
||
[(pand q p)])
|
||
[p simplification]
|
||
[q simplification]
|
||
[(pand q p) conjunction]))
|
||
|
||
;; TODO: make this expressible better
|
||
;; TODO: use proofs for other proofs nicely
|
||
;; the mismatch between what is written and what is shown is hideous
|
||
;; avoidable by being explicit ig
|
||
(define and-assoc.mp
|
||
(proof (p q r)
|
||
(argument (p q r)
|
||
[(pand p (pand q r))]
|
||
[(pand (pand p q) r)])
|
||
[p simplification]
|
||
[(pand q r) simplification]
|
||
[q simplification]
|
||
[r simplification]
|
||
[(pand p q) conjunction]
|
||
[(pand (pand p q) r) conjunction]))
|
||
|
||
(proof-valid? and-assoc.mp)
|