# Zulip Chat Archive

## Stream: new members

### Topic: working with finset and fintype

#### Yakov Pechersky (Jun 11 2020 at 08:16):

Trying to show a result about finite bases of matrices. I'm running into converting between set, finset, and fintype. The proof I have comes from reading various lemmas in src#linear_algebra/finite_dimensional. I tried employing various set and finset lemmas, but I think I'm missing something:

```
import data.real.basic
import data.matrix.basic
import linear_algebra.matrix
variables {n : ℕ}
-- An n × n matrix has some finite basis of cardinality n ^ 2
example : ∃ (b : finset (matrix (fin n) (fin n) ℝ)),
(is_basis ℝ (subtype.val : (↑b : set (matrix (fin n) (fin n) ℝ)) -> (matrix (fin n) (fin n) ℝ)) ∧
(finset.card b = n ^ 2)) :=
begin
rcases finite_dimensional.exists_is_basis_finite ℝ (matrix (fin n) (fin n) ℝ) with ⟨s, s_basis, s_finite⟩,
rw nat.pow_two,
use s_finite.to_finset,
split,
{ convert s_basis,
funext, rw set.finite.coe_to_finset,
funext, rw set.finite.coe_to_finset },
haveI : fintype s := s_finite.fintype,
haveI : finite_dimensional ℝ (matrix (fin n) (fin n) ℝ) := by apply_instance,
have := finite_dimensional.dim_eq_card_basis s_basis,
rw <-finite_dimensional.findim_eq_dim at this,
simp at this,
norm_cast at this,
rw this, -- goal is s_finite.to_finset.card = fintype.card {x // x ∈ s}
rw fintype.subtype_card s_finite.to_finset -- seems like set.finite.mem_to_finset should work
(by {intros x,
split,
{ intros h,
-- why doesn't the exact statement here work?
-- exact set.finite.mem_to_finset.mp h,
sorry, },
{ intros h,
exact set.finite.mem_to_finset.mpr h, },
funext} ),
-- but rw fails with
-- rewrite tactic failed, did not find instance of the pattern in the target expression
-- fintype.card {x // (λ (x : matrix (fin n) (fin n) ℝ), x ∈ s) x}
-- how does one funext inside the subtype expression?
sorry,
end
```

#### Kevin Buzzard (Jun 11 2020 at 08:32):

I think that the concept of finiteness in type theory is genuinely messy. Either that or there's a trick I don't know about.

#### Kenny Lau (Jun 11 2020 at 08:40):

an irrelevant hint: if you're gonna provide an explicit witness, don't obscure it inside an existential, but rather construct it and prove its properties

#### Kenny Lau (Jun 11 2020 at 08:41):

aha you didn't provide an expllicit basis, alright

#### Kevin Buzzard (Jun 11 2020 at 08:52):

I'm not at lean right now but looking at your code I think that `fintype`

is data so you should use `letI`

#### Patrick Massot (Jun 11 2020 at 08:57):

Did you read https://leanprover-community.github.io/theories/sets.html?

#### Kenny Lau (Jun 11 2020 at 10:23):

```
import data.real.basic
import data.matrix.basic
import linear_algebra.matrix
variables {n : ℕ}
theorem finset.attach_eq_univ {α : Type*} {s : finset α} :
s.attach = finset.univ :=
rfl
theorem set.finite.card_to_finset {α : Type*} {s : set α} [fintype s] (h : s.finite) :
h.to_finset.card = fintype.card s :=
by { rw [← finset.card_attach, finset.attach_eq_univ, ← fintype.card], congr' 2, ext x,
rw set.finite.mem_to_finset }
-- An n × n matrix has some finite basis of cardinality n ^ 2
example : ∃ (b : finset (matrix (fin n) (fin n) ℝ)),
(is_basis ℝ (subtype.val : (↑b : set (matrix (fin n) (fin n) ℝ)) -> (matrix (fin n) (fin n) ℝ)) ∧
(finset.card b = n ^ 2)) :=
begin
rcases finite_dimensional.exists_is_basis_finite ℝ (matrix (fin n) (fin n) ℝ) with ⟨s, s_basis, s_finite⟩,
refine ⟨s_finite.to_finset, _, _⟩,
{ rw set.finite.coe_to_finset, exact s_basis },
cases id s_finite, resetI,
erw [set.finite.card_to_finset, ← finite_dimensional.findim_eq_card_basis s_basis,
matrix.findim_matrix, fintype.card_fin, nat.pow_two],
end
```

#### Jalex Stark (Jun 11 2020 at 13:24):

These theory pages are great

#### Kyle Miller (Jun 11 2020 at 19:16):

