Zulip Chat Archive

Stream: Is there code for X?

Topic: Converting from one type to another


view this post on Zulip Ariel Fridman (Feb 18 2021 at 14:35):

I have an x^(int.of_nat n) (where n is nat) in my goal, and I wanted to convert it into just x^n.

I found int.cast_of_nat, but it seems like the conversion arrow thing is required for it to work. Is there some way I can still do this convertion?

view this post on Zulip Johan Commelin (Feb 18 2021 at 14:36):

You can write show (some new expression) if it is definitionally equal to your current goal

view this post on Zulip Johan Commelin (Feb 18 2021 at 14:37):

And int.of_nat n is defeq to (n : \Z)

view this post on Zulip Ariel Fridman (Feb 18 2021 at 14:38):

Ah, this worked! Thank you very much!

view this post on Zulip Johan Commelin (Feb 18 2021 at 14:38):

After that, there should be a lemma called gpow_eq_pow or something like that, that will convert from powers with integers in the exponent to powers with nat in the exponent

view this post on Zulip Ruben Van de Velde (Feb 18 2021 at 14:42):

Though I wonder how you ended up with of_nat in the first place

view this post on Zulip Sebastien Gouezel (Feb 18 2021 at 14:43):

You can also apply simp and see how it changes your expression to something more canonical.

view this post on Zulip Ariel Fridman (Feb 18 2021 at 14:47):

Ruben Van de Velde said:

Though I wonder how you ended up with of_nat in the first place

I used cases on an integer, since for this lemma I needed to split into positive and negative branches.

view this post on Zulip Ariel Fridman (Feb 18 2021 at 14:48):

There might be a better way though.

view this post on Zulip Johan Commelin (Feb 18 2021 at 14:51):

It probably makes sense to first prove whatever you are proving for nats, and then apply that lemma twice in the two branches for int

view this post on Zulip Johan Commelin (Feb 18 2021 at 14:51):

But I'm just guessing

view this post on Zulip Ariel Fridman (Feb 18 2021 at 14:53):

You're probably right, and it might've been wiser to prove some other lemmas before it in order to be able to do this more generically.

view this post on Zulip Yakov Pechersky (Feb 18 2021 at 15:02):

Doing cases on an int is breaking the abstraction layer. I would just do by_cases on a statement about positivity, or cases lt_or_ge. Then you wouldn't be in a situation where you have to deal with the underlying definition of int

view this post on Zulip Eric Wieser (Feb 18 2021 at 15:04):

induction using int.induction_on (docs#int.induction_on) is often a good bet too

view this post on Zulip Ariel Fridman (Feb 18 2021 at 15:29):

Eric Wieser said:

induction using int.induction_on (docs#int.induction_on) is often a good bet too

Yesss, This is exactly what I needed. Thank you very much ^^!


Last updated: May 07 2021 at 22:14 UTC