Zulip Chat Archive

Stream: new members

Topic: symmetry of congruence mod 37


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Nicholas Siedlaczek (Dec 06 2018 at 21:52):

Thanks Chris

view this post on Zulip Kevin Buzzard (Dec 06 2018 at 22:50):

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

view this post on Zulip Mario Carneiro (Dec 06 2018 at 22:59):

I'm sure the 37 was a coincidence

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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]

view this post on Zulip 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