Alethe walker M1.β: clausal layer (scaffolding + assume/resolution/or/false) - #42
Merged
Conversation
…/false) Second slice of the Lean-side Alethe walker. The foundation (PR #41) shipped the FFI + step ADTs; this PR adds the walker proper for the clausal-reasoning layer. The architectural play: turn a cvc5 Tier-3 alethe-2024 cert from a cert-gated omega trigger into the proof itself — per-step kernel elaboration, parallel to how the Tier-1 Farkas term-mode closer consumes Tier-1 certs. **Walker** (`ProofBroker/Alethe.lean`): - `WalkerContext` (Alethe atom → Lean local hypothesis Expr, harvested from the goal's `LocalContext` by `mkContext`) + `WalkerM` (`StateRefT` over a step-id → proof-term map). - `sexpToExpr` / `listToExpr` / `andOrChain` (mutual): translate an Alethe `Sexp` to a Lean `Expr` over the LIA fragment — integer literals (incl. cvc5's `n/1` rational-of-integer form), variable/hypothesis refs, `+`/`-`/`*`, `<=`/`<`/`>=`/ `>`/`=`, `not`/`and`/`or`/`=>`, and the clausal `cl` constructor (`(cl)` → `False`, `(cl L)` → `L`, `(cl L1 …)` → `L1 ∨ …`). - Rule elaborators for the clausal layer: `resolution` (binary ¬-elimination shape — the empty-clause closing step), `or` (clause restatement), `false` (`¬False` premise). - `walkProof`: two-phase — seed each top-level `assume` by `isDefEq`-matching its literal against a local hypothesis, then fold `elabStep` over the step list, returning the last step's proof term. **closeOrFail wiring** (`ProofBroker/Tactic.lean`): the LIA arm now tries `tryAletheWalkerLIA` first for alethe-2024 certs over a `False` goal — walker success closes via the reconstructed term; any walker failure (unsupported rule, non-`False` goal, parse failure) returns `false` and falls through to the existing `omega`. Behavior on every current test is unchanged: real cvc5 LIA traces use ~14 rules of which M1.β covers 4, so the walker throws and omega runs — but the architecture is in place to extend rule-cluster by rule-cluster. **Test-only tactic** `alethe_walker_test "<trace>"` drives the walker on a hand-written alethe-2024 trace (no live cvc5 needed) — same CI-stable pattern as `llm_replay_test`. **Tests**: `alethe_walker_clausal_axiom_free` and its premise-order-flipped twin reconstruct `False` from `A`/`¬A` via `assume` + `resolution`. Both close **axiom-free** — the walker emits `hNA hA` directly, no decision procedure, no axiom. Pinned `[]` in `tools/axiom_allowlist.json`. Scope honesty: even a tiny cvc5 Farkas proof (`x ≥ 3, x ≤ 1 ⊢ False`) uses ~14 rules. M1.β is the clausal foundation; follow-up PRs add `la_generic`+`la_mult_neg` (arithmetic), `refl`/`symm`/`trans`/`cong` (equality), and the boolean- cleanup cluster (`hole`/`rare_rewrite`/`equiv_*`/`implies`/ `and_neg`) cvc5 sprinkles everywhere. Until then real cvc5 traces fall through to omega — no regression, no progression. Verified: full lean-bridge build (16695 jobs) with pinned Vampire, trust-footprint gate, roundtripTest, SDK suite, Python gates — all green. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
levineuwirth
added a commit
that referenced
this pull request
May 21, 2026
Third slice of the Lean-side Alethe walker. The clausal layer (PR #42) shipped assume/resolution/or/false; this PR adds the two linear-arithmetic leaf rules. `la_generic` and `la_mult_neg` are LIA-tautology *leaves* in Alethe: the step's clause is a linear-arithmetic tautology (its negation is LIA-unsat, Farkas multipliers in `:args`), and cvc5 does not decompose them further. Per the recorded scoping decision, the walker discharges these leaves with a scoped `omega` call — the cert drives the surrounding proof skeleton (resolution / congruence / boolean cleanup), the arithmetic leaves are decided. omega is axiom-free; omega-ing the leaf mirrors Alethe's own structure (la_generic IS a leaf). **`elabLiaLeaf`** (`ProofBroker/Alethe.lean`): builds the clause Prop, makes a synthetic mvar, `falseOrByContra`s it into a `False` goal, and runs the `MetaM`-level `Lean.Elab.Tactic.Omega.omega` over the local hypotheses — mirroring `omegaTactic`'s own frontend. Wired into `elabStep` for both `la_generic` and `la_mult_neg`. **`mkIntLit` fix**: the walker now builds Int numerals in the exact form omega's recogniser (`Expr.nat?`/`Expr.int?`) accepts — `@OfNat.ofNat Int ⟨rawNatLit k⟩ inst`. Two traps hit during this PR, both documented in the code: * the `OfNat` form is required (a bare `Int.ofNat k` is an opaque atom to omega); * the inner Nat index must be a *raw* literal via `mkRawNatLit` — `mkNatLit` wraps it in another `OfNat.ofNat`, and `Expr.nat?`'s inner `lit (.natVal _)` match then fails, again leaving the literal an opaque atom. **`alethe_walker_test` relaxed**: previously required a `False` goal; now accepts any goal whose type is defeq to the walked proof's final-step clause. This lets `la_generic` leaves be unit-tested directly (a trace whose last step is a la_generic clause proves that clause as the goal). **Tests**: * `alethe_walker_la_generic_lit` — single-literal unconditional tautology `(cl (<= 0 5))` → goal `(0:Int) ≤ 5`. Footprint `[propext, Quot.sound]` (omega's). * `alethe_walker_la_generic_disj` — multi-literal disjunction `(cl (not (>= x 3)) (>= x 1))` → goal `¬(x ≥ 3) ∨ (x ≥ 1)`, a conditional LIA tautology. Footprint adds `Classical.choice` (`falseOrByContra`'s classical byContra on the disjunction goal). Both pinned in `tools/axiom_allowlist.json`. Still honest: real cvc5 LIA traces interleave la_generic with the boolean-cleanup rules (`hole`/`equiv_*`/`cong`/`implies`/ `and_neg`) and multi-literal resolution, none of which the walker covers yet — so they still fall through to omega. The arithmetic leaves are now ready for when those clusters land. Verified: full lean-bridge build (16695 jobs), trust gate, roundtripTest, SDK suite, Python gates — all green. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This was referenced May 25, 2026
levineuwirth
added a commit
that referenced
this pull request
May 27, 2026
Mirror of Lean PR #42 — the biggest single PR in the Rocq arc. Establishes the EConstr construction template every subsequent PR follows. What's added: * Reference resolution helpers mirroring `term_mode.ml`'s lazy `Rocqlib.lib_ref` pattern: num.Z.* arithmetic operators and comparisons, num.pos.* positive constructors, core.* logical connectives, core.eq.type, core.False.type, etc. * `positive_of_z` / `z_lit` integer literal construction (the walker emits Z constructors directly; `parse_int_atom` handles both "-3" and rational-denominator-1 "-3/1" forms cvc5 emits). * Walker types: `walker_ctx` (Names.Id.Map of atom name → EConstr local-var), `walker_state` (mutable Hashtbl of step id → proof+clause). Lean used `StateRefT MetaM`; Coq plugin convention is OCaml refs + Hashtbl since the walking phase itself is pure OCaml (no Proofview) — only goal assignment crosses into `Proofview.Refine.refine`. * `sexp_to_constr` / `list_to_constr` / `and_or_chain` covering the LIA fragment: integer literals, +/-/*/<=/</>=/>/= over Z, not/and/or/cl/=>, true/false. For `=` we hardcode the type as Z for R-2's scope; boolean equality arrives in R-7 alongside equiv1/equiv2. * Four rule elaborators (clausal layer): - `elab_assume_literal` — match assume literal against local hyp by `Reductionops.is_conv`, return `mkVar` of the match. - `elab_false_step` — `(cl (not false))` → `fun (h : False) => h` via raw `EConstr.mkLambda` + `mkRel 1`. - `elab_or` — passthrough restating premise's proof under the step's flattened clause-literal list. - `elab_resolution_simple` — complementary-singleton pair only (n-ary lift in R-4). * `walk_proof` dispatch: phase 1 seeds assumes against local context, phase 2 walks steps in order. * `walker_test` tactic entry point — parses, walks, defeq- checks against goal, refines. On any error (parse fail, walker error, type mismatch) raises `tclZEROMSG` cleanly so test failures surface as tactic errors, not crashes. Exposed via `g_proof_broker.mlg`: alethe_walker_test "..." (string literal trace) Mirror of Lean's `aletheWalkerTest`. One test in `Test.v` (`alethe_walker_clausal_axiom_free`) closes `forall A, A -> ~A -> False` via a hand-written 3-step trace, proves axiom-free (allowlist entry: []). Validation: local Rocq env broken per project memory (no zarith/rocq-runtime locally); rely on CI for build + axiom gate. May need iterations to nail down exact EConstr API names (`Reductionops.is_conv` vs `Equality.conv?`, `Tacticals.tclZEROMSG` vs `Proofview.tclZERO`, `Sorts.Relevant` enum location, etc.) — that's the documented Rocq parity workflow. Co-Authored-By: Claude Opus 4.7 <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.
What
Second slice of the Lean-side Alethe walker. Foundation PR #41 shipped the FFI + step ADTs; this PR adds the walker proper for the clausal-reasoning layer.
The architectural play: turn a cvc5 Tier-3 `alethe-2024` cert from a cert-gated `omega`-trigger into the proof itself — per-step kernel elaboration, parallel to how the Tier-1 Farkas term-mode closer consumes Tier-1 certs as proofs.
Pieces
Walker (`ProofBroker/Alethe.lean`)
closeOrFail wiring (`ProofBroker/Tactic.lean`): the LIA arm tries `tryAletheWalkerLIA` first for alethe-2024 certs over a `False` goal. Walker success closes via the reconstructed term; any failure (unsupported rule, non-`False` goal, parse failure) falls through to the existing `omega`. Behavior on every current test is unchanged.
Test-only tactic `alethe_walker_test ""` drives the walker on a hand-written trace — no live cvc5 needed.
Tests: `alethe_walker_clausal_axiom_free` + premise-order-flipped twin reconstruct `False` from `A`/`¬A` via `assume`+`resolution`. Both close axiom-free — the walker emits `hNA hA` directly, no decision procedure, no axiom. Pinned `[]` in the allowlist.
Scope honesty
Even a tiny cvc5 Farkas proof (`x ≥ 3, x ≤ 1 ⊢ False`) uses ~14 rules. M1.β is the clausal foundation; real cvc5 LIA traces still fall through to omega (the walker covers 4 of ~14 rules, throws on the rest). No regression, no progression yet — but the architecture is in place to extend rule-cluster by rule-cluster:
Verification
Full lean-bridge build (16695 jobs) with pinned Vampire, trust-footprint gate, roundtripTest, SDK suite, Python gates — all green.
🤖 Generated with Claude Code