set tactic doesn't work with dependent functions

Stream: mathlib4

[Floris van Doorn]

The set tactic doesn't work well with dependent functions:

import Mathlib.Tactic.Set

example {ι : Type} {α : ι → Type} {i i' : ι} (h : α i = α i') (x : α i) (y : α i') :
    (cast h x, i) = (y, i) := by
  set j := i -- duplicates hypothesis `h` and `x` and doesn't replace i in the goal

The reason is that set internally uses rw, which is problematic. It would be much better to use dsimp.

However, I have also no idea how to use simp or dsimp to do this without duplicating hypotheses:

set_option trace.Meta.Tactic.simp true
example {ι : Type} {α : ι → Type} {i i' : ι} (h : α i = α i') (x : α i) (y : α i') :
    cast h x = y := by
  let j := i
  dsimp only [show i = j from rfl] at h -- dsimp made no progress
  simp only [show i = j from rfl] at h -- succeeds, but duplicates the hypothesis h.

simp duplicates hypotheses, and dsimp doesn't fire, presumably because it doesn't recognize show i = j from rfl as a rfl-proof.

[Kyle Miller]

Maybe this would be a good use of the un-merged refold_let tactic? #12745

[Floris van Doorn]

Ohh, that looks good. We should definitely use that to improve the set tactic.

[Floris van Doorn]

However, we need a version of refold_let that is willing to reorder hypotheses so that it can fold more lets.

[Kyle Miller]

Could you give an example of what this variation on refold_let should do to support set?

[Kyle Miller]

Maybe there needs to be a variant of let that defines something as early as possible?

[Floris van Doorn]

It should be able to handle the examples above, i.e. something like

example {ι : Type} {α : ι → Type} {i i' : ι} (h : α i = α i') (x : α i) (y : α i') :
    (cast h x, i) = (y, i) := by
  let j := i
  refold_let j at *

[Floris van Doorn]

@Kyle Miller I see that #12745 has been merged. It would be great if it were used in the set tactic!

[Floris van Doorn]

In the Carleson project there is an occurrence of the set tactic that takes >1 second to compile (because of the internal rws it's using). So I'm still hoping for this new set tactic :smile: