numerating elements of a set causing type issues

Stream: new members

[Christopher Schmidt]

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]

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]

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]

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]

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

[Martin Dvořák]

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

[Christopher Schmidt]

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]

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]

@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]

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]

@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]

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]

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]

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]

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

[Kyle Miller]

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]

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]

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

[Kyle Miller]

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

[Kyle Miller]

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

[Christopher Schmidt]

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]

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]

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]

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]

@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]

@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]

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]

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]

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]

(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]

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]

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]

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]

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

[Yaël Dillies]

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

[Junyan Xu]

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]

@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]

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

[Kyle Miller]

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]

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

[Junyan Xu]

Thanks for the diagnosis!

[Joseph Myers]

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]

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]

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]

Where can I see the current progress on the book?

[Patrick Massot]

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

[Yaël Dillies]

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

[Kevin Buzzard]

I just Google for mathematics in lean to find it

[Yaël Dillies]

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

[Christopher Schmidt]

@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]

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

[Kyle Miller]

What's the error?

[Kyle Miller]

(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]

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

[Christopher Schmidt]

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]

Christopher Schmidt has marked this topic as resolved.

[Notification Bot]

Christopher Schmidt has marked this topic as unresolved.

[Christopher Schmidt]

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]

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]

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.