## 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

#### 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:

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:

1. you can use obtain ... in the first line, which is perhaps slightly more readable
2. put braces around the proofs steps of the second case coming from refine.
3. 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.

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: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?