## Stream: general

### Topic: Can abs_of_nonneg be a simp lemma?

#### Kevin Buzzard (Jan 18 2022 at 00:55):

I have been experimenting with using tactics like ring and simp as nonterminal tactics; perhaps this is a sin in mathlib but I think it might have pedagogical advantages sometimes, as it enables mathematicians to reason forwards more easily; furthermore the situation my students will find themselves in is that they will need to prove theorems as part of one-off projects but they will not have to worry about writing maintainable code.

Experimenting with this idea I ran into the following issue:

import tactic
import data.real.basic

-- norm_num will simplify goals
example (x : ℝ) (h : x = 49) : x = 7 * 7 :=
begin
-- "arguing forwards"
norm_num, -- ⊢ 49 = x
assumption,
end

/-
abs_of_nonneg : ∀ {α : Type u} [_inst_1 : add_group α] [_inst_2 : linear_order α]
[_inst_3 : covariant_class α α has_add.add has_le.le] {a : α}, 0 ≤ a → |a| = a
-/

-- next example doesn't work without this
attribute [simp] abs_of_nonneg abs_of_nonpos

example (x y : ℝ) (h : x = y / 37) : |37| * x = y :=
begin
-- arguing forwards
norm_num, -- ⊢ 37 * x = y ; but norm_num does nothing without the simp attribute above
linarith, -- works
end


I don't really understand simp. Can abs_of_nonneg and abs_of_nonpos be simp lemmas, or is that somehow a bad idea?

#### Anne Baanen (Jan 18 2022 at 10:26):

These can probably work fine as simp lemmas: to apply a simp lemma its parameters need to be inferrable from the goal, or instances, or Prop-valued and solvable by a recursive call to simp. I think there are a few simp lemmas about nonnegativity so the recursive calls can probably be solved in the common cases.

#### Stuart Presnell (Jan 18 2022 at 11:06):

I guess I don't really understand simp either. If abs_of_nonneg was a simp lemma, then wouldn't simp always re-write 0 ≤ a to |a| = a whenever it can, regardless of whether this is helpful or relevant?

#### Anne Baanen (Jan 18 2022 at 11:08):

That would only happen if the return type is (0 ≤ a) ↔ (|a| = a), here the return type is |a| = a, so simp will only try to rewrite |a| into a.

#### Stuart Presnell (Jan 18 2022 at 11:23):

Ah, because 0 ≤ a is just one of the preconditions, and |a| = a is the thing that simp is using to rewrite.

#### Kevin Buzzard (Jan 18 2022 at 12:26):

Right. And the thing I didn't understand about simp was whether it would aggressively change all |a|s to a and then throw a>=0 at the user as a goal whether or not it was true. My understanding of the comments above is that fortunately this is not what happens.

#### Gabriel Ebner (Jan 18 2022 at 12:27):

No, but rw would do that (though you need to write rw abs_of_nonneg explicitly of course).

Last updated: Aug 03 2023 at 10:10 UTC