Converting from one type to another

Stream: Is there code for X?

[Ariel Fridman]

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]

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

[Johan Commelin]

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

[Ariel Fridman]

Ah, this worked! Thank you very much!

[Johan Commelin]

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]

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

[Sebastien Gouezel]

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

[Ariel Fridman]

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]

There might be a better way though.

[Johan Commelin]

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]

But I'm just guessing

[Ariel Fridman]

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]

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]

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

[Ariel Fridman]

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 ^^!