Zulip Chat Archive

Stream: new members

Topic: Zmod37 tutorial


view this post on Zulip Joseph Corneli (Apr 04 2019 at 13:39):

@Kevin Buzzard the tutorial you added to mathlib a few days ago is very nice. Great idea to have some interactive tutorials like this in the repo, in my opinion. Link so others can find it: https://github.com/leanprover-community/mathlib/blob/master/docs/tutorial/Zmod37.lean

view this post on Zulip Joseph Corneli (Apr 04 2019 at 13:42):

Is there a way to get Lean to be more explicit about the goal? E.g., here, the goal is described in comments:

theorem cong_mod_symm : symmetric (cong_mod37) :=
begin
  intros a b H,
  -- H : cond_mod37 a b
  cases H with l Hl,
  -- Hl : l * 37 = (b - a)
  -- Goal is to find an integer k with k * 37 = a - b
  use -l,
  simp [Hl],
end

But at that point in the file my Goals buffer just has the goal down as ⊢ cong_mod37 b a. This means that use -l in the next line comes a bit out of the blue.

view this post on Zulip Johan Commelin (Apr 04 2019 at 13:54):

You could try unfold cong_mod37

view this post on Zulip Joseph Corneli (Apr 04 2019 at 13:58):

@Johan Commelin oh, yeah that's nicer

view this post on Zulip Joseph Corneli (Apr 04 2019 at 14:18):

I wonder if a bit more commenting/cross referencing would help. For example to explain the use of cases, above.

-- "Cases can be used to decompose any element of an inductively defined type", TPIL 5.3

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 19:01):

Joe -- feel free to PR more clarifications on that tutorial. @Patrick Massot I never thanked you for merging it. I think the community might like more of this sort of stuff.


Last updated: May 09 2021 at 23:10 UTC