v4.3.0-rc2 - comp_def and #8023

Stream: mathlib4

[Eric Wieser]

Are you happy for me to try this with the comp_def PR above to make the rest easier to review, or is that just going to create lots more work for you?

[Scott Morrison]

Sure!

[Eric Wieser]

Done in #8367

[Yaël Dillies]

Out of curiosity, why is unfolding Function.comp not an option anymore?

[Eric Wieser]

because the equation lemma is now for (f \comp g) x = f (g x)

[Scott Morrison]

Hmm, many conflicts with #8366. Could you do the merge into #8366 and resolve?

[Eric Wieser]

That would require me to first merge master into nightly-testing-2023-11-06

[Eric Wieser]

Which presumably you'll need to do anyway?

[Eric Wieser]

Yaël Dillies said:

Out of curiosity, why is unfolding Function.comp not an option anymore?

Yes, maybe we should just use @[eqns] on comp so that unfolding it "just works"

[Scott Morrison]

No, I wasn't planning on ever merging master into nightly-testing-YYYY-MM-DD. Others are welcome to. :-)

[Eric Wieser]

Oh sorry, I misread the PR number you pasted; indeed, that's not necessary

[Scott Morrison]

@[eqns] on comp is a reasonable thing to consider, but I think it would best for it to happen in Lean, so it isn't going to happen immediately.

[Eric Wieser]

Scott Morrison said:

Hmm, many conflicts with #8366. Could you do the merge into #8366 and resolve?

git merge eric-wieser/with-comp_defs -s ours leaves no conflicts and creates no diff

[Eric Wieser]

Though perhaps a manual resolution would indeed be better

[Scott Morrison]

Interesting. A plain merge had lots of conflicts, but I didn't look at them at all.

[Yaël Dillies]

Eric Wieser said:

because the equation lemma is now for (f ∘ g) x = f (g x)

Hmm, that's a bit sad that unfolding doesn't mean the same thing anymore. What motivated this change?

[Eric Wieser]

It's not unfold that changed meaning I don't think, it's simp [Function.comp]

[Eric Wieser]

Would you prefer the @[eqns] approach?

[Eric Wieser]

Arguably with function.comp, you almost always just want to directly unfold it, rather than unfold the applied version

[Yaël Dillies]

Yes, the @[eqns] approach sounds more principled given that we already have Function.comp_apply as a simp lemma and indeed usually want to get rid of unapplied ∘.

[Eric Wieser]

I think I should be able to reuse most of my work in #8367, and just use the commit I cherry-picked as a reversion commit

[Yaël Dillies]

Eric Wieser said:

It's not unfold that changed meaning I don't think, it's simp [Function.comp]

And what motivated the change to simp?

[Eric Wieser]

The fact that it's not always the right thing to completely unfold a definition given to it; that's not what it did in Lean 3

[Eric Wieser]

lean4#2042 was the issue I opened requesting this

[Yaël Dillies]

Ah, but the fix is not solving exactly what you asked for!

[Yaël Dillies]

I agree with your motivation: Tagging foo with @[simp] should make simp simplify applied instances of foo.
However I believe that giving foo to a simp call should unfold foo, whether it's applied or not.

[Eric Wieser]

Having attribute [simp] foo not match simp [foo] sounds like a bad idea to me

[Yaël Dillies]

In other words, I wanted a change of behavior to what equation lemmas are tagged with simp when doing @[simp] def foo, not what equation lemmas are included in a simp call when doing simp [foo].

[Yaël Dillies]

I'm happy to make this a job for @[simps] if you want instead.

[Yaël Dillies]

But certainly if I write simp [foo], I want all foos to be gone from my goal!

[Eric Wieser]

Eric Wieser said:

Would you prefer the @[eqns] approach?

I pushed a pair of commits to #8023 with this change

[Eric Wieser]

Yaël Dillies said:

But certainly if I write simp [foo], I want all foos to be gone from my goal!

Even if that means turning them into a match?

[Notification Bot]

32 messages were moved here from #mathlib4 > v4.3.0-rc2 by Eric Wieser.

[Yaël Dillies]

Yes, otherwise I would have given simp the foo_apply lemma.

[Eric Wieser]

Ah, but this is only true if foo_apply exists!

[Eric Wieser]

So I think it's up to you to use eqns to change the meaning of simp [foo] if you want to manually write foo_apply.

[Yaël Dillies]

No I still believe this is a bad default.

[Yaël Dillies]

simp [foo] should mean the same as unfold foo, namely remove all instances of foo.

