Feedback on Konig's lemma proof

Stream: new members

[One Happy Fellow]

Hi everyone, I've formalised Konig's lemma as an exercise while learning lean, here's the code: https://github.com/happyfellow-one/lean-and-mean/blob/master/LeanAndMean/KonigLemma.lean

I'd be grateful if anyone found a moment to skim through my code and gave me some feedback on it: particularly, I feel rather weak with my tactics knowledge so I'd appreciate any tips. Thanks in advance!

[Mirek Olšák]

I find it a bit non-standard to do definitions by tactics. I would rather phrase for example the main statement as theorem (there exists).

[One Happy Fellow]

@Mirek Olšák to check if I get it right, you're saying that the last statement should return Nonempty (InfiniteWalk tree) and I'd need to change def to theorem, is that what you meant?

[Mirek Olšák]

Yes, make it a Prop with Nonempty, and change it to theorem. Alternatively, you could skip the definition of InfiniteWalk, and inline it with ∃ node : ℕ → tree.V, ...

[Ruben Van de Velde]

This also works, btw:

noncomputable
def konigLemma'
    (tree : RootedLocallyFiniteTree) :
    InfiniteWalk tree where
  node n := (konig_node tree n).1
  properWalk i := by
    let node (n) := (konig_node tree n).1
    suffices : node (i+1) ∈ tree.children (node i) ∧ (tree.descendants (node (i+1))).Infinite
    · exact this.1
    simp [node, konig_node]
    apply Classical.choose_spec
      (p := (fun x => x ∈ tree.children (node i) ∧ (tree.descendants x).Infinite))

[One Happy Fellow]

@Ruben Van de Velde oh wow, I didn't know you could do that! Thanks.

[Ruben Van de Velde]

But maybe this is more readable:

noncomputable
def konigNode
    (tree : RootedLocallyFiniteTree)
    (n : ℕ) : Σ' v, (tree.descendants v).Infinite :=
  match n with
  | .zero => ⟨tree.root, tree.infiniteDescendants⟩
  | .succ n =>
    let ⟨prev, hprev⟩ : Σ' prev, (tree.descendants prev).Infinite := konigNode tree n
    have inf : ∃ w ∈ tree.children prev, (tree.descendants w).Infinite :=
      infinite_descendants_step tree prev hprev
    ⟨Classical.choose inf, (Classical.choose_spec inf).2⟩

lemma konigNode_zero (tree : RootedLocallyFiniteTree) :
    konigNode tree 0 = ⟨tree.root, tree.infiniteDescendants⟩ := rfl

lemma konigNode_add_one_mem (tree : RootedLocallyFiniteTree) :
    (konigNode tree (n + 1)).1 ∈ tree.children (konigNode tree n).1 := by
  simp [konigNode]
  generalize_proofs h
  exact (Classical.choose_spec h).1

lemma infinite_konigNode_add_one (tree : RootedLocallyFiniteTree) :
    (tree.descendants (konigNode tree (n + 1)).1).Infinite := by
  -- Or exact (konigNode tree (n + 1)).2
  simp [konigNode]
  generalize_proofs h
  exact (Classical.choose_spec h).2

noncomputable
def konigLemma'
    (tree : RootedLocallyFiniteTree) :
    InfiniteWalk tree where
  node n := (konigNode tree n).1
  properWalk i := konigNode_add_one_mem tree