concrete finset and operations

Stream: new members

[Callum Cassidy-Nolan]

Is this the best way to define a concrete finset ?

#eval ({1, 2, 3} : finset ℕ )

I was looking around here: https://leanprover-community.github.io/mathlib_docs_demo/data/finset/basic.html#finset but I couldn't see the notation for constructing a concrete finset aside from this:

Finset constructions

singleton: Denoted by {a}; the finset consisting of one element.
finset.empty: Denoted by ∅. The finset associated to any type consisting of no elements.
finset.range: For any n : ℕ, range n is equal to {0, 1, ... , n - 1} ⊆ ℕ. This convention is consistent with other languages and normalizes card (range n) = n. Beware, n is not in range n.
finset.attach: Given s : finset α, attach s forms a finset of elements of the subtype {a // a ∈ s}; in other words, it attaches elements to a proof of membership in the set.

[Mario Carneiro]

yes that's a way to construct a finset, although it has some disadvantages since for example it's not obvious that it has cardinality 3

[Callum Cassidy-Nolan]

What are one of the other methods to construct that set?

[Mario Carneiro]

If you can construct the set in such a way that nodup is automatically true, then you can use the constructor finset.mk instead

[Callum Cassidy-Nolan]

is .mk a method for any structure?

[Mario Carneiro]

Most of the finsets constructed in data.fintype.basic are like this, for example src#bool.fintype

[Mario Carneiro]

finset.mk is the constructor of finset

[Mario Carneiro]

usually written with angle brackets

[Mario Carneiro]

in the linked example, ⟨tt ::ₘ ff ::ₘ 0, by simp⟩ : finset bool

[Callum Cassidy-Nolan]

::ₘ is this notation for appending them together somehow?

[Mario Carneiro]

that's notation for multiset.cons

[Mario Carneiro]

you can also write ⟦[1, 2]⟧

[Callum Cassidy-Nolan]

Ah I see

[Mario Carneiro]

to build a multiset from a list

[Callum Cassidy-Nolan]

So another way of building it could be like : finset.mk ⟦[1, 2, 3]⟧ (by simp) ? ( Looks like it works)

[Callum Cassidy-Nolan]

If I want to get the minimum element of a list I've tried (finset.mk ⟦[1, 2, 3]⟧ (by simp)).min which becomes (some 1) what does some mean?

[Mario Carneiro]

docs#finset.min returns an option

[Callum Cassidy-Nolan]

I just checked out that definition: image.png

[Callum Cassidy-Nolan]

Could you help me understand that?

[Mario Carneiro]

a value of option A is either none or some a where a : A

[Mario Carneiro]

it is used to indicate the possibility of failure in functions

[Callum Cassidy-Nolan]

I see

[Callum Cassidy-Nolan]

So like if the set was empty

[Mario Carneiro]

yes, read the doc

[Mario Carneiro]

docs#finset.min

[Callum Cassidy-Nolan]

But since we know our set isn't empty we can do something like this right? finset.min' (finset.mk ⟦[1, 2, 3]⟧ (by simp)) (by simp) ?

[Mario Carneiro]

you tell me, does it typecheck?

[Callum Cassidy-Nolan]

it evals to 1 so yes!

[Mario Carneiro]

there you have it

[Callum Cassidy-Nolan]

Is that really the shortest way to get the min of a non-empty finset though?

[Mario Carneiro]

there are other ways to write that expression that are shorter in terms of characters, but that's the function to call

[Callum Cassidy-Nolan]

Ok, I understand

[Callum Cassidy-Nolan]

Thanks for helping me with this

[Callum Cassidy-Nolan]

I'm having some trouble using this feature in a theorem:

theorem test
  (a : ℕ → ℝ)
  (S : finset ℝ)
  (h₀ : ∀ (i : ℕ), (1 < i ∧ i <= 7) → a 1 < a i )
  (h₁ : S = {a 1, a 2, a 3, a 4, a 5, a 6, a 7}) :
  finset.min' S (by simp) = a 1 := sorry

The simp doesn't seem to solve it:

simplify tactic failed to simplify
state:
a : ℕ → ℝ,
S : finset ℝ,
h₃ : S = {a 1, a 2, a 3, a 4, a 5, a 6, a 7}
⊢ S.nonempty

[Mario Carneiro]

by simp [h₃]

[Mario Carneiro]

the theorem is also false

[Mario Carneiro]

probably you just want to use min instead if the proof is complex though

[Callum Cassidy-Nolan]

Ah ok, so something like this:

theorem test
  (a : ℕ → ℝ)
  (S : finset ℝ)
  (h₀ : ∀ (i : ℕ), (1 < i ∧ i <= 7) → a 1 < a i )
  (h₁ : S = {a 1, a 2, a 3, a 4, a 5, a 6, a 7}) :
  finset.min S = a 1 := sorry

[Callum Cassidy-Nolan]

What if I wanted to do some operation on the finset.min S like this:

theorem test
  (a : ℕ → ℝ)
  (S : finset ℝ)
  (h₀ : ∀ (i : ℕ), (1 < i ∧ i <= 7) → a 1 < a i )
  (h₁ : S = {a 1, a 2, a 3, a 4, a 5, a 6, a 7})
  (h₂ : a 1 = 30) :
  (finset.min S) / 10 = 3 := sorry

[Callum Cassidy-Nolan]

It doesn't seem to work out because the goal state becomes:

failed to synthesize type class instance for
A a : ℕ → ℝ,
S : finset ℝ,
h₀ :
  a 1 = 64 / 25 ∧
    a 2 = 261 / 100 ∧ a 3 = 53 / 20 ∧ a 4 = 271 / 100 ∧ a 5 = 279 / 100 ∧ a 6 = 141 / 50 ∧ a 7 = 143 / 50,
h₁ : ∑ (i : ℕ) in finset.Icc 1 7, A i = 19,
h₃ : S = {a 1, a 2, a 3, a 4, a 5, a 6, a 7}
⊢ has_add (option ℝ)

[Mario Carneiro]

The examples are very contrived, but you would do something like \exists s \in S.min, s/10 = 3

[Callum Cassidy-Nolan]

So S.min : option R, but what allows us to use the \in operator on that?

[Mario Carneiro]

there is an instance of has_mem A (option A)