Having `ring` understand when i ≠ -i

Stream: new members

[Alex Griffin]

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]

ring doesn't know anything about proving disequalities

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

Thank you very much.

[Alex Griffin]

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]

rw sub_eq_add_neg, congr will do

[Eric Rodriguez]

there's probably better ways

[Eric Rodriguez]

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

[Alex Griffin]

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]

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.