From 75a57d0586fb18143a7fa8c30d80166c2734058d Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Wed, 27 May 2026 09:57:21 -0400 Subject: [PATCH] Alethe walker: cong over built-in operators (lia_axiom_free now walker-first) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- lean-bridge/ProofBroker/Alethe.lean | 71 +++++++++++++++++++---------- lean-bridge/Test/Tactic.lean | 60 +++++++++++++++++++++--- tools/axiom_allowlist.json | 8 +++- 3 files changed, 108 insertions(+), 31 deletions(-) diff --git a/lean-bridge/ProofBroker/Alethe.lean b/lean-bridge/ProofBroker/Alethe.lean index 4214e5f..151f8dd 100644 --- a/lean-bridge/ProofBroker/Alethe.lean +++ b/lean-bridge/ProofBroker/Alethe.lean @@ -646,45 +646,68 @@ private def elabTrans (s : Step) : WalkerM (Expr × List Sexp) := do 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 +/-- `cong`: n premises proving `(= a₁ b₁)`, …, `(= aₙ bₙ)`, + conclusion `(= (f a₁ … aₙ) (f b₁ … bₙ))`. 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 + cascade (`(f a₁) a₂ = (f b₁) b₂` 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. -/ + Implementation works at the `Expr` level rather than the + `Sexp` level so it handles built-in operator atoms uniformly: + LHS and RHS are translated via `sexpToExpr` (which knows + `(+ a b)` → `mkAppM ``HAdd.hAdd …`, `(not a)` → `Not a`, UF + `(f x)` → applied free var, etc.), then `pids.length` apps + are peeled off the LHS via `Expr.appFn!` to expose the + operator with its implicit/typeclass args bound. `Eq.refl + opE` becomes the fold seed. + + Concretely: for `cong h : x = y ⊢ (= (+ x z) (+ y z))` over + `Int`, `lhsE = @HAdd.hAdd Int Int Int inst x z` has 6 app + levels (4 implicit + 2 explicit); stripping 2 (= 1 premise, + since the cong is only over the `x = y` arg) gives + `@HAdd.hAdd Int Int Int inst x` — but wait, that strips one + explicit AND not the right one. Actually cvc5 emits cong with + a premise per arg position, so for binary ops the trace has + two premises; stripping 2 gives `@HAdd.hAdd Int Int Int + inst`, the right operator to seed mkCongr from. Mismatched + arities or differing operators throw. -/ 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 + | [.list [.atom "=", lhsSexp, rhsSexp]], some pids => do + let lhsE ← sexpToExpr ctx lhsSexp + let rhsE ← sexpToExpr ctx rhsSexp + let lhsArity := lhsE.getAppNumArgs + let rhsArity := rhsE.getAppNumArgs + unless lhsArity == rhsArity do + throwError m!"alethe walker: 'cong' app-arity mismatch: \ + LHS has {lhsArity} app levels, RHS has \ + {rhsArity}" + unless pids.length ≤ lhsArity 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] + premises but LHS only has {lhsArity} app \ + levels (translated form: {lhsE})" + let mut opE := lhsE + let mut opERhs := rhsE + for _ in [0:pids.length] do + opE := opE.appFn! + opERhs := opERhs.appFn! + unless ← Meta.isDefEq opE opERhs do + throwError m!"alethe walker: 'cong' operator heads differ \ + after stripping {pids.length} explicit args: \ + {opE} vs {opERhs}" + let mut acc ← mkAppM ``Eq.refl #[opE] 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 \ + (cl (= LHS RHS)) with a premise list, got \ clause {repr s.clause}, premises {repr s.premises}" /-- Shared omega-discharge helper. Translates the step's clause to diff --git a/lean-bridge/Test/Tactic.lean b/lean-bridge/Test/Tactic.lean index 6e8e259..e4bfe60 100644 --- a/lean-bridge/Test/Tactic.lean +++ b/lean-bridge/Test/Tactic.lean @@ -71,12 +71,16 @@ example (n m : Int) (h1 : n + m = 10) (h3 : 0 ≤ m) : n ≤ 10 := by /-- Named LIA goal proven via the default `proof_broker` form, which `preferHigherTier := true` floats to cvc5's Tier 3 - alethe-2024 path. Even with a Tier 3 cert (no Lean-side - Alethe walker yet) the closer is `omega` because the goal is - LIA — cert verification gates the call, omega does the rest. - omega is axiom-free, so this theorem's transitive axiom set - stays within the core-Lean ceiling; verified inline by - `#print axioms` below. -/ + alethe-2024 path. The Lean-side Alethe walker now elaborates + the trace into a kernel proof term ("cert IS the proof") — + this is the first test in the suite where a real cvc5 + dispatch closes walker-first rather than via the omega + fallback. Footprint is `[propext, Classical.choice, + Quot.sound]` because cvc5's trace uses boolean-cleanup rules + (`equiv_pos1` / `equiv_pos2`) whose proof terms invoke + `Classical.em`; same classical baseline as the + `proof_broker_term` paths. Verified inline by `#print axioms` + below. -/ theorem lia_axiom_free (n m : Int) (h1 : n + m = 10) (h3 : 0 ≤ m) : n ≤ 10 := by proof_broker @@ -889,4 +893,48 @@ theorem alethe_walker_equiv_pos2_axiom_free #print axioms alethe_walker_equiv_pos2_axiom_free +/- Alethe walker — `cong` over built-in operators. + + Real cvc5 LIA traces use `cong` to lift argument equalities + through built-in operators (`not`, `+`, `<=`, etc.) — not just + UF symbols. The Expr-level `elabCong` refactor handles these + by translating LHS/RHS via `sexpToExpr` (which already knows + how to translate operator-headed lists) and stripping + `pids.length` apps to expose the typed operator. -/ + +/-- `cong` over `not` (unary Prop operator). Trace shape mirrors + UF cong but with `not` as the function head. -/ +theorem alethe_walker_cong_not_axiom_free + (a b : Prop) (h : a = b) : (¬a) = (¬b) := by + alethe_walker_test + "( (assume a0 (= a b)) \ + (step t0 (cl (= (not a) (not b))) :rule cong :premises (a0)) )" + +#print axioms alethe_walker_cong_not_axiom_free + +/-- `cong` over `+` (binary polymorphic operator over `Int`). + cvc5 emits this when lifting arg equalities through an + addition during LIA normalization. -/ +theorem alethe_walker_cong_add_axiom_free + (x y z w : Int) (h1 : x = y) (h2 : z = w) : x + z = y + w := by + alethe_walker_test + "( (assume a0 (= x y)) \ + (assume a1 (= z w)) \ + (step t0 (cl (= (+ x z) (+ y w))) :rule cong :premises (a0 a1)) )" + +#print axioms alethe_walker_cong_add_axiom_free + +/-- `cong` over `<=` (binary comparison, predicate-valued). + Slightly different from `+`: the conclusion's equality is + between two `Prop`s, exercising the `mkCongr` chain when the + operator's result type is `Prop`. -/ +theorem alethe_walker_cong_le_axiom_free + (x y : Int) (h : x = y) : (x ≤ 5) = (y ≤ 5) := by + alethe_walker_test + "( (assume a0 (= x y)) \ + (step t_refl (cl (= 5 5)) :rule refl) \ + (step t0 (cl (= (<= x 5) (<= y 5))) :rule cong :premises (a0 t_refl)) )" + +#print axioms alethe_walker_cong_le_axiom_free + end ProofBroker.Test diff --git a/tools/axiom_allowlist.json b/tools/axiom_allowlist.json index 9290900..ce61b3e 100644 --- a/tools/axiom_allowlist.json +++ b/tools/axiom_allowlist.json @@ -3,7 +3,7 @@ "lean": { "ProofBroker.Test.lia_axiom_free": - ["propext", "Quot.sound"], + ["propext", "Classical.choice", "Quot.sound"], "ProofBroker.Test.tier1_lia_axiom_free": ["propext", "Quot.sound"], "ProofBroker.Test.pb_term_axiom_free": @@ -106,6 +106,12 @@ ["propext", "Classical.choice", "Quot.sound"], "ProofBroker.Test.alethe_walker_equiv_pos2_axiom_free": ["propext", "Classical.choice", "Quot.sound"], + "ProofBroker.Test.alethe_walker_cong_not_axiom_free": + [], + "ProofBroker.Test.alethe_walker_cong_add_axiom_free": + [], + "ProofBroker.Test.alethe_walker_cong_le_axiom_free": + [], "ProofBroker.TestMathlib.lra_axiom_free": ["propext", "Classical.choice", "Quot.sound"], "ProofBroker.TestMathlib.pb_term_case_split_axiom_free":