Generate ext_iff lemmas

Stream: lean4

[Kyle Miller]

(Original context: a request by Floris)

It still needs to be tested against mathlib, but here's a PR: lean4#4543

[Eric Wieser]

I'm curious to see if this does the right thing on all the "partially-applied ext lemmas" in mathlib

[Kim Morrison]

@Kyle Miller, I tried deleting the manual Fin.ext_iff, as this fails the build in stage2, but then of course stage1 won't build. We need an update-stage0 here, right? I think I'll wait to let you do that; I'd prefer not to update stage0 on others' PRs!

[Kyle Miller]

Here's a question: what should the binder types be for ext_iff lemmas? They are inconsistent in mathlib, and also we need to modify them because sometimes mathlib uses strict implicits in ext lemmas, which result in unusable ext_iff lemmas.

Two options:

Fin.ext_iff {n : Nat} {a b : Fin n} : a = b ↔ ↑a = ↑b

Fin.ext_iff {n : Nat} (a b : Fin n) : a = b ↔ ↑a = ↑b

It's fairly common to need to specify a and b, so the second one is seeming better to me.

[Kyle Miller]

I'm about 40% through mathlib now. Before I keep going, what do we think about these changes? https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-4543

[Notification Bot]

5 messages were moved here from #general > "Missing Tactics" list by Kyle Miller.

[Kim Morrison]

I only looked through about a quarter of that, but looks great.

[Eric Wieser]

Kyle Miller said:

Here's a question: what should the binder types be for ext_iff lemmas? They are inconsistent in mathlib, and also we need to modify them because sometimes mathlib uses strict implicits in ext lemmas, which result in unusable ext_iff lemmas.

Two options:

Fin.ext_iff {n : Nat} {a b : Fin n} : a = b ↔ ↑a = ↑b

Fin.ext_iff {n : Nat} (a b : Fin n) : a = b ↔ ↑a = ↑b

It's fairly common to need to specify a and b, so the second one is seeming better to me.

Is it that common? Skimming your patch to mathlib I think I only see the case where they are not specified

[Eric Wieser]

My guess is that the vast majority of uses are just "rewrite the whole goal", and so implicit would be fine (and match our general convention for argument explicitness of Iffs)

[Yaël Dillies]

Yeah, I have never heard of a rule saying that ext_iff lemmas were an exception to the "arguments to iff are implicit" rule

[Kim Morrison]

Is that rule written somewhere? I would like to start improving our documentation of rules for explicitness, but can't find much to start with!

[Yaël Dillies]

Uh, it's not in #style

[Ruben Van de Velde]

I think it's in Yaël's head :)

[Eric Wieser]

I think it's a collective hallucination, which if widespread enough should probably end up in #style

[Yaël Dillies]

I need to fetch croissants now, but I will explain the rules as I understand them later.

[Damiano Testa]

I also know about this: it is a difference between goals that are iff and goals that are eq, right?

[Kyle Miller]

Is it that common? Skimming your patch to mathlib I think I only see the case where they are not specified

The PR would only be touching places where they aren't specified and where making them explicit causes an issue, right? I don't have any metrics on what I didn't need to change, but earlier I had skimmed through uses of ext_iff lemmas in mathlib and saw that passing in one or both terms via keyword arguments wasn't rare.

[Kyle Miller]

Here are some considerations:

• The ext_iff generator for @[ext] placed on a structure makes the two arguments be explicit. I'm not sure if it's part of the interface that x and y are the names of these arguments, so relying on named arguments here is not great. (We can't just declare they're part of the interface: x or y might be names of parameters for the structure, and so these may be inaccessible.)
• We might want to leave this problem to the user and leave implicit/explicit alone for the ext_iff derived from a user @[ext] lemma, but like I said before, sometimes the "x" and "y" are strict implicit arguments here, making generated ext_iff unusable since the last arguments would be strict implicit.
  • We could decide to throw an error in this case. A source this problem is mathlib using the Injective theorem as the ext theorem, which we could say is not supported.
  • Or we could turn strict implicits into implicits.
  • However, in both these cases, we're allowing ext_iff lemmas to have inconsistent interfaces.
