## Stream: Is there code for X?

### Topic: Converting from one type to another

#### 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?

#### Johan Commelin (Feb 18 2021 at 14:36):

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

#### Johan Commelin (Feb 18 2021 at 14:37):

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

#### Ariel Fridman (Feb 18 2021 at 14:38):

Ah, this worked! Thank you very much!

#### 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

#### Ruben Van de Velde (Feb 18 2021 at 14:42):

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

#### Sebastien Gouezel (Feb 18 2021 at 14:43):

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

#### 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.

#### Ariel Fridman (Feb 18 2021 at 14:48):

There might be a better way though.

#### 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

#### Johan Commelin (Feb 18 2021 at 14:51):

But I'm just guessing

#### 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.

#### 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

#### Eric Wieser (Feb 18 2021 at 15:04):

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

#### 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