# Zulip Chat Archive

## Stream: new members

### Topic: symmetry of congruence mod 37

#### Nicholas Siedlaczek (Dec 06 2018 at 21:46):

I know what I am trying to achieve, however not sure about how to actually execute it in Lean.

import tactic.ring definition R (a b : ℤ) := ∃ (k : ℤ), k * 37 = a - b theorem R_is_symmetric : symmetric R := begin unfold symmetric, intro x, intro y, unfold R, intro H, existsi((-k) : ℤ), end

As you can see I have the hypothesis the k * 37 = x - y, however want to show existence of -k to show -k * 37 = y - x which will show that it is symmetric.

Thanks

#### Chris Hughes (Dec 06 2018 at 21:48):

This should help. Use cases.

theorem R_is_symmetric : symmetric R := begin unfold symmetric, intro x, intro y, unfold R, intro H, cases H with k hk, existsi( -k : ℤ), end

#### Nicholas Siedlaczek (Dec 06 2018 at 21:52):

Thanks Chris

#### Kevin Buzzard (Dec 06 2018 at 22:50):

Are you an Imperial undergraduate doing my equivalence relation challenge @Nicholas Siedlaczek ?

#### Mario Carneiro (Dec 06 2018 at 22:59):

I'm sure the 37 was a coincidence

#### Patrick Massot (Dec 06 2018 at 23:36):

@Nicholas Siedlaczek , after you're done with this, it will be useful to realize that all those `unfold`

are only psychological comfort for you, but Lean doesn't need them. The tactic proof of your lemma needs no more than three lines, one for introductions (using tactic `rintros`

), one for instanciating the existential (using tactic `use`

, or `existsi`

but you should get used to `use`

which is newer and more powerful), and one for the tiny computation (using tactic `simp`

).

#### Nicholas Siedlaczek (Dec 06 2018 at 23:41):

@Patrick Massot Thanks so what you're saying is all `unfold`

does is display to the user what it actually means and shows you what to prove while lean basically 'ignores' them and is of no consequences to it?

#### Patrick Massot (Dec 06 2018 at 23:46):

Sometimes it's useful also to Lean, eg for type class instance resolution but, in my experience, almost every unfold that I type is unnecessary.

#### Patrick Massot (Dec 06 2018 at 23:47):

In your case, the full proof is

definition R (a b : ℤ) := ∃ (k : ℤ), k * 37 = a - b theorem R_is_symmetric : symmetric R := begin rintros x y ⟨k, H⟩, use -k, simp[H] end

#### Patrick Massot (Dec 06 2018 at 23:49):

If you want to emphasize which part really uses tactics seriously, you can also write it as:

theorem R_is_symmetric : symmetric R := λ x y ⟨k, H⟩, ⟨-k, by simp[H]⟩

#### Patrick Massot (Dec 06 2018 at 23:50):

It shows clearly that, in this proof, the only tactic which actually does work for you is the simplifier

Last updated: May 08 2021 at 09:11 UTC