Feedback requested on PR #30962: lattice path lemmas

Stream: PR reviews

[WangYiran01]

Hi everyone

I’ve opened (PR #30962), which adds some lemmas and counts for lattice paths in the Combinatorics/Enumerative part of mathlib.

I’d really appreciate feedback on:

• whether the statements and proofs are idiomatic for mathlib,
• lemma naming or organization,
• possible generalizations or simplifications.

Thanks in advance for your time and suggestions!

[WangYiran01]

Hi all,
Following up on PR#30962 — it’s been open for a while, and I’d really appreciate any comments or suggestions when convenient.
Thanks in advance for taking a look!

[Thomas Waring]

Hi :-) my suggestions would be that a) you should prove that your inductive definition count the concrete List Step objects you define and b) these objects could be generalised a lot, to any type with Mul or Add.

I'm no expert here, but I had a go at defining a version of this, and proving the result that your function does indeed count the lattice paths

import Mathlib

@[to_additive existing]
def prodPathsTo {α} [Mul α] [One α] (gs : Set α) (a : α) : Set (List α) := {l : List α | (∀ x ∈ l, x ∈ gs) ∧ l.prod = a}

section

variable {α} [Mul α] [One α] (gs : Set α)

@[to_additive existing]
def cons_mem_prodPathsTo (g a : α) (l : List α) :
    g :: l ∈ prodPathsTo gs a ↔ g ∈ gs ∧ (∀ x ∈ l, x ∈ gs) ∧ g * l.prod = a := by
  rw [←and_assoc]
  simp [prodPathsTo]

@[to_additive existing]
theorem prodPathsTo_inj (a b : α) (h_eq : prodPathsTo gs a = prodPathsTo gs b) :
    (Set.Nonempty <| prodPathsTo gs a) → a = b
  | ⟨l, hl⟩ => by rw [←hl.2, show l.prod = b by exact (h_eq ▸ hl).2]

@[to_additive existing]
theorem prodPathsTo_union (a : α) (ha : a ≠ 1) :
    prodPathsTo gs a = ⋃ (g : gs), ⋃ (a' : {a' : α // g * a' = a}), (fun l : List α => (g : α) :: l)'' (prodPathsTo gs a') := by
  ext l
  simp only [Set.iUnion_coe_set, Set.mem_iUnion, Set.mem_image, Subtype.exists, exists_prop]
  constructor
  · intro ⟨hl_gs, hla⟩
    have : l ≠ [] := by grind [List.prod_nil]
    obtain ⟨g, l', hl'⟩ := List.exists_cons_of_ne_nil this
    have : g ∈ gs := by grind
    refine ⟨g, this, l'.prod, ?_, l', ?_, ?_⟩
    · rw [←hla, hl']
      simp
    all_goals grind [prodPathsTo]
  · intro h
    rcases h with ⟨g, hg, a', rfl, l', ⟨hl'_gs, rfl⟩, rfl⟩
    constructor
    · grind
    · exact List.prod_cons

end

def numSumPath : ℕ × ℕ → ℕ
  | ⟨0, _⟩ => 1
  | ⟨_, 0⟩ => 1
  | ⟨m + 1, n + 1⟩ => numSumPath ⟨m + 1, n⟩ + numSumPath ⟨m, n + 1⟩

theorem foo : (m : ℕ) → (n : ℕ) → numSumPath ⟨m, n⟩ = (sumPathsTo (α := ℕ × ℕ) {⟨1,0⟩, ⟨0,1⟩} ⟨m, n⟩).encard
  | 0, _ => sorry
  | _, 0 => sorry
  | m + 1, n + 1 => by
    have : sumPathsTo (α := ℕ × ℕ) {⟨1,0⟩, ⟨0,1⟩} ⟨m + 1, n + 1⟩ =
        (fun l => (⟨0, 1⟩) :: l)'' sumPathsTo (α := ℕ × ℕ) {⟨1,0⟩, ⟨0,1⟩} ⟨m + 1, n⟩ ∪
        (fun l => ⟨1, 0⟩ :: l)'' sumPathsTo (α := ℕ × ℕ) {⟨1,0⟩, ⟨0,1⟩} ⟨m, n + 1⟩ := by
      ext l
      cases l
      case nil =>
        simp [sumPathsTo, OfNat.ofNat, Zero.zero]
      case cons g l =>
        rw [cons_mem_sumPathsTo]
        have : AddLeftCancelMonoid (ℕ × ℕ) := by infer_instance
        have : (⟨m + 1, n + 1⟩ : ℕ × ℕ) = ⟨1, 0⟩ + ⟨m, n + 1⟩ := by norm_num; rw [add_comm]
        have : (⟨m + 1, n + 1⟩ : ℕ × ℕ) = ⟨0, 1⟩ + ⟨m + 1, n⟩ := by norm_num; rw [add_comm]
        constructor
        · intro ⟨hg, hl, hsum⟩
          simp only [Set.mem_union, Set.mem_image, List.cons.injEq, exists_eq_right_right]
          simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hg
          cases hg
          case inl hg =>
            refine Or.inr ⟨⟨hl, ?_⟩, Eq.symm hg⟩
            grind
          case inr hg =>
            refine Or.inl ⟨⟨hl, ?_⟩, Eq.symm hg⟩
            grind
        · grind [sumPathsTo]
    rw [this, Set.encard_union_eq, numSumPath, Nat.cast_add]
    congr
    · rw [Function.Injective.encard_image]
      · exact foo ..
      · intro l l' h
        grind
    · rw [Function.Injective.encard_image]
      · exact foo ..
      · intro l l' h
        grind
    · grind [Set.disjoint_iff]

Lastly, I would guess that the specificity of ℕ × ℕ is not the right generality to prove this result — you can play the same game for any power ℕᵏ (where the closed form is a multinomial coefficient).