Zulip Chat Archive

Stream: new members

Topic: x * x = 100 → x = 10


view this post on Zulip Huỳnh Trần Khanh (Mar 28 2021 at 08:24):

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

view this post on Zulip Huỳnh Trần Khanh (Mar 28 2021 at 08:25):

and i wanna keep the lemma signature too

view this post on Zulip Ruben Van de Velde (Mar 28 2021 at 08:37):

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

view this post on Zulip Mario Carneiro (Mar 28 2021 at 08:43):

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

view this post on Zulip Ruben Van de Velde (Mar 28 2021 at 08:46):

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

view this post on Zulip Shing Tak Lam (Mar 28 2021 at 08:48):

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]

view this post on Zulip Eric Wieser (Mar 28 2021 at 08:51):

I'd expect norm_num to be faster than rfl there

view this post on Zulip Shing Tak Lam (Mar 28 2021 at 08:55):

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

view this post on Zulip Ruben Van de Velde (Mar 28 2021 at 15:20):

Turns out it's called nat.mul_self_inj


Last updated: May 18 2021 at 16:25 UTC