# Zulip Chat Archive

## 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:21):

#### 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