automate ring hom props

Stream: mathlib4

[Kenny Lau]

Kenny Lau said:

here's the real one-line proof using typeclass:

theorem isStableUnderBaseChange' : IsStableUnderBaseChange Flat :=
  .auto respectsIso

(full code)

[Kenny Lau]

so, this has been sitting in the other chat for a few days now, do people want this?

[Christian Merten]

Sorry for my slow response time, I was on vacation and am slowly catching up again. Your recent PRs #28225 and #28238 were already good improvements, so the proofs are now nice and readable. Thanks for that!
Therefore, I don't think we need any more machinery right now to automate the RingHom.Property files. The number of such proofs is low and is not expected to grow significantly. We can (and should) of course revisit if this changes.

What I would be in favour of though, would be to extend algebraize to also replace tagged RingHom properties with Algebra properties in the goal (i.e. if the goal is RingHom.Flat f, algebraize [f] would turn the goal into Module.Flat R S, possibly with an option algebraize -goal to turn this behaviour of). This would require some refactoring of algebraize though.

[Kenny Lau]

@Christian Merten that would naturally require algebraize to store the iff lemmas, which opens us up to the possibility of also automating that part; is it a good idea to only automate the iff lemmas and nothing more?

[Christian Merten]

Yes, I think letting a @[algebraize +mk_iff] attribute also add the iff lemma (there is precedent in the form of @[mk_iff]) would be reasonable, but mostly orthogonal to my above proposal.
The blocking point for the above is that currently algebraize can only store one "constructor lemma" per property, because we tag the Algebra property and give it the lemma name as an argument. I have discussed this with @Edward van de Meent before (who is on vacation this week): Probably we should change the tagging to happen on the lemmas instead of on the property. This way we can tag multiple lemmas and for algebraize to rewrite in hypothesis and goal, it would need either one iff lemma or two implications.

[Kenny Lau]

well can we store both?

[Christian Merten]

Yes we could, but tagging the lemmas instead of the property would be more extensible.
An alternative would be to only replace f by algebraMap R S and let simp do the replacement (this would require us to tag RingHom.flat_algebraMap with simp.

[Kenny Lau]

I am in favour of more custom tactics instead of relying on simp

[Kenny Lau]

/-- A ring homomorphism `f : R →+* S` is flat if `S` is flat as an `R` module. -/
def RingHom.Flat {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) : Prop :=
  letI : Algebra R S := f.toAlgebra
  Module.Flat R S

@[algebraize]
lemma RingHom.flat_algebraMap_iff {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] :
    (algebraMap R S).Flat ↔ Module.Flat R S := by
  rw [RingHom.Flat, toAlgebra_algebraMap]

@Christian Merten to make sure I understand correctly, the above code is your current proposal, is that correct?

[Christian Merten]

Yes, but we should still be able to tag more lemmas.
But still, put this way it really starts looking like we should just have a algebraize simp set that algebraize can invoke after replacing f by algebraMap R S.

[Christian Merten]

Of course your proposed @[algebraize +mk_iff] can not be done by simp.

[Kenny Lau]

Christian Merten said:

Yes, but we should still be able to tag more lemmas.
But still, put this way it really starts looking like we should just have a algebraize simp set that algebraize can invoke after replacing f by algebraMap R S.

well i'm not sure that simp is really the right thing here, e.g. i don't think the scalar tower can be simp either

[Christian Merten]

Yes, I agree. I am not saying we don't need algebraize, I am just saying that (parts of) the property translation can be done by a custom simp set that algebraize invokes after creating the Algebra and IsScalarTower instances.

[Yaël Dillies]

Christian Merten said:

extend algebraize to also replace tagged RingHom properties with Algebra properties in the goal (i.e. if the goal is RingHom.Flat f, algebraize [f] would turn the goal into Module.Flat R S, possibly with an option algebraize -goal to turn this behaviour of).

Whatever you do, could you please make sure it's consistent with simp acting on the goal, simp at h acting on h, simp at h ⊢ acting on h and the goal, simp at * acting everywhere?

[Kenny Lau]

@Yaël Dillies Heather currently has a PR to make this part smoother