# 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 `j`

s 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 `j`

s 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 `j`

s 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