make simp use variable names instead of expanding structures

Stream: lean4

[Robert Maxton]

It seems quite often that I find myself working with structures with quite a lot of internal data -- most particularly things like LinearMap or RingHom with half-a-dozen fields, each of which is likely to have their own complexity or in some cases contain their own copy of similarly dense fields. Whenever possible, I would very much like to give such structures a short, abbreviated name, and then have Lean (most particularly simp and aesop) use those names instead of the expanded structures, expanding only as necessary or directed.

[Robert Maxton]

What's the best way to do this? Or am I fundamentally making a mistake in how I work with these structures in the first place?

[Alex J. Best]

Can you give an example of the sort of thing you want to do? I'm not sure I understand what you mean by you want to give a structure a shorter name

[Robert Maxton]

Well, for example, I'm currently trying to prove that RingCat has all finite coproducts. In the process, I'm working with the value

f: ↑L →ₗ[ℤ] ↑R →ₗ[ℤ] ↑cocone.pt := {
  toAddHom :=
    {
      toFun := fun x =>
        {
          toAddHom :=
            { toFun := fun y => fL x * fR y,
              map_add' :=
                (_ :
                  ∀ (r₁ r₂ : ↑R),
                    (fun y => fL x * fR y) (r₁ + r₂) = (fun y => fL x * fR y) r₁ + (fun y => fL x * fR y) r₂) },
          map_smul' :=
            (_ :
              ∀ (n : ℤ) (y : ↑R),
                { toFun := fun y => fL x * fR y,
                        map_add' :=
                          (_ :
                            ∀ (r₁ r₂ : ↑R),
                              (fun y => fL x * fR y) (r₁ + r₂) =
                                (fun y => fL x * fR y) r₁ + (fun y => fL x * fR y) r₂) }.toFun
                    (n • y) =
                  (RingHom.id ℤ) n •
                    { toFun := fun y => fL x * fR y,
                          map_add' :=
                            (_ :
                              ∀ (r₁ r₂ : ↑R),
                                (fun y => fL x * fR y) (r₁ + r₂) =
                                  (fun y => fL x * fR y) r₁ + (fun y => fL x * fR y) r₂) }.toFun
                      y) },
      map_add' :=... },
  map_smul' :=... }

and on and on and on; the whole thing is 19k characters. When this value comes up in my goal, simp and dsimp will tend to replace occurrences of f with the entire absurdly long definition; I can sometimes fix this with congr and the like, but not always (when the structure occurs under binders, usually). eta_reduce doesn't seem to fix the problem. I would like to designate certain definitions, within a proof, as simp-norm, basically, so that unless I override the default it uses f instead of {<19k characters >}.

[Eric Wieser]

set_option pp.proofs.withType false will make that a lot shorter

[Eric Wieser]

Using (LinearMap.mul _ _).compl₁₂ fL fR as the entirw expression would make it ever shorter

[Robert Maxton]

Eric Wieser said:

set_option pp.proofs.withType false will make that a lot shorter

Ooh, very nice! Thanks!
Eric Wieser said:

Using (LinearMap.mul _ _).compl₁₂ fL fR as the entirw expression would make it ever shorter

Also very nice, I should've looked through LinearMap more carefully first!
(It actually ended up being (LinearMap.mul _ _).compl₁₂ ⟨fL, by simp⟩ ⟨fR, by simp⟩, but close enough)