refactor(Computability): make PFun a one-field structure

[AlexeyMilovanov]

This PR refactors PFun from def PFun α β := α → Part β to a structure with a FunLike instance.

Discussion

Main changes

• Redefine PFun as a structure with one field, toFun : α → Part β.
• Add the FunLike (α →. β) α (Part β) instance and configure simps projections.
• Add the projection and application simp lemmas required by the structure wrapper.
• Add fun x ↦. ... notation for partial-function literals.
• Adapt downstream equality proofs to use PFun.ext or DFunLike.ext where
  funext no longer applies directly.
• Remove 33 local backward.isDefEq.respectTransparency false workarounds that
  are no longer needed after the refactor.

Downstream impact

The refactor mainly impacts Computability Theory and Category Theory (Category/PartialFun.lean). Since PFun is no longer definitionally equal to α → Part β, tactics such as rfl, simp, and funext can no longer always see through the old raw-function representation.

Note on LLM usage

The core PFun change caused numerous downstream errors. I initially used an LLM to help draft fixes for these files. Afterwards, I spent a significant amount of time manually correcting and modifying all of the generated changes.

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary 371cb47e8f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ coe_mk
+ instance : FunLike (α →. β) α (Part β)
+ mk_apply
+ mk_coe
+ partialFunEquivPointed_inverse_map_Dom
+ partialFunEquivPointed_inverse_map_get_coe
+ toFun_eq_coe
+ unpaired_part
+ unpaired_part'
+++ id
+++--- some
-+-+ comp
-+-+-+ none

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 371cb47).

• +26 new declarations
• −2 removed declarations

+Nat.Partrec.id
+PFun.casesOn
+PFun.coe_mk
+PFun.ctorIdx
+PFun.instFunLikePart
+PFun.mk
+PFun.mk.inj
+PFun.mk.injEq
+PFun.mk.noConfusion
+PFun.mk.sizeOf_spec
+PFun.mk_apply
+PFun.mk_coe
+PFun.noConfusion
+PFun.noConfusionType
+PFun.rec
+PFun.recOn
+PFun.toFun
+PFun.toFun_eq_coe
+Partrec.id
+Partrec₂.unpaired_part
+Partrec₂.unpaired_part'
-Pointed.Iso.mk.congr_simp
+RecursiveIn.id
-Turing.ToPartrec.Code.eval.eq_def
+partialFunEquivPointed_inverse_map_apply_Dom
+partialFunEquivPointed_inverse_map_apply_get_coe
+«term_Fun_:_↦._»
+«term_Fun_↦._»

---

Decrease in strong tech debt: (relative, absolute) = (13.57, 0.01)

Current number	Change	Type (strong)
backward.isDefEq.respectTransparency	4744	-32
backward.isDefEq.respectTransparency.types	2465	-4

No changes to weak technical debt.

Current commit 371cb47e8f
Reference commit 5315eef9e4

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-bors]

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

[YaelDillies]

Can you make sure that (fun x \mapsto f x : PFun _ _) gets replaced by (fun x \mapsto. f x : PFun _ _) everywhere? The latter is the simp normal form (or at least I hope it is?)

Sorry, I meant (\u(fun x \mapsto f x) : PFun _ _) to be clear, where the coercion is that of total function to partial functions.

[YaelDillies]

Can you please get the hang of resolving the comments you've satisfactorily addressed and removing awaiting-author once you've resolved or replied to every outstanding comment?

[AlexeyMilovanov]

-awaiting-author

[YaelDillies]

Thanks!

maintainer delegate

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[jcommelin]

!radar

[leanprover-radar]

Benchmark results for 8492528 against fa6385b are in. No significant results found. @jcommelin

• ✅ build//instructions: -67.0G (-0.05%)

Medium changes (1🟥)

• 🟥 build/module/Mathlib.Computability.Partrec//instructions: +4.1G (+15.75%)

Small changes (2✅, 4🟥)

• ✅ build/module/Mathlib.CategoryTheory.Category.PartialFun//instructions: -1.1G (-12.79%)
• 🟥 build/module/Mathlib.Computability.Ackermann//instructions: +410.2M (+2.47%)
• 🟥 build/module/Mathlib.Computability.PartrecCode//instructions: +1.8G (+3.16%)
• 🟥 build/module/Mathlib.Computability.RE//instructions: +896.7M (+9.28%)
• 🟥 build/module/Mathlib.Computability.TuringMachine.Config//instructions: +1.2G (+5.05%)
• ✅ build/module/Mathlib.NumberTheory.NumberField.FinitePlaces//instructions: -88.0M (-1.89%)

[jcommelin]

Thanks for your PR!

I think I understand the motivation for this PR: using fun_prop in computability proofs. Do you have particular examples of this to demonstrate that the PR works? Because as it stands, this patch mostly seems to be making proofs a bit longer, instead of shorter.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[AlexeyMilovanov]

!bench

[leanprover-radar]

Benchmark results for bed3641 against 5315eef are in. No significant results found. @AlexeyMilovanov

• 🟥 build//instructions: +15.7G (+0.01%)

Small changes (2✅, 1🟥)

• ✅ build/module/Mathlib.CategoryTheory.Category.PartialFun//instructions: -1.2G (-14.39%)
• ✅ build/module/Mathlib.Computability.Ackermann//instructions: -487.8M (-2.97%)
• 🟥 build/module/Mathlib.Computability.TuringMachine.Config//instructions: +1.2G (+5.18%)

[AlexeyMilovanov]

!radar

[leanprover-radar]

Benchmark results for 371cb47 against 5315eef are in. No significant results found. @AlexeyMilovanov

• 🟥 build//instructions: +5.8G (+0.00%)

Small changes (2✅, 2🟥)

• 🟥 build/module/Aesop.Frontend.Extension//instructions: +26.7M (+0.96%)
• ✅ build/module/Mathlib.CategoryTheory.Category.PartialFun//instructions: -1.2G (-14.10%)
• ✅ build/module/Mathlib.Computability.Ackermann//instructions: -494.8M (-3.01%)
• 🟥 build/module/Mathlib.Computability.TuringMachine.Config//instructions: +1.2G (+5.13%)