symmetry of congruence mod 37

Stream: new members

[Nicholas Siedlaczek]

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]

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]

Thanks Chris

[Kevin Buzzard]

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

[Mario Carneiro]

I'm sure the 37 was a coincidence

[Patrick Massot]

@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]

@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]

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]

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]

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]

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