Finsets and operations on them

Stream: new members

[Gabriel Moise]

Hello! My name is Gabriel Moise and I am an undergraduate working on my licence project in Lean. I started learning it a couple of weeks ago and I am struggling with some basic concepts and therefore have some (probably silly) questions about finsets:

1. I defined a new type for my application to be

universes u
variables {V : Type u} [fintype V]

and I don't know how to create a finset V object that would contain all the elements of the finite type V. I need this for example in case I want to use this set to make a sum over it, something like Σ i in V, f i.

2. The sum above gets me to my next question: I am trying to prove the following lemma, which is something pretty common to use, but I fail to find anything that could help me solve it:

lemma subset_sum (s s' : finset V) (H : s' ⊆ s) (f : V → ℤ):
∑ j in s, f j = (∑ j in s', f j) + (∑ j in s \ s', f j) :=
begin
  sorry
end

3. Additionally, if I want to use a particularfinset V (let's call itA, which can be defined to be a portion of the elements that are in V) to define a matrix, the following doesn't work because A is not a type:

def example_matrix : matrix A A ℤ
| i j = ....

Is there a way to construct this matrix to be defined only on the entries which correspond to the entries of A?

4. Lastly, two silly things: for a type V, how do I specifiy that V is an ordered type (like in the variables construct where for example I say that [decidable_eq V] to specify that we can have equality between terms of type V) and if I have an if-then-else construct, how do I link together two conditions into one? (like the && that is used in C) :

if condition1 ??? condition2 then branch1 else branch2

Thank you very much for your help! Looking forward to hearing from you! :smiley:

[Anne Baanen]

Gabriel Moise said:

Hello! My name is Gabriel Moise and I am an undergraduate working on my licence project in Lean. I started learning it a couple of weeks ago and I am struggling with some basic concepts and therefore have some (probably silly) questions about finsets:

1. I defined a new type for my application to be

universes u
variables {V : Type u} [fintype V]

and I don't know how to create a finset V object that would contain all the elements of the finite type V. I need this for example in case I want to use this set to make a sum over it, something like Σ i in V, f i.

The finset containing all elements of a fintype is called docs#finset.univ. In fact, Σ (i : V), f i is short for Σ i in finset.univ, f i.

[Anne Baanen]

Gabriel Moise said:

2. The sum above gets me to my next question: I am trying to prove the following lemma, which is something pretty common to use, but I fail to find anything that could help me solve it:

lemma subset_sum (s s' : finset V) (H : s' ⊆ s) (f : V → ℤ):
∑ j in s, f j = (∑ j in s', f j) + (∑ j in s \ s', f j) :=
begin
  sorry
end

Almost what you want is available: docs#finset.sum_sdiff. How I found it: I know most results about sums are in algebra/big_operators.lean. The \ operator is called sdiff in lemma names, so I searched for sdiff in that file and it turns out there is a definition prod_sdiff:

@[to_additive]
lemma prod_sdiff [decidable_eq α] (h : s₁ ⊆ s₂) :
  (∏ x in (s₂ \ s₁), f x) * (∏ x in s₁, f x) = (∏ x in s₂, f x) :=
by rw [←prod_union sdiff_disjoint, sdiff_union_of_subset h]

The @[to_additive] line means Lean will copy this result to an "additive" version, replacing the product with a sum, * with +, 1 with 0, etc.

[Kevin Buzzard]

The other trick (the one I would have used) would have been to make sure I had 'algebra.big_operators' imported and to simply have guessed the name of the lemma I wanted. I would guess finset.sum_sdiff or something close to this, and then VS code auto complete would start suggesting sensible options.

[Anne Baanen]

Gabriel Moise said:

3. Additionally, if I want to use a particularfinset V (let's call itA, which can be defined to be a portion of the elements that are in V) to define a matrix, the following doesn't work because A is not a type:

def example_matrix : matrix A A ℤ
| i j = ....

Is there a way to construct this matrix to be defined only on the entries which correspond to the entries of A?

Unfortunately, coercing a finset to a type has awkward syntax. We should really get around to fixing it :( Here's a working example:

import data.finset.basic
import data.matrix.basic

variables (A : finset ℕ)

def example_matrix : matrix (↑A : set ℕ) (↑A : set ℕ) ℤ
| i j := 0

[Kevin Buzzard]

Note that A : set nat isn't a type either :-) But it does have a coercion to a type, so it works

[Kevin Buzzard]

By the way, what is a license project?

[Anne Baanen]

Gabriel Moise said:

4. Lastly, two silly things: for a type V, how do I specifiy that V is an ordered type (like in the variables construct where for example I say that [decidable_eq V] to specify that we can have equality between terms of type V)

It depends what kind of ordering you want :) The lowest-level is [has_le V], but you can ask for [preorder V] or [linear_order V], or ...

if I have an if-then-else construct, how do I link together two conditions into one? (like the && that is used in C) :

if condition1 ??? condition2 then branch1 else branch2

You can use the logic symbols in if-then-else expressions, i.e. ∧, ∨, ...

[Kevin Buzzard]

We have && too IIRC but it's used for bools. If you're reasoning you should use the much richer world of Props.

[Gabriel Moise]

Oh apparently this wasn't the correct term: by license project I meant a project that I have to do in my final year at university which counts towards my degree result. Sorry about that!

[Anne Baanen]

&& and || also exist (docs#band, docs#bor) but those only work on booleans. The nice thing about the logic symbols like∧, ∨, ... are that they will work with any Prop, and if infers the decidable instances automatically.

[Kevin Buzzard]

Are you a mathematician or a computer scientist? What will your project be about?

[Gabriel Moise]

I am a computer scientist, 3rd year. My project is about graphs and my supervisor has some ideas of how to use the Laplacian matrix for proving interesting properties. I am only at the beginning, but I hope I can make progress quickly.

[Anne Baanen]

Gabriel Moise said:

Oh apparently this wasn't the correct term: by license project I meant a project that I have to do in my final year at university which counts towards my degree result. Sorry about that!

I was thinking whether it had anything to do with a licentiate degree :)

[Kevin Buzzard]

@Bhavik Mehta and I are giving an intensive one-day course about finsets for beginners in April (I think), so let us know any problems you run into!

[Anne Baanen]

You might also be interested in the semi-secret #graph theory stream in that case.

[Kevin Buzzard]

Graphs -- oh nice! You know we have the beginnings of graph theory in mathlib?

[Kevin Buzzard]

I don't know if they're focusing on practical computation though, I do know they just proved Hall's dog-owner theorem

[Kevin Buzzard]

formerly marriage theorem

[Gabriel Moise]

yes, I would love being part of the semi-secret stream. And yes, I went through the graph theory part and tried to understand as much of it as possible, actually I followed the model for the adjacency matrix file so far and now I want to come up with my own ideas.

[Patrick Massot]

Gabriel, are you French?

[Gabriel Moise]

No, I am Romanian :smile:

[Patrick Massot]

That "license" thing sounded very French.

[Patrick Massot]

(I had no trouble at all understand that sentence)

[Anne Baanen]

Patrick Massot said:

That "license" thing sounded very French.

It seems to be a Romance thing. My wife also got a "licenciatura" before her master.

[Ryan Lahfa]

Patrick Massot said:

Gabriel, are you French?

(I admit that I was thinking the same until the expected question :>)

[Gabriel Moise]

def V_elems : finset V := finset.univ

lemma... :=
begin
  ...
  have h : {i} ⊆ V_elems, {unfold V_elems, exact subset_univ ({i})},
end

Apparently I get the error : don't know how to synthesize placeholder and I don't get why, since to me I used correctly the theorem subset_univ from data.fintype.basic.

[Kevin Buzzard]

An important thing to learn in this community is that you will get much better quality answers to your questions if you post what is called minimal working examples #mwe for your questions. So -- add the imports, give the lemma a name or just say example : false := , actually make the code compile up to the point where the error or problem occurs. Hopefully any questions you have about this are answered in the mwe link above.

The reason for it is that the 1 minute it takes you to make it is more cost-effective than the n minutes it takes for n people to do the job themselves.

In short, don't just tell us the error, show us the exact code which makes the error, so we can make the same error ourselves.