Extending distance of graphs

Stream: mathlib4

[Rida Hamadani]

It turns out that it is useful to have an extended version of docs#SimpleGraph.dist, so that it returns ⊤ when the graph is disconnected (see this to see why). However, I'm not sure what's the best way to define it, does this seem reasonable?

import Mathlib.Combinatorics.SimpleGraph.Metric
import Mathlib.Data.ENat.Lattice
variable {V : Type*} (G : SimpleGraph V)

noncomputable def edist [Decidable G.Connected] (u v : V) : ℕ∞ :=
  if G.Connected then G.dist u v else ⊤

I'm worried about this definition requiring [Decidable G.Connected]. I wonder if there is a way to do this without needing it.

[Yaël Dillies]

The general pattern between finite and extended stuff is that the extended stuff is defined first, and then the finite stuff is defined in terms of it. So here it would mean defining

noncomputable def edist (u v : V) : ℕ∞ := ⨅ w : G.Walk u v, w.length
noncomputable def dist (u v : V) : ℕ := (edist u v).toNat

[Rida Hamadani]

Great!
In order to avoid a huge refactor (I'm not sure how many theorems use the old dist), is it possible to do something like:

theorem dist_def {u v : V} :
    G.dist u v = sInf (Set.range (Walk.length : G.Walk u v → ℕ)) := by -- this is the current (to be changed) definition of `dist`
  sorry

And then have lean understand this as a "second way to define dist"? Is there an annotation to be applied to the theorem that allows this?

[Yaël Dillies]

No, you would have to rewrite using that lemma in every theorem that (currently) unfolds the definition. I am pretty sure the new definition will provide a nicer API, though. You should try!

[Rida Hamadani]

I see, I will try this at evening
Do you have any APIs in mind that I can take inspiration from?

[Yaël Dillies]

The corresponding one for metric spaces. See file#Topology/MetricSpace/PseudoMetric

[Peter Nelson]

The infimum definition is definitely the right thing.

[Rida Hamadani]

But we are using infrimum in both cases, right?

[Yaël Dillies]

Yes, but no. One of them is not a proper infimum but a conditional infimum

[Kyle Miller]

In order to avoid a huge refactor

Yaël's suggestion seems right to me. Don't worry about refactoring if you need to.

Please include the dist_def theorem (perhaps as dist_eq_sInf?) using the old definition. Ideally you wouldn't use it in your refactor, instead it's just nice to have around.

[Rida Hamadani]

I've finally managed to prove dist_eq_sInf when G.dist u v = 0, but something feels wrong, I wanna check whether the proof is supposed to be this annoying, or am I doing something wrong.
Note that I've proved the helper ENat lemmas in mathlib4#14043, and I feel annoyed by the proofs in that PR too. They feel overcomplicated for such simple statements!

import Mathlib.Combinatorics.SimpleGraph.Connectivity
import Mathlib.Data.ENat.Lattice

namespace ENat

variable {m n : ℕ∞} {s : Set ℕ∞}

lemma lt_one_iff_eq_zero : n < 1 ↔ n = 0 := by
  rw [← not_le, one_le_iff_ne_zero.not, not_not]

lemma sInf_eq_zero : sInf s = 0 ↔ 0 ∈ s := by
  refine ⟨fun h ↦ ?_, inf_eq_bot_of_bot_mem⟩
  rw [← bot_eq_zero, sInf_eq_bot] at h
  obtain ⟨n , hn₁, hn₂⟩  := h 1 (by decide)
  exact lt_one_iff_eq_zero.mp hn₂ ▸ hn₁

end ENat

namespace SimpleGraph

variable {V : Type*} (G : SimpleGraph V)

noncomputable def edist (u v : V) : ℕ∞ :=
  ⨅ w : G.Walk u v, w.length

noncomputable def dist (u v : V) : ℕ :=
  (G.edist u v).toNat
#align simple_graph.dist SimpleGraph.dist

variable {G} {u v : V}

lemma dist_eq_sInf_of_dist_eq_zero (h : G.dist u v = 0) :
    G.dist u v = sInf (Set.range (Walk.length : G.Walk u v → ℕ)) := by
  rw [h]
  rw [dist, ENat.toNat_eq_zero, edist] at h
  symm
  rw [Nat.sInf_eq_zero]
  cases' h with h h
  · rw [iInf, ENat.sInf_eq_zero] at h
    apply Or.inl
    simp_all
  · rw [iInf, sInf_eq_top] at h
    apply Or.inr
    by_contra x
    rw [Set.range_eq_empty_iff, not_isEmpty_iff] at x
    obtain ⟨x, hx⟩ := x
    · simp_all [forall_const]
    · rename_i q p
      have : G.Walk u v := .cons q p
      aesop

[Yaël Dillies]

Surely you should case on whether G.edist u v = ∞ (or any equivalent statement)?

[Yaël Dillies]

If it's ∞, then the sInf is zero. If it's finite, then the ENat-valued and Nat-valued sInfs agree.

[Yaël Dillies]

Also isn't dist_eq_sInf_of_dist_eq_zero a weird statement?

[Rida Hamadani]

I will try doing that, thanks!

[Rida Hamadani]

Yaël Dillies said:

Also isn't dist_eq_sInf_of_dist_eq_zero a weird statement?

I do not plan to include it in the API, it is just that I found dist_eq_sInftoo hard so I decided to start with something simpler.

[Yaël Dillies]

Yaël Dillies said:

Surely you should case on whether G.edist u v = ∞ (or any equivalent statement)?

I believe this should be your general strategy when trying to reduce the extended statement to the corresponding finite one

[Yaël Dillies]

The annoying part in that strategy will always be relating the proper no-junk extended operations to the junkful finite ones. Here, that will be incarnated by goals of the form ENat.toNat (⨅ i, f i) = ⨅ i, ENat.toNat (f i)

[Rida Hamadani]

Yes! In the above lemma, this boils down to proving that G.dist u v = ⨅ w : G.Walk u v, w.length, which is the iInf version of the lemma.

[Rida Hamadani]

I would like to prove the following statement about edist:

import Mathlib.Combinatorics.SimpleGraph.Connectivity
import Mathlib.Data.ENat.Lattice

namespace SimpleGraph

variable {V : Type*} (G : SimpleGraph V)

noncomputable def edist (u v : V) : ℕ∞ :=
  ⨅ w : G.Walk u v, w.length

variable {G} {u v : V}

lemma edist_eq_top_of_not_reachable (h : ¬G.Reachable u v) : G.edist u v = ⊤ := by
  sorry

Here is the idea of the prove:
Since u and v are not reachable, there is no walks between them, thus w : G.Walk u v, w.length is ∅, which means that its infrimum is top by docs#sInf_empty

[Rida Hamadani]

I'm having trouble translating this argument to lean, I don't know how to say "there is no walk between u and v since they are not reachable", and I don't know how to turn this into "there is no length of walks between them either".
Can you help me please?

[Kyle Miller]

Here's an unrefined "stream-of-conciousness" proof, where I had a feeling if I did simp after unfolding edist it would be amenable to simp:

lemma edist_eq_top_of_not_reachable (h : ¬G.Reachable u v) : G.edist u v = ⊤ := by
  unfold edist
  simp only [iInf_eq_top, ENat.coe_ne_top] -- found via `simp?`
  contrapose! h
  obtain ⟨p, _⟩ := h
  use p

[Kyle Miller]

This one is closer to your idea:

lemma edist_eq_top_of_not_reachable (h : ¬G.Reachable u v) : G.edist u v = ⊤ := by
  rw [reachable_iff_nonempty_univ, ← Set.nonempty_iff_univ_nonempty, not_nonempty_iff] at h
  simp [edist]

A trick here is that simp [edist] can pick up on the resulting IsEmpty (G.Walk u v) hypothesis since it's an instance.

[Kyle Miller]

Maybe it's worth having a helper lemma for ¬G.Reachable u v ↔ IsEmpty (G.Walk u v), to replace that rw?

[Rida Hamadani]

Thank you very much!
Kyle Miller said:

Maybe it's worth having a helper lemma for ¬G.Reachable u v ↔ IsEmpty (G.Walk u v), to replace that rw?

I think this is nice to have in the connectivity file, I'll add it.

[Rida Hamadani]

#14315

[Rida Hamadani]

Kyle Miller said:

A trick here is that simp [edist] can pick up on the resulting IsEmpty (G.Walk u v) hypothesis since it's an instance.

One more question, how did Lean understand that this is an instance, as opposed to just a normal Prop?

[Kyle Miller]

It's because docs#IsEmpty is defined as a class

[Rida Hamadani]

Done! #14582 :cat:

[Rida Hamadani]

I'm trying to prove the instance PseudoMetricSpace V, but when I do this:

instance : PseudoMetricSpace V where
  dist := G.dist

I get the error:

type mismatch
  G.dist
has type
  V → V → ℕ : Type u_1
but is expected to have type
  V → V → ℝ : Type u_1

Is coercing dist to ℝ an acceptable way to solve this issue? And if so, how to do so? Because (G.dist : V → V → ℝ) is not coercing.

[Ruben Van de Velde]

Probably dist x y := (G.dist x y : Real)

[Adam Topaz]

You probably don’t even need to write : Real

[Adam Topaz]

Coercions work on elements, not codomains of functions.

[Kyle Miller]

This instance won't work, since V does not determine G

[Kyle Miller]

You could make a type abbreviation like

def Verts (G : SimpleGraph V) := V

and then define

instance : PseudoMetricSpace (Verts G) where
  ...

But then you have to be very careful to always write (u v : Verts G) rather than (u v : V).

[Rida Hamadani]

I see, do you think it is worth including that or is it useless? Because I rarely see Verts G being used.

[Rida Hamadani]

This is giving weird errors, I'm not sure what's the problem here.

import Mathlib.Combinatorics.SimpleGraph.Metric
import Mathlib.Topology.MetricSpace.Pseudo.Defs

variable (V : Type*) (G : SimpleGraph V)

def Verts (G : SimpleGraph V) := V

instance : PseudoMetricSpace (Verts G) where
  dist x y := (G.dist x y : ℝ)
  dist_self := sorry
  dist_comm := sorry
  dist_triangle := sorry
  edist_dist := sorry
  toUniformSpace := sorry
  uniformity_dist := sorry
  toBornology := sorry
  cobounded_sets := sorry

[Edward van de Meent]

the problem is that Verts in your definition has 2 explicit variables.
the fix is to use this:

variable {V} in
def Verts (_ : SimpleGraph V):= V

alternatively, you can do this:

import Mathlib.Combinatorics.SimpleGraph.Metric
import Mathlib.Topology.MetricSpace.Pseudo.Defs

def Verts {V : Type*} (_ : SimpleGraph V) := V
variable (V : Type*) (G : SimpleGraph V)

...

[Rida Hamadani]

Both suggestions are still giving the same error:

compiler IR check failed at 'instPseudoMetricSpaceVerts._rarg._lambda_1', error: unknown declaration 'SimpleGraph.dist'

At instance : PseudoMetricSpace (Verts G) where.

[Edward van de Meent]

i think the problem there is that the compiler doesn't know if G.dist is noncomputable or not, in general. I believe this depends on wether the field G.Adj is decidable (and possibly equality in V too), meaning that in general this will be noncomputable. The only fix i know for this would be to add noncomputable before the instance, although there might be another solution i don't know here....

[Kyle Miller]

Yeah, add noncomputable before instance since the distance function can't be compiled.

[Kyle Miller]

do you think it is worth including that or is it useless?

I would proceed with caution and treat this as a good exercise for yourself.

Another option is to make a definition that creates a Quiver from a SimpleGraph, since I think over there you get some of these metric spaces instances. You could then locally do let inst := G.toQuiver to locally use the quiver instance.

[Rida Hamadani]

One of the TODOs in the Metric.lean file is "Provide an additional computable version of SimpleGraph.dist for when G is connected."

Perhaps doing this is a third option that kills two birds with one stone?

[Rida Hamadani]

But I wonder how we can have computable distance, and if that's possible at all.
Can I somehow provide lean with an algorithm that computes the distance and this will make it computable?

[Kyle Miller]

I think the TODO is saying "implement breadth-first search". You need some additional assumptions on G for that to work though. I think it can either be (1) G is connected and locally finite or (2) G is finite.

[Kyle Miller]

Breadth-first search is useful in algorithms, but I'm not sure how useful it is to complete this TODO item (without a motivating formalization project, it's hard to know what you'd want out of such an algorithm).

[Kyle Miller]

Rida Hamadani said:

Perhaps doing this is a third option that kills two birds with one stone?

If you're thinking about how it removes the need for noncomputable, that's not something we should do. It is perfectly fine for the instance to be noncomputable.

[Kyle Miller]

One of the problems with making mathematics definitions computable is that, for generic data structures like a SimpleGraph, what can often happen is that the result is a merely computable definition. It's inefficient in practice since it isn't able to make use of the specific features of more efficient data structures.

[Kyle Miller]

Oh, I forgot I basically already implemented breadth-first search for finite graphs as part of the implementation of the docs#SimpleGraph.instDecidableConnected instance. It's a really badly implemented algorithm, but it works for small enough graphs. It's also not classic breadth-first search. It enumerates all walks up to a particular length, which is usually exponential time.

[Rida Hamadani]

I'm referencing this TODO item, it is not clear to me how it is referencing breadth-first search. My first thought was using Dijkistra's algorithm instead.

[Edward van de Meent]

Kyle Miller said:

One of the problems with making mathematics definitions computable is that, for generic data structures like a SimpleGraph, what can often happen is that the result is a merely computable definition. It's inefficient in practice since it isn't able to make use of the specific features of more efficient data structures.

so then... best practice would be to not change the definition, but provide a separate definition/implementation which gives provably the same result provided some conditions hold? (and then possibly make a tactic to do this efficient calculation?)

[Rida Hamadani]

Kyle Miller said:

If you're thinking about how it removes the need for noncomputable, that's not something we should do. It is perfectly fine for the instance to be noncomputable.

I see! If that's the case, I'll prove it as a noncomputable instance for now, I have no project in mind to develop this, I am doing this for the sake of completion (it feels like something is missing when we have a distance but no metric space).

[Rida Hamadani]

Edward van de Meent said:

so then... best practice would be to not change the definition, but provide a separate definition/implementation which gives provably the same result provided some conditions hold? (and then possibly make a tactic to do this efficient calculation?)

This is very nice! Do you have any examples in mind where something like this was done so I can learn from them?

[Rida Hamadani]

The MetricSpace instance is added in #14715, it depends on #14582 is in order to use the new definition and API of dist.
The linter fails because apparently instances cannot have named hypotheses (I didn't know this). What is the proper way to deal with this? I thought that due to docs#SimpleGraph.instDecidableConnected which Kyle mentioned above, lean should be able to infer connectivity. Did I misunderstand something?

[Kyle Miller]

Rida Hamadani said:

I'm referencing this TODO item, it is not clear to me how it is referencing breadth-first search. My first thought was using Dijkistra's algorithm instead.

Yeah, I understood which todo item it was :-). It comes from this PR, and although it's been a couple years, I'm pretty sure I was thinking about breadth-first search.

Dijkstra's algorithm is a generalization of breadth-first search when there is a weighted graph, but the dist measure under consideration is for unweighted graphs.

[Kyle Miller]

I left a comment on #14715, but I don't think mathlib should have this Verts G definition or the metric space structure on Verts G. At best, we might consider it if there's a project that proves it's a good idea, but there are issues with having both Verts G and V to refer to the same type without developing a bunch of boilerplate.

[Rida Hamadani]

Surprisingly, lean accepted the instance without defining Verts, I pushed the commit to #14715.
The CI still doesn't pass but it is due to something else (it is the issue I was talking about above regarding instances that take a hypothesis).

[Kyle Miller]

The lint output explains the issue:

/- The `impossibleInstance` linter reports:
SOME INSTANCES HAVE ARGUMENTS THAT ARE IMPOSSIBLE TO INFER
These are arguments that are not instance-implicit and do not appear in
another instance-implicit argument or the return type. -/

From V itself it can't determine what G should be. It's not about named hypotheses, but about having hypotheses at all.

Even if this instance passed the linter, it's not a good one since it's trying to put a metric space structure on V from some graph G, and instances are supposed to be canonical. Each G gives a different metric space structure, so it fails canonicity.

This is a reason why it's not a good idea having such an instance.

[Kyle Miller]

The Verts G idea solves the linter problem, since it puts G into the term. You can go further and have Verts G hG where hG : Connected G, if you want to experiment (not for the PR though)

[Rida Hamadani]

Ahh, that makes sense. Thank you for explaining.
It turns out that this will take a lot of effort for something that probably won't be useful, so I will close #14715, but I'll keep the idea of building a bridge to Quiver in mind for the future.
I learnt a lot from this nonetheless! :big_smile:

[Kyle Miller]

Even if it's not an instance, it's possible to have a def

[Kyle Miller]

There's also a question of whether there ought to be a class that says a function is a metric, rather than requiring a type to be equipped with a metric space structure

[Rida Hamadani]

I've found examples where def was used to prove metric spaces, such as docs#instL2OpMetricSpace
Do you think it is okay if we did this in our case?

[Yakov Pechersky]

You might also be interested in docs#MetricSpace.ofDistTopology

[Jeremy Tan]

@Kyle Miller how does this look like for breadth-first search?

import Mathlib.Data.Fintype.Basic

variable {α : Type*} [Fintype α] [DecidableEq α] (r : α → α → Prop) [DecidableRel r]

def elemsAtDepthAux (p : Finset α × Finset α) : Finset α × Finset α :=
  let k := p.2.filter (fun b ↦ ∃ a ∈ p.1, r a b)
  (k, p.2 \ k)

/-- Elements at distance `d` from the given set of roots. -/
def elemsAtDepth (roots : Finset α) (d : ℕ) : Finset α :=
  ((elemsAtDepthAux r)^[d] (roots, rootsᶜ)).1

[Jeremy Tan]

Or how about this? Is it usable and how can it be neatened up?

import Mathlib.Data.ENat.Basic
import Mathlib.Data.Fintype.Basic

variable {α : Type*} (r : α → α → Prop) [DecidableRel r]

def bfsRun : List (α × ℕ∞) × List (α × ℕ∞) × List α → List (α × ℕ∞) × List (α × ℕ∞) × List α
  | (res, [], cant_reach) => ((cant_reach.map (·, ⊤) ++ res).reverse, [], [])
  | (res, v :: queue, not_yet) =>
    let ll := not_yet.partition (r v.1)
    bfsRun (v :: res, queue ++ ll.1.map (·, v.2 + 1), ll.2)
termination_by x => x.2.1.length + x.2.2.length
decreasing_by
  simp_wf
  change queue.length + (List.filter (fun b ↦ decide (r v.1 b)) not_yet).length +
    (List.filter (fun b ↦ !decide (r v.1 b)) not_yet).length < _
  rw [add_assoc, ← List.length_eq_length_filter_add]; omega

def bfs (roots searchSpace : List α) : List (α × ℕ∞) :=
  (bfsRun r ([], roots.map (·, 0), searchSpace)).1

def rr (a b : Fin 10) : Prop := (b + 10 - a) % 10 = 7

instance : DecidableRel rr := inferInstanceAs <| DecidableRel fun a b ↦ (b + 10 - a) % 10 = 7

#eval bfs rr [0] (List.range 10).tail
/-
[(0, some 0),
 (7, some 1),
 (4, some 2),
 (1, some 3),
 (8, some 4),
 (5, some 5),
 (2, some 6),
 (9, some 7),
 (6, some 8),
 (3, some 9)]
-/

[Jeremy Tan]

hey, this works

variable {α : Type*} [Fintype α] [DecidableEq α] (r : α → α → Prop) [DecidableRel r]

def elemsAtDepthAux (p : Finset α × Finset α) : Finset α × Finset α :=
  let k := p.2.filter (fun b ↦ ∃ a ∈ p.1, r a b)
  (k, p.2 \ k)

/-- Elements at depth `d` relative to the given set of roots. -/
def elemsAtDepth (roots : Finset α) (d : ℕ) : Finset α :=
  ((elemsAtDepthAux r)^[d] (roots, rootsᶜ)).1

def collatz (a b : Fin 100) : Prop := 3 * b.1 + 1 = a.1 ∨ 2 * a.1 = b.1

instance : DecidableRel collatz :=
  inferInstanceAs <| DecidableRel fun (a b : Fin 100) ↦ 3 * b.1 + 1 = a.1 ∨ 2 * a.1 = b.1

#eval (elemsAtDepth collatz {1} 0).sort (· ≤ ·) -- [1]
#eval (elemsAtDepth collatz {1} 1).sort (· ≤ ·) -- [0, 2]
#eval (elemsAtDepth collatz {1} 2).sort (· ≤ ·) -- [4]
#eval (elemsAtDepth collatz {1} 3).sort (· ≤ ·) -- [8]
#eval (elemsAtDepth collatz {1} 4).sort (· ≤ ·) -- [16]
#eval (elemsAtDepth collatz {1} 5).sort (· ≤ ·) -- [5, 32]
#eval (elemsAtDepth collatz {1} 6).sort (· ≤ ·) -- [10, 64]
#eval (elemsAtDepth collatz {1} 7).sort (· ≤ ·) -- [3, 20, 21]
#eval (elemsAtDepth collatz {1} 8).sort (· ≤ ·) -- [6, 40, 42]
#eval (elemsAtDepth collatz {1} 9).sort (· ≤ ·) -- [12, 13, 80, 84]
#eval (elemsAtDepth collatz {1} 10).sort (· ≤ ·) -- [24, 26]
#eval (elemsAtDepth collatz {1} 11).sort (· ≤ ·) -- [48, 52]
#eval (elemsAtDepth collatz {1} 12).sort (· ≤ ·) -- [17, 96]
#eval (elemsAtDepth collatz {1} 13).sort (· ≤ ·) -- [34]
#eval (elemsAtDepth collatz {1} 14).sort (· ≤ ·) -- [11, 68]
#eval (elemsAtDepth collatz {1} 15).sort (· ≤ ·) -- [22]
#eval (elemsAtDepth collatz {1} 16).sort (· ≤ ·) -- [7, 44]

end