Force visibility of certain proof terms

Stream: lean4

[Alex Meiburg]

There are some functions where there's a Prop-type argument, and it should pretty much always be shown by the pretty printer by default. For instance, if I have two positive semidefinite matrices A and B (and the proofs that they are, are hA and hB), and now I'm talking about the expression sqrt A + sqrt B, I will actually have things in my goal of the form Matrix.PosSemidef.add (Matrix.PosSemidef.sqrt hA) (Matrix.PosSemidef.sqrt hB). More succinctly, the "expression" is really hA.sqrt.add hB.sqrt. But this gets pretty-printed as ⋯.add ⋯.

This is a problem with pretty much all of the IsHermitian and PosSemidef API: the expressions you're working with, you don't see the expressions, you just see the proofs, and if you want to keep a useful infoview you need to write a really oddly structured proof.

I guess I'd hope that one of two things would be possible:

• Mark the hA and hB arguments in Matrix.PosSemidef.add as "display in the pretty printer by default". Ideally this would act like pp.proofs.withType but just for that one argument.
• Some sort of custom delaborator, so that it renders as just (sqrt A + sqrt B).PSD or something similar. I know approximately zero about delaborators so I don't even know if this is the right kind of question.

[Alex Meiburg]

Here's an illustration of the kind of problem I mean:

import Mathlib.LinearAlgebra.Matrix.PosDef

open Classical
variable {n : Type*} [Fintype n]

theorem Matrix.IsHermitian.smul_real (c : ℝ) {A : Matrix n n ℝ} (hA : A.IsHermitian) : (c • A).IsHermitian := by
  sorry

/-- Claim: each eigenvalue of (A+B)/2 is at most than the average of the largest eigenvalues of A and B. -/
theorem eigenvalue_mixing {A B : Matrix n n ℝ} (hA : A.PosSemidef) (hB : B.PosSemidef) :
    ∀ i, ((hA.1.smul_real (1/2)).add (hB.1.smul_real (1/2))).eigenvalues i ≤
    (⨆ j, hA.1.eigenvalues j)/2 + (⨆ j, hB.1.eigenvalues j)/2
     := by
  sorry

That goal now renders as

∀ (i : n), ⋯.eigenvalues i ≤ (⨆ j, ⋯.eigenvalues j) / 2 + (⨆ j, ⋯.eigenvalues j) / 2

which is pretty useless to read!

[Patrick Massot]

The question is legitimate, but I’m surprised the API doesn’t define those functions on all matrices (with junk values in irrelevant cases).

[Patrick Massot]

I would really expect to see A.eigenvalues i here, defined as 0 when it doesn’t make sense.

[Alex Meiburg]

Yeah. It does make me really appreciate why e.g. x / y doesn't require a proof that y ≠ 0. (Besides the pretty-printing, it makes doing rewrites much more annoying, because there is a constant bunch of proof terms that are equal, but still creates blockages.)

[Jireh Loreaux]

Patrick Massot said:

The question is legitimate, but I’m surprised the API doesn’t define those functions on all matrices (with junk values in irrelevant cases).

I've used this API a bit. I didn't find it too painful, but I also didn't do terribly much with it. Certainly it would be a pain if you need to rewrite A.