Zulip Chat Archive
Stream: new members
Topic: How to cast types properly
Jihoon Hyun (Feb 05 2025 at 08:25):
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