## Stream: new members

### Topic: numerating elements of a set causing type issues

#### Christopher Schmidt (Jan 16 2023 at 11:34):

Hello everyone,

I defined a directed walk in a directed graph with start and ending points in V. However, I would like to have a path which starting and ending points are in A and B, respectively. Additionally, as I want to define n different path, I want to numerate the elements in A.verts and B.verts by making them a list. But then the nth member of that list hast the wrong type to be plugged in the direct walk. Here a MWE:

import tactic

universes u
variables {V : Type u} {u v : V} {n : ℕ}

@[ext]
structure directed_simple_graph (V : Type u):= (adj : V → V → Prop)

namespace directed_simple_graph
variables (G : directed_simple_graph V)

@[derive decidable_eq]
inductive directed_walk : V → V → Type u
| nil {u : V} : directed_walk u u
| cons {u v w: V} (h : G.adj u v) (p : directed_walk v w) : directed_walk u w

@[ext]
structure vertex_subset_n (n : ℕ) (V : Type u) :=
(verts : finset V)
(card : verts.card = n)

variables {A B : vertex_subset_n n V}
namespace directed_walk

variables {start : A.verts} {finish : B.verts}
variables {p : G.directed_walk u v}
variables {p2 : G.directed_walk start finish} --works but start and end point are not numerated

noncomputable def t := (A.verts).to_list.nth 1
variables {p3 : directed_walk t v} -- does not work

end directed_walk
end directed_simple_graph


The knowledge that .nth 0 up to .nth (n-1) is a member of the list :

lemma A_verts_list_length_eq_n : A.verts.to_list.length = n := by  {simp only [finset.length_to_list], exact A.card}


How can I combine those such that I can numerate my start and end points, as it is important to differentiate between different ones ?
Any help is appreciated.

#### Martin Dvořák (Jan 16 2023 at 11:35):

I didn't read your code so my answer is possibly OT, but I wanna say that list.nth and list.nth_le indexes elements from zero.

#### Christopher Schmidt (Jan 16 2023 at 11:37):

Martin Dvořák schrieb:

I didn't read your code so my answer is possibly OT, but I wanna say that list.nth and list.nth_le indexes elements from zero.

Thats true, but unfortunately not helpful. Nevertheless, edited the last part, should be correct now.

#### Kyle Miller (Jan 16 2023 at 11:41):

Can we #xy this? What is the main theorem you're wanting to prove? You're getting into territory where it's helpful to know the goal.

#### Damiano Testa (Jan 16 2023 at 11:45):

Also, having a universe u and a "graph vertex u" is probably not a good idea.

#### Martin Dvořák (Jan 16 2023 at 11:47):

Is there a way to make the compiler complain about these name collisions?

#### Christopher Schmidt (Jan 16 2023 at 11:50):

Kyle Miller schrieb:

Can we #xy this? What is the main theorem you're wanting to prove? You're getting into territory where it's helpful to know the goal.

Fair enough.
Well I am trying to formalize the Lindström Gessel Viennot Lemma as a bachelor thesis (therefore all the directed stuff). So I am working on establishing all the necessary objects which are weights, weight of a walk, path system, weight of path system, path matrix.

The current goal is to define the structure of a (vertex disjoint) path system which needs

• a permutation s and its sign
• n paths p_i : A_i \to B_s(i), whereas A and B are subsets of the vertices of cardinality n
(- vertex disjointness of the paths)

Therefor the effort to numerate A.verts and B.verts and get the correct elements as an input for direct walks.

#### Kyle Miller (Jan 16 2023 at 13:48):

Damiano Testa said:

Also, having a universe u and a "graph vertex u" is probably not a good idea.

Maybe not, but for better or for worse we've been doing this in mathlib code throughout the graph library and its seems to work out fine

#### Kyle Miller (Jan 16 2023 at 13:51):

@Christopher Schmidt I'm not sure I understand exactly what you're trying to do yet (what does it mean to numerate a set?), but maybe it's helpful to know that the way we talk about ordered finite lists of elements is either f : fin n -> V or the combination [fintype α] with f : α -> V. Sometimes we use a coercion, where s : finset α and then use f : s -> V.

#### Kyle Miller (Jan 16 2023 at 13:56):

