Can `abs_of_nonneg` be a simp lemma?

Stream: general

[Kevin Buzzard]

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]

(docs#abs_of_nonneg)

[Anne Baanen]

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]

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]

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]

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

[Kevin Buzzard]

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]

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