Zulip Chat Archive

Stream: general

Topic: ring


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 16 2019 at 10:14):

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

view this post on Zulip 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

view this post on Zulip Sebastien Gouezel (Nov 16 2019 at 10:17):

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

view this post on Zulip 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'

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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}

view this post on Zulip 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

view this post on Zulip 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