Don't rely on layout of C enums in FFI code

C/ffi.c

@@ -1,5 +1,6 @@
 #include <lean/lean.h>
 #include <stdio.h>
+#include <stdlib.h>
 #include "ffi.h"
 
 size_t nat_from_lean_obj(lean_obj_arg nat) {
@@ -29,6 +30,16 @@ typedef enum rw_dirs {
   RW_DIR_BOTH
 } rw_dirs;
 
+rw_dirs rw_dirs_from_lean(uint8_t dirs) {
+    switch (dirs) {
+        case 0:  return RW_DIR_NONE;
+        case 1:  return RW_DIR_FORWARD;
+        case 2:  return RW_DIR_BACKWARD;
+        case 3:  return RW_DIR_BOTH;
+        default: exit(11);
+    }
+}
+
 typedef struct rewrite {
     const char* name;
     const char* lhs;
@@ -57,7 +68,7 @@ rewrite rewrite_from_lean_obj(lean_obj_arg rw) {
         .name  = lean_string_cstr(lean_ctor_get(rw, 0)),
         .lhs   = lean_string_cstr(lean_ctor_get(rw, 1)),
         .rhs   = lean_string_cstr(lean_ctor_get(rw, 2)),
-        .dirs  = lean_ctor_get_uint8(rw, scalar_base_offset + 0),
+        .dirs  = rw_dirs_from_lean(lean_ctor_get_uint8(rw, scalar_base_offset + 0)),
         .conds = str_array_from_lean_obj(lean_ctor_get(rw, 3))
     };
 }
@@ -158,15 +169,22 @@ inductive StopReason where
 */
 
 typedef enum stop_reason {
-    SATURATED,
-    TIME_LIMIT,
-    ITERATION_LIMIT,
-    NODE_LIMIT,
-    OTHER
+    STOP_REASON_SATURATED,
+    STOP_REASON_TIME_LIMIT,
+    STOP_REASON_ITERATION_LIMIT,
+    STOP_REASON_NODE_LIMIT,
+    STOP_REASON_OTHER
 } stop_reason;
 
 uint8_t stop_reason_to_lean(stop_reason reason) {
-    return (uint8_t)reason;
+    switch (reason) {
+        case STOP_REASON_SATURATED:       return 0;
+        case STOP_REASON_TIME_LIMIT:      return 1;
+        case STOP_REASON_ITERATION_LIMIT: return 2;
+        case STOP_REASON_NODE_LIMIT:      return 3;
+        case STOP_REASON_OTHER:           return 4;
+        default:                          exit(12);
+    }
 }
 
 /*
@@ -183,7 +201,12 @@ typedef enum expl_kind {
 } expl_kind;
 
 uint8_t expl_kind_to_lean(expl_kind kind) {
-    return (uint8_t)kind;
+    switch (kind) {
+        case EXPL_KIND_NONE:        return 0;
+        case EXPL_KIND_SAME_ECLASS: return 1;
+        case EXPL_KIND_EQ_TRUE:     return 2;
+        default:                    exit(13);
+    }
 }
 
 /*

Lean/Egg/Tests/Math/Math/Lie.lean

@@ -0,0 +1,52 @@
+import Mathlib.Algebra.Lie.Basic
+import Egg
+
+universe u v w w₁ w₂
+
+variable {R : Type u} {L : Type v} {M : Type w} {N : Type w₁}
+variable [CommRing R] [LieRing L] [LieAlgebra R L]
+variable [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M]
+variable [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N]
+variable (t : R) (x y z : L) (m n : M)
+
+example : ⁅-x, m⁆ = -⁅x, m⁆ := by
+  rw [← sub_eq_zero, sub_neg_eq_add, ← add_lie]
+  simp only [neg_add_cancel, zero_lie]
+
+example : ⁅x, -m⁆ = -⁅x, m⁆ := by
+  rw [← sub_eq_zero, sub_neg_eq_add, ← lie_add]
+  simp only [neg_add_cancel, lie_zero]
+
+example : ⁅x - y, m⁆ = ⁅x, m⁆ - ⁅y, m⁆ := by
+  simp only [sub_eq_add_neg, add_lie, neg_lie]
+
+example : ⁅x, m - n⁆ = ⁅x, m⁆ - ⁅x, n⁆ := by
+  simp only [sub_eq_add_neg, lie_add, lie_neg]
+
+example : ⁅-x, m⁆ - -⁅x, m⁆ = 0 := by
+  egg [neg_add_cancel, zero_lie, sub_neg_eq_add, add_lie]
+
+def f : Prop := sorry
+theorem h : (⁅-x, m⁆ - -⁅x, m⁆ = 0) ↔ f := sorry
+
+-- PROBLEM: The fact that the type `M` appears in the subtraction of `?a - ?b = 0` but not in the
+--          equality `?a = ?b` causes `sub_eq_zero` to not be applicable in both directions by
+--          default. The nested split in the `←` direction *is* bidirectional, but contains `M` as
+--          an unbound mvar in the condition `AddGroup ?m`. This should be resolved by type class
+--          specialization. Why is it not?
+set_option trace.egg true in
+example : (⁅-x, m⁆ = -⁅x, m⁆) ↔ f := by
+  egg [sub_eq_zero]
+
+set_option trace.egg true in
+example : ⁅-x, m⁆ = -⁅x, m⁆ := by
+  egg [neg_add_cancel, zero_lie, sub_eq_zero, sub_neg_eq_add, add_lie] -- using ⁅-x, m⁆ - -⁅x, m⁆ = 0
+
+example : ⁅x, -m⁆ = -⁅x, m⁆ := by
+  egg [sub_eq_zero, sub_neg_eq_add, lie_add, neg_add_cancel, lie_zero] using ⁅x, -m⁆ - -⁅x, m⁆ = 0
+
+example : ⁅x - y, m⁆ = ⁅x, m⁆ - ⁅y, m⁆ := by
+  egg [sub_eq_add_neg, add_lie, neg_lie]
+
+example : ⁅x, m - n⁆ = ⁅x, m⁆ - ⁅x, n⁆ := by
+  egg [sub_eq_add_neg, lie_add, lie_neg]

README.md

@@ -72,7 +72,7 @@ If you need more control, you can use `egg calc` to specify a chain of equations
 -- From `Lean/Egg/Tests/Freshman Calc.lean`
 import Egg
 
-theorem freshmans_dream₃ [CharTwoRing α] (x y : α) : (x + y) ^ 3 = x ^ 3 + x * y ^ 2 + x ^ 2 * y + y ^ 3 := by
+example [CharTwoRing α] (x y : α) : (x + y) ^ 3 = x ^ 3 + x * y ^ 2 + x ^ 2 * y + y ^ 3 := by
   egg calc [/- axioms of ring of characteristic 2 -/]
     _ = (x + y) * (x + y) * (x + y)
     _ = (x + y) * (x * (x + y) + y * (x + y))