There is no integer y such that y+y=1

Stream: new members

[Lars Ericson]

I'm stuck on this:

lemma this_diophantine_not_solvable : ¬ ∃ (y:ℤ), 1 = y+y :=
begin
  intro h1,
  cases h1 with y py,
  sorry
end

The goal state is

y: ℤ
py: 1 = y + y
⊢ false

I don't know where to begin. ℤ is a simple type to start with.

Generalizing a bit, I see there is a dioph in matlib, but is this theorem available? If not, any hints on how to prove?

-- Linear Diophantine equations ax + by = c are solvable if and only if
-- the greatest common divisor of a and b divides c
-- http://mathforum.org/library/drmath/view/51595.html
-- https://en.wikipedia.org/wiki/Diophantine_equation#One_equation

theorem solvable_diophantine (a b c : ℕ) :
     (∃ (x y : ℕ), a * x + b * y = c) ↔ (int.gcd a b) ∣ c :=
sorry

[Thomas Browning]

First you need to figure out the human proof (i.e., the proof that you would see when learning elementary number theory)

[Thomas Browning]

nat.gcd_eq_gcd_ab might help with the solvable_diophantine theorem

[Eric Wieser]

Applying even to both sides of py would be a straightforward way to prove that

[Mario Carneiro]

You can show that it is equivalent to ¬ (2 | 1), and there is a decision procedure for the latter so dec_trivial will prove it

[Mario Carneiro]

or simply ¬ even 1, which I'm sure also has a decision procedure

[Mario Carneiro]

in fact it's probably literally a theorem

[Mario Carneiro]

docs#nat.not_even_one

[Lars Ericson]

Thanks, I see the theory of even is well developed in mathlib.

For the general case I will follow @Thomas Browning suggestion to translate the elementary number theory proof. There seems a fair amount to unpack. I will look at how docs#nat.not_even_one is proven to look for clues on how to do the general case:
Screenshot-from-2020-12-25-19-44-20.png

[Mario Carneiro]

wait what? It sounds like you are massively overcomplicating things with this diophantine business

[Mario Carneiro]

divisibility is easily decidable

[Mario Carneiro]

if you want an elementary proof that there is no integerx such that x + x = 1, observe that either x <= 0 or x >= 1, and in the first case x + x <= 0 and in the second x + x >= 2, so it can't be 1

[Mario Carneiro]

If you want Bezout's theorem, you can use nat.gcd_eq_gcd_ab as Thomas suggested, but it's not necessary for your theorem at all

[Lars Ericson]

The x+x=1 is artificial, I started with

def ℤ_even := {x : ℤ | ∃ y, x = 2 * y}

and I rewrote 2*y as y+y in the hope that it would make simplification easier.

However now that I know even is defined I can write

def ℤ_even := {x : ℤ | even x}

and directly apply the available theorems in mathlib for even, so it takes me out of the Diophantine equation business.

I just threw in the general case a * x + b * y = c to look more eager to drown myself in the details of a Number Theory course I took in 1982 from a guy named Oswald Wyler whose favorite thing to say was "I like the integers".

[Mario Carneiro]

Take a look at the definition of divisibility. It is exactly the same as your Z_even up to commutation

[Mario Carneiro]

docs#monoid_has_dvd

[Mario Carneiro]

actually I take it back, it's exactly the same: Z_even is defeq to {x | 2 \| x}

[Mario Carneiro]

and there is a decision procedure for divides, hence not (2 \| 1) is true by dec_trivial

[Mario Carneiro]

it's also defeq to {x | even x}

[Lars Ericson]

DONE

theorem ℤ_even_is_not_a_submonoid: ¬ is_submonoid {x:ℤ  | 2 ∣ x} :=
begin
  intro h1,
  have h2 := h1.one_mem,
  simp at h2,
  have h3 := int.not_even_one,
  exact h3 h2,
end

Since submonoid is required for integral_domain I guess that's good enough to prove that {x:ℤ | 2 ∣ x} is not an integral domain.

Here are related tangents I will drop:

lemma solvable_diophantine (a b c : ℕ) :
       (∃ (x y : ℕ), a * x + b * y = c) ↔ (int.gcd a b) ∣ c :=
sorry

theorem ℝ_1_is_unique :
  ∀ (u : ℝ), (∀ (x : ℝ), u * x = x ∧ x * u = x) → u=1 :=
begin
  intro h1,
  intro h2,
  sorry,
end

theorem ℝ_0_is_unique :
  ∀ (z : ℝ),
    (∀ (x : ℝ),
      z + x = x ∧
      x + z = x ∧
      (∀ (y : ℝ), x * y = z → (x = z ∨ y = z)))
    → z=0 :=
begin
  intro h1,
  intro h2,
  sorry,
end

But on the third hand it is not completely automated because first I try to do is_integral_domain and it says "well I want an is_monoid" so then I manually rewrite the proof to is_submonoid. This involves a manual rewriting step. There doesn't seem to be a way to write that as code.

So that part is in my head instead of being a checkable proof step.

So the next one comes easier

theorem ex6b: ¬ is_subring {x:ℤ | odd x} :=
begin
  intro h1,
  have h2 := h1.to_is_add_subgroup.to_is_add_submonoid.zero_mem,
  simp at h2,
  assumption,
end

but it has that missing proof step because if I start with

theorem ex6b: ¬ is_integral_domain {x:ℤ | odd x} := sorry

then I get the error message

failed to synthesize type class instance for
⊢ ring ↥{x : ℤ | odd x}

So then I manually rewrite the theorem to be is_subring.

Is there any way to automate this issue of the missing sub-instance when I am trying to prove that a set is not an instance of an algebraic structure type?