Zulip Chat Archive

Stream: new members

Topic: How to cast types properly


Jihoon Hyun (Feb 05 2025 at 08:25):

#mwe

def α : Type _ := sorry

def β : Type _ := α

def func : α  α := sorry

instance : HasEquiv β := sorry

example (b : β) : (func b : β)  b := by
  sorry

I want to make the example work as expected. Of course it is possible to define an explicit coersion method, like of\alpha : \alpha \to \beta, but it will lead to not-simp-normal-form error if the theorem of\alpha a = a is simp, which is very reasonable if I'm right.

Kevin Buzzard (Feb 05 2025 at 11:51):

func b is defeq abuse so I'm not sure what "work as expected" means here, if you commit defeq abuse then it's hard to know what to expect.

Jihoon Hyun (Feb 05 2025 at 11:56):

So I'd like to state an equivalence between func b and b as an element of type \beta. In my case, \alpha is actually a list, so it bothers me quite a lot.

Kevin Buzzard (Feb 05 2025 at 12:16):

But func is not a function on beta

Jihoon Hyun (Feb 05 2025 at 12:17):

Then should I make a copy of func and its related theorems which works with \beta?

Kevin Buzzard (Feb 05 2025 at 12:17):

And of\alpha a = a is also defeq abuse so shouldn't be a simp lemma or indeed a lemma

Kevin Buzzard (Feb 05 2025 at 12:19):

Jihoon Hyun said:

Then should I make a copy of func and its related theorems which works with \beta?

Sure! In mathlib we have plenty of examples of avoiding defeq abuse by carefully using of\alpha and to\alpha even on types which are defeq

Edward van de Meent (Feb 05 2025 at 12:19):

usually in this kind of situation, we have a few casting equivalences (for example, docs#FreeMonoid.toList) which allow you to convert from one to the other

Edward van de Meent (Feb 05 2025 at 12:20):

see for example docs#FreeMonoid.countP'

Jihoon Hyun (Feb 05 2025 at 12:23):

Edward van de Meent said:

see for example docs#FreeMonoid.countP'

Thank you for a nice example!


Last updated: May 02 2025 at 03:31 UTC