Zmod37 tutorial

Stream: new members

[Joseph Corneli]

@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

[Joseph Corneli]

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.

[Johan Commelin]

You could try unfold cong_mod37

[Joseph Corneli]

@Johan Commelin oh, yeah that's nicer

[Joseph Corneli]

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

[Kevin Buzzard]

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.