Then when you have a pair of such a family of elements (for example [fintype α] with f g : α -> V), you can work with Π (i : α), G.directed_walk (f i) (g i), which is an α-indexed family of walks.

#### Kyle Miller (Jan 16 2023 at 13:58):

@Martin Dvořák I see your :prohibited:, but universe level variables and normal variables are in different namespaces, so it can't cause problems for Lean at least.

#### Martin Dvořák (Jan 16 2023 at 14:00):

Christopher Schmidt said:

Kyle Miller schrieb:

Can we #xy this? What is the main theorem you're wanting to prove? You're getting into territory where it's helpful to know the goal.

Fair enough.
Well I am trying to formalize the Lindström Gessel Viennot Lemma as a bachelor thesis (therefore all the directed stuff). So I am working on establishing all the necessary objects which are weights, weight of a walk, path system, weight of path system, path matrix.

The current goal is to define the structure of a (vertex disjoint) path system which needs

• a permutation s and its sign
• n paths p_i : A_i \to B_s(i), whereas A and B are subsets of the vertices of cardinality n
(- vertex disjointness of the paths)

Therefor the effort to numerate A.verts and B.verts and get the correct elements as an input for direct walks.

Let's rather focus on the question.

#### Christopher Schmidt (Jan 16 2023 at 14:19):

Kyle Miller schrieb:

Christopher Schmidt I'm not sure I understand exactly what you're trying to do yet (what does it mean to numerate a set?), but maybe it's helpful to know that the way we talk about ordered finite lists of elements is either f : fin n -> V or the combination [fintype α] with f : α -> V. Sometimes we use a coercion, where s : finset α and then use f : s -> V.

Maybe, what I have got by now, illustrates my issue more clearly.

@[ext]
structure path_system {V : Type u} {n : ℕ} {A B : vertex_subset_n n V}
{σ : equiv.perm (finset.range n)} :=
(start_pts := A.verts)
(finish_pts : B.verts)
(start  : ℕ → A.verts := sorry) -- λ i, A.verts.to_list.nth i
(finish : ℕ → B.verts := sorry) -- λ i, B.verts_to_list.nth σ(i)
(n_walks : ℕ → (G.directed_walk start_pt finish_pt) :=
λ i, {p : (G.directed_walk start_pt finish_pt) | start_pt = start(i) ∧ finish_pt = finish(i)})
(sgn := σ.sign)


I somehow want to manage that the starting and ending point of a walk are precisely the corresponding ones in the following sense:
n_walk (i) goes from i to \sigma(i).
Therefore, I need to be able to numerate the elements of A and B. But a list as suggested in the comments cuases type issues. Is there a way out of this arising type issue ?

I also thought about leaving away the \sigma and just claim that any starting and ending point of A and B is only used once. However, I need the concrete bijection as I need the sign.

#### Kyle Miller (Jan 16 2023 at 14:25):

Kyle Miller said:

Then when you have a pair of such a family of elements (for example [fintype α] with f g : α -> V), you can work with Π (i : α), G.directed_walk (f i) (g i), which is an α-indexed family of walks.

Let me mention this again, since this is how you can have a system of walks that go between corresponding vertices.

#### Kyle Miller (Jan 16 2023 at 14:25):

There are a few formulations of this, but this is the general idea.

#### Kyle Miller (Jan 16 2023 at 14:27):

In Lean, you usually have to translate things from set theory to type theory. Oftentimes, if you see "a finite set $\{a_1,\dots,a_n\}$" it's better to translate it to "a function f : fin n -> A" rather than speak of sets at all.

#### Christopher Schmidt (Jan 16 2023 at 14:28):

Kyle Miller schrieb:

There are a few formulations of this, but this is the general idea.

Ok thank you. I thought its just shifting the problem to defining the sign, but I will try.

#### Kyle Miller (Jan 16 2023 at 14:28):

The sign of a permutation should already exist somewhere in mathlib.

#### Kyle Miller (Jan 16 2023 at 14:29):

Unless you're talking about defining a new concept, like a sign of a path system or something.

#### Kyle Miller (Jan 16 2023 at 14:30):

Oh, I see, you already found docs#equiv.perm.sign

#### Christopher Schmidt (Jan 16 2023 at 14:35):

