Alethe walker: cong over built-in operators (lia_axiom_free now walker-first) - #51
Merged
Merged
Conversation
…r-first) Refactors elabCong from Sexp-level to Expr-level analysis, which handles built-in operators (not, +, <=, etc.) uniformly without per-operator special-casing. The old code did `sexpToExpr ctx fA` where fA was the function head atom — fine for UF symbols in ctx.vars (`f`, `g`), but failed for built-in operator atoms (`+`, `not`) since they aren't variables and aren't integer literals. cvc5's actual LIA traces use cong heavily over `not` and arithmetic ops, so this was the blocker for any real cvc5 dispatch closing walker-first. New logic translates LHS and RHS as wholes via sexpToExpr (which already understands operator-headed lists like `(+ a b)` → mkAppM HAdd.hAdd …), then strips `pids.length` apps off the LHS to expose the typed operator with its implicit args bound. Eq.refl on that becomes the mkCongr fold seed. Works for: - UF symbols `f`: stripped to `fE` (existing tests pass) - Unary monomorphic `not`: stripped to `Not` - Binary polymorphic `+`, `<=`: stripped to fully-typed `@HAdd.hAdd Int Int Int inst` / `@LE.le Int instLEInt` Three new tests pin cong over `not` / `+` / `<=`, all axiom-free (just propext nowhere — pure mkCongr machinery). VISIBLE END-TO-END IMPACT: lia_axiom_free now closes walker-first (the "cert IS the proof" architectural payoff). Footprint widens from [propext, Quot.sound] (omega path) to [propext, Classical.choice, Quot.sound] (walker path with Classical.em via equiv_pos1/equiv_pos2 in cvc5's trace) — still within the standard classical baseline, no new trust axioms. Verified by removing temporary diagnostic logging from this branch: all four `proof_broker` LIA tests (lines 41, 53, 57, 82 in Test/Tactic.lean) now report "walker closed via tryAletheWalkerLIA" before reaching the omega fallback. Updates lia_axiom_free's docstring to reflect the walker-first path. Trust gate PASS: 96 allowlisted theorems within ceiling (was 93). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
This was referenced May 27, 2026
levineuwirth
added a commit
that referenced
this pull request
May 30, 2026
Mirror of Lean #51. Real cvc5 LIA traces use [cong] to lift argument equalities through built-in operators (not / + / <=), not just UF symbols. This is the congruence shape that lets a real alethe-2024 trace walk end-to-end instead of falling through to lia -- the capability the whole arc was building toward, now wired live via R-9. No elaborator change was needed. The plan budgeted a Constr-level refactor of elab_cong here, but it landed early in R-5: because Coq has no mkCongr, elab_cong was open-coded at the Constr level from the start (translate LHS/RHS via sexp_to_constr, peel the app spine via decompose_app, per-argument f_equal + eq_trans chain). Operator heads (Zadd / Zle / not) decompose exactly like UF heads -- no UF-specific assumption anywhere in the elaborator. Three tests confirm the operator cases: - cong over not (unary, Prop -> Prop) - cong over + (binary over Z) - cong over <= (binary, predicate-valued: result type Prop, the constant arg carried by a refl premise) All axiom-free (cong is f_equal / eq_trans / eq_refl). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
elabCongfrom Sexp-level to Expr-level analysis. The old code didsexpToExpr ctx fAwherefAwas the function head atom — fine for UF symbols inctx.vars(f,g), but failed for built-in operator atoms (+,not) since they aren't variables and aren't integer literals.sexpToExpr(which already understands operator-headed lists), then stripspids.lengthapps off the LHS to expose the typed operator with its implicit args bound.Eq.reflon that becomes themkCongrfold seed. Works uniformly for UF symbols, unary monomorphic operators (Not), and binary polymorphic operators (HAdd.hAdd,LE.le).congovernot/+/<=, all axiom-free.VISIBLE END-TO-END IMPACT
lia_axiom_freenow closes walker-first — the "cert IS the proof" architectural payoff for the entire arc. cvc5's alethe-2024 trace is elaborated step-by-step into a kernel proof term rather than re-proven by omega. Verified by temporary diagnostic logging in this branch (removed before commit): all fourproof_brokerLIA tests reportwalker closed via tryAletheWalkerLIAbefore reaching the omega fallback.Trust footprint change
lia_axiom_free's footprint widens from[propext, Quot.sound](omega path) to[propext, Classical.choice, Quot.sound](walker path withClassical.emviaequiv_pos1/equiv_pos2in cvc5's trace) — still within the standard classical baseline, no new trust axioms. Allowlist updated and docstring synced.Walker arc
This closes the loop opened by PR #41: from FFI scaffold to a real cvc5 LIA dispatch closed by walker-elaborated kernel proof term, axiom-free under the classical baseline.
Test plan
lake buildclean inlean-bridge/(16695 jobs)congtests still pass axiom-free (backward compat)lia_axiom_freepasses at the new walker-path footprintroundtripTestexit 0🤖 Generated with Claude Code