Zulip Chat Archive

Stream: new members

Topic: Having `ring` understand when i ≠ -i


Alex Griffin (May 14 2021 at 01:28):

I am trying to show that the elements sr (-i + 1) and sr (i + 1) of a given (non-degenerate) dihedral group dihedral_group n are distinct elements whenever i is such that 2i does not divide n. I happen to know that this is precisely the condition that implies -i and i are distinct elements modulo n, which should then imply that sr (-i + 1) and sr (i + 1) are distinct elements. There are a couple of problem with this: first, ring cannot seem to figure out that -i ≠ i, which makes some amount of sense considering that there are elements of zmod n that are their own inverses, but how do I get Lean to figure out that this is the case? Second, even if Lean knew this to be the case, it would not know that sr (-i + 1) and sr (i + 1) are necessarily distinct. What is the best way to show that this must be true?

The MWE for this:

import group_theory.specific_groups.dihedral
open dihedral_group
variables {n : }

theorem dihedral_example [fact (n > 2)] (i : zmod n): 2 * i  0  sr (-i + 1)  sr (i + 1) :=
  begin
    intro hyp,
    sorry,
  end

Mario Carneiro (May 14 2021 at 01:29):

ring doesn't know anything about proving disequalities

Mario Carneiro (May 14 2021 at 01:30):

it can only prove equalities, and only equalities that are true in all rings

Mario Carneiro (May 14 2021 at 01:30):

what is sr (at least, what about it is relevant to the proof)?

Mario Carneiro (May 14 2021 at 01:32):

sr is a constructor, so you can simplify the goal to -i + 1 ≠ i + 1 and then to -i ≠ i or 2*i ≠ 0

Mario Carneiro (May 14 2021 at 01:33):

which in zmod n is equivalent to 2*i does not divide n

Mario Carneiro (May 14 2021 at 01:35):

theorem dihedral_example (i : zmod n): 2 * i  0  sr (-i + 1)  sr (i + 1) :=
begin
  intro h,
  simp,
  rwa [eq_comm,  sub_eq_zero, sub_neg_eq_add,  two_mul],
end

Alex Griffin (May 14 2021 at 01:37):

Thank you very much.

Alex Griffin (May 14 2021 at 12:58):

I actually have another question, which I'll tack on to the end of this topic because it originated from the prior discussion. I have a similar scenario to before, illustrated below:

import data.zmod.basic

theorem zmod_example (i : zmod n): 2 * i = 0   (j : zmod n), j - i = j + i :=
  begin
    intros hyp j,
    sorry,
  end

Now, from the previous example, it is very clear how to solve this. The current goal once sorry is removed is ⊢ j - i = j + i, which should be as simple as simplifying the current goal to ⊢ -i = i and then using the hypothesis to show that this must be true. Except, if you try to use tactics like ring or simp to get rid of the js from the goal, it claims to not be able to simplify any further. What am I missing that Lean cannot figure out to remove the js from the goal?

Eric Rodriguez (May 14 2021 at 13:01):

rw sub_eq_add_neg, congr will do

Eric Rodriguez (May 14 2021 at 13:01):

there's probably better ways

Eric Rodriguez (May 14 2021 at 13:03):

library_search suggests refine norm_num.sub_pos _ _ _ _ rfl (congr_arg ((+) j) _), but I feel like this is nowhere near as legible

Alex Griffin (May 14 2021 at 13:05):

Thank you for the answer, thought I am also curious why Lean had trouble realizing that removing the js was a possibility with my initial setup. Was I not providing enough information, or was it something else?

Yakov Pechersky (May 14 2021 at 13:23):

Removing the js isn't always obviously the right step. Imagine you had something like j * i = j * - i, with i j in the integers. Obviously this is only true if j = 0 or i = 0. But perhaps you don't know that currently, and you have complex side hypothesese that if you did follow through their conclusions, you'd get j = 0. But before that, if you congr'd the j's away, you'd be left with an unsolvable goal.


Last updated: Dec 20 2023 at 11:08 UTC