Yes. Well, I better try to use your suggested approach with f and g and hoepfully get the points and sign right.
Thanks again.
I apologize if I have not stated the problem properly and/or wasted your time.

#### Kyle Miller (Jan 16 2023 at 14:42):

Getting right type definitions at the beginning is a difficult part of formalization.

If you haven't done it already, you should try to very carefully specify as formally as possible what it is you're trying to enter into Lean. This will likely help you with what you're doing, but also as you get stuck you can point to a part of this "blueprint" to get more precise help.

#### Kyle Miller (Jan 16 2023 at 14:44):

Combinatorics is already more difficult to formalize than abstract math since it tends to be done more informally on paper since the objects are more intuitive. You have to do the paper formalization yourself here before it's as amenable to formalization.

#### Kyle Miller (Jan 16 2023 at 14:45):

This takes some thinking (or more likely, experimentation) with how this will interact with how the definitions will be used in your theorems. That can be hard to think about though if you haven't gotten to thinking carefully about the theorems because you don't have formalized definitions, which points toward why definitions can be hard.

#### Christopher Schmidt (Jan 16 2023 at 14:51):

@Kyle Miller
I have noticed that and could not agree more. As it is my first Lean project, it takes a lot of nerve.
I largely appreciate your consistent help.

#### Kyle Miller (Jan 16 2023 at 15:05):

@Christopher Schmidt Here's a start:

import tactic
import logic.equiv.fintype
import group_theory.perm.sign

open_locale classical

universes u
variables {V : Type u} {u v : V} {n : ℕ}

@[ext]
structure directed_simple_graph (V : Type u):= (adj : V → V → Prop)

namespace directed_simple_graph
variables (G : directed_simple_graph V)

@[derive decidable_eq]
inductive directed_walk : V → V → Type u
| nil {u : V} : directed_walk u u
| cons {u v w : V} (h : G.adj u v) (p : directed_walk v w) : directed_walk u w

def directed_walk.support {G : directed_simple_graph V} : Π {u v : V}, G.directed_walk u v → list V
| _ v directed_walk.nil := [v]
| u _ (directed_walk.cons h p) := u :: p.support

