Zulip Chat Archive

Stream: new members

Topic: int or nat


view this post on Zulip Tianchen Zhao (Apr 05 2021 at 14:45):

Hi all! I encounter this problem trying to replicate this proof in lean (figure 1). I don't know whether to make x y a b to be integers or natural numbers. If they are nat, usually I can stuck on some tedious calculations especially involving subtraction (I guess it's because subtraction is defined differently e.g. 0 - 1 = 0). You can also check figure 2 where I give some examples that library_search cannot solve conjectures about nat but work in int. However, if I make them int, I'll need to combine nat and int using ↑, e.g. ↑q = x^2 + y^2 instead of q = x^2 + y^2 and it takes a lot of work to convert between int and nat.

Are there any suggestions? Thank you!
oringinal-proof.PNG
int-vs-nat.PNG

view this post on Zulip Kevin Buzzard (Apr 05 2021 at 14:46):

I would work with int all the time, because whilst this is a theorem about naturals there is a lot of subtraction going on.

view this post on Zulip Kevin Buzzard (Apr 05 2021 at 14:48):

I would just use ints for everything -- then you don't even have up-arrows.

view this post on Zulip Kevin Buzzard (Apr 05 2021 at 14:49):

As for the not working stuff -- the second example is not true (try slim_check and see if it finds a counterexample) and the first example could perhaps be solved by omega, but honestly I would avoid naturals.

view this post on Zulip Eric Rodriguez (Apr 05 2021 at 15:05):

woah first time I see slim_check, that's really cool

view this post on Zulip Ruben Van de Velde (Apr 05 2021 at 16:44):

If you get stuck, feel free to check https://github.com/Ruben-VandeVelde/flt/blob/tmp/src/cox.lean for my proof

view this post on Zulip Tianchen Zhao (Apr 05 2021 at 17:27):

(deleted)

view this post on Zulip Tianchen Zhao (Apr 05 2021 at 17:28):

Kevin Buzzard said:

I would just use ints for everything -- then you don't even have up-arrows.

I see. I will stick to int later on. Thanks!

view this post on Zulip Tianchen Zhao (Apr 05 2021 at 17:30):

Ruben Van de Velde said:

If you get stuck, feel free to check https://github.com/Ruben-VandeVelde/flt/blob/tmp/src/cox.lean for my proof

Oh that's fantastic! Thank you!

view this post on Zulip Tianchen Zhao (Apr 12 2021 at 11:02):

Kevin Buzzard said:

I would just use ints for everything -- then you don't even have up-arrows.

By the way, there is no defintions for prime in int. To avoid nat, I've seen a lot of works importing field_theory.finite.basic to use the definition of prime. Is that the right thing to do?

view this post on Zulip Ruben Van de Velde (Apr 12 2021 at 11:11):

Not sure why you'd go through field_theory.finite.basic, though it probably works fine. Importing algebra.associated should be sufficient

view this post on Zulip Ruben Van de Velde (Apr 12 2021 at 11:11):

ring_theory.int.basic is probably also useful

view this post on Zulip Tianchen Zhao (Apr 12 2021 at 13:04):

Ruben Van de Velde said:

Not sure why you'd go through field_theory.finite.basic, though it probably works fine. Importing algebra.associated should be sufficient

Yeah I also noticed that ring_theory.int.basic works as well in your proof on cox, but I get the same results unfolding prime with the three imports. Is there a preference?

import algebra.associated

example {n : } (h : prime n) :  :=
begin
  unfold prime at h,
  sorry
end

/-
n: ℤ
h: n ≠ 0 ∧ ¬is_unit n ∧ ∀ (a b : ℤ), n ∣ a * b → n ∣ a ∨ n ∣ b
⊢ ℤ
-/
import field_theory.finite.basic

example {n : } (h : prime n) :  :=
begin
  unfold prime at h,
  sorry
end

/-
n: ℤ
h: n ≠ 0 ∧ ¬is_unit n ∧ ∀ (a b : ℤ), n ∣ a * b → n ∣ a ∨ n ∣ b
⊢ ℤ
-/
import ring_theory.int.basic

example {n : } (h : prime n) :  :=
begin
  unfold prime at h,
  sorry
end

/-
n: ℤ
h: n ≠ 0 ∧ ¬is_unit n ∧ ∀ (a b : ℤ), n ∣ a * b → n ∣ a ∨ n ∣ b
⊢ ℤ
-/

view this post on Zulip Kevin Buzzard (Apr 12 2021 at 13:05):

It's the same function you're using every time.


Last updated: May 14 2021 at 21:11 UTC