From ed85f01850546dce8e1ea97a83fe8f2b111348cd Mon Sep 17 00:00:00 2001
From: mehbark <terezi@pyrope.net>
Date: Fri, 21 Feb 2025 00:51:21 -0500
Subject: [PATCH] chore: output tweaks

---
 formal.scm | 27 +++++++++++++++++++++++----
 1 file changed, 23 insertions(+), 4 deletions(-)

diff --git a/formal.scm b/formal.scm
index 1eb57a2..ba1ec0d 100644
--- a/formal.scm
+++ b/formal.scm
@@ -205,12 +205,13 @@
               (return #f))))
       (proof-steps proof))
      (when (or (member #f prems) (premises<=? goals prems))
+       (printf "Proof complete!\n")
        (return #t))
-     (format #t "Unsolved goals:\n~{~a\n~}~{⊢ ~a\n~}\n"
-             prems (filter (lambda (g) (not (member g prems))) goals)))))
+     (printf "Unsolved goals:\n~{~a\n~}~{⊢ ~a\n~}\n"
+             (reverse prems)
+             (filter (lambda (g) (not (member g prems))) goals)))))
 
-;; TODO: i can just guess lol
-;; this really isn't far from the macroless version....
+;; TODO: this really isn't far from the macroless version....
 (define and-comm
   (proof (p q)
     (argument (p q)
@@ -228,3 +229,21 @@
     [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.inl 
+  (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.inl)