Alethe walker: equality cluster (refl / symm / trans / cong)

Adds the four equality rules cvc5's alethe-2024 emits for UF and
equality reasoning. All four reconstruct the kernel proof from
premise proofs directly (no decision procedure), so the resulting
theorems are axiom-free.

* `refl`: Eq.refl on the LHS of (cl (= t t)).
* `symm`: Eq.symm on the single premise.
* `trans`: left-fold of Eq.trans over the premise list.
* `cong`: left-fold of Lean.Meta.mkCongr over premise equations,
  seeded with Eq.refl on the (Sexp-equal) function head.

`sexpToExpr`'s `listToExpr` gains a generic-application fallback:
unknown-head atoms are resolved through `ctx.vars` and applied to
their reified args via `mkAppM'`. This is what lets `cong`
translate `(f a1 … an)` for an arbitrary UF symbol `f` in scope.

Six new tests in Test/Tactic.lean exercise each rule in isolation
plus an end-to-end UF refutation (`x = y, ¬(f x = f y) ⊢ False`
via cong + resolution); all six close axiom-free. Allowlist
entries updated accordingly.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

Author: levineuwirth

lean-bridge/ProofBroker/Alethe.lean

@@ -341,6 +341,21 @@ partial def listToExpr (ctx : WalkerContext) : List Sexp → MetaM Expr
     let aE ← sexpToExpr ctx a
     let bE ← sexpToExpr ctx b
     return mkForall .anonymous .default aE bE
+  -- Generic application fallback. Used by `cong` to translate
+  -- `(f a1 … an)` into `f a1 … an` for UF symbols. The head is
+  -- looked up in `ctx.vars` (UF symbols are local free vars in
+  -- the home-system goal); arguments recurse through
+  -- `sexpToExpr`. Falls through to the catch-all error if the
+  -- head is not in scope, keeping unrecognized shapes as honest
+  -- failures rather than silently building ill-typed apps.
+  | (.atom name) :: args => do
+    match ctx.vars.find? (Name.mkSimple name) with
+    | some fE => do
+      let argEs ← args.mapM (sexpToExpr ctx)
+      Lean.Meta.mkAppM' fE argEs.toArray
+    | none =>
+      throwError m!"alethe walker: unsupported applied head '{name}' \
+                    (not a recognized operator, not in local scope)"
   | other =>
     throwError m!"alethe walker: unsupported Sexp shape: \
                   ({String.intercalate " " (other.map fun s => reprStr s)})"
@@ -548,6 +563,105 @@ private def elabResolution (ctx : WalkerContext) (s : Step)
     throwError m!"alethe walker: 'resolution' needs at least one \
                    premise, got {repr s.premises}"
 
