int or nat

Stream: new members

[Tianchen Zhao]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Eric Rodriguez]

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

[Ruben Van de Velde]

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

[Tianchen Zhao]

(deleted)

[Tianchen Zhao]

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!

[Tianchen Zhao]

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!

[Tianchen Zhao]

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?

[Ruben Van de Velde]

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

[Ruben Van de Velde]

ring_theory.int.basic is probably also useful

[Tianchen Zhao]

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
⊢ ℤ
-/

[Kevin Buzzard]

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