ext tactic intros too few variables

Stream: mathlib4

[Eric Wieser]

Some weirdness in !4#2960; this works:

import Mathlib.Tactic.Basic

variable (m : Type u) (n : Type u') (α : Type v)
@[ext] structure SMatrix : Type max u u' v := (elem : m → n → α)

-- works
example (m : Type u) (n : Type u') (α : Type v) (M N : SMatrix m n α)
  (h : ∀ i j, M.elem i j = N.elem i j) : M = N :=
by
  ext i j
  exact h i j

but this doesn't

import Mathlib.Tactic.Basic


variable (m : Type u) (n : Type u') (α : Type v)
def Matrix : Type max u u' v := m → n → α

@[ext]
lemma Matrix.ext (M N : Matrix m n α)
  (h : ∀ i j, M i j = N i j) : M = N :=
by
  funext i j
  exact h i j

-- doesn't work
example (m : Type u) (n : Type u') (α : Type v) (M N : Matrix m n α)
  (h : ∀ i j, M i j = N i j) : M = N :=
by
  ext i j  -- `j` wasn't introd!
  exact h i j

[Eric Wieser]

Presumably ext is getting confused because Matrix is defeq to the type of functions

[Eric Wieser]

But it feels like a bug, since even on functions it would intro both variable!

[Jon Eugster]

This is merely a hack, but it might illustrate well what's wrong with ext: If you change the ext-Lemma so that it only
introduces one variable then it works fine:

import Mathlib.Tactic.Basic

variable (m : Type u) (n : Type u') (α : Type v)
def Matrix : Type max u u' v := m → n → α

@[ext]
theorem Matrix.ext' (M N : Matrix m n α) (h : ∀ i, M i = N i) : M = N := by
  funext i j
  rw [h i]

-- does work!
example (m : Type u) (n : Type u') (α : Type v) (M N : Matrix m n α)
  (h : ∀ i j, M i j = N i j) : M = N :=
by
  ext i j  -- now `j` is introduced as well
  exact h i j

[Jon Eugster]

I think what's happening is the following:

1. Using Matrix.ext the tactic turns M = N into ∀ i j, M i j = N i j
2. In TryIntros (see source, Std/Tactic/Ext.lean, l.116-119) in the case | p::ps => it only introduces the first variable and then tries to apply the next ext-lemma to ∀ j, M i j = N i j which fails as that's not an equality. (note: p is the first name and ps is the list of all further names, [j] in this case.)

I'm not quite confident enough to fix this myself, but I'd hope with that any meta-programmer would be able to help :fingers_crossed:

[Eric Wieser]

I think it's more complicated than that, because it works fine above for SMatrix, the structure

[Eric Wieser]

So it's something to do with the fact that Matrix is being confused for a function type somewhere within ext

[Jon Eugster]

That is probably true. I still think the above might not quite be the expected behaviour of ext. The following fails as well because the bad_ext_lemma introducing two variables at once takes priority over the correct ext-Lemma for functions:

import Mathlib.Tactic.Basic

@[ext 1001]
lemma bad_ext_lemma (f g : A → B → C) (h : ∀ i j, f i j = g i j) : f = g := by
  ext i j
  exact h i j

-- fails
example (f g : A → B → C) (h : ∀ i j, f i j = g i j) : f = g := by
  ext i j -- fails to introduce `j` if priority of the `bad_ext_lemma` is `> 1000`.
  exact h i j

-- works
example (f g : A → B → C) (h : ∀ i j, f i j = g i j) : f = g := by
  ext -- but it works if the variables are not given names
  exact h _ _

[Jon Eugster]

I realised my suggestion would be a quite simple change: std4#111 . We can discuss over there if it makes sense at all or not.

[Eric Wieser]

I think the isForall test might be to blame

[Eric Wieser]

And that its misfiring on matrices

[Eric Wieser]

I'm not convinced that allowing custom ext lemmas on functions is really sensible