Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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?

view this post on Zulip 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