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 :=
  -- "arguing forwards"
  norm_num, -- ⊢ 49 = x

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 :=
  -- arguing forwards
  norm_num, -- ⊢ 37 * x = y ; but `norm_num` does nothing without the simp attribute above
  linarith, -- works

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