Patrick Massot said:

Did you read https://leanprover-community.github.io/theories/sets.html?

This seems like a good place to ask about the following definition (as it appears in mathlib, rather than how it appears on the given page):

```
class fintype (α : Type*) :=
(elems [] : finset α)
(complete : ∀ x : α, x ∈ elems)
```

What is the `[]`

after `elems`

? In the Lean documentation, I could only find something about `{}`

.

(Also, for `finset`

, is there a short way to extract a representative `list`

along with a proof of `nodup`

for that list? I don't need this right now, but I had spent an hour or two trying to figure it out before I settled on a construction through induction using `finset.induction`

. )

#### Johan Commelin (Jun 11 2020 at 19:17):

@Kyle Miller That recently changed... (that's why you only find mention of `{}`

in the docs, and the def is different from that documentation page.

#### Johan Commelin (Jun 11 2020 at 19:18):

@Gabriel Ebner Will know the details better than I do.

#### Patrick Massot (Jun 11 2020 at 19:19):

These brackets refer to the binder of `fintype.elems`

#### Patrick Massot (Jun 11 2020 at 19:21):

See

```
#check @fintype.elems
class fintype' (α : Type*) :=
(elems : finset α)
(complete : ∀ x : α, x ∈ elems)
#check @fintype'.elems
```

#### Patrick Massot (Jun 11 2020 at 19:22):

You'll see that `α`

is explicit in `fintype.elems`

and implicit in `fintype'.elems`

.

#### Patrick Massot (Jun 11 2020 at 19:22):

The default value changed recently.

#### Kyle Miller (Jun 11 2020 at 19:25):

I see, thanks for the example. Somehow it didn't strike me as odd that every use of `fintype.elems`

in `data.fintype.basic`

had an explicit type.

#### Patrick Massot (Jun 11 2020 at 19:39):

It's not meant to be odd.

#### Yakov Pechersky (Jun 11 2020 at 20:44):

Worth it to add Kenny's theorems to mathlib?

```
theorem finset.attach_eq_univ {α : Type*} {s : finset α} :
s.attach = finset.univ :=
rfl
theorem set.finite.card_to_finset {α : Type*} {s : set α} [fintype s] (h : s.finite) :
h.to_finset.card = fintype.card s :=
by { rw [← finset.card_attach, finset.attach_eq_univ, ← fintype.card], congr' 2, ext x,
rw set.finite.mem_to_finset }
```

#### Yakov Pechersky (Jun 11 2020 at 21:00):

In the proof here, the first `rw`

does not change my tactic state in a visible way. `s_basis : is_basis ℝ subtype.val`

matches the tactic goal of `is_basis ℝ subtype.val`

, but it only works when the `rw set.finite.coe_to_finset`

is included. What's going on?

```
-- An n × n matrix has some finite basis of cardinality n ^ 2
example : ∃ (b : finset (matrix (fin n) (fin n) ℝ)),
(is_basis ℝ (subtype.val : (↑b : set (matrix (fin n) (fin n) ℝ)) -> (matrix (fin n) (fin n) ℝ)) ∧
(finset.card b = n ^ 2)) :=
begin
rcases finite_dimensional.exists_is_basis_finite ℝ (matrix (fin n) (fin n) ℝ) with ⟨s, s_basis, s_finite⟩,
refine ⟨s_finite.to_finset, _, _⟩,
{ rw set.finite.coe_to_finset, exact s_basis }, -- here; exact s_basis is not enough
cases id s_finite, resetI,
erw [set.finite.card_to_finset, ← finite_dimensional.findim_eq_card_basis s_basis,
matrix.findim_matrix, fintype.card_fin, nat.pow_two],
end```
```

#### Kevin Buzzard (Jun 11 2020 at 21:53):

Isn't this a special case of a more general theorem about a by b matrices?

#### Mario Carneiro (Jun 11 2020 at 21:56):

Isn't this a special case of a more general theorem about findim vector spaces?

#### Mario Carneiro (Jun 11 2020 at 21:57):

the only thing that is specific to matrices is the claim that the dimension is a * b or n ^ 2

#### Yakov Pechersky (Jun 11 2020 at 22:10):

Yeah it is a specialized case. But proving the general case would look the same, other than getting rid of the last three rewrite terms, `matrix.findim_matrix, fintype.card_fin, nat.pow_two`

, correct?

#### Yakov Pechersky (Jun 11 2020 at 22:16):

```
example (K : Type u) (V : Type v) [field K] [add_comm_group V]
[module K V] [finite_dimensional K V] :
∃ (b : finset V),
(is_basis K (subtype.val : (↑b : set V) -> V) ∧
(finset.card b = finite_dimensional.findim K V)) :=
begin
rcases finite_dimensional.exists_is_basis_finite K V with ⟨s, s_basis, s_finite⟩,
refine ⟨s_finite.to_finset, _, _⟩,
{ rw set.finite.coe_to_finset, exact s_basis },
cases id s_finite, resetI,
erewrite [set.finite.card_to_finset, ←finite_dimensional.findim_eq_card_basis s_basis]
end
```

#### Scott Morrison (Jun 11 2020 at 23:59):

Sounds reasonable to me. This example would presumably be a lemma called `finite_dimensional.exists_finset_is_basis`

.

#### Scott Morrison (Jun 12 2020 at 00:00):

Some minor stylistic points:

- you can use
`obtain ...`

in the first line, which is perhaps slightly more readable - put braces around the proofs steps of the second case coming from
`refine`

. `erw`

instead of`erewrite`

#### Scott Morrison (Jun 12 2020 at 00:02):

Did you work out why the `erw`

is necessary? It means some definitional unfolding needs to happen, preventing `rw`

from matching purely syntactically. Often an additional `rw`

or `dsimp`

can be used instead, and it's usually easier to understand if you do this.

#### Scott Morrison (Jun 12 2020 at 00:02):

But sometimes, sadly, `erw`

seems unavoidable.

#### Yakov Pechersky (Jun 12 2020 at 01:32):

Yeah, that makes sense about the `erw`

. The conversion between the four types (for lack of a better word) of values and types of sets is clunky. That's why the `erw`

is needed, to convert the `↥s`

to `{x // x ∈ s}`

. And the `cases id s_finite, resetI`

is needed to populate the `fintype ↥s`

instance into the tactic state. I think the difference I've understood to be between `finsets `

and `finite`

is that finsets are our regular old enumerable finite sets. While `finite`

describes something that can be grouped into a finite set in a meaningful and non-trivial way, but also in a axiom-of-choice way.

#### Scott Morrison (Jun 12 2020 at 01:41):

Is there a lemma that says `↥s = {x // x ∈ s}`

? (Presumably yes.) If so, you can rewrite along that first.

#### Yakov Pechersky (Jun 12 2020 at 02:31):

Seems like `refl`

proves that. Which I guess is why `erw`

works.

#### Yakov Pechersky (Jun 12 2020 at 02:32):

Is it possible to trace which relations `refl`

uses?

#### Mario Carneiro (Jun 12 2020 at 03:01):

anything with a `@[refl]`

tag

#### Mario Carneiro (Jun 12 2020 at 03:01):

or are you asking something else?

#### Mario Carneiro (Jun 12 2020 at 03:02):

If you mean proofs by defeq, i.e. `exact rfl`

, then anything is fair game, it will unfold whatever it has to

#### Scott Morrison (Jun 12 2020 at 03:37):

@Yakov Pechersky, could you post the actual statement you're proving with `refl`

here? I'd like to test a new variant of `library_search`

on it.

#### Scott Morrison (Jun 12 2020 at 03:46):

Oh, got it.

#### Yakov Pechersky (Jun 12 2020 at 04:00):

```
example (α : Type*) (s : set α) : ↥s = {x // x ∈ s} :=
begin
refl,
end
```

#### Yakov Pechersky (Jun 12 2020 at 04:02):

Similar to how one can `set_option trace.simplify true`

for `simp`

, what would it be for `refl`

?

#### Yakov Pechersky (Jun 12 2020 at 04:05):

Scott Morrison said:

Happily #3038 makes this test fast again, so I've restored it there.

I see you got it.

#### Bryan Gin-ge Chen (Jun 12 2020 at 04:07):

I learned this from some of @Kevin Buzzard's messages:

```
import data.finset
set_option trace.type_context.is_def_eq true
set_option trace.type_context.is_def_eq_detail true
example (α : Type*) (s : set α) : ↥s = {x // x ∈ s} :=
begin
refl,
end
/- when your cursor is on `refl`:
[type_context.is_def_eq_detail] [1]: ?m_2 = ?m_2 =?= ↥s = {x // x ∈ s}
[type_context.is_def_eq_detail] [2]: eq =?= eq
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_coe_to_sort.S (set α)
[type_context.is_def_eq_detail] assign: ?m_1 := has_coe_to_sort.S (set α)
[type_context.is_def_eq_detail] process_assignment ?m_1 := ↥s
[type_context.is_def_eq_detail] assign: ?m_1 := ↥s
[type_context.is_def_eq_detail] [2]: ↥s =?= {x // x ∈ s}
[type_context.is_def_eq_detail] unfold left: coe_sort
[type_context.is_def_eq_detail] [3]: has_coe_to_sort.coe s =?= {x // x ∈ s}
[type_context.is_def_eq_detail] [4]: (λ (s : set α), {x // x ∈ s}) s =?= {x // x ∈ s}
[type_context.is_def_eq_detail] after whnf_core: {x // x ∈ s} =?= {x // x ∈ s}
[type_context.is_def_eq] ?m_2 = ?m_2 =?= ↥s = {x // x ∈ s} ... success (approximate mode)
-/
```

Don't ask me exactly what all the steps mean though...

#### Bryan Gin-ge Chen (Jun 12 2020 at 04:08):

It does suggest looking at `#print set.has_coe_to_sort`

.

#### Yakov Pechersky (Jun 12 2020 at 04:15):

It would seem inserting `rw set.set_coe_eq_subtype s`

should work, but it gives a motive error:

```
lemma finite_dimensional.exists_finset_is_basis
(K : Type u) (V : Type v) [field K] [add_comm_group V]
[module K V] [finite_dimensional K V] :
∃ (b : finset V),
(is_basis K (subtype.val : (↑b : set V) -> V) ∧
(finset.card b = finite_dimensional.findim K V)) :=
begin
obtain ⟨s, s_basis, s_finite⟩ := finite_dimensional.exists_is_basis_finite K V,
refine ⟨s_finite.to_finset, _, _⟩,
{ rw set.finite.coe_to_finset, exact s_basis },
{ cases id s_finite, resetI,
rw set.finite.card_to_finset,
rw set.set_coe_eq_subtype s,
-- error here: rewrite tactic failed, motive is not type correct
-- λ (_a : has_coe_to_sort.S (set V)),
-- fintype.card ↥s = finite_dimensional.findim K V = (fintype.card _a = finite_dimensional.findim K V)
rw ←finite_dimensional.findim_eq_card_basis s_basis }
end
```

#### Scott Morrison (Jun 12 2020 at 04:33):

The problem is that the goal involves a `fintype`

instance, which Lean isn't clever enough to move across the equality.

#### Scott Morrison (Jun 12 2020 at 04:33):

Perhaps `simp`

instead of `rw`

at that step?

#### Yakov Pechersky (Jun 12 2020 at 04:39):

Yes, `simp only`

works:

```
lemma finite_dimensional.exists_finset_is_basis
(K : Type u) (V : Type v) [field K] [add_comm_group V]
[module K V] [finite_dimensional K V] :
∃ (b : finset V),
(is_basis K (subtype.val : (↑b : set V) -> V) ∧
(finset.card b = finite_dimensional.findim K V)) :=
begin
obtain ⟨s, s_basis, s_finite⟩ := finite_dimensional.exists_is_basis_finite K V,
refine ⟨s_finite.to_finset, _, _⟩,
{ rw set.finite.coe_to_finset, exact s_basis },
{ cases id s_finite, resetI,
rw set.finite.card_to_finset,
simp only [set.set_coe_eq_subtype s],
rw ←finite_dimensional.findim_eq_card_basis s_basis }
end
```

#### Scott Morrison (Jun 12 2020 at 04:40):

Good exercise for learning, but I think at the end of the day both options are unfortunate (`rw, simp, rw`

, or `erw`

), and neither obviously superior. :-)

#### Scott Morrison (Jun 12 2020 at 04:40):

Welcome to dependent type theory...

#### Yakov Pechersky (Jun 12 2020 at 04:43):

I haven't yet grokked what the Sort coercion of `↥s`

is doing yet. Regular coercion can turn a `finset`

into a `set`

, so that's from one Type to another Type. While `↥s`

is turning something from value-level to type-level. Is that correct? So it is similar to what `fin n`

does. Then why can't one do `↥n`

to get `fin n`

?

#### Mario Carneiro (Jun 12 2020 at 04:46):

`↥s`

is the subtype of elements of `s`

#### Mario Carneiro (Jun 12 2020 at 04:46):

that is, `↥s = {x // x ∈ s}`

#### Mario Carneiro (Jun 12 2020 at 04:46):

but you know this already?

#### Mario Carneiro (Jun 12 2020 at 04:47):

`↥n`

doesn't work because there is no defined `has_coe_to_sort nat`

instance

#### Mario Carneiro (Jun 12 2020 at 04:49):

and if you did define one, isn't `1 : 4`

exactly the sort of nonsense question from ZFC that type theory was built to avoid?

#### Bryan Gin-ge Chen (Jun 12 2020 at 04:49):

(In case it's helpful, here's the section in TPiL about coercions.)

Last updated: May 16 2021 at 05:21 UTC