Spelling of Subtype.val in LinearIndependent

Stream: mathlib4

[Peter Nelson]

In Mathlib.Data.LinearAlgebra.LinearIndependent, many lemmas are hard to read in the infoview/docs because they use Subtype.val without the domain showing up. For example, in this one, the hypothesis and conclusion look exactly the same.

theorem LinearIndependent.insert {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V]
[Module K V] {s : Set V} {x : V} (hs : LinearIndependent K fun b => ↑b)
 (hx : x ∉ Submodule.span K s) :
LinearIndependent K fun b => ↑b := sorry

It occurs to be that this could be solved using Set.restrict, so in the lemma above, we would have the (defeq)
hs : LinearIndependent K (s.restrict id)
and the conclusion would be
LinearIndependent K ((insert x s).restrict id)
That way it is much clearer what the lemma is saying. A similar thing could be used for composing an arbitrary f with Subtype.val (which also happens in the API), using
example (f : α → β) (s : Set α) : f ∘ ((↑) : s → α) = s.restrict f := rfl

Would it make sense to do this? I was worried that for the identity case, there might be a problem with simp normal form, but it turns out there is no simp lemma for s.restrict id = Subtype.val

[Johan Commelin]

I think this is a sensible idea. How about the following: whenever the subtype is of the form "set s coerced to a type" then s.restrict is probably a better choice then Subtype.val. Of course for types such as PNat or NNReal that are defined directly as subtype, this option is not available.

