pushing casts into structures

Stream: lean4

[James Gallicchio]

for a i : Fin n, if you cast with h : n = m, the cast can be pushed into the structure like so:

theorem push_cast (a : Fin n) (h : n = m) : h ▸ a = ⟨a.1, h ▸ a.2⟩ :=
  by cases h; simp

is there a better way to deal with this sort of situation? marking this lemma simp solved my particular problem but I'm not sure if I'm totally off base.

[James Gallicchio]

I'm trying to reduce the number of suffices ... I write :laughing:

[Kyle Miller]

I find it's usually better to avoid explicit rewrites like this and instead develop API for rewriting type arguments in a more controlled way. In this case, there's already docs4#Fin.cast

[Kyle Miller]

The fact Fin.cast gives an order isomorphism complicates things a bit, but it also unlocks further simplification opportunities.

[James Gallicchio]

Yeah. I'm working in Std right now so I will need to move the Fin.cast infrastructure up to Std (this is fine).

[James Gallicchio]

oh, actually, it is not fine, since Fin.cast is an order isomorphism. hm

[James Gallicchio]

I don't think we're trying to move all of that infrastructure up to Std yet. @Mario Carneiro thoughts? maybe something akin to push_cast (but not @[simp]) is a reasonable addition to Std.

[Mario Carneiro]

Fin.cast can be a function

[James Gallicchio]

and then rename the mathlib isomorphism?

[Mario Carneiro]

once upon a time it was a function, but people started upgrading functions to equivs because it is notationally almost invisible, although this is less true in lean 4 than in lean 3

[Mario Carneiro]

it's only used as a function most of the time, IMO it was the wrong call to make it the default

[Kyle Miller]

Adding to this, I'd suggest that we rename mathlib's Fin.cast to say Fin.castIso or Fin.castEquiv, keep the API surrounding it, and add a lemma that Fin.cast n h = Fin.castEquiv n h. There are places where you do want the equivalence version.

[James Gallicchio]

I probably can't do the refactor today, so if someone is feeling like doing a little refactor feel free :) otherwise I'll work on it tomorrow.