ring

Stream: general

[Sebastien Gouezel]

ring just failed me on

lemma come_on_ring (x y : ℂ) :
   x * (2 : ℂ)⁻¹ = -((-1) * (2 : ℂ)⁻¹ * x) :=
begin
  ring,
  rw neg_neg,
  rw mul_comm
end

First line should work but does not close the goal. Also, if you replace the line rw mul_comm with ring, it fails again but expands the definition of the inverse, which it didn't do in the first step.

[Mario Carneiro]

this works for me:

import tactic.ring
variables {ℂ : Type} [linear_ordered_field ℂ]
lemma come_on_ring (x y : ℂ) :
   x * (2 : ℂ)⁻¹ = -((-1) * (2 : ℂ)⁻¹ * x) :=
by ring1

[Mario Carneiro]

On further review, though, that typeclass is nonsense. Something requires a linear ordered semiring

[Mario Carneiro]

I think it is because it is trying to use rat.cast to make sense of the one half

[Sebastien Gouezel]

Yes, ℂ is not really ordered, but still it has characteristic 0...

[Mario Carneiro]

The culprit is tactic.norm_num from core:

#eval tactic.norm_num `(1 / (2 : ℂ)) >>= tactic.trace
-- failed to synthesize 'linear_ordered_semiring'

[Mario Carneiro]

mathlib has a char_zero typeclass to address this, but we used linear_ordered_field before that and the norm_num lemmas use it too

[Mario Carneiro]

It uses

#print norm_num.div_eq_div_helper
-- theorem norm_num.div_eq_div_helper : ∀ {α : Type u} [_inst_1 : field α] (a b c d v : α),
--   a * d = v → c * b = v → b ≠ 0 → d ≠ 0 → a / b = c / d

to prove equality of divisions by cross multiplication (causing a 2 ≠ 0 subgoal), followed by

#print norm_num.nonzero_of_pos_helper
-- theorem norm_num.nonzero_of_pos_helper : ∀ {α : Type u} [_inst_1 : linear_ordered_semiring α] (a : α), a > 0 → a ≠ 0

to deduce this from 2 > 0 (at which point we are talking nonsense since there is no such order on complexes)

[Mario Carneiro]

In any case, you can solve the lemma like this:

lemma come_on_ring (x y : ℂ) :
   x * (2 : ℂ)⁻¹ = -((-1) * (2 : ℂ)⁻¹ * x) :=
by {generalize: (2 : ℂ)⁻¹ = a, ring}

[Sebastien Gouezel]

OK. Finally, in my more complex computation, I cheated by hiding 1/2 from ring, with (a variant of)

lemma come_on_ring (x y : ℂ) :
   x * (2 : ℂ)⁻¹ = -((-1) * (2 : ℂ)⁻¹ * x) :=
begin
  set u : ℂ := (2 : ℂ)⁻¹,
  ring
end

[Sebastien Gouezel]

Yes, it's essentially the same as your solution with generalize.