How to learn "idiomatic" lean?

Stream: general

[Theo Sandstrom]

I have just begun to learn Lean, and I am struggling to get a good idea of what "idiomatic" lean should look like. The basic issue, in my mind, is that there seem to be many totally different ways to yield a proof of the same claim. For example, browsing Mathlib, I came upon the following lemma:

lemma «exists» : ∃ p, CharP R p :=
  letI := Classical.decEq R
  by_cases
    (fun H : ∀ p : ℕ, (p : R) = 0 → p = 0 =>
      ⟨0, ⟨fun x => by rw [zero_dvd_iff]; exact ⟨H x, by rintro rfl; simp⟩⟩⟩)
    fun H =>
    ⟨Nat.find (not_forall.1 H),
      ⟨fun x =>
        ⟨fun H1 =>
          Nat.dvd_of_mod_eq_zero
            (by_contradiction fun H2 =>
              Nat.find_min (not_forall.1 H)
                (Nat.mod_lt x <|
                  Nat.pos_of_ne_zero <| not_of_not_imp <| Nat.find_spec (not_forall.1 H))
                (not_imp_of_and_not
                  ⟨by
                    rwa [← Nat.mod_add_div x (Nat.find (not_forall.1 H)), Nat.cast_add,
                      Nat.cast_mul,
                      of_not_not (not_not_of_not_imp <| Nat.find_spec (not_forall.1 H)),
                      zero_mul, add_zero] at H1,
                    H2⟩)),
          fun H1 => by
          rw [← Nat.mul_div_cancel' H1, Nat.cast_mul,
            of_not_not (not_not_of_not_imp <| Nat.find_spec (not_forall.1 H)),
            zero_mul]⟩⟩⟩

In an effort to understand this proof, I decided to walk through it step by step and rewrite it, and I found that this version feels much more readable to me:

lemma «exists» : ∃ p, CharP R p :=
  letI := Classical.decEq R
  by
    by_cases H : ∀ (p : ℕ), (p : R) = 0 → p = 0
    . exists 0; constructor; intro x
      rw [zero_dvd_iff]; constructor; exact H x; rintro rfl; simp
    . push_neg at H
      let p := Nat.find H
      have Hp : (p : R) = 0 := (Nat.find_spec H).left
      have Hpnz : p ≠ 0 := (Nat.find_spec H).right
      have Hpmin : ∀ {m : ℕ}, m < p → ¬((m : R) = 0 ∧ m ≠ 0) := @Nat.find_min _ _ H
      exists p; constructor; intro x; constructor
      . intro Hx
        apply Nat.dvd_of_mod_eq_zero
        have := Hpmin (Nat.mod_lt x (Nat.pos_of_ne_zero Hpnz))
        push_neg at this
        apply this
        rwa [← Nat.mod_add_div x p, Nat.cast_add, Nat.cast_mul, Hp, zero_mul, add_zero] at Hx
      . rintro ⟨k, Hdiv⟩; rw [Hdiv, Nat.cast_mul, Hp, zero_mul]

Is there a preference in the Mathlib codebase to avoid the tactical style where possible? Or does this just come down to the personal preference of the individual who proved this lemma? In general, are there any particularly good resources for learning to write more idiomatic proofs?

Edit: I hope this is an acceptable place for this question; please let me know if not.

[Ruben Van de Velde]

I would certainly not consider the code you quoted from mathlib to be idiomatic; I'd say your rewritten code is more so

[Ruben Van de Velde]

I'd probably have used refine for the places where you put multiple tactics on one line, but that's more taste than anything else

[Patrick Massot]

I am pretty sure I can guess who wrote the original version.

[Ruben Van de Velde]

Who might that be?

[Patrick Massot]

And my guess was correct. Note the date in that commit answers many of your questions. This is code from 2018 that was ported to Lean 4 without style changes. Everything was very experimental in 2018 and there was no notion of idiomatic Mathlib code at that time.

[Theo Sandstrom]

@Ruben Van de Velde Out of curiosity, what would those lines look like using refine?

[Ruben Van de Velde]

I'd write it like this:

lemma «exists» : ∃ p, CharP R p := by
  classical
  by_cases H : ∀ (p : ℕ), (p : R) = 0 → p = 0
  · refine ⟨0, ⟨fun x => ?_⟩⟩
    rw [zero_dvd_iff]; constructor; exact H x; rintro rfl; simp
  · push_neg at H
    let p := Nat.find H
    have Hp : (p : R) = 0 := (Nat.find_spec H).left
    have Hpnz : p ≠ 0 := (Nat.find_spec H).right
    have Hpmin : ∀ {m : ℕ}, m < p → ¬((m : R) = 0 ∧ m ≠ 0) := @Nat.find_min _ _ H
    refine ⟨p, ⟨fun x => ⟨?_, ?_⟩⟩⟩
    · intro Hx
      apply Nat.dvd_of_mod_eq_zero
      have := Hpmin (Nat.mod_lt x (Nat.pos_of_ne_zero Hpnz))
      push_neg at this
      apply this
      rwa [← Nat.mod_add_div x p, Nat.cast_add, Nat.cast_mul, Hp, zero_mul, add_zero] at Hx
    · rintro ⟨k, Hdiv⟩
      rw [Hdiv, Nat.cast_mul, Hp, zero_mul]

[Kyle Miller]

Here's another way to write that first case, for comparison:

  . use 0
    simp (config := {contextual := true}) [charP_iff, zero_dvd_iff, iff_def, H]

[Notification Bot]

3 messages were moved from this topic to #general > simp contextual tactic syntax by Joachim Breitner.

[Ruben Van de Velde]

Oh, I overlooked that line. If I didn't go for Kyle's approach, I'd probably split it as

  · refine ⟨0, ⟨fun x => ?_⟩⟩
    rw [zero_dvd_iff]
    constructor
    · exact H x
    · rintro rfl
      simp
```µ

[Theo Sandstrom]

A few follow-ups: is the line defining Hpmin reasonable? It felt ugly as I was writing it, and took some wrestling to get it to work. Also, is it generally preferred to use simp or rw with a long list of lemmas?

[Kyle Miller]

Regarding later, here's a sequence you can use:

      specialize Hpmin (Nat.mod_lt x (Nat.pos_of_ne_zero Hpnz))
      push_neg at Hpmin
      apply Hpmin

It doesn't save any lines, but it replaces Hpmin in the local context.

[Kyle Miller]

is the line defining Hpmin reasonable?

For the four lines starting from let p, I feel like there ought to be a single-line have ⟨p, ⟨Hp, Hpnz⟩, Hpmin⟩ := ??? H, but I'm not sure that theorem exists yet.

[Yaël Dillies]

I would not indent the second goal produced by by_cases since it is clearly the main one.