Conversation
Port the `cfc_pull` tactic from j-loreaux/mathlib4#cfc-pull, staged under the
paths it will occupy in mathlib:
* `LeanOA/Mathlib/Tactic/CFCPull{.lean,/}` — the `@[cfc_pull]` attribute and its
lemma database, the core recursion, and the tactic/`conv` frontend, together
with the specification and design documents.
* `LeanOA/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/CFCPull/`
— the lemmas the tactic needs (`Lemmas`), the `@[cfc_pull]` tags on mathlib's
own lemmas (`Tags`), and `CFC.sqrt` via the complex calculus (`ComplexSqrt`).
* `LeanOA/MathlibTest/CFCPull/` — the test suite, mirroring `MathlibTest/` the
way `LeanOA/Mathlib/` mirrors `Mathlib/`.
Adaptations to this repo, each marked with a comment where it is not just an
import path:
* `Tracing.lean` expects `fun x ↦ _` rather than `fun x => _`, since LeanOA sets
`pp.unicode.fun` package-wide and mathlib's `MathlibTest` library does not.
* One Hermitian-matrix example needs `backward.isDefEq.respectTransparency true`
restored; under the repo-wide `false` workaround `cfc_star` fails to match and
the pull falls through to the non-unital calculus.
* Two deliberately degenerate `@[cfc_pull]` fixtures in `Failures.lean` are
tagged `nolint synTaut`, as LeanOA lints its whole library.
`LeanOA/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean`
is deleted: its four lemmas are now in mathlib's `RealImaginaryPart`, and the
duplicate declarations clashed once `Tags.lean` imported that file.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Give `PullM` a `MonadBacktrack` instance whose saved state pairs `Meta.SavedState` with the `State` of the run, so one checkpoint covers the metavariable assignments, the accumulated side goals and the predicate cache. This also reverts `postponed` and `zetaDeltaFVarIds`, which the hand-rolled `getMCtx`/`setMCtx` checkpoint leaked into the next candidate. Run every candidate attempt under a trace node headed by the lemma being tried. The trace becomes a tree that says which lemma caused which recursion, rather than a flat list of failures. A candidate that declines to apply is reported as a trace failure and not as an error, since that is the routine outcome of trying one. Since the node names the lemma, the messages raised while applying it no longer do; `collectHypotheses` thereby loses its only use of `declName`. For the same reason `synthesizeInstances` no longer re-wraps the exception from `synthAppInstances`; the wrapper itself stays, as what documents its arguments. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Ported from `cfc-pull-with-spec` (2a2d5a3, 7de9af2): the changes to `Attr.lean` and `Core.lean`, with the new examples added to `MathlibTest/CFCPull.lean`. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
There is probably some important thinking that needs to be done here to set the priorities appropriately. I'm not yet sure what is best.
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.
Currently, this PR contains lots of documentation written by Claude, which is unpleasant to read and overly verbose. I will distill this down to the important points soon, so don't read it if you don't want to yet.
cfc_pullrewrites an expression in a C⋆-algebra into an application ofcfcorcfcₙ. For a very basic example, given a scalar ringRand an elementa, it turnsstar a * aintocfc (fun x : R ↦ star x * x) a. If there is a continuous functional calculus for different scalar rings,cfc_pullcan be used to rewrite the expression into an application with a function in that scalar ring, e.g., by writingcfc_pull ℝ a. Likewise, it can rewrite using both the unital and non-unital functional calculi and convert between them, automatically preferring the unital one whenever an instance can be found, but allowing the user to specify.This is of course doable by hand, but each step must be its own
rw(so that the side goals are discharged by the autoparams). The example in the previous paragraph would berw [← cfc_id' R a, ← cfc_star, ← cfc_mul ..]. This can get quite cumbersome for large expressions, especially as things like← cfc_id' R amight rewrite more occurrences ofathan you actually intend if used in a different order. Moreover, the autoparams that discharge the hypotheses of these theorems are often redoing the same work repeatedly, like proving that the elementais selfadjoint or normal, or showing that a given function is continuous on some set.In contrast,
cfc_pullcollects these hypotheses as metavariables while traversing he expression and constructing the proof. These are then deduplicated and then the autoparams are attempted to discharge all these goals. The tactic succeeds if no side goals are generated. If some side goals remain, the tactic can either return only the unsolved goals, or else all the generated side goals.The most common application for
cfc_pullis showing that two elementsbandcof a C⋆-algebra are equal by writing each ascfc f aandcfc g a, and then proving thatf = gon the spectrum ofa. The step which turns the goalb = cintocfc f a = cfc g bis the purview ofcfc_pull. However, because this is fundamentally rewriting individual expressions, the tactic also features aconvmode, and usingconv at htherefore allows usingcfc_pullat hypotheses in context. The tactic offers special support for dealing with generated side goals withinconv.Lemmas are added to the database with the
@[cfc_pull]attribute, but can also be locally added or removed at the call site. The attribute automatically sorts lemmas into the various categories used by the tactic.🤖 Generated with Claude Code