[Eric Wieser]

This might be a bad time to express that opinion... are you happy with the @[eqns] compromise for the sake of this release?

[Yaël Dillies]

Sure, but I'm afraid we'll have to revert whatever Leo did to fix your issue and ask for what we actually wanted instead.

[Eric Wieser]

Can you add a more RFC-style comment to the lean4 issue explaining why you dislike the current fix?

[Eric Wieser]

Eric Wieser said:

Eric Wieser said:

Would you prefer the @[eqns] approach?

I pushed a pair of commits to #8023 with this change

@[eqns] doesn't work for dsimp :(

[Scott Morrison]

I'm skeptical of making such a change using @[eqns] in Mathlib to such basic functions, and think if we want to do this we should put the @[eqns] in Lean or Std.

[Scott Morrison]

I would like us to make the minimal changes now, so that Mathlib can stay on release candidates, and then work out what changes we want from Lean.

[Eric Wieser]

If we measure in terms of diff size, the eqns solution is far more minimal

[Scott Morrison]

That is certainly true.

[Eric Wieser]

I suspect that in the short term the eqns thing being inconsistent between Std and Mathlib is not really going to cause any major issue

[Eric Wieser]

But I agree it would be nice to upstream it one or two steps

[Scott Morrison]

Okay.

[Eric Wieser]

The @[eqns] attribute itself certainly makes more sense in Std

[Scott Morrison]

I'm happy with @[eqns] then. It would be nice to hear @Mario Carneiro's opinion on this.

[Eric Wieser]

I think Yael's remarks above can maybe be interpreted as a vote for the simp [!def] proposal you originally made, but it's not fully clear to me what behavior they want.

[Eric Wieser]

I think if we did end up deciding @[eqns] was a bad idea, it would be easy enough to delete those two lines and restore the comp_applys via a cherry-pick; so I think it's harmless to let #8371 merge

[Scott Morrison]

Yes, I think the !def option is pretty good. I worry about the complexity it will add in processing simp args.

[Eric Wieser]

It sounds like we'd need it for rw too, though maybe that counts as a "simp arg"

[Kyle Miller]

I haven't looked at the changes to Lean -- would it make any sense to be able to set the arity when lean generates equation lemmas? Or maybe there could be a command to regenerate them with a specific arity? I suppose even with this, you'd still sometimes want to simp [!def] to eliminate a definition.

[Eric Wieser]

The suggestion I made somewhere on github was def foo : Nat -> Nat -> Nat := fun x => unfold_to_here% fun y => x + y

[Eric Wieser]

Which is a little more visible than the surprising behavior in lean3 of caring where the colon was.

[Mario Carneiro]

I'd be fine with @[eqns] on comp in std if needed to mitigate migration issues (I think we would have to upstream @[eqns] first though)

[Mario Carneiro]

I don't think that "we already have comp_apply" is a good argument for not having simp [comp] do the same thing; the reason we write those apply lemmas in the first place is because simp [foo] wasn't doing what we want!

[Mario Carneiro]

I'm also not sure it is true that we always want to unfold unapplied f \circ g

[Mario Carneiro]

(f \circ g) x is much more clearly a simp lemma

[Mario Carneiro]

we should have a lemma to be applied manually for unfolding f \circ g though

[Mario Carneiro]

which I guess is comp_def

[Eric Wieser]

Yes, really the question is, given we have both comp_def and @[simp] comp_apply, what should rw [comp] / rw [(· ∘ ·)] mean?

[Eric Wieser]

The behavior matrix for what a bare comp means is:

	v4.3.0-rc1	v4.3.0-rc2
No @[eqns]	comp_apply if that matches, else comp_def	comp_apply
@[eqns]	comp_def	comp_def

[Yaël Dillies]

Mario Carneiro said:

I'm also not sure it is true that we always want to unfold unapplied f ∘ g

Yes, that's never what I claimed. I claimed that if I write simp [comp] that means I want comp to be gone.

[Eric Wieser]

That's not what it meant in Lean3, is it?

[Yaël Dillies]

Well, that's what it did, right?

[Eric Wieser]

For comp yes, but not for declarations in general

[Eric Wieser]

In lean 3 it unfolded to the colon

[Scott Morrison]

Mario Carneiro said:

I'd be fine with @[eqns] on comp in std if needed to mitigate migration issues (I think we would have to upstream @[eqns] first though)

@[eqns] has been hanging out on the PR queue for two months: #245. :-)

[Kyle Miller]

std#245