positive integers

Stream: new members

[Lawrence Lin]

Hi, all! How do I define the positive integers in lean? I want to introduce the equivalent of
x, y \in \mathbb{Z}^+in lean...

resolved! i just used (x, y : \N) and (hpos : x > 0) same with y

[Hanting Zhang]

There's docs#pnat

[Hanting Zhang]

But sometimes what you're doing with (x : \N) (hp : x > 0) works just as well

[Lawrence Lin]

thanks-

[Lawrence Lin]

right so i ran into another funny situation.. is it possible to introduce a new variable k = x^3 + y^3? i don't think lean's letting me do that. can't find where to do it in the documentation either

[Lawrence Lin]

trying to introduce it in an example environment, but it's not happening :(

[Hanting Zhang]

you can do

example (x y : \N) (hp : x > 0) : true :=
begin
  let k := x^3 + y^3
  sorry
end

[Lawrence Lin]

... i should've known... thanks again

[Hanting Zhang]

btw let is different from have in that it retains the definition, while have is for Props (and so definition irrelevant). One neat trick is that is you're using an IDE, you can hover over the keywords let, have, or any other tactic to see documentation on what it does

[Yaël Dillies]

set k :) x^3 + y^3 with hk is also useful to know.

[Kevin Buzzard]

:= not :) :)

[Patrick Johnson]

generalizing hk : x^3 + y^3 = k may be useful if you have x^3 + y^3 in the goal statement or if you plan to use rw, subst or induction later in the proof (with let/set you may get type errors).

[Martin Dvořák]

I use (x_pos : x > 0) all the time. It isn't necessary to express positivity by a data type.