+/- ----------------------------------------------------------------
+   Equality cluster: `refl` / `symm` / `trans` / `cong`.
+
+   These are the rules cvc5's `alethe-2024` emits for the UF /
+   equality fragment. None of them touch a decision procedure
+   (unlike `la_generic` / `la_mult_neg` which omega-discharge a
+   tautological leaf): they reconstruct the kernel proof from the
+   premises directly, so the resulting proof terms are axiom-free
+   (no `propext` / `Classical.choice`, just `Eq.rec` underneath).
+   ---------------------------------------------------------------- -/
+
+/-- `refl`: a leaf rule with no premises, concluding `(cl (= t t))`
+    for any term `t`. The walker requires LHS and RHS to be
+    syntactically identical at the Sexp level (the form cvc5
+    emits after preprocessing); the proof term is `Eq.refl t`. -/
+private def elabRefl (ctx : WalkerContext) (s : Step)
+    : WalkerM (Expr × List Sexp) := do
+  match s.clause with
+  | [.list [.atom "=", lhs, rhs]] => do
+    unless lhs == rhs do
+      throwError m!"alethe walker: 'refl' expects (= t t) with \
+                     identical sides, got (= {repr lhs} {repr rhs})"
+    let lhsE ← sexpToExpr ctx lhs
+    let proof ← mkAppM ``Eq.refl #[lhsE]
+    pure (proof, s.clause)
+  | _ =>
+    throwError m!"alethe walker: 'refl' expects clause \
+                   (cl (= t t)), got {repr s.clause}"
+
+/-- `symm`: one premise proving `(= t u)`, conclusion `(= u t)`.
+    The proof term is `Eq.symm` of the premise. -/
+private def elabSymm (s : Step) : WalkerM (Expr × List Sexp) := do
+  match s.premises with
+  | some [p] => do
+    let (eP, _) ← lookupStep p
+    let proof ← mkAppM ``Eq.symm #[eP]
+    pure (proof, s.clause)
+  | _ =>
+    throwError m!"alethe walker: 'symm' expects exactly one \
+                   premise, got {repr s.premises}"
+
+/-- `trans`: n premises proving `(= t1 t2)`, `(= t2 t3)`, …,
+    `(= t_{n} t_{n+1})`, conclusion `(= t1 t_{n+1})`. The proof
+    term is the left-fold of `Eq.trans` over the premise list.
+    A single-premise `trans` is a no-op (passthrough). -/
+private def elabTrans (s : Step) : WalkerM (Expr × List Sexp) := do
+  match s.premises with
+  | some (p0 :: rest) => do
+    let (e0, _) ← lookupStep p0
+    let mut acc := e0
+    for pi in rest do
+      let (ei, _) ← lookupStep pi
+      acc ← mkAppM ``Eq.trans #[acc, ei]
+    pure (acc, s.clause)
+  | _ =>
+    throwError m!"alethe walker: 'trans' expects at least one \
+                   premise, got {repr s.premises}"
+
+/-- `cong`: n premises proving `(= a1 b1)`, …, `(= an bn)`,
+    conclusion `(= (f a1 … an) (f b1 … bn))`. The proof term is
+    built by left-folding `Lean.Meta.mkCongr` over the premise list,
+    starting from `Eq.refl f`. `mkCongr` collapses the
+    `Eq.refl f` seed into `mkCongrArg` automatically, then chains
+    through `mkCongr`'s general case for each subsequent
+    argument — so the resulting term is a curried congruence
+    cascade (`(f a1) a2 = (f b1) b2` etc.) matching Lean's own
+    curried application convention.
+
+    The function head is required to be identical on both sides
+    (Sexp `BEq`); typically `fA = .atom "f"` for a UF symbol the
+    walker resolves through `sexpToExpr`'s context lookup, but a
+    higher-order head (an applied list) is also accepted as long
+    as both sides agree structurally. Arity mismatch or differing
+    heads throw a clear error. -/
+private def elabCong (ctx : WalkerContext) (s : Step)
+    : WalkerM (Expr × List Sexp) := do
+  match s.clause, s.premises with
+  | [.list [.atom "=", .list (fA :: argsA), .list (fB :: argsB)]],
+    some pids => do
+    unless fA == fB do
+      throwError m!"alethe walker: 'cong' function heads differ: \
+                     {repr fA} vs {repr fB}"
+    unless argsA.length == argsB.length do
+      throwError m!"alethe walker: 'cong' arity mismatch: LHS has \
+                     {argsA.length} args, RHS has {argsB.length}"
+    unless argsA.length == pids.length do
+      throwError m!"alethe walker: 'cong' has {pids.length} \
+                     premises but {argsA.length} argument pairs"
+    let fExpr ← sexpToExpr ctx fA
+    let mut acc ← mkAppM ``Eq.refl #[fExpr]
+    for pid in pids do
+      let (eqProof, _) ← lookupStep pid
+      acc ← Lean.Meta.mkCongr acc eqProof
+    pure (acc, s.clause)
+  | _, _ =>
+    throwError m!"alethe walker: 'cong' expects clause \
+                   (cl (= (f …) (f …))) with a premise list, got \
+                   clause {repr s.clause}, premises {repr s.premises}"
+
 /-- LIA-tautology leaf rules (`la_generic`, `la_mult_neg`). The
     step's clause is a linear-arithmetic tautology — its negation
     is LIA-unsatisfiable, with the Farkas multipliers carried in
@@ -591,16 +705,19 @@ def elabStep (ctx : WalkerContext) (s : Step) : WalkerM Unit := do
     | "false" => elabFalseStep ctx s
     | "la_generic" => elabLiaLeaf ctx s
     | "la_mult_neg" => elabLiaLeaf ctx s
+    | "refl" => elabRefl ctx s
+    | "symm" => elabSymm s
+    | "trans" => elabTrans s
+    | "cong" => elabCong ctx s
     | other =>
       throwError m!"alethe walker: rule '{other}' not yet \
                      supported (current scope: resolution / or / \
-                     false / la_generic / la_mult_neg, plus \
-                     seeded assumes. Subsequent PRs add the \
-                     equality (cong / refl / trans / symm) and \
-                     boolean-cleanup (hole / rare_rewrite / \
-                     equiv_* / implies / and_neg) clusters — the \
-                     omega fallback handles full cvc5 traces in \
-                     the meantime)."
+                     false / la_generic / la_mult_neg / refl / \
+                     symm / trans / cong, plus seeded assumes. \
+                     Subsequent PRs add the boolean-cleanup \
+                     cluster (hole / rare_rewrite / equiv_* / \
+                     implies / and_neg) — the omega fallback \
+                     handles full cvc5 traces in the meantime)."
   storeStep s.id proof clause
 
 /-- Walk an Alethe proof and return the `Expr` proving the final

lean-bridge/Test/Tactic.lean

@@ -525,4 +525,86 @@ theorem alethe_walker_resolution_axiom_free
 
 #print axioms alethe_walker_resolution_axiom_free
 
