Alethe walker: cong over built-in operators (lia_axiom_free now walker-first)

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

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

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":