structure path_system {α : Type*} (A B : α ↪ V) :=
(B' : α ↪ V)
(range_B' : set.range B' = set.range B)
(walk : Π (i : α), G.directed_walk (A i) (B' i))
(walk_disj : ∀ (i j : α), i ≠ j → list.disjoint (walk i).support (walk j).support)

variables {G}

noncomputable def path_system.σ {α : Type*} {A B : α ↪ V} (s : G.path_system A B) : α ≃ α :=
(equiv.of_injective s.B' s.B'.inj').trans
((equiv.set.of_eq s.range_B').trans (equiv.of_injective B B.inj').symm)

noncomputable def path_system.sign {α : Type*} [fintype α] {A B : α ↪ V} (s : G.path_system A B) :=
equiv.perm.sign s.σ


#### Kyle Miller (Jan 16 2023 at 15:07):

Another design for path_system could have been to include sigma as a permutation on α or as a permutation on set.range B.

#### Kyle Miller (Jan 16 2023 at 15:07):

But you don't need anything saying it's a finite system of paths in any case. That only comes in for sign.

#### Kyle Miller (Jan 16 2023 at 15:10):

For another example of this idea of generalizing indices so that you take an arbitrary index type rather than just the set of 1,...,n, take a look at matrix. Matrices are indexed by arbitrary types, not numbers.

#### Kyle Miller (Jan 16 2023 at 15:13):

(Also, quick disclaimer, I just read the wikipedia page for the theorem and wrote up these definitions. They might be wrong or unoptimal for any number of reasons, but hopefully it's in the right direction.)

#### Kyle Miller (Jan 16 2023 at 15:19):

Just for illustration, an option using sigma. I can't tell immediately whether this is better or worse than the previous definition.

structure path_system {α : Type*} (A B : α ↪ V) :=
(σ : equiv.perm α)
(walk : Π (i : α), G.directed_walk (A i) (B (σ i)))
(walk_disj : ∀ (i j : α), i ≠ j → list.disjoint (walk i).support (walk j).support)

variables {G}

-- This definition is not actually necessary since one can write s.σ.sign just as easily as s.sign.
noncomputable def path_system.sign {α : Type*} [fintype α] {A B : α ↪ V} (s : G.path_system A B) :=
s.σ.sign


#### Damiano Testa (Jan 16 2023 at 16:48):

Kyle Miller said:

Damiano Testa said:

Also, having a universe u and a "graph vertex u" is probably not a good idea.

Maybe not, but for better or for worse we've been doing this in mathlib code throughout the graph library and its seems to work out fine

Living on the directed edge! :smiley:

#### Yaël Dillies (Jan 16 2023 at 18:19):

Kyle Miller said:

Combinatorics is already more difficult to formalize than abstract math since it tends to be done more informally on paper since the objects are more intuitive. You have to do the paper formalization yourself here before it's as amenable to formalization.

I would even phrase it as "Combinatorics is harder to formalise than other subjects until you understand why it is easy"

#### Yaël Dillies (Jan 16 2023 at 18:20):

I am having a lot of success formalising combinatorics now, but this took two years of trying.

#### Yaël Dillies (Jan 16 2023 at 18:21):

I would be very interested in writing a chapter of the new Mathematics in Lean book on how to formalise combinatorics.

#### Junyan Xu (Jan 16 2023 at 19:37):

You could use docs#pairwise for walk_disj.

Kyle Miller said:

Martin Dvořák I see your :prohibited:, but universe level variables and normal variables are in different namespaces, so it can't cause problems for Lean at least.

If universe variables clash with declaration names you get trouble though. Last time I changed v' to w in this file I got weird errors when Lean got to line 76 (lemma w).

#### Kyle Miller (Jan 16 2023 at 19:49):

@Junyan Xu I tried two things:

1. I changed that lemma to lemma w', and there was no error.
2. I renamed the universe variable from v' to w, and then both res_π and w had a universe variable error. Removing the @[elementwise] attribute, though, removes the error.

It seems more likely to me that there is some subtle bug in that attribute.

#### Kyle Miller (Jan 16 2023 at 19:51):

This line might be why having a universe variable that's a w is a problem.

#### Kyle Miller (Jan 16 2023 at 19:54):

Universes are in a different namespace, so get_unused_name_reserved doesn't seem like the right way to get a fresh universe variable name.

#### Junyan Xu (Jan 16 2023 at 19:54):

Oh! So it's just a red herring that the lemma is named w.

#### Junyan Xu (Jan 16 2023 at 19:55):

Thanks for the diagnosis!

#### Joseph Myers (Jan 16 2023 at 20:12):

Yaël Dillies said:

I am having a lot of success formalising combinatorics now, but this took two years of trying.

I suspect that if I now redid my formalization of British MO 2020 round 2 problem 3 it would be rather less than 3000 lines of Lean for a not-very-hard combinatorics problem (that was the third Lean formalization I ever did after NNG).

#### Christopher Schmidt (Jan 16 2023 at 20:21):

Kyle Miller schrieb:

Just for illustration, an option using sigma. I can't tell immediately whether this is better or worse than the previous definition.

structure path_system {α : Type*} (A B : α ↪ V) :=
(σ : equiv.perm α)
(walk : Π (i : α), G.directed_walk (A i) (B (σ i)))
(walk_disj : ∀ (i j : α), i ≠ j → list.disjoint (walk i).support (walk j).support)

variables {G}

-- This definition is not actually necessary since one can write s.σ.sign just as easily as s.sign.
noncomputable def path_system.sign {α : Type*} [fintype α] {A B : α ↪ V} (s : G.path_system A B) :=
s.σ.sign


Thanks for the effort! Thats more than one could as for. I will implement both versions and see which is more practical.

#### Patrick Massot (Jan 17 2023 at 09:05):

Yaël Dillies said:

I would be very interested in writing a chapter of the new Mathematics in Lean book on how to formalise combinatorics.

This could be nice if it fits with the style of other parts. You can write something anyway, and then decide what to do with it.

#### Yaël Dillies (Jan 17 2023 at 09:06):

Where can I see the current progress on the book?

#### Patrick Massot (Jan 17 2023 at 09:07):

I'm not sure I understand the question, but the source is at https://github.com/avigad/mathematics_in_lean_source/

#### Yaël Dillies (Jan 17 2023 at 09:09):

I am simply trying to get a sense of what "the style of other parts" is

#### Kevin Buzzard (Jan 17 2023 at 09:13):

I just Google for mathematics in lean to find it

#### Yaël Dillies (Jan 17 2023 at 09:22):

Ah! I understand the confusion now. I thought there was some Mathematics in Lean 4 whose writing was underway.

#### Christopher Schmidt (Jan 17 2023 at 11:15):

@Kyle Miller I have added the following to your first approach :

open_locale big_operators

instance : partial_order (directed_simple_graph V) := partial_order.lift adj ext

def edge_set : directed_simple_graph V ↪o set (V × V) :=
order_embedding.of_map_le_iff (λ (G : directed_simple_graph V), {p : V × V | G.adj p.1 p.2}) \$
begin
intros G G',
rw [set.le_eq_subset, set.set_of_subset_set_of, prod.forall],
refl,
end

namespace directed_walk
variables {A B : α ↪ V}
variable {weight : G.edge_set → ℝ}

def walk_weight {G : directed_simple_graph V} {weight : G.edge_set → ℝ} :
Π {u v : V}, G.directed_walk u v → ℝ
| u v nil := 1
| u v (cons h p) := weight ⟨(u, _), h⟩ * walk_weight p

def path_system_weight {G : directed_simple_graph V} {weight : G.edge_set → ℝ}
{A B : α ↪ V} (s : G.path_system A B) : ℝ :=
∏ (i : α), walk_weight (s.walk i) -- not working

variables {s : G.path_system A B} {i : α}
#check walk_weight (s.walk i) -- works

end directed_walk


I do not understand, why it is not working in the first but working in the second case. What have I messed up again?

#### Christopher Schmidt (Jan 17 2023 at 11:16):

The opening statement being at the begining of the file after imports.

#### Kyle Miller (Jan 17 2023 at 11:20):

What's the error?

#### Kyle Miller (Jan 17 2023 at 11:21):

(Without running any code, I'm guessing it's that you don't have [fintype α], which you need to take a product like that.)

#### Kyle Miller (Jan 17 2023 at 11:22):

Design suggestion: make weight an explicit variable since it can't be inferred from the other arguments.

#### Christopher Schmidt (Jan 17 2023 at 11:27):

Kyle Miller schrieb:

Design suggestion: make weight an explicit variable since it can't be inferred from the other arguments.

Had the fintype, but this solved the issue. I do not get how but now it seems to work. Thanks !

#### Notification Bot (Jan 18 2023 at 11:42):

Christopher Schmidt has marked this topic as resolved.

#### Notification Bot (Jan 18 2023 at 13:56):

Christopher Schmidt has marked this topic as unresolved.

#### Christopher Schmidt (Jan 18 2023 at 14:04):

Hello everyone I am running into a type issue again,

namespace directed_walk
variables {A B : α ↪ V}
variables {R : Type} [field R]

def new_weight {G : directed_simple_graph V} {A B : α ↪ V} (weight : G.edge_set → R) :
Type u → R :=
sorry

def path_matrix {α : Type*} [fintype α] {R : Type} {A B : α ↪ V} (weight : G.edge_set → R) :
α → α → R :=
λ i j, new_weight weight (G.directed_path (A i) (B j)) -- error : failed to synthesize class instance for ... ⊢ field R

variables {weight : G.edge_set → R}
variables {i j : α}
#check G.directed_path (A i) (B j) -- Type u
#check new_weight weight (G.directed_path (A i) (B j)) -- type R
end directed_walk


the new_weight weight (G.directed_path (A i) (B j)) is type R as shown below but the def of "path matrix" does not work. I do not understand how this is possible. Anyone got an idea?

#### Kevin Buzzard (Jan 18 2023 at 15:18):

You have variable {R : Type} [field R] so that R is a field, but you have def path_matrix... {R : Type}... and this means "use a new R which isn't a field".

#### Christopher Schmidt (Jan 18 2023 at 15:56):

Kevin Buzzard schrieb:

You have variable {R : Type} [field R] so that R is a field, but you have def path_matrix... {R : Type}... and this means "use a new R which isn't a field".

Thank you.

Last updated: Dec 20 2023 at 11:08 UTC