[Merged by Bors] - chore: unsimp Set.coe_setOf

[plp127]

See #mathlib4 > `Set.coe_setOf` @ 💬

---

[github-actions]

PR summary c02dada2cf

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

No declarations were harmed in the making of this PR! 🐙

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 c02dada).

• +0 new declarations
• −0 removed declarations

No declaration differences.

---

Increase in strong tech debt: (relative, absolute) = (0.45, 0.00)

Current number	Change	Type (strong)
502	1	erw
4515	-1	backward.defeqAttrib.useBackward
5675	-4	backward.isDefEq.respectTransparency

No changes to weak technical debt.

Current commit c02dada2cf
Reference commit aaedc74a09

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.sh 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-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.

[TwoFX]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Test and lint
• ci (staging) / Post-CI job
• ci (staging) / Lint style
• ci (staging) / Post-Build Step
• ci (staging) / Build

[YaelDillies]

I am very worried about this PR. There are plenty of lemmas about the coercion of a set to a type, and now we will need to duplicate each of them to have both a version for sets and a version for predicates. See #41223. This issue is widespread enough that I suggest we revert this PR.

[TwoFX]

Reading through the Zulip thread again more closely, I guess there wasn't really consensus that unsimping the lemma is a good idea. Personally, I think the diff in this PR is an overall improvement, and I think it is inconsistent that coe_setOf is simp but coe_eq_subtype is not, but oh well... ping me on the revert PR and I'll bors it @YaelDillies

[plp127]

I am very worried about this PR. There are plenty of lemmas about the coercion of a set to a type, and now we will need to duplicate each of them to have both a version for sets and a version for predicates. See #41223. This issue is widespread enough that I suggest we revert this PR.

Why do we need such a duplication? The lemma Set.coe_setOf still exists, it's just not @[simp] anymore, so you can still use it to rewrite things. The issue with being @[simp] is that it changes the types of things to something that's not defeq at reducible-and-instances transparency, which you don't want happening automatically.

[YaelDillies]

As you say, in an ideal world one shouldn't be rewriting with the current Set.coe_setOf because it changes types at semireducible transparency. The solution IMO however isn't to unsimp it (after all, one could still stumble upon the LHS of Set.coe_setOf and in the ideal world there is no way to get rid of it) but instead to make it defeq at reducible-and-instances transparency. Have you tried doing that?

[plp127]

to make it defeq at reducible-and-instances transparency. Have you tried doing that?

The only solution I can think of for this is to make Set a one-field structure. Indeed I have not tried doing this yet.

[YaelDillies]

Why does this have anything to do with Set being a one-field structure? Mind enlightening me?

[plp127]

Why does this have anything to do with Set being a one-field structure? Mind enlightening me?

When s is a set, ↥s is reducibly defeq to { x // x ∈ s }. So the lhs of Set.coe_setOf is { x // x ∈ {x | p x} }, and the rhs is { x // p x }. The issue is then making Set.mem_setOf defeq at lower transparency (currently it only works at default transparency). The reason this doesn't happen now is because Set.Mem and setOf are defs, and so won't be unfolded when checking Set.Mem (setOf p) a = p a. However, we also don't want Set α = α → Prop leaking out. So the solution I came up with is to make Set a one-field structure, which lets us have the eta rule at reducible transparency without confusing Set α with α → Prop.

[YaelDillies]

I got this far myself, except for the fact that making it a one-field structure is the only remedy. Is the forbidden defeq for Set really going to leak out if we increase the transparency of the "translation functions" Set.Mem and setOf from semireducible to instance_reducible? After all, this only affects TC search. Is the issue somehow that the only way to make foo (bar x) reduce to x without foo nor bar themselves reducing is to make them the constructor/destructor of a one-field structure?

[plp127]

If you have another solution I'd love to hear it!

[YaelDillies]

Okay, let's fix it: #41506