fix: many tweaks

formal.scm

@@ -6,7 +6,7 @@
   (case-lambda
     [() #t]
     [(p) p]
-    [(p . qs) (fold-left make-pand p qs)]))
+    [(p . qs) (make-pand p (apply pand qs))]))
 
 (define (make-por p q) `(∨ ,p ,q))
 
@@ -14,7 +14,7 @@
   (case-lambda
     [() #f]
     [(p) p]
-    [(p . qs) (fold-left make-por p qs)]))
+    [(p . qs) (make-por p (apply por qs))]))
 
 ;; iirc, or: (not p) or q
 (define (make-p-> p q) `(→ ,p ,q))
@@ -57,29 +57,12 @@
      (lambda (var* ...)
        (make-argument (list premise* ...) (list conclusion* ...)))]))
 
-(define modus-ponens
-  (argument (p q)
-    [(p-> p q)
-     p]
-    [q]))
+(define (argument->statement arg)
+  (apply p-> (append (argument-premises arg)
+                     (list (apply pand (argument-conclusions arg))))))
 
-(define modus-tollens
-  (argument (p q)
-    [(p-> p q)
-     (~ q)]
-    [(~ p)]))
-
-;; YES: multiple conclusions (no more simplification-{l,r})
-(define simplification
-  (argument (p q)
-    [(pand p q)]
-    [p q]))
-
-(define conjunction
-  (argument (p q)
-    [p
-     q]
-    [(pand p q)]))
+(define (general-argument->statement arg)
+  (lambda ps (argument->statement (apply arg ps))))
 
 ;; (follows (P* ... (-> p q) p Q* ...) q modus-ponens) => #t
 ;; iterative argument
@@ -161,14 +144,16 @@
                           xs))
                    exp-1)))]))
 
-(define (proof-valid? proof%)
-  (define (gensyms n xs)
-    (if (zero? n)
-        ;; less confusing to apply (proof g0 g1 ...)
+(define (gensyms n)
+  (let loop ([i 0]
+             [xs '()])
+    (if (>= i n)
         (reverse xs)
-        (gensyms (sub1 n)
-                 (cons (gensym (symbol->string (proof-variable (sub1 n)))) xs))))
-  (define proof (apply proof% (gensyms (procedure-arity proof%) '())))
+        (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)))
@@ -182,8 +167,9 @@
     #f)
 
   (define (handle-general-step concl rule)
+    (define base-targets (append prems goals))
     (define targets
-      (apply append prems (map (lambda (p) (if (pair? p) (cdr p) '())) prems)))
+      (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))))
@@ -209,7 +195,66 @@
        (return #t))
      (printf "Unsolved goals:\n~{~a\n~}~{⊢ ~a\n~}\n"
              (reverse prems)
-             (filter (lambda (g) (not (member g prems))) goals)))))
+             (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
@@ -234,7 +279,7 @@
 ;; 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.inl 
+(define and-assoc.mp 
   (proof (p q r)
     (argument (p q r)
       [(pand p (pand q r))]
@@ -246,4 +291,4 @@
     [(pand p q) conjunction]
     [(pand (pand p q) r) conjunction]))
 
-(proof-valid? and-assoc.inl)
+(proof-valid? and-assoc.mp)