• The LHS of the ext_iff theorem has very little structure. My thought earlier was that if you are going to be using it, it's not unlikely that you would want to rewrite a particular equality that appears in your goal, and these being explicit doesn't hurt its use in rw or simp.
• Most changes I've needed to make are messing around with term proofs that might be too clever. Many of them are also just using the mp direction, which is a trivial theorem that requires absolutely no knowledge about the type — this direction is a sort of basic congruence lemma for some function that happens to appear in the ext lemma.
  • I would rather see the forward direction be given its own name, if it should exist at all. Many times I've found it can be replaced with a congr_arg.
  • I don't think the ext_iff theorem should care about being nice to use with .mp and .mpr since (1) I've already said what I don't like about the .mp direction and (2) the .mpr direction may as well use the ext lemma itself.

[François G. Dorais]

See also lean4#3643

[François G. Dorais]

There's lots of bugs with ext, it needs a major overhaul!

[François G. Dorais]

I think there should be a rule saying that ext_iff lemmas are an exception to the "arguments to iff are implicit" rule.

[Kyle Miller]

Here's the current status:

• Now lean4#4543 makes all the arguments implicit for ext_iff theorems. It also makes the generated ext theorem use implicit arguments for the equated terms — this is at the suggestion of François in issue lean4#3643, but also in practice it seems that mathlib doesn't use these arguments (lots of Foo.ext _ _ ...).
• The ext attribute now "realizes" the ext and ext_iff lemmas, meaning it creates them if they do not already exist. This helps get @[ext local] to work.
• I've built about 1400 mathlib files, with changes to about 90 (see the diff). It's merely tedious work, and there do not seem to be any issues so far. Sometimes you have to write @[ext (iff := false)] for user ext lemmas that have dependent hypotheses, which is not supported at the moment.
• I've set up the core Lean PR to build and work without a stage0 update and still work with one (at least locally — still waiting on CI), but after the stage0 update there are a few lines that would be good to clean up. They're marked with "TODO(kmill)" comments.

[Kyle Miller]

Adding @[scoped ext] on a structure isn't implemented. One could imagine it means adding the scoped ext attribute to the generated ext lemma, but the general attribute processing logic throws an error if it sees any scoped attribute applied to a top-level declaration.

[Eric Wieser]

Kyle Miller said:

• It also makes the generated ext theorem use implicit arguments for the equated terms — this is at the suggestion of François in issue #3643, but also in practice it seems that mathlib doesn't use these arguments (lots of Foo.ext _ _ ...).

I've often seen mathlib try to use ⦃⦄ arguments instead of {} for the equated terms: I think this is motivated by making it behave more like Function.Injective

[Eric Wieser]

Certainly mathlib is not consistent about this, and {} is already a nice improvement over ()

[Kyle Miller]

I was thinking it would be better to restate injective lemmas rather than "misuse" the ext lemma. Mathlib's also not very consistent about stating these injective lemmas.

Plus, sticking with {} here means that the lemma generator doesn't need special casing when there are no fields:

@[ext] structure Unit' where

#check Unit'.ext
/-
Unit'.ext {x y : Unit'} : x = y
-/

Maybe that would be better with explicit arguments, since there are no other arguments determining x and y by unification, but it's usable.

[Kyle Miller]

@Kim Morrison I was wondering if we might merge lean4#4543 before finishing fixing mathlib, given that there don't seem to be any surprises, and then I can finish fixing it on a next nightly-testing. Otherwise I'll keep plodding along.

[Kim Morrison]

Yes, no objections to merging. Tonight's nightly-testing will be broken by various changes I've made today (upstreaming some things, changing some List lemmas). So merging today will result in nightly-testing being a bit of a mess, but I'm game.

[Kim Morrison]

Most of my fixes will just come in from git merge lean-pr-testing-4678.