## Stream: new members

### Topic: is this something nlinarith should be able to do?

#### Chris M (Jul 26 2020 at 13:06):

import data.real.basic
import tactic

open function

theorem aux {x y : ℝ} (h : x^2 + y^2 = 0) : x = 0 :=
begin
have h' : x^2 = 0,
{ nlinarith },
exact pow_eq_zero h'
end

example (x y : ℝ) : x^2 + y^2 = 0 ↔ x = 0 ∧ y = 0 :=
begin
split,
{ intros, split, {
apply aux a},{
rw add_comm at a, apply aux a}},{
intros, cases a,
nlinarith
}
end


This doesn't work, because nlinarith gives an error, it doesn't work if I replace it with norm_num either, and only works when I replace it with

have h:x^2=0, {exact tactic.ring_exp.pow_p_pf_zero a_left rfl},
have h2:y^2=0, {exact tactic.ring_exp.pow_p_pf_zero a_right rfl},
finish


I'm curious: is this something that we would want nlinarith or norm_num to know about or am I misunderstanding what they should be able to do?

#### Mario Carneiro (Jul 26 2020 at 13:09):

I don't think linarith does case splits

Last updated: May 14 2021 at 06:16 UTC