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


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