Zulip Chat Archive

Stream: maths

Topic: non-natural exponents?


view this post on Zulip Belisarius Cawl (Mar 24 2021 at 10:46):

Hi all, apologies if I am misusing this. Tried the search unsuccessfully at least.

Am just getting started with LEAN, played the numbers game and read through the docs. Now for my own application I have equations with real exponents, but for anything other than natural exponents it says "failed to synthesize type class instance for [...] [base number type] ℝ" (stuff in brackets is mine).

What am I doing wrong? Any help would be greatly appreciated, learning curve's steep.

view this post on Zulip Johan Commelin (Mar 24 2021 at 10:47):

@Belisarius Cawl What did you import at the top of your file?

view this post on Zulip Johan Commelin (Mar 24 2021 at 10:47):

Also "equations" of what? You can't take real exponents of arbitrary things. They have to be something like real numbers.

view this post on Zulip Johan Commelin (Mar 24 2021 at 10:47):

docs#real.has_pow should work

view this post on Zulip Johan Commelin (Mar 24 2021 at 10:49):

So if you import analysis.special_functions.pow then you should be able to take real exps of real numbers

view this post on Zulip Belisarius Cawl (Mar 24 2021 at 10:49):

hey cool, will try it out right away. thanks a lot!

view this post on Zulip Belisarius Cawl (Mar 24 2021 at 10:50):

works, woohoo!

view this post on Zulip Belisarius Cawl (Mar 24 2021 at 11:00):

wait a second... This is very strange. Depending on whether the first occurence of exponentiation im my equation is real^real or whole^real, respectively, the other occurences of whole^real don't cause an error or do cause one. (At least until further down at another equation).

In any case I guess I have to convert my wholes to reals, no? How would I do that? In the docs (https://leanprover-community.github.io/mathlib_docs/data/real/basic.html#real) I don't see anything analogous to int.from_nat or however it's called.

As a related question - is it possible to add whole numbers with the "+" infix notation? LEAN complains until I use int.add.
(EDIT: only complains when I add wholes to nats which I guess is okay)

Again apologies for the messy noob questions, if you would like to point out a suggested way to deal with those myself I'd be happy to do so.

view this post on Zulip Johan Commelin (Mar 24 2021 at 11:04):

(n:ℝ) coerces an integer to a real

view this post on Zulip Johan Commelin (Mar 24 2021 at 11:05):

You can certainly just write n + m for integer addition

view this post on Zulip Johan Commelin (Mar 24 2021 at 11:05):

If that doesn't work, you've messed something up, somewhere

view this post on Zulip Johan Commelin (Mar 24 2021 at 11:05):

But we can't tell if you don't show us your code

view this post on Zulip Belisarius Cawl (Mar 24 2021 at 11:05):

Yeah, I guess I tried to plus nats and wholes

view this post on Zulip Belisarius Cawl (Mar 24 2021 at 11:06):

ok sure, wanted to avoid walls of text. will try what you said now first. Thanks!

view this post on Zulip Belisarius Cawl (Mar 24 2021 at 11:17):

(works)

view this post on Zulip Kevin Buzzard (Mar 24 2021 at 11:46):

You can only add numbers of the same type. If lean sees a + b then it assumes you're adding things of a's type and if b isn't of a's type then it will try to coerce it into a's type. So real + nat will work but nat + real won't.

view this post on Zulip Kevin Buzzard (Mar 24 2021 at 11:47):

For nat + real you need to coerce the nat yourself with (n : real)


Last updated: May 12 2021 at 07:17 UTC