Using a field of a structure in another field ?

Stream: lean4

[Sophie Morel]

The question is in the title: when defining a structure, can I use one of its fields to define another field, and if so how? I thought I saw some things like that in mathlib, but I can't find them anymore. More precisely, I am trying to define a LinearIsometryEquiv between two normed spaces E and F. So I write:

def MyBeautifulIsometry : E ≃ₗᵢ[𝕜] F where
  toFun := SomeExpression
  map_add' := proof
  map_smul' := proof
  invFun := SomeComplicatedExpression
  left_inv := proof
  right_inv := proof
  norm_map' := proof that uses the proof of left_inv

Is there a way to make the proof of norm_map' use the fact that I have already proved left_inv, or do I need to make a separate lemma ? The expression for invFun is a bit complicated, so I'd rather not repeat it unless necessary.

[Johan Commelin]

The easiest solution is probably to first define MyBeautifulEquiv.

[Sophie Morel]

Johan Commelin said:

The easiest solution is probably to first define MyBeautifulEquiv.

That's what I am currently doing, but then I ran into another problem. Now the definition of MyBeautifulIsometry looks like this:

def MyBeautifulIsometry : E ≃ₗᵢ[𝕜] F :=
  {MyBeautifulEquiv with
   norm_map' := proof that uses the proof of left_inv}

Then I wanted to put a @[simps!] before the definition of MyBeautifulIsometry to generate a bunch of useful lemmas, but the linter complains that some (not all) of them can be proved by simp. But if I remove the @[simps!], then simp is unable to prove some results later, and I have to manually unfold the definition of MyBeautifulIsometry. I am not sure what I should do, write out the lemmas myself? I don't know which lemmas @[simps!] creates, but there seems to be a lot of them.

[Ruben Van de Velde]

@[simps!?] prints the theorems it creates

[Ruben Van de Velde]

Did you also put @[simps] on MyBeautifulEquiv?

[Sophie Morel]

Ruben Van de Velde said:

@[simps!?] prints the theorems it creates

Ah, thanks !

[Sophie Morel]

Ruben Van de Velde said:

Did you also put @[simps] on MyBeautifulEquiv?

I did, was that the fatal mistake?

[Sophie Morel]

No it wasn't, I removed the @[simps] on MyBeautifulEquiv and the linter still complains for the same reason. It looks like I will have to generate those lemmas by hand. :-(

[Yaël Dillies]

Nono, you shouldn't have to. But you need to understand how initialize_simp_projections works and fiddle with it.

[Sophie Morel]

What I ended up doing was see the auto-generated lemmas thanks to @[simps!?], see that there were a bunch of them but they all said one of only two things (and not in the way I would like them to say it), extract the two statements, put them in a form I thought was better, make two lemmas out of them and @[simp] these lemmas. Now simp can still prove the later statements, and in one case it actually works better. Whew. Let's hope that CI is happy now.

[Sophie Morel]

I have no idea how to even start understanding how initialize_simp_projections works. Is there some doc about it that i should read?

[Filippo A. E. Nuccio]

A doc?! You dream... :night_sky: :rofl: My strategy is normally to find a maintainer to stalk until I undersand a bit more...

[Sophie Morel]

I like reading stuff by myself and taking time to understand...
I guess I'll just keep pestering people on Zulip instead.

[Matthew Ballard]

There is a fairly long doc string in Simps.Basic

[Filippo A. E. Nuccio]

Sophie Morel said:

I like reading stuff by myself and taking time to understand...
I guess I'll just keep pestering people on Zulip instead.

I also like this, that's why I called it a "dream"...

[Sophie Morel]

Matthew Ballard said:

There is a fairly long doc string in Simps.Basic

Thanks ! See, Filippo, sometimes it is useful to dream.

[Sophie Morel]

Matthew Ballard said:

There is a fairly long doc string in Simps.Basic

Thanks ! See, Filippo, sometimes it is useful to dream.

[Filippo A. E. Nuccio]

OK, then since we're here I have a question: the sentence "generate simplification lemmas for each projection of the instance" does it mean that if my class looks like

myclass (R :Type) [NiceClass R] where
 blabla

a [@simps] creates a sort of myclass.toNiceClasssimp lemma? Because I understand the doc insofar "projections" are concerned, but less so when it speaks about simp lemma for instances.

[Adam Topaz]

You could also git grep initialize_simps_projections in your local mathlib4 folder to see examples of its usage

[Sophie Morel]

So something really weird happened with the new version of my PR: I got rid of most of the @[simps!]-generated lemmas, but I still still had two, say one of them is lemma_1. Then a bit later I had a lemma_2, whose proof used lemma_1 (inside a simp). Once lemma_2 was known, then lemma_1 became provable by simp, but that would have been a circular proof as I was using lemma_1 to prove lemma_2. Well, the linter still complained that lemma_1 could be proved by a simp, and gave a suggested proof that used lemma_2. :exploding_head:

I solved it by erasing lemma_1 and writing a different proof of lemma_2, but still, I'm not sure why the linter would do that.

[Sophie Morel]

My latest lemma sacrifice has appeased the Mighty Linter! I have a sudden urge to find a church and go light a votive candle in it. :candle: :tada:

[Yaël Dillies]

I'm really sorry Lean is costing you so much in candles

[Sophie Morel]

It's nothing compared to the time I almost threw my computer out a window while trying to update mathlib; that would have been really expensive. Updating works so much better now.