separate proofs or inline?

Stream: new members

[Jakub Nowak]

Which of the two approaches do you think is better? Writing implementation and proving its desired properties separately, or to have it together?

In the code I've made namespace Approach1 and namespace Approach2.
In the 2nd approach there's a function odd_cycle_of_odd_walk : (p : G.walk u u) → p.length.bodd → Σ v : V, { p : G.Walk v v // p.IsCycle ∧ p.length.bodd } which extracts odd cycle from an odd-length walk.
In the 1st approach odd_cycle_of_odd_walk signature is odd_cycle_of_odd_walk : G.Walk u u → Σ v : V, G.Walk v v. The function does the same as in the 2nd approach, but the proof of the desired property is in a separate theorem odd_cycle_of_odd_walk.is_odd_cycle : (p : G.walk u u) → p.length.bodd → (odd_cycle_of_odd_walk p).snd.IsCycle ∧ (odd_cycle_of_odd_walk p).snd.length.bodd. (Well, it isn't cause it's sorry and I wasn't able to do it)

import Mathlib

open SimpleGraph
open Walk

variable {V : Type u} {G : SimpleGraph V}


namespace Approach1

private def odd_cycle_of_odd_walk_step [DecidableEq V] {u v : V}
    (pref : G.Walk u v) (suf : G.Walk v u) :
    Σ w : V, G.Walk w w :=
  match suf with
  | .nil => ⟨u, Walk.nil⟩ -- unreachable
  | .cons' v w u hAdj suf' =>
    if h : w ∈ pref.support then
      let pref_pre_part : G.Walk u w := pref.takeUntil w h
      let pref_cycle_part : G.Walk w v := pref.dropUntil w h
      let cycle : G.Walk v v := Walk.cons hAdj pref_cycle_part
      if cycle.length.bodd then
        ⟨v, cycle⟩
      else
        odd_cycle_of_odd_walk_step pref_pre_part suf'
    else
      odd_cycle_of_odd_walk_step (Walk.concat pref hAdj) suf'

private def odd_cycle_of_odd_walk [DecidableEq V] (p : G.Walk u u) : Σ v : V, G.Walk v v :=
  odd_cycle_of_odd_walk_step Walk.nil p

theorem odd_cycle_of_odd_walk.is_odd_cycle [DecidableEq V] (p : G.Walk u u) (hOdd : p.length.bodd) :
    (odd_cycle_of_odd_walk p).snd.IsCycle ∧ (odd_cycle_of_odd_walk p).snd.length.bodd := by
  sorry

end Approach1


namespace Approach2

theorem SimpleGraph.Walk.cons_isCycle_of_path_length_ne_1 {u v : V}
    (h : G.Adj u v) (p : G.Walk v u) (hp : p.IsPath) (hl : p.length ≠ 1) :
    (cons h p).IsCycle := by
  rw [cons_isCycle_iff]
  apply And.intro
  · assumption
  · intro hh
    apply hl
    clear hl
    cases p with
    | nil => contradiction
    | cons hAdj rest =>
      rename_i w
      rw [cons_isPath_iff] at hp
      obtain ⟨hp₀, hp₁⟩ := hp
      rw [edges_cons, List.mem_cons] at hh
      rw [length_cons, Nat.add_eq_right]
      obtain hh | hh := hh
      · have : u = w := by
          rw [Sym2.eq, Sym2.rel_iff', Prod.swap_prod_mk, Prod.mk.injEq, Prod.mk.injEq] at hh
          obtain hh | hh := hh <;> simp [hh]
        subst this
        rwa [length_eq_zero_iff, ←isPath_iff_eq_nil]
      · have : v ∈ rest.support := snd_mem_support_of_mem_edges rest hh
        contradiction


private def odd_cycle_of_odd_walk_step [DecidableEq V] {u v : V}
    (pref : G.Path u v) (suf : G.Walk v u) (hOdd : (pref.val.append suf).length.bodd) :
    Σ w : V, { p : G.Walk w w // p.IsCycle ∧ p.length.bodd } :=
  let ⟨pref, hPref⟩ := pref
  match suf with
  | .nil => by
    exfalso
    simp only [] at hOdd
    simp_all
  | .cons' v w u hAdj suf' =>
    have hOdd : pref.length.bodd = suf'.length.bodd := by simp_all
    if h : w ∈ pref.support then
      let pref_pre_part : G.Walk u w := pref.takeUntil w h
      have : pref_pre_part.IsPath := hPref.takeUntil h
      let pref_cycle_part : G.Walk w v := pref.dropUntil w h
      have : pref_cycle_part.IsPath := hPref.dropUntil h
      let cycle : G.Walk v v := Walk.cons hAdj pref_cycle_part
      -- `cycle` is not necessarily a cycle here, it might have a length of 2.
      if _ : cycle.length.bodd then
        have : cycle.IsCycle := by
          apply SimpleGraph.Walk.cons_isCycle_of_path_length_ne_1
          · assumption
          · intro
            subst cycle
            simp_all
        ⟨v, cycle, ‹cycle.IsCycle›, ‹cycle.length.bodd›⟩
      else
        odd_cycle_of_odd_walk_step ⟨pref_pre_part, ‹pref_pre_part.IsPath›⟩ suf' (by
          simp only []
          subst cycle
          have : pref = pref_pre_part.append pref_cycle_part := Eq.symm (Walk.take_spec pref h)
          rw [this] at hOdd
          simp_all)
    else
      let next_pref : G.Walk u w := pref.concat hAdj
      have : next_pref.IsPath := hPref.concat h hAdj
      odd_cycle_of_odd_walk_step ⟨next_pref, ‹next_pref.IsPath›⟩ suf' (by
        simp only []
        subst next_pref
        simpa)

private def odd_cycle_of_odd_walk [DecidableEq V] (p : G.Walk u u) (hOdd : p.length.bodd) :
    Σ v : V, { p : G.Walk v v // p.IsCycle ∧ p.length.bodd } :=
  odd_cycle_of_odd_walk_step Path.nil p (by simpa)

end Approach2

[Kyle Miller]

I think the first approach is usually preferable.

Interleaving proofs with the definition makes it hard to read, and it can lead to some more complex dependent types that are harder to work with.

Also, you're going to have a lot more lemmas about the definition. Why encode just these couple lemmas (IsCycle and odd length) into the definition and not others?

[Jakub Nowak]

Kyle Miller said:

Also, you're going to have a lot more lemmas about the definition.

Well, not really. In this case it's private def used as a lemma for an actual theorem.

[Kyle Miller]

You're confident that no one would ever find use for this definition in other contexts?

People have used docs#SimpleGraph.Walk.bypass and its supporting takeUntil/dropUntil even though they were only for proving that if there's a walk between two vertices there's a path between them.

[Jakub Nowak]

I see. And bypass is indeed defined as G.Walk u v → G.Walk u v.