Idiomatic way to compute things on types

Stream: lean4

[Jihoon Hyun]

There are cases where I should compute on definition of types, like {n : Nat} -> Fin (2 * n). In such cases when n is given some value, for example n = 0, Fin (2 * 0) is not considered the same as Fin 0. What is the most idiomatic way to deal with this?

[Aaron Liu]

Fin (2 * 0) is considered the same as Fin 0

[Kyle Miller]

docs#Fin.cast is usually what you would insert, when it's necessary

[Kenny Lau]

so usually you will have some sort of cast functions for types that look like F x

[Kenny Lau]

where x is a term that is not a type

[Kyle Miller]

(Sometimes there are other functions for casting when types are involved, like List has docs#List.map)

[Jihoon Hyun]

Kyle Miller 말함:

docs#Fin.cast is usually what you would insert, when it's necessary

Yes, I would insert X.cast in such scenarios for any reasonable X, but...

Aaron Liu 말함:

Fin (2 * 0) is considered the same as Fin 0

Then why does lean fail to convert from Fin (2 * 0) to Fin 0 in place? This makes some confusion when looking at the infoview.

[Robin Arnez]

Hmm I'm not sure where exactly you have errors but:

example (x : Fin (2 * 0)) : Fin 0 := x

works. If it's part of a function application this might be different though show Fin 0 from x (where x : Fin (2 * 0)) should still work then

[Kyle Miller]

Fin (2 * 0) and Fin 0 are definitionally equal, but that doesn't mean that Lean will reduce the types in the Infoview.

In this case you could use dsimp at x (maybe simp only at x) to simplify the type temporarily, to help understand what you need to do next.

[Kyle Miller]

(It wouldn't be impossible for Lean to reduce some simple arithmetic when computing types of things, but there are times when you don't want that, so it's not clear that it should be done.)

[Max Nowak 🐉]

I have stumbled on an issue where dsimp at h works, but dsimp at * doesn't. Given h : T ⟨a, b⟩.fst. Is there a reason why this is?

[Aaron Liu]

This could be an instance of lean4#8300 or lean4#8696