Working with primitive projections

Stream: lean4

[Mario Carneiro]

There seems to be a difference between .1 when produced by unification (via eta-for-structures) and .1 when written directly:

example (f : Fin n → Prop) (h : ∀ i h, i = 0 → f ⟨i, h⟩) : f i := by
  apply h
  -- ⊢ i.1 = 0
  fail_if_success rw [show i.1 = 0 from sorry]
  -- tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  --   i.val
  change i.1 = 0
  -- ⊢ i.val = 0
  rw [show i.1 = 0 from sorry] -- ok

[Leonardo de Moura]

Yes, "eta-for-structures" is using Expr.proj, and the "elaborator for i.<idx> is using the auto-generated projection functions (Fin.val in this case). rw uses keyed matching, and it thinks the key is Fin.val here.
BTW, simp [show i.1 = 0 from sorry]works as expected since it indexes after unfolding [reducible] constants.

[Leonardo de Moura]

There are multiple possible fixes here:

• Modify keyed matching
• Modify "eta-for-structures"
• Modify field access elaborator (and delaborator). This one will probably generate problems for the Mathlib port.

[Mario Carneiro]

My inclination is to hide the primitive projections when possible. That would mean changing eta-for-structures (in unification) to automatically hide the projections behind the definitions. Probably they can still appear sometimes, so rw might also need to be able to match through reducible definitions (which I believe is also what lean 3 rw does).

[Leonardo de Moura]

Note that rw matches through reducible definitions. The issue here is the head symbol only.

[Mario Carneiro]

Even if the head symbol is keyed after unfolding, won't it be a very uninformative key Expr.proj 1?

[Mario Carneiro]

like that could apply to any structure

[Leonardo de Moura]

The Expr.proj contains the structure name. We have been using this approach for simp, and it seems to be working well.

[Mario Carneiro]

I think we can also have a (mathlib4) tactic to re-fold all projections in the goal. My guess is that most tactics will choke on primitive projections because the assumption that expressions are mostly structured around Expr.const and Expr.app is widespread

[Leonardo de Moura]

Yes, this macro will probably be useful even if we modify the behavior of "eta-for-structurer" in the elaborator.

[Jeremy Salwen]

Does such a tactic now exist that re-folds projections?