+/- Alethe walker — equality cluster (`refl` / `symm` / `trans` /
+   `cong`).
+
+   These rules are how cvc5's `alethe-2024` walks
+   uninterpreted-function and equality reasoning. None of them
+   touch a decision procedure (unlike `la_generic`): the proof
+   term is reconstructed kernel-side from the premise proofs
+   directly, so the resulting theorems are axiom-free (no
+   `propext` / `Classical.choice`, just `Eq.rec` underneath). -/
+
+/-- `refl`: a leaf rule concluding `t = t` for any `t`. No
+    premises, just `Eq.refl t`. -/
+theorem alethe_walker_refl_axiom_free (a : Int) : a = a := by
+  alethe_walker_test
+    "( (step t0 (cl (= a a)) :rule refl) )"
+
+#print axioms alethe_walker_refl_axiom_free
+
+/-- `symm`: flips an equality. Premise `a = b`, conclusion
+    `b = a`; proof term is `Eq.symm h`. -/
+theorem alethe_walker_symm_axiom_free
+    (a b : Int) (h : a = b) : b = a := by
+  alethe_walker_test
+    "( (assume a0 (= a b)) \
+       (step t0 (cl (= b a)) :rule symm :premises (a0)) )"
+
+#print axioms alethe_walker_symm_axiom_free
+
+/-- `trans`: chains equalities. Premises `a = b`, `b = c`;
+    conclusion `a = c`; proof term is the left-fold of
+    `Eq.trans`. Exercises the n-ary premise list. -/
+theorem alethe_walker_trans_axiom_free
+    (a b c : Int) (h1 : a = b) (h2 : b = c) : a = c := by
+  alethe_walker_test
+    "( (assume a0 (= a b)) \
+       (assume a1 (= b c)) \
+       (step t0 (cl (= a c)) :rule trans :premises (a0 a1)) )"
+
+#print axioms alethe_walker_trans_axiom_free
+
+/-- `cong` over a unary UF symbol: `x = y ⊢ f x = f y`. The
+    walker's generic application case translates `(f x)` /
+    `(f y)` by looking up `f` in the local context; the proof
+    term is `mkCongr (Eq.refl f) h` — i.e., `congrArg f h`. -/
+theorem alethe_walker_cong_axiom_free
+    (f : Int → Int) (x y : Int) (h : x = y) : f x = f y := by
+  alethe_walker_test
+    "( (assume a0 (= x y)) \
+       (step t0 (cl (= (f x) (f y))) :rule cong :premises (a0)) )"
+
+#print axioms alethe_walker_cong_axiom_free
+
+/-- `cong` over a 2-arg UF symbol: `a = c ∧ b = d ⊢ f a b = f c d`.
+    The `mkCongr` left-fold builds the curried cascade
+    `(f a) b = (f c) d` via two `mkCongr` steps. -/
+theorem alethe_walker_cong_two_arg_axiom_free
+    (f : Int → Int → Int) (a b c d : Int)
+    (h1 : a = c) (h2 : b = d) : f a b = f c d := by
+  alethe_walker_test
+    "( (assume a0 (= a c)) \
+       (assume a1 (= b d)) \
+       (step t0 (cl (= (f a b) (f c d))) \
+        :rule cong :premises (a0 a1)) )"
+
+#print axioms alethe_walker_cong_two_arg_axiom_free
+
+/-- End-to-end UF refutation: combine `cong` with the clausal
+    layer. From `x = y` and `f x ≠ f y`, derive `False` via
+    `cong` (to get `f x = f y`) + `resolution` against the
+    inequality. The walker reconstructs the full proof skeleton
+    axiom-free — UF reasoning all the way down. -/
+theorem alethe_walker_cong_refutation_axiom_free
+    (f : Int → Int) (x y : Int)
+    (h : x = y) (hne : ¬(f x = f y)) : False := by
+  alethe_walker_test
+    "( (assume a0 (= x y)) \
+       (assume a1 (not (= (f x) (f y)))) \
+       (step t0 (cl (= (f x) (f y))) :rule cong :premises (a0)) \
+       (step t1 (cl) :rule resolution :premises (t0 a1)) )"
+
+#print axioms alethe_walker_cong_refutation_axiom_free
+
 end ProofBroker.Test

tools/axiom_allowlist.json

@@ -58,6 +58,18 @@
       ["propext", "Classical.choice", "Quot.sound"],
     "ProofBroker.Test.alethe_walker_resolution_axiom_free":
       [],
+    "ProofBroker.Test.alethe_walker_refl_axiom_free":
+      [],
+    "ProofBroker.Test.alethe_walker_symm_axiom_free":
+      [],
+    "ProofBroker.Test.alethe_walker_trans_axiom_free":
+      [],
+    "ProofBroker.Test.alethe_walker_cong_axiom_free":
+      [],
+    "ProofBroker.Test.alethe_walker_cong_two_arg_axiom_free":
+      [],
+    "ProofBroker.Test.alethe_walker_cong_refutation_axiom_free":
+      [],
     "ProofBroker.TestMathlib.lra_axiom_free":
       ["propext", "Classical.choice", "Quot.sound"],
     "ProofBroker.TestMathlib.pb_term_case_split_axiom_free":