feat: extend tendsto_cont with dischargers, nhdsWithin, and trace mode - #384
Open
cameronfreer wants to merge 30 commits into
Open
feat: extend tendsto_cont with dischargers, nhdsWithin, and trace mode#384cameronfreer wants to merge 30 commits into
cameronfreer wants to merge 30 commits into
Conversation
… arg syntax Add two features to the `tendsto_cont` tactic: - `@[tendsto_cont]` attribute to permanently register closed `Tendsto` lemmas for automatic use (global scope only; local/scoped rejected) - `tendsto_cont [h₁, h₂]` syntax to pass lemmas inline without bringing them into the local context via `have` Three-bucket candidate collection with cross-bucket shadowing: inline args > local context > attribute registry. Candidates from a lower-priority source are dropped if a higher-priority source provides a candidate with the same `fn`, preserving within-source ambiguity detection. The environment extension is in a separate file (TendstoContAttr.lean) so that `meta` tactic code can reference it from a pre-compiled module.
The attribute handler now checks that the declaration's type is `Tendsto f l (nhds a)` (after stripping forall binders). Non-Tendsto declarations and wrong-target-filter declarations are rejected with descriptive errors instead of being silently ignored at tactic time. Also rename unused `h₁` to `_h₁` in the shadowing test to silence the linter warning.
The attribute now rejects any declaration with binders (forall/Pi types) up front, enforcing the "closed lemmas only" contract. Previously, parameterized theorems were accepted at registration but silently ignored at tactic time via catch/continue.
Use Bool with the indiscrete topology (⊤) where nhds = ⊤ and Tendsto holds trivially for any limit. This lets us register two @[tendsto_cont] lemmas for the same function with different limits (false vs true) without sorry, triggering the same-level ambiguity error.
Add tests showing inline and local-context candidates correctly shadow conflicting attribute-registered candidates, resolving the ambiguity that would otherwise error with bare `tendsto_cont`.
Replace the mixed shadowing tests with a separate AttrShadowing section that has a single attributed lemma (limit false) and tests that local context and inline args correctly shadow it with limit true. The goal uses nhds true, so if shadowing fails the proof genuinely breaks. Also fix copyright year in TendstoContAttr.lean (2025 → 2026).
The shadowing tests verify that a higher-priority candidate prevents the ambiguity error, but cannot verify that the correct limit is actually used: in any topology where both Tendsto facts are provable, nhds values coincide and reconcileLimits bridges the gap regardless.
Replace the indiscrete-topology shadowing tests with a Sierpinski-style topology via mkOfNhds where nhds false = ⊤ ≠ pure true = nhds true. Both Tendsto facts remain provable (good always returns true), but using the wrong limit now genuinely fails reconcileLimits. Also fix copyright year in TendstoContAttr.lean (2025 → 2026).
Replace trivial positive tests for `tendsto_cont [...]` and `@[tendsto_cont]` with failure-before-success patterns using private defs/theorems and #guard_msgs, so CI enforces that the features are genuinely needed.
Emit a warning when `tendsto_cont [h]` is passed a local hypothesis that would have been picked up automatically, unless the inline arg serves a disambiguation purpose (conflicting limits for the same atom).
The redundancy warning for inline FVars now also checks other inline arguments for same-fn/different-limit conflicts, not just the local context. Prevents false warnings when an inline FVar disambiguates against a non-local inline arg.
Add failure-before-success test using an opaque axiomatized function where fun_prop can't help, making the @[tendsto_cont] attribute genuinely load-bearing.
Extract the composite-atom discovery and product-abstraction logic from tendsto_cont into a reusable AtomEngine module, keeping tendsto_cont as the first client. New features: - `tendsto_cont (disch := tac)`: pass a discharger to fun_prop for side conditions (inv, div, log, sqrt, etc.) - `tendsto_cont?`: report matched atoms and computed limit before solving - Accept `nhdsWithin` hypotheses: extracts limit and wraps via Tendsto.mono_right nhdsWithin_le_nhds Also adds compound-atom test cases (Group A: pure gap isolations, Group B: integration coverage with continuous wrappers and limit reconciliation) motivated by Tomas Skrivan's fun_prop PR #37056.
…provenance Two fixes from code review: 1. tendsto_cont? now reports the actual computed limit (body evaluated at atom values) instead of the raw product value point. Uses new AtomEngine.substituteAtomValues to replace atoms with their values directly, avoiding product projection reduction issues. 2. nhdsWithin hypothesis wrapping preserves original hypothesis via Atom.origHyp field, so redundancy warnings still fire correctly when nhdsWithin hypotheses are passed as inline args. Adds tests for nhdsWithin redundancy warnings and tendsto_cont? with disch.
- nhdsWithin inline shadowing (no warning when inline overrides local) - nhdsWithin ambiguity detection (two nhdsWithin hyps, different limits) - disch := positivity as non-norm_num discharger example
Accept goals of the form `Tendsto body l (nhdsWithin c s)`, not just `nhds c`. Strategy: split via `tendsto_nhdsWithin_iff` into an nhds subgoal (proved by existing machinery) and an `∀ᶠ x in l, body x ∈ s` subgoal (closed by univ_mem/assumption/simp/trivial, or left for the user). Tests cover Set.univ (trivially closed), explicit ∀ᶠ hypothesis in context, and nhdsWithin + limit reconciliation.
Fixes: - Constant-body nhdsWithin goals now work (was hitting tendsto_const_nhds which only targets nhds) - ∀ᶠ discharge uses safe tryEvGoal: tries assumption first, then univ_mem' only after checking the predicate reduces to True (avoids logged errors from failed exact elaboration) - Updated module docs and error hints for nhdsWithin goal support Tests: - Constant body + Set.univ: auto-closed - Constant body + Set.Ioi: user provides membership proof - Atom body + undischargeable ∀ᶠ: tactic leaves subgoal (sorry test) - Atom body + assumption finds ∀ᶠ: auto-closed
- Replace sorry-based negative test with proper #guard_msgs(error) asserting the exact remaining ∀ᶠ goal from nhdsWithin splitting - Fix docs: discharge list now matches implementation (assumption + guarded univ_mem', not simp/trivial)
New feature: - `tendsto_cont (within_disch := tac)`: discharge the `∀ᶠ x in l, body x ∈ s` obligation for nhdsWithin goals. Runs after built-in `assumption` and `univ_mem'` fail. Composes with `disch :=`: `tendsto_cont (disch := positivity) (within_disch := exact hev)`. - `tendsto_cont?` now reports the nhdsWithin set and membership obligation status for nhdsWithin goals. Tests: - within_disch on constant body + nontrivial set - within_disch on atom body with pointwise hypothesis - Both disch + within_disch together - Negative test: without within_disch, same goal left open - tendsto_cont? trace for nhdsWithin goals
- Support both option orders: (disch := ...) (within_disch := ...) and (within_disch := ...) (disch := ...) - Fix misleading doc example (positivity doesn't close ∀ᶠ goals) - tendsto_cont? now reports when ∀ᶠ membership obligation is left for the user after nhdsWithin discharge attempt - Add reversed-order option test
Pointwise lift: - within_disch tactics are now auto-lifted via Filter.univ_mem' when they fail on the ∀ᶠ goal directly. This means users can write `within_disch := norm_num` instead of `within_disch := exact Filter.univ_mem' (fun _ => by norm_num)`. - Tried first directly, then with pointwise intro. Syntax consolidation: - 10 syntax rules (down from 14) + 10 elab_rules (down from 20) via shared `tc` handler with named optional parameters. - Cleaner, easier to maintain when adding future options. Tests updated to use simpler within_disch invocations.
Attribute extension: - @[tendsto_cont] now accepts nhdsWithin lemmas (not just nhds). The tactic already handled nhdsWithin hypotheses via mono_right; the attribute registrar now matches. Trace consistency: - tendsto_cont? on constant bodies now reports "constant body" with computed limit and nhdsWithin set info (was silently returning). - EvDischargeMethod enum tracks which strategy closed the ∀ᶠ goal: assumption, univ_mem', within_disch (direct), pointwise lift, or undischarged. tendsto_cont? reports this in its trace output. Tests: - tendsto_cont? constant body (nhds and nhdsWithin) - tendsto_cont? nhdsWithin with discharge method reporting - tendsto_cont? with within_disch (pointwise lift reported) - @[tendsto_cont] nhdsWithin positive test - Updated existing #guard_msgs for widened error messages
Replace constant-body attribute test (which was solved by the constant fast path regardless of attribute support) with an opaque function that exercises the actual attribute → nhdsWithin → nhds wrapping pipeline. Uses before/after registration pattern.
- Add tendsto_cont? test exercising the direct within_disch discharge path (not pointwise lift). Uses ∀ x hypothesis (not ∀ᶠ) so assumption can't match, forcing through within_disch. - Note brittleness of candidate list in before-registration test (depends on earlier atTop attribute registrations). All four EvDischargeMethod arms are now covered by #guard_msgs tests: assumption, univMem, withinDisch, pointwiseLift, undischarged.
Adds #guard_msgs test for the undischarged EvDischargeMethod arm, completing trace coverage for all five discharge outcomes: assumption, univMem, withinDisch, pointwiseLift, undischarged.
cameronfreer
added a commit
to cameronfreer/Sphere-Packing-Lean
that referenced
this pull request
Mar 30, 2026
Extract each candidate-collection bucket into its own function per b-mehta's review feedback: - collectInlineCands: inline argument candidates - warnRedundantInlineArgs: redundancy warnings for inline FVars - collectContextCands: local context candidates (shadowed by inline) - collectAttrCands: attribute registry candidates (shadowed by both) - checkAmbiguity: same-fn-different-limit detection collectAtoms now composes these, improving readability and preparing for the AtomEngine extraction in the follow-up PR thefundamentaltheor3m#384.
4 tasks
Conflict resolutions: - SpherePacking.lean: main's import list + AtomEngine import - TendstoCont.lean: branch version kept; main's collectAtoms bucket-split refactor is superseded by the AtomEngine extraction (same logic) - TendstoContAttr.lean: branch version (main's + nhdsWithin validation) - Test/TendstoCont.lean: branch tests + copyright header and #guard_msgs docstring from thefundamentaltheor3m#414 (header is load-bearing for linter.style.header)
- replaceAtoms: single generic traversal for abstractBody and substituteAtomValues (callback decides projection vs value) - add forallE arm so replacement traverses the same constructors as exprChildren discovery (previously atoms under a forall binder were discovered but never abstracted) - foldrAtoms: generic right-associated fold subsuming buildProdType, buildValuePoint, and TendstoCont's buildProdMkNhds - fix AtomEngine copyright year (file created 2026)
tendstoContOption groups (disch := tac) / (within_disch := tac) as a repeated element, collapsing 10 syntax rules x 10 elab_rules into 2 + 2. Order flexibility now falls out of the grammar; duplicate options are rejected at elaboration with #guard_msgs tests locking in the errors.
cameronfreer
marked this pull request as ready for review
June 11, 2026 03:12
cameronfreer
requested review from
CBirkbeck,
b-mehta,
pitmonticone,
seewoo5,
thefundamentaltheor3m and
viazovska
as code owners
June 11, 2026 03:12
Contributor
Author
|
awaiting-review |
1 task
seewoo5
pushed a commit
that referenced
this pull request
Jun 23, 2026
## Summary One-line style cleanup matching PR #422's `tendsto_cont` convention. In `RamanujanIdentities.lean`, replace the older throwaway-`have` form with the inline-argument form: ```lean -- before (by have := E₄_tendsto_one_atImInfty; tendsto_cont) -- after (by tendsto_cont [E₄_tendsto_one_atImInfty]) ``` `E₄_tendsto_one_atImInfty` is a *global* theorem fact, so passing it inline is the correct spelling — not the redundant-local-argument case that #384's tests warn about (those are for named local hypotheses already in context, where bare `tendsto_cont` stays right). ## Test plan - [x] `lake build` passes.
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
tendsto_cont (disch := tac)— pass a discharger tofun_propfor continuity side conditions (inv, div, log)tendsto_cont (within_disch := tac)— discharge∀ᶠ x in l, body x ∈ sobligations fornhdsWithingoals; auto-lifts pointwise proofs viaFilter.univ_mem'nhdsWithinsupport — accepts hypotheses (wrapped viamono_right), goals (split viatendsto_nhdsWithin_iff), and@[tendsto_cont]attributestendsto_cont?— trace mode reporting matched atoms, computed limit, nhdsWithin set info, and discharge methodAlso adds compound-atom test cases for the compound-atom pattern reported as a gap in the
fun_propcomparison (discussion).Both hooks compose in either order.
Depends on #378 (cameronfreer/tendsto-cont-attr). Please merge that first.Architecture
The reusable composite-atom discovery and product-abstraction logic is extracted into
AtomEngine.lean, withTendstoCont.leanas the first client. This isolates reusable atom-matching logic for future tactic work.New syntax
Test coverage
Adds extensive tests covering compound atoms,
nhdsWithin(hypotheses, goals, cross-bucket shadowing, ambiguity,@[tendsto_cont]with opaque nhdsWithin function), dischargers (disch/within_dischwith pointwise lift, both hooks composed, reversed order),tendsto_cont?trace assertions via#guard_msgs(all five discharge outcomes), and negative tests for undischargeable goals and attribute validation.Motivation
During discussion around mathlib #37056, Tomas Skrivan reported that
fun_prophandled the existingtendsto_contsuite except the compound-atom cases — hypotheses about composed functions likeTendsto (fun x => f (g x)) l (nhds a). This branch adds compound-atom tests as a richer comparison suite and extracts the atom-matching engine so the advantage is reusable.