(Tangent: I don't really like the name s.restrict. I think s.incl or something like that might be better. Of course Set.inclusion already exists, and turns s \subset t into a map between the two respective subtypes.)

[Peter Nelson]

Yes, I've always thought f.restrict s would even be a better name that s.restrict f

[Johan Commelin]

Yes, that would make sense!

[Johan Commelin]

Back in the day, we couldn't use dot-notation on functions. But now that we can, we should probably rename it to Function.restrict!

[Johan Commelin]

And maybe make s.incl an abbreviation for Subtype.val and/or Function.restrict id s.

[Eric Wieser]

To be clear, this is only a problem in the docs not the source: docs#LinearIndependent.insert

[Eric Wieser]

I thought lean 4 was supposed to have "fixed" pretty printing so that things round-tripped and this ambiguity wouldn't be present?

[Mario Carneiro]

yeah that... didn't ship

[Mario Carneiro]

there is pp.analyze but it's not really maintained

[Eric Wieser]

I assume docs#Lean.pp.analyze won't lead me to any documentation... (Edit: it does!)

[Peter Nelson]

It seems like there's a problem with dot notation, because s.restrict f is defined for dependent functions.

import Mathlib.Data.Set.Basic

variable {π : α → Type _}

def Function.restrict (f : ∀ a : α, π a) (s : Set α) : ∀ a : s, π a := fun x => f x

theorem restrict_eq (f : α → β) (s : Set α) : Function.restrict f s = f ∘ Subtype.val := rfl
-- works

theorem restrict_eq' (f : α → β) (s : Set α) : f.restrict s = f ∘ Subtype.val := rfl
/-
fails:
application type mismatch
  @restrict ?m.472 f
argument
  f
has type
  α → β : Type (max u_1 u_2)
but is expected to have type
  ?m.472 → Type ?u.466 : Type (max ?u.465 (?u.466 + 1))
-/

Is there a way around this?

[Peter Nelson]

What about a symbol for restriction?

import Mathlib.Data.Set.Basic

variable {π : α → Type _}

def Function.restrict (f : ∀ a : α, π a) (s : Set α) : ∀ a : s, π a := fun x => f x

infix:99 " ↾ " => Function.restrict

theorem restrict_eq (f : α → β) (s : Set α) : f ↾ s = f ∘ Subtype.val := rfl

[Peter Nelson]

there is a minor annoyance there, unlike dot notation, it looks like you have to write (f ↾ s) x rather than
f ↾ s x for application, since there is no precedence for the infix that makes it work.

[Peter Nelson]

#8107

[Kyle Miller]

This dependent function problem is a known issue lean4#1629

[Eric Wieser]

Instead of introducing a new definition or restating all our lemmas, should we just make the ι argument to LinearIndependent explicit?

[Peter Nelson]

That feels like it would be more unwieldy in the general case of linear independence of actual indexed tuples, rather than sets.

What is the problem with the solution in the PR? It is really just changing spellings rather than restating lemmas. This was a bit of work, but the PR does it. It also introduces a standard for something that was previously ad hoc (currently different spellings are used in different files, which causes annoyances when rewriting).

[Eric Wieser]

Peter Nelson said:

That feels like it would be more unwieldy in the general case of linear independence of actual indexed tuples, rather than sets.

At worst the cost is a single _ at each use, isn't it? That seems less bad than having to unfold id and restrict all the time

[Peter Nelson]

Having to explicitly specify the ring (which mathematically is clear from context the majority of the time) is already a slight pain with LinearIndependent terms; this would just be yet another little thing.

I don't know how frequently the unfolding for sets will actually need to happen, since so much of the LinearIndependent api deals directly with sets anyway. While making the changes for the PR, it seems that the simplifier (plus restrict_eq) could do what was needed easily in every case.

[Eric Wieser]

Peter Nelson said:

Having to explicitly specify the ring (which mathematically is clear from context the majority of the time) is already a slight pain with LinearIndependent terms; this would just be yet another little thing.

This is not the same situation though; if you omit the ring and write a _, lean can never work it out. If you omit the index, lean can almost always work it out

[Peter Nelson]

Yes, there is no way around the explicit ring. But it is still just a little annoyance that comes with every single use of LinearIndependent. The extra underscore would be another, and the need for it can be avoided by a spelling change. Having to sometimes use the simplifier to unfold things seems less bad.

[Eric Wieser]

Here's an alternate approach:

import Mathlib.LinearAlgebra.LinearIndependent

open Qq Lean PrettyPrinter.Delaborator SubExpr in
@[delab app.LinearIndependent]
def delabLinearIndependent : Delab := do
  let e ← getExpr
  -- it would be really nice to use `~q()` here
  guard <| e.isAppOfArity ``LinearIndependent 7
  let f ← withNaryFn delabAppFn
  let ι ← withNaryArg 0 delab
  let R ← withNaryArg 1 delab
  let v ← withNaryArg 3 delab
  let ιe ← Meta.whnf (e.getArg! 0)
  -- check that `ιe` is a subtype with set membership
  let #[_, .lam _ _ body _] := ιe.getAppArgs | failure
  guard <| body.isAppOf ``Membership.mem
  let #[_, _, inst, .bvar 0, _] := body.getAppArgs | failure
  guard <| inst.isAppOfArity ``Set.instMembershipSet 1
  -- use the binder if we have it
  if let `(fun $x:ident => $body) := v then
    let v ← withNaryArg 3 (`(fun $x : $ι => $body) >>= annotateCurPos)
    `($f $R $v)
  else
    `($f ($(mkIdent `ι) := $ι) $R $v)

-- shows `LinearIndependent K fun b : ↑(insert x s) => ↑b`
#check LinearIndependent.insert
-- unchanged
#check LinearIndependent.fin_cons

[Eric Wieser]

The nice thing about this solution is that it solves a pretty-printing-only problem with a pretty-printing-only solution

[Peter Nelson]

what am I doing wrong? (added these lines at the end of the same code)

variable {V R : Type _} [Field R] [AddCommGroup V] [Module R V] {s : Set V}

example (hs : LinearIndependent R (Subtype.val : s → V)) : False := by
  -- infoview shows
  -- hs : LinearIndependent✝ R Subtype.val
  sorry

[Eric Wieser]

Ah, now you've hit upon something nasty; the difference between Set.Elem and Subtype! I'll attempt a fix

[Peter Nelson]

oh, I see that it works if I write fun (x : s) ↦ (x : V) instead. But that kind of thing is quite hard to read when terms become complicated.

[Peter Nelson]

I am actually still quite a fan of @Johan Commelin 's Set.incl. It is much more readable for a mathematician than Subtype.val, and this is true even in contexts that have nothing to do with linear independence.

[Eric Wieser]

Edited above

[Eric Wieser]

The infoview now shows hs: LinearIndependent✝ (ι✝ := { x // x ∈ s }) R Subtype.val. Maybe @Kyle Miller can tell me how to make those tombstones go away fixed using mkIdent

[Damiano Testa]

Is

set_option hygiene false in

Too radical?

[Peter Nelson]

Eric Wieser said:

The infoview now shows hs: LinearIndependent✝ (ι✝ := { x // x ∈ s }) R Subtype.val. Maybe Kyle Miller can tell me how to make those tombstones go away

Ok, I see that this is workable. But there is still a lot of DTT cruft in there; it takes someone from the initiated to recognize that the s is the important thing in the above.

There is a lot of stuff appearing in the infoview in the linear algebra API that is quite hard to read for this sort of reason - I've really dived into it for the first time in recent weeks, and it's been an adjustment getting past all the overhead. It would be good to see a solution that minimizes such things.

[Eric Wieser]

Ok, I see that this is workable. But there is still a lot of DTT cruft in there; it takes someone from the initiated to recognize that the s is the important thing in the above.

Yes, but this is a feature; you accidentally created the DTT cruft by passing Subtype.val in

[Peter Nelson]

So what is the preferred way to do it?

[Eric Wieser]

For that specific example you can set ι manually

example (hs : LinearIndependent (ι := s) R (Subtype.val : s → V)) : False := by
  -- infoview shows
  -- hs : LinearIndependent (ι := ↑s) R Subtype.val
  sorry

[Eric Wieser]

Or the solution you already found, which is what mathlib has been using:

example (hs : LinearIndependent R (fun x : s ↦ x.1)) : False := by
  -- infoview shows
  -- hs : LinearIndependent R fun x : ↑s => ↑x
  sorry

[Damiano Testa]

There is also docs#Lean.MVarId.renameInaccessibleFVars, but I'm on mobile and I'm not sure that it is what you want.

[Eric Wieser]

@Damiano Testa, I think I solved the tombstones now, but thatnks!

[Eric Wieser]

It's annoying that { x // x ∈ s } and s are different things; we could solve this by deleting docs#Set.Elem from core, and adding a custom elaborator to use ↥s as notation for { x // x ∈ s }

[Eric Wieser]

Oh, it's not even in core!

[Kyle Miller]

I wonder if there's anything interesting we could do with, for example, dot notation API by preserving Set.Elem.

What is the concrete problem with there being this reducible Set.Elem wrapper? The docstring is indicating that norm_cast needs it.

[Eric Wieser]

Mainly just that if we have Set.Elem, then the goal view should probably show the difference between when it's there and when it's not (otherwise norm_num will appear to fail randomly); and only one of those two spellings can be called ↥s.

[Eric Wieser]

I wonder if the norm_num comment is still true

[Peter Nelson]

Eric Wieser said:

Or the solution you already found, which is what mathlib has been using:

example (hs : LinearIndependent R (fun x : s ↦ x.1)) : False := by
  -- infoview shows
  -- hs : LinearIndependent R fun x : ↑s => ↑x
  sorry

I would even say the fun notation and coercions appearing in the infoview is not ideal if it can be avoided (which it can).

What is there would still look cryptic to a curious mathematician.

[Eric Wieser]

Eric Wieser said:

I wonder if the norm_num comment is still true

I tested it, and it was; norm_num has a somewhat arbitrary list of functions that it is allowed to apply to (specifically, things that are explicitly tagged as coercions)

[Eric Wieser]

@Kyle Miller, would you be in favor of me PRing the delaborator above?

[Peter Nelson]

Can we still have s.incl?

[Eric Wieser]

I worry slightly that having two ways to spell the same thing is setting ourselves up for more pain

[Eric Wieser]

abbrev and @[simp] theorem Set.incl_apply (s : Set α) (x : s) : Set.incl s x = x := rfl make that less true, but might cause problems elsewhere

[Kyle Miller]

@Eric Wieser I'd suggest doing something like this:

/-- If `e` is a coercion of a set to a type, return the set.
Succeeds either for `Set.Elem s` terms or `{x // x ∈ s}` subtype terms. -/
def Lean.Expr.coeTypeSet? (e : Expr) : Option Expr := do
  if e.isAppOfArity ``Set.Elem 2 then
    return e.appArg!
  else if e.isAppOfArity ``Subtype 2 then
    let .lam _ _ body _ := e.appArg! | failure
    guard <| body.isAppOfArity ``Membership.mem 5
    let #[_, _, inst, .bvar 0, s] := body.getAppArgs | failure
    guard <| inst.isAppOfArity ``Set.instMembershipSet 1
    return s
  else
    failure

open Lean PrettyPrinter.Delaborator SubExpr in
@[delab app.LinearIndependent]
def delabLinearIndependent : Delab := whenPPOption getPPNotation do
  let e ← getExpr
  guard <| e.isAppOfArity ``LinearIndependent 7
  let some _ := (e.getArg! 0).coeTypeSet? | failure
  let f ← withNaryFn delabAppFn
  let ι ← withNaryArg 0 delab
  let R ← withNaryArg 1 delab
  if (e.getArg! 3).isLambda then
    let v ← withNaryArg 3 do
      let enableFunBinder (subExpr : SubExpr) :=
        let expr := subExpr.expr
        let expr := mkAppN (expr.getAppFn.setOption pp.funBinderTypes.name true) expr.getAppArgs
        { subExpr with expr }
      withTheReader SubExpr enableFunBinder delab
    `($f $R $v)
  else
    let v ← withNaryArg 3 delab
    `($f ($(mkIdent `ι) := $ι) $R $v)

-- shows `LinearIndependent K fun (b : ↑(insert x s)) ↦ ↑b`
#check LinearIndependent.insert
-- unchanged, shows `LinearIndependent K (Fin.cons x v)`
#check LinearIndependent.fin_cons

variable (s : Set Nat)
-- shows `LinearIndependent ?m.20493 fun (x : ↑s) ↦ ↑x`
#check LinearIndependent _ fun (x : s) ↦ (x : Nat)
-- shows `LinearIndependent ?m.20842 fun (x : { x // x ∈ s }) ↦ ↑x`
#check LinearIndependent _ fun (x : {x // x ∈ s}) ↦ (x : Nat)
-- shows `LinearIndependent (ι := { x // x ∈ s }) ?m.21215 Subtype.val`
#check LinearIndependent _ (Subtype.val : s → _)

[Kyle Miller]

(I'm just assuming it's a good idea to pretty print it this way. I only thought about how to organize the code.)

[Eric Wieser]

Other than wanting to use Qq for Lean.Expr.coeTypeSet?, I agree that looks nicer!

[Eric Wieser]

My question for you was more "is this type of thing a good excuse to use a custom delaborator?". I guess it's all just a hack for pp.analyze not working well enough to be the default, but maybe that's fine

[Kyle Miller]

If we do whnf, I'd want it to be reducible transparency. I removed that and did matching by hand, hoping that the terms would be OK

[Kyle Miller]

My understanding is that pp.analyze works by inserting these sorts of pp options into a term (though in a globally accessible table rather than into the term itself). We're kind of doing that here, but there's not a good way to say "ok, I'm done, now delaborate from here" since it'll just be indirectly calling itself again, so it's responsible for finishing up the delaboration itself. Maybe it could explicitly set a pp option on the term that turns itself off.

[Peter Nelson]

Eric Wieser said:

I worry slightly that having two ways to spell the same thing is setting ourselves up for more pain

Note that my PR uses abbrev.

I think it's such a boon for readability to talk about 'the inclusion map from s' rather than using fun notation. Defining incl is in the same spirit as having s.restrict and Set.inclusion, which already happily exist in mathlib.

[Kyle Miller]

@Eric Wieser This strategy, of making a custom analysis pass, does work.

/-- If `e` is a coercion of a set to a type, return the set.
Succeeds either for `Set.Elem s` terms or `{x // x ∈ s}` subtype terms. -/
def Lean.Expr.coeTypeSet? (e : Expr) : Option Expr := do
  if e.isAppOfArity ``Set.Elem 2 then
    return e.appArg!
  else if e.isAppOfArity ``Subtype 2 then
    let .lam _ _ body _ := e.appArg! | failure
    guard <| body.isAppOfArity ``Membership.mem 5
    let #[_, _, inst, .bvar 0, s] := body.getAppArgs | failure
    guard <| inst.isAppOfArity ``Set.instMembershipSet 1
    return s
  else
    failure

def Lean.PrettyPrinter.Delaborator.OptionsPerPos.setBool (opts : OptionsPerPos)
    (p : SubExpr.Pos) (n : Name) (v : Bool) : OptionsPerPos :=
  let e := opts.findD p {} |>.setBool n v
  opts.insert p e

open Lean PrettyPrinter.Delaborator SubExpr in
@[delab app.LinearIndependent]
def delabLinearIndependent : Delab :=
  whenPPOption getPPNotation <|
  whenNotPPOption getPPAnalysisSkip <|
  withOptionAtCurrPos `pp.analysis.skip true do
    let e ← getExpr
    guard <| e.isAppOfArity ``LinearIndependent 7
    let some _ := (e.getArg! 0).coeTypeSet? | failure
    let optionsPerPos ← if (e.getArg! 3).isLambda then
      withNaryArg 3 do return (← read).optionsPerPos.setBool (← getPos) pp.funBinderTypes.name true
    else
      withNaryArg 0 do return (← read).optionsPerPos.setBool (← getPos) `pp.analysis.namedArg true
    withTheReader Context ({· with optionsPerPos}) delab

[Peter Nelson]

What is the status on the pp stuff here? I can see that the docs have changed, but they are still not readable : for example, the statement of the following lemma would need a mouseover to understand.

theorem LinearIndependent.insert {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V]
 [Module K V] {s : Set V} {x : V} (hs : LinearIndependent K fun b => ↑b) (hx : x ∉ Submodule.span K s) :
LinearIndependent K fun b => ↑b

[Eric Wieser]

I think neither Kyle nor I have opened a PR with the above; so I'm surprised if the docs have changed!

[Peter Nelson]

Oops! I misremembered seeing the equally unhelpful Subtype.val there. That might have been in the pretty-printer.

[Kyle Miller]

Here @Peter Nelson: #8602

[Eric Wieser]

insert now reads:

theorem LinearIndependent.insert
    {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V]
    {s : Set V} {x : V} (hs : LinearIndependent K fun (b : ↑s) => ↑b) (hx : x ∉ Submodule.span K s) :
    LinearIndependent K fun (b : ↑(insert x s)) => ↑b

which I think is a big improvement

[Eric Wieser]

It's a bit unfortunate that fun looks like a regular variable name in the docs