From b6c0dd1f227b072600dbf2b63fa5b90ae36f6c4c Mon Sep 17 00:00:00 2001 From: Marcus Rossel Date: Mon, 13 Jan 2025 16:53:20 +0100 Subject: [PATCH] Don't rely on layout of C enums in FFI code --- C/ffi.c | 39 ++++++++++++++++++----- Lean/Egg/Tests/Math/Math/Lie.lean | 52 +++++++++++++++++++++++++++++++ README.md | 2 +- 3 files changed, 84 insertions(+), 9 deletions(-) create mode 100644 Lean/Egg/Tests/Math/Math/Lie.lean diff --git a/C/ffi.c b/C/ffi.c index 063e927..d1485bd 100644 --- a/C/ffi.c +++ b/C/ffi.c @@ -1,5 +1,6 @@ #include #include +#include #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); + } } /* diff --git a/Lean/Egg/Tests/Math/Math/Lie.lean b/Lean/Egg/Tests/Math/Math/Lie.lean new file mode 100644 index 0000000..df2c127 --- /dev/null +++ b/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] diff --git a/README.md b/README.md index fc75086..0b73783 100644 --- a/README.md +++ b/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))