Finite sum notation in lean4:

Stream: lean4

[Shreyas Srinivas]

In the repository referenced here: https://leanprover.zulipchat.com/#narrow/stream/252551-graph-theory/topic/max-flow.20min-cut.20help
they try to prove the max flow min cut theorem in graphs. In this the total flow into a set of vertices as follows:

def mk_in {V : Type* } [inst : fintype V]
  (f : V -> V -> ℝ) (s : finset V) : ℝ := ∑ x in finset.univ \ s, ∑ y in s, f x y

I tried to replicate this in lean4:

noncomputable def flow_in {V : Type u} [Fintype V] [DecidableEq V]
  (flow : V → V → ℝ)
  (vSet : Finset V) : ℝ :=
    ∑' s in (Finset.univ \ vSet),  ∑' t in vSet, flow s t

Lean 4 complains that in is an error and says expected ','

[Shreyas Srinivas]

I suspect I can do it by explicitly using the fold functions for Finsets and tsum, but is there a neat way to use the sum notation?

[Eric Wieser]

Why did you use ∑' instead?

[Shreyas Srinivas]

I followed the docs (docs4#tsum)

[Shreyas Srinivas]

Also it was recommended here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20Beginner.20question.20on.20infinite.20sums

[Shreyas Srinivas]

Tried ∑ first but got expected token and then searched zulip to find this thread.

[Reid Barton]

tsum is intended for infinite sums

[Reid Barton]

And there's no in in its notation.

[Reid Barton]

But anyways, you want ∑

[Shreyas Srinivas]

noncomputable def flow_out {V : Type} [Fintype V] [DecidableEq V]
  (flow : V → V → ℝ)
  (vSet : Finset V)
  : ℝ :=
    ∑ s in vSet, (∑ t in (Finset.univ \ vSet), flow s t)

This throws the error expected token

[Shreyas Srinivas]

Error underlining ∑

[Reid Barton]

Do you have open BigOperators?

[Shreyas Srinivas]

ah no

[Shreyas Srinivas]

Works. Thanks :)

[Yaël Dillies]

Finset.univ \ vSet is vSetᶜ, by the way

[Shreyas Srinivas]

it works (although it gets a bit hard to read). Do we have a way to put a bar on top (like latex's \overline{}?)

[Yaël Dillies]

Don't think so! That sounds like WYSIWYG witchcraft.

[Shreyas Srinivas]

I hope I can use this thread for further questions about notation that I am trying out in this file: When defining a subset of a finset, the set brackets/builder notation constructs a set. At first I hoped there would be a simple way to translate this into a Finset. It seems more convoluted though since Finset consists of a multiset and a nodup predicate and so on. What's the quickest (notationally neatest) way to do this?:

Simple example:

def inNeighbours {V : Type u} [Fintype V] (G : Digraph V) (v : V) : Finset V := {w ∈ Fintype.elems | G.isEdge w v}

[Shreyas Srinivas]

This is an error because the RHS is a set. But I am creating a subset of Fintype.elems which is a Finset.

[Ruben Van de Velde]

Do we not have nice syntax for Finset.filter?

[Kyle Miller]

No, generally you use Finset.filter directly.

Also, @Shreyas Srinivas, one thing to know about the Finset API is that you almost never need to worry about the fact it's a multiset with a nodup predicate. There should be enough functions to construct whatever Finset you need.

[Kyle Miller]

If you want to use set notation, you can try using docs4#Set.toFinset, which works if you have enough Fintype/Decidable instances lying around.

[Kyle Miller]

It can look like this

def inNeighbours {V : Type u} [Fintype V] (G : Digraph V) (v : V) : Finset V :=
  {w | G.isEdge w v}.toFinset

though you might need to write it as Set.toFinset {w | G.isEdge w v}. I expect you'll need a [DecidableRel G.isEdge] argument.

Note that you shouldn't use docs4#Fintype.elems -- the API expects that you use docs4#Finset.univ (i.e., lemmas are about the latter, not the former).

[Shreyas Srinivas]

Ah okay got it. Thanks :)

Additionally @Sebastian Ullrich that macOS issue occurred again.

[Shreyas Srinivas]

Kyle Miller said:

It can look like this

def inNeighbours {V : Type u} [Fintype V] (G : Digraph V) (v : V) : Finset V :=
  {w | G.isEdge w v}.toFinset

though you might need to write it as Set.toFinset {w | G.isEdge w v}. I expect you'll need a [DecidableRel G.isEdge] argument.

Note that you shouldn't use docs4#Fintype.elems -- the API expects that you use docs4#Finset.univ (i.e., lemmas are about the latter, not the former).

Since I am not using this for computations yet, I marked the defs noncomputable and then lean stopped asking for a DecidableRel instance