## Stream: general

### Topic: ring

#### Sebastien Gouezel (Nov 16 2019 at 10:10):

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 (Nov 16 2019 at 10:13):

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 (Nov 16 2019 at 10:14):

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

#### Mario Carneiro (Nov 16 2019 at 10:15):

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

#### Sebastien Gouezel (Nov 16 2019 at 10:17):

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

#### Mario Carneiro (Nov 16 2019 at 10:20):

The culprit is tactic.norm_num from core:

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


#### Mario Carneiro (Nov 16 2019 at 10:20):

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 (Nov 16 2019 at 10:26):

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 (Nov 16 2019 at 10:28):

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 (Nov 16 2019 at 10:29):

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 (Nov 16 2019 at 10:30):

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

Last updated: May 15 2021 at 23:13 UTC