Algebra in nnreal

Stream: new members

[Callum Cassidy-Nolan]

What would be an easy way to prove this ?

import data.real.nnreal

theorem help (a b : nnreal): a^2 + b^2 = (a + b)^2 - 2 * (a * b) :=
begin
  sorry
end

I tried using library_search to see if there was a theorem that I could use, but it didn't show up I've also tried ring and ring_nf but I guess they don't work since nnreal isn't a ring...

[Yaël Dillies]

Use docs#eq_tsub_of_add_eq and go on from there.

[Callum Cassidy-Nolan]

Thanks Yaël

theorem help (a b : nnreal): a^2 + b^2 = (a + b)^2 - 2 * (a * b) :=
begin
  apply eq_tsub_of_add_eq,
  ring,
end

got it with this^

[Ruben Van de Velde]

I'd start with docs#add_sq

[Ruben Van de Velde]

But if that works, all the better :)

[Callum Cassidy-Nolan]

This was part of a larger question:

theorem full
  (a b : nnreal)
  (h₁ : (a * b)=180)
  (h₂ : 2 * (a + b)=54) :
  (a^2 + b^2) = 369 :=
begin
  have ha : (a + b) = 27, sorry,
  -- {
  --   exact eq_div_of_mul_eq'' h₂,
  -- }
  have hb : 2 * (a * b) = 360, sorry,
  have h₃ : a^2 + b^2 = (a + b)^2 - 2 * (a * b),
  {
    apply eq_tsub_of_add_eq,
    ring,
  },
  rw h₃,
  rw ha,
  rw hb,
  norm_num,
end

I'm having some difficulty filling out the two sorries and the norm_num at the bottom isn't completely finishing the proof, am I missing something? This proof seems to be getting overcomplicated.

[Alex J. Best]

These calculations might be easier if you work in real rather than nnreal and use tactic#linarith.

[Callum Cassidy-Nolan]

Thinking about that...

[Callum Cassidy-Nolan]

That helped a lot thanks

[Alex J. Best]

To answer the question about getting the nnreal version from the real, you can use the mod_cast tactics

import data.real.nnreal
theorem full'
  (a b : real)
  (h₁ : (a * b)=180)
  (h₂ : 2 * (a + b)=54) :
  (a^2 + b^2) = 369 :=
  sorry
theorem full
  (a b : nnreal)
  (h₁ : (a * b)=180)
  (h₂ : 2 * (a + b)=54) :
  (a^2 + b^2) = 369 :=
begin
  exact_mod_cast (full' a b _ _),
  assumption_mod_cast,
  assumption_mod_cast,
end