Non-terminal rings

Stream: new members

[James Arthur]

I've heard about non-terminal simps, but is there a similar rule for rings ? Its mentioned in #3801 and I thought I'd ask here. @Shing Tak Lam looked through mathlib and saw it never happened.

[Kevin Buzzard]

non-terminal rings are also uncool I think. Why would you need one?

[Ruben Van de Velde]

I suspect it's less brittle - simp output could change as a result of simp lemmas changing (and maybe imports?), but I think ring output will only change if the tactic itself changes. They both do have the issue that the output is not clearly specified, though

[Ruben Van de Velde]

I don't remember where, but I've had cases where I needed to do ring, ring to finish

[Kevin Buzzard]

ring uses simp I believe, which is probably why it's not an ideal tactic if you're not finishing. The ring, ring thing is a bug, this is to do with metavariables

[Ruben Van de Velde]

Oh, does it? That makes sense, then

[Kevin Buzzard]

I might be wrong, but I think it uses simp to try and tidy up if it doesn't close the goal

[James Arthur]

If its bad, I can refactor code. I kind of used it as a short cut not to write out a load of rewrites. Thanks, I'll go refactor some code.

[Kenny Lau]

@James Arthur there's always a smarter way to use less automation:

import analysis.special_functions.trigonometric

open real
noncomputable theory

private lemma aux_lemma (x : ℝ) : 1 / (x + sqrt(1 + x^2)) = - x + sqrt(1 + x^2) :=
begin
  refine (eq_one_div_of_mul_eq_one _).symm,
  have : 0 ≤ 1 + x ^ 2 := add_nonneg zero_le_one (pow_two_nonneg x),
  rw [add_comm, ← sub_eq_neg_add, ← mul_self_sub_mul_self,
      mul_self_sqrt this, pow_two, add_sub_cancel]
end

[Mario Carneiro]

ring actually has a separate tidying step, not simp, that is done if it can't close the goal. The idea is to write the polynomial more plainly so you can see why it's not zero. It is intended primarily for debugging your proof, I wouldn't suggest using it non-terminally.

[Mario Carneiro]

ring uses the core simplifier routine internally but not anything that makes it simp, i.e. the default simp set