Why does this rewrite fail

Stream: new members

[Mark Fischer]

I've been trying to come up with a better minimum working example, but since I don't understand the problem, it's a bit tough to replicate.

The following code fails at the indicated rewrite. Somehow I managed to use the "throw everything at the wall and see what sticks" approach to come up with a solution. So you can see that if I simp only [IndexList.length] at i before I try to rewrite, then I have a complete proof.

What I'm missing is why. Based on my limited understanding, simp at i should do the opposite, and make i no longer match the value in get_eq. What's happening?

(Sorry for the amount of code here)

import Mathlib

namespace Foo

structure IndexList {β : Type u} : Type u where
  l : List β
  idxs: Finset (Fin l.length)

@[simp]
def IndexList.length (l : @IndexList α) := l.idxs.card
def getElem (l : @IndexList α) (i : Fin l.length) : α := l.l[(l.idxs.sort LE.le)[i]]
def mem (a : α) (l : @IndexList α) : Prop := ∃i, getElem l i = a

theorem mem_finset_union_left {n : ℕ} (l r : Finset (Fin n)) (i : Fin l.card) : (l.sort LE.le)[i] ∈ (l ∪ r).sort LE.le := by
  simp only [Finset.mem_sort, Finset.mem_union]
  apply Or.inl ∘ (Finset.mem_sort LE.le).mp
  exact List.mem_iff_get.mpr ⟨⟨i, by
    simp only [Finset.length_sort, Fin.is_lt]
  ⟩, rfl⟩

theorem mem_indexlist_union_left (a : α) (l : List α) (is₁ is₂ : Finset (Fin l.length)) : mem a ⟨l, is₁⟩ → mem a ⟨l, is₁ ∪ is₂⟩ := by
  intro ⟨i, get_i_eq_a⟩
  have h₁ := mem_finset_union_left is₁ is₂ i
  have ⟨i', get_eq⟩ := List.mem_iff_get.mp h₁
  use ⟨i', by
    convert i'.isLt
    simp only [IndexList.length, Finset.length_sort]
  ⟩
  -- simp only [IndexList.length] at i -- Uncomment this to fix
  have h₂ : l.get (is₁.sort LE.le)[i] = a := get_i_eq_a
  rw [← get_eq] at h₂ -- This rw fails
  exact h₂

[Mark Fischer]

It seems to me like

have h₂ : l.get (is₁.sort LE.le)[i] = a := get_i_eq_a

is doing something mysterious. Somehow i is changed in a way I can't inspect via the infoview.

It feels like I should be able to finish the proof (or get close) with
convert get_i_eq_a

[Mark Fischer]

I can change the last few lines to

simp only [IndexList.length] at i
simp only [getElem] at get_i_eq_a
change l[(Finset.sort LE.le is₁)[i]] = a at get_i_eq_a
rw [← get_eq] at get_i_eq_a
exact get_i_eq_a

In the infoview, the change tactic shows no changes to get_i_eq_a's type (they're character for character identical), but without that line, the proof doesn't compile.

[Kyle Miller]

If you set set_option pp.explicit true, you can see that there are differences in h2. It appears that rw is not able to see through these differences when locating the expression.

Here are three options:

• Live with needing to unfold IndexList.length
• Change IndexList.length from a def to an abbrev, which makes it reducible and in this case makes the rw go through.
• Use erw instead of rw, which is more forceful with reduction when trying to find matches.

[Kyle Miller]

Another option is figuring out why you have this difference, and somehow getting get_eq to be in the correct form.

[Kyle Miller]

(The mystery in l.get (is₁.sort LE.le)[i] is that if you change the type of i it causes it to elaborate slightly differently; some implicit arguments get syntactically-different-yet-defeq values.)

[Mark Fischer]

Thanks for the help! :)

set_option pp.explicit true certainly does show me more, but suddenly it's so much.

Doing a quick diff on get_i_eq_a and h₂ shows they're different for sure. So at least it's no longer a mystery what the change tactic is doing. Though I feel like I came to this solution (change the type) almost by accident, so I'm not confident I could do so again.

It feels a bit undirected/magical/lucky that the change tactic should elaborate slightly differently in a way that happens to help. Probably the thing to do is to come back around to this when I have a bit more experience under my belt. :)