controlling how ext introduces variables

Stream: new members

[Paul Nelson]

With the following code, ext v introduces two goals, one with v : V₁, the other with v : V₂. Is there a simple way to get it to introduce just one goal, with v : (V₁ × V₂)?

import Mathlib

example
  (R : Type) [Ring R]
  (V₁ : Type) [AddCommGroup V₁] [Module R V₁]
  (V₂ : Type) [AddCommGroup V₂] [Module R V₂]
  (f : (V₁ × V₂) →ₗ[R] R)
  : f = f := by
  ext v
  sorry

[Ruben Van de Velde]

  -- ext picks
  -- refine LinearMap.prod_ext ?hl ?hr
  refine LinearMap.ext fun v => ?_

[Paul Nelson]

thanks

[Kyle Miller]

The canonical way is ext1 v

[Kyle Miller]

std4#525 adjusts the docstrings of these tactics so that you can find ext1 from ext

[Paul Nelson]

import Mathlib

example
  (R : Type) [Ring R]
  (V₁ : Type) [AddCommGroup V₁] [Module R V₁]
  (V₂ : Type) [AddCommGroup V₂] [Module R V₂]
  (f : (V₁ × V₂) →ₗ[R] R)
  : f = f := by
  ext1 v -- tactic 'introN' failed, insufficient number of binders
  sorry

[Kyle Miller]

Huh, I should have tested it. Maybe you need multiple ext1s. There's also ext v : 2 I believe for limiting the iterations (to two in this example). I'm on my phone, so haven't tested these.

[Paul Nelson]

ext v : 2 behaves like ext v here (and ext v : 1 gives an error)

[Ruben Van de Velde]

It's not about iterations

[Ruben Van de Velde]

It's prod_ext being an ext lemma

[Kyle Miller]

How do you mean? Isn't the point that in iteration one ext applies LinearMap.ext and then in iteration two it applies prod_ext?

[Ruben Van de Velde]

No, prod_ext applies in the first iteration

[Kyle Miller]

Oh, you mean LinearMap.prod_ext, not Prod.ext

[Kyle Miller]

This seems like a bad @[ext] lemma... I would have never expected the very first step of ext with a linear map to create two goals.

[Ruben Van de Velde]

Perhaps so, yeah

[Eric Wieser]

It's a very useful ext lemma for when equating terms of the form (A ⊗ B) × C →ₗ D

[Eric Wieser]

As without it you can't apply the tensor product ext

[Eric Wieser]

Perhaps we should have ext (simple := true) or something that bypasses these more unusual ext lemmas

[Kyle Miller]

It makes sense as an ext lemma, but a reason I worry about this as an @[ext] lemma is that it conditionally applies different ext lemmas depending on the domain. My own expectation is that ext sees that it's a linear map and then applies the standard linear map ext lemma.

Extending your idea @Eric Wieser, maybe there should be "ext sets" kind of like simp sets, or maybe specialized ext lemmas for different circumstances. It seems to me that LinearMap.prod_ext lives in a categorical world, where you "evaluate" by pre-composing with other morphisms, and in particular you wouldn't necessarily apply the pointwise ext lemma. Or maybe you would as a last resort, since you're precomposing with an arbitrary linear map from the ground field.

[Paul Nelson]

Ruben Van de Velde said:

  -- ext picks
  -- refine LinearMap.prod_ext ?hl ?hr
  refine LinearMap.ext fun v => ?_

Is there a way to get Lean to report which ext lemma is being used by ext?

[Eric Wieser]

show_term ext

[Paul Nelson]

oh wow, that looks super useful (more broadly). thanks