R-11: Alethe walker cong over built-in operators (not / + / <=) - #63
Merged
Conversation
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.
R-11 — cong over built-in operators (the payoff)
Eleventh PR of the Rocq walker port arc (mirror of Lean #51). Real cvc5 LIA traces use
congto lift argument equalities through built-in operators (not,+,<=), not just UF symbols. This is the congruence shape that lets a realalethe-2024trace walk end-to-end instead of falling through tolia— the capability the whole arc was building toward, now live via the R-9 closer wiring.No elaborator change needed
The plan budgeted a Constr-level refactor of
elab_conghere, but it landed early in R-5: Coq has nomkCongr, soelab_congwas open-coded at the Constr level from the start — translate LHS/RHS viasexp_to_constr, peel the app spine viadecompose_app, per-argumentf_equal+eq_transchain. Operator heads (Zadd/Zle/not) decompose exactly like UF heads; there is no UF-specific assumption anywhere in the elaborator. So R-11 is purely the tests that confirm the operator cases.Three tests (all axiom-free)
not— unary,Prop → Prop:(~a) = (~b)froma = b+— binary overZ:x + z = y + wfromx = y,z = w<=— binary, predicate-valued (result typeProp); the constant5position is carried by areflpremisecongisf_equal/eq_trans/eq_reflthroughout, so the footprint stays empty[].This unlocks R-12 (snapshot test against a verbatim cvc5 trace), where the full operator+clausal+arithmetic pipeline walks a real refutation.
🤖 Generated with Claude Code