x * x = 100 → x = 10

Stream: new members

[Huỳnh Trần Khanh]

this proof is way too complicated i'm pretty sure there is a very simple way to prove this can anyone help me out

import tactic.linarith

example { x y a : ℕ } { h : x < y } : x + a < y + a := add_lt_add_right h a

lemma less ( x : ℕ ) ( h : x < 10 ) : x * x < 100 := begin
  dec_trivial!,
end

lemma greater : ∀ x : ℕ, ∀ h : x > 10, x * x > 100
| 0 h := by linarith
| (n + 1) h := begin
  have : (n + 1) * (n + 1) = n * n + 2 * n + 1 := by ring,
  rw this,
  exact if equal: n = 10 then begin
    rw equal,
    linarith,
  end else begin
    have : n * n > 100 := greater n begin
      by_contradiction,
      have : n ≤ 10 := by linarith,
      have : n < 10 ∨ n = 10 := lt_or_eq_of_le this,
      cases this with a b,
      {
        linarith,
      },
      {
        exact equal b,
      }
    end,
    linarith,
  end
end

lemma something { x : { x : ℕ // x * x = 100 } } : (x : ℕ) = 10 := begin
  cases x with x hx,
  exact if h: x > 10 then begin
    have := greater x h,
    linarith,
  end else begin
    exact if h1: x < 10 then begin
      have := less x h1,
      linarith,
    end else begin
      have : x = 10 := by linarith,
      exact this,
    end,
  end
end

[Huỳnh Trần Khanh]

and i wanna keep the lemma signature too

[Ruben Van de Velde]

import data.nat.basic
import tactic

lemma something' (n : ℕ) (h : n * n = 100) : n = 10 :=
begin
  have h1 : 100 = 10 * 10,
  { norm_num },
  rw h1 at h,
  zify at *,
  rw mul_self_eq_mul_self_iff at h,
  apply h.resolve_right,
  linarith,
end

lemma something { x : { x : ℕ // x * x = 100 } } : (x : ℕ) = 10 := something' x x.prop

or without the auxiliary lemma:

import data.nat.basic
import tactic

lemma something { x : { x : ℕ // x * x = 100 } } : (x : ℕ) = 10 := begin
  have h := x.prop,
  have h1 : 100 = 10 * 10,
  { norm_num },
  simp_rw h1 at h,
  zify at *,
  rw mul_self_eq_mul_self_iff at h,
  apply h.resolve_right,
  linarith,
end

[Mario Carneiro]

There should be a version of this for nat that doesn't have the disjunction

[Ruben Van de Velde]

You expect there to be one or you think it would be a useful addition?

[Shing Tak Lam]

Here's a different proof of the auxiliary lemma

import tactic

example (n : ℕ) (hn : n * n = 100) : n = 10 :=
by rw [←nat.sqrt_eq n, hn, (show 100 = 10 * 10, from rfl), nat.sqrt_eq]

[Eric Wieser]

I'd expect norm_num to be faster than rfl there

[Shing Tak Lam]

Eric Wieser said:

I'd expect norm_num to be faster than rfl there

import tactic

set_option profiler true

-- elaboration of foo took 28.5ms
lemma foo (n : ℕ) (hn : n * n = 100) : n = 10 :=
by rw [←nat.sqrt_eq n, hn, (show 100 = 10 * 10, from rfl), nat.sqrt_eq]

-- elaboration of bar took 61.2ms
lemma bar (n : ℕ) (hn : n * n = 100) : n = 10 :=
by rw [←nat.sqrt_eq n, hn, (show 100 = 10 * 10, by norm_num), nat.sqrt_eq]

I'm not sure that's the case.

import tactic

set_option profiler true

-- elaboration of foo took 4.52ms
lemma foo : 100 = 10 * 10 := rfl

-- elaboration of bar took 34.2ms
lemma bar : 100 = 10 * 10 := by norm_num

[Ruben Van de Velde]

Turns out it's called nat.mul_self_inj