Add converse operation

truth-table.lisp

@@ -131,7 +131,8 @@ line."))
     (or "\\/" "or" "||" "|" "∥" "+" "∨")
     (xor "xor" "⊕" "⊻" "↮" "≢" "^" "!=")
     (not "¬" "~" "!" "not")
-    (implies "->" ">" "=>" "⇒" "→" "⊃" "implies")
+    (implies "->" ">" "=>" "⇒" "⟹" "→" "⊃" "implies")
+    (converse "<-" "<" "<=" "←" "⇐" "⟸" "⊂" "converse")
     (iff "<->" "<>" "<=>" "⇔" "↔" "≡" "iff" "=" "=="))
   "Alist table of operator symbols and their possible string representations.")
 
@@ -149,6 +150,7 @@ line."))
     (xor 3)
     (or 4)
     (implies 5)
+    (converse 5)
     (iff 6)
     (open-paren most-positive-fixnum)
     (t nil)))
@@ -162,6 +164,7 @@ and the maximum number (or nil for infinity) as a second value."
     (xor (values 2 nil))
     (not (values 1 1))
     (implies (values 2 2))
+    (converse (values 2 2))
     (iff (values 2 2))
     (t (error "unknown operator: ~S" oper))))
 
@@ -399,6 +402,7 @@ found variables."
     (xor . "^")
     (not . "~")
     (implies . "->")
+    (converse . "<-")
     (iff . "<->")
     (open-paren . "(")
     (close-paren . ")")
@@ -412,6 +416,7 @@ found variables."
     (xor . "⊕")
     (not . "¬")
     (implies . "→")
+    (converse . "←")
     (iff . "↔")
     (open-paren . "(")
     (close-paren . ")")
@@ -425,6 +430,7 @@ found variables."
     (xor . "\\oplus")
     (not . "\\lnot ")
     (implies . "\\to")
+    (converse . "\\gets")
     (iff . "\\leftrightarrow")
     (open-paren . "\\left(")
     (close-paren . "\\right)")
@@ -513,6 +519,15 @@ NOTE: This is NOT a macro, so all arguments, so there is no short circuit
 evaluation (all arguments are evaluated no matter what)."
   (not (not (member t args))))
 
+(defun logical-implies (prop1 prop2)
+  "Evaluate the logical implies operation on PROP1 and PROP2. That is \"if
+PROP1, then PROP2\".
+NOTE: This is NOT a macro, so all arguments, so there is no short circuit
+evaluation (all arguments are evaluated no matter what)."
+  (if prop1 ;; only if first is true
+      prop2 ;; eval second
+      t)) ;; otherwise, just return true
+
 (defun check-operator-argument-count (oper args)
   "Raise an error if OPER cannot be called with ARGS."
   (multiple-value-bind (min max) (operator-argument-count oper)
@@ -581,9 +596,12 @@ NOTE: the second value does not include individual variables, literal values
                         (not
                          (not (car arg-values)))
                         (implies
-                         (if (car arg-values) ;; if first is true
+                         (logical-implies (car arg-values)
-                             (second arg-values) ;; eval second
+                                          (second arg-values)))
-                             t)) ;; otherwise, just return true
+                        (converse
+                         ;; this is just implies with the arguments flipped
+                         (logical-implies (second arg-values)
+                                          (car arg-values)))
                         (iff
                          (eq (car arg-values) ;; both must have the same value
                              (second arg-values))))))