!4#3484, Analysis.Seminorm

Stream: mathlib4

[Jeremy Tan]

(deleted)

[Jeremy Tan]

!4#3484 Most of the remaining errors in this file stem from the comp declaration at line 302:

/-- Composition of a seminorm with a linear map is a seminorm. -/
def comp (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) : Seminorm 𝕜 E :=
  { p.toAddGroupSeminorm.comp f.toAddMonoidHom with
    toFun := fun x => p (f x)
    smul' := fun _ _ => by rw [map_smulₛₗ, map_smul_eq_mul, RingHomIsometric.is_iso] }
#align seminorm.comp Seminorm.comp

If I could make this definition compile without making another error at [IsScalarTower R ℝ≥0 ℝ] (L299) I'd cut the error count by about half

[Jeremy Tan]

Note that I haven't committed any s yet

[Scott Morrison]

I've done a bunch of work on !4#3484, dealing with most but not quite all of the errors. If anyone would like to take another look that would be great. This is the highest priority file for now!

[Thomas Murrills]

I was taking a look just out of curiosity and noted this terrible way to get comp_smul to typecheck:

theorem comp_smul (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) (c : 𝕜₂) :
    (set_option synthInstance.etaExperiment true in p.comp (c • f)) = ‖c‖₊ • p.comp f :=
  ext fun _ => by
    rw [comp_apply, smul_apply, LinearMap.smul_apply, map_smul_eq_mul, NNReal.smul_def, coe_nnnorm,
      smul_eq_mul, comp_apply]

I'd assume this is a last resort. (Note: set_option at least doesn't appear in the type of the lemma when used later on.) What do you do when the lhs needs eta experiment but the rhs needs to not have eta experiment?

[Eric Wieser]

Often "needs to not have eta experiment" is just "needs a higher heartbeat limit with eta experiment than without"

[Thomas Murrills]

Hmm, that does work eventually...but I will note that in this case upping the heartbeats causes the declaration to take 116 seconds instead of 6 seconds :woozy_face:

[Thomas Murrills]

Hesitantly offering

/-- Elaborate the following term with `set_option synthInstance.etaExperiment true`. -/
macro "eta% " a:term : term => `(term|set_option synthInstance.etaExperiment true in $a)

for legibility and speedups during this eta era. But, I don't know if that ~2 minutes is actually fine and negligible, or if there's another, better way to fix this lemma

[Patrick Massot]

I think we can't stay with a declaration taking two minutes, especially when the proof is two lines long.

[Scott Morrison]

I'm game to use eta%, perhaps renamed to etaExperiment% so it's a big easier to track / more obviously a hack. :-)

[Thomas Murrills]

Ok, sounds good! (I think snake case is the standard for elaborators, so I guess it ought to be eta_experiment%!) What's a good location to put the macro in?

[Thomas Murrills]

Different issue: I took a look at the remaining error and fixed it, but it's weird: I needed to force Subtype.val to be used as the coercion instead of .toAddGroupSeminorm. Or, at least, that's what I think is happening.

...
          refine' csupᵢ_le fun i =>
            ((i : Seminorm 𝕜 E).add_le' x y).trans <| add_le_add
              -- Porting note: `f` is provided to force `Subtype.val` to appear.
              -- A type ascription on `_` would have also worked, but would have been more verbose.
              (le_csupᵢ (f := fun i => (Subtype.val i : Seminorm 𝕜 E).toFun x) ⟨q x, _⟩ i)
              (le_csupᵢ (f := fun i => (Subtype.val i : Seminorm 𝕜 E).toFun y) ⟨q y, _⟩ i)
...

Removing Subtype.val produces the following error message

application type mismatch
  add_le_add (le_csupᵢ (Exists.intro (q x) ?m.711983) ↑i)
argument
  le_csupᵢ (Exists.intro (q x) ?m.711983) ↑i
has type
  AddGroupSeminorm.toFun (↑i).toAddGroupSeminorm x ≤ ⨆ i, AddGroupSeminorm.toFun i.toAddGroupSeminorm x : Prop
but is expected to have type
  AddGroupSeminorm.toFun (↑i).toAddGroupSeminorm x ≤ ⨆ i, ↑↑i x : Prop

Removing f altogether causes lean to struggle to unify the type (?m.711950 i ≤ supᵢ ?m.711950 : Prop).

Is the above an acceptable fix? Or is there an obvious better way to do this?

[Thomas Murrills]

Ok, I pushed since I'm going to sleep soonish and I know this is a high-prio file; that should fix all the errors, unless something's weird with my setup (it might be). if any choices I made were suboptimal, we can always change them :)

[Thomas Murrills]

I put the eta_experiment% macro in Mathlib/Lean/Meta.lean, where it's imported by most things. (synthInstance.etaExperiment was registered in Lean.Meta.SynthInstance, but I didn't think we should make a whole file for just this macro—especially because Mathlib's Lean.Meta file is a grab-bag of Meta utilities, unlike Lean's version of that file.)

[Thomas Murrills]

(Well, couldn't sleep.) Huh, that's really weird. The file does just fine in my VS code, but fails under lake build (both in CI and locally). The Lean version is the same according to #eval Lean.versionString...what could be going on?

[Thomas Murrills]

Whoa, this is weird. Writing set_option synthInstance.etaExperiment false in before the first offending declaration (smul_le_smul) causes it to error the same way lake does—but omitting that shows no errors. Can anyone reproduce?

[Thomas Murrills]

(Note that #eval show MetaM Bool from do return synthInstance.etaExperiment.get (← getOptions) evaluated the line just before returns false, so it's definitely not true—and turning eta on instead causes worse errors.)

[Thomas Murrills]

Interestingly, setting other options to either true or false (such as pp.explicit) also causes the (correct?) lake-like erroring behavior. Setting them at the top of the file works too. But other commands, like #check or #eval, don't.

[Thomas Murrills]

Anyway, the actual problem here seems to be something like "HSMul can't find the return type, even when it's provided as a type ascription"—I'm not sure what to do about that.

[Thomas Murrills]

Wow, if the return type of smul_le_smul is anything less than

(HSMul.hSMul (γ := Seminorm 𝕜 E) a p : Seminorm 𝕜 E) ≤ b • q

then HSMul can't find its return type in time, giving the error failed to synthesize HSMul ℝ≥0 (Seminorm 𝕜 E) ?m.454788 (deterministic) timeout at 'typeclass'.... Both means of specifying the output type need to be there...but I don't quite understand why there's a metavariable in the first place when we supply the argument directly? Does this have to do with outParam shenanigans somehow?

[Thomas Murrills]

MWE, sufficiently far down in the file:

#synth HSMul ℝ≥0 (Seminorm 𝕜 E) (Seminorm 𝕜 E)
-- failed to synthesize HSMul ℝ≥0 (Seminorm 𝕜 E) ?m.202055 (deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)

Huh?? The argument is right there! Why is it a metavariable?

[Mario Carneiro]

probably because it is an out param

[Thomas Murrills]

But why doesn't it get unified with what is there?

[Mario Carneiro]

the typeclass problem is solved without it

[Mario Carneiro]

it appears to have timed out before returning

[Thomas Murrills]

Weird! Isn't that a lot of heartbeats to figure out what you "already know", so to speak...?

[Mario Carneiro]

it's not trying to figure out the out param, it's trying to figure out the instance to get there

[Thomas Murrills]

Oh, I see—which I could see making sense if you didn't want to venture on a long unification search. But I feel like an exception should be made when the info is "immediate" somehow, lest this happen...ofc I have no idea what this entails, tho.

[Mario Carneiro]

I'm saying that the value of the out param doesn't help much to find the instance, and it can get in the way sometimes so it is temporarily replaced by a metavariable

[Mario Carneiro]

the real question is why the instance problem HSMul ℝ≥0 (Seminorm 𝕜 E) ?_ isn't being solved

[Thomas Murrills]

ahh ok

[Thomas Murrills]

Anyway, I'm pretty sure that accounts for the last two errors in the file. I'll leave the decision of whether to increase max heartbeats, make everything explicit as above, or figure out the underlying problem to others—I'm heading to sleep :)

[Thomas Murrills]

(Also, that "invisible error" issue above all this maybe deserves a separate thread if anyone can reproduce it (if relevant, I'm on macOS ventura)—not seeing errors that are actually there is quite jarring)

[Scott Morrison]

This instance problem HSMul ℝ≥0 (Seminorm 𝕜 E) ?_ is in fact solved, it just needs slightly beyond the 20000 heartbeat limit.

[Scott Morrison]

Okay, I have this building, and given this file is on the critical path and has been for a long while, I think I would like to merge. We still have some signs of sickness here, that we should keep thinking about.

The worst one, with a double porting note, is:

-- Porting note: unhappily, turning on `synthInstance.etaExperiment` isn't enough here:
-- we need to elaborate a fragment of the type using `eta_experiment%`, but then can't use it for the proof!
-- Porting note:
-- finding the instance `SMul ℝ≥0 (Seminorm 𝕜 E)` is slow,
-- and needs an increase to `synthInstance.maxHeartbeats`.
set_option synthInstance.maxHeartbeats 30000 in
theorem comp_smul (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) (c : 𝕜₂) :
    p.comp (eta_experiment% c • f) = ‖c‖₊ • p.comp f :=
  ext fun _ => by
    rw [comp_apply, smul_apply, LinearMap.smul_apply, map_smul_eq_mul, NNReal.smul_def, coe_nnnorm,
      smul_eq_mul, comp_apply]

[Jeremy Tan]

It passes CI now. Since (the apparently now correct) coe_smul is not needed in the rest of the file, should I revert the last changes I made that replaced coe_smul with rfl?

[Scott Morrison]

I don't think there's any need to revert. It's not like the rfls you added are expensive.

[Scott Morrison]

I've hit merge.