working with finset and fintype

Stream: new members

[Yakov Pechersky]

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]

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]

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]

aha you didn't provide an expllicit basis, alright

[Kevin Buzzard]

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]

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

[Kenny Lau]

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]

These theory pages are great

[Kyle Miller]

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]

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

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

[Patrick Massot]

These brackets refer to the binder of fintype.elems

[Patrick Massot]

See

#check @fintype.elems

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

#check @fintype'.elems

[Patrick Massot]

You'll see that α is explicit in fintype.elems and implicit in fintype'.elems.

[Patrick Massot]

The default value changed recently.

[Kyle Miller]

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]

It's not meant to be odd.

[Yakov Pechersky]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Yakov Pechersky]

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]

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]

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

[Scott Morrison]

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]

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]

But sometimes, sadly, erw seems unavoidable.

[Yakov Pechersky]

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]

Is there a lemma that says ↥s = {x // x ∈ s}? (Presumably yes.) If so, you can rewrite along that first.

[Yakov Pechersky]

Seems like refl proves that. Which I guess is why erw works.

[Yakov Pechersky]

Is it possible to trace which relations refl uses?

[Mario Carneiro]

anything with a @[refl] tag

[Mario Carneiro]

or are you asking something else?

[Mario Carneiro]

If you mean proofs by defeq, i.e. exact rfl, then anything is fair game, it will unfold whatever it has to

[Scott Morrison]

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

Oh, got it.

[Yakov Pechersky]

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

[Yakov Pechersky]

Similar to how one can set_option trace.simplify true for simp, what would it be for refl?

[Yakov Pechersky]

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]

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]

It does suggest looking at #print set.has_coe_to_sort.

[Yakov Pechersky]

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]

The problem is that the goal involves a fintype instance, which Lean isn't clever enough to move across the equality.

[Scott Morrison]

Perhaps simp instead of rw at that step?

[Yakov Pechersky]

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]

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]

Welcome to dependent type theory...

[Yakov Pechersky]

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]

↥s is the subtype of elements of s

[Mario Carneiro]

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

[Mario Carneiro]

but you know this already?

[Mario Carneiro]

↥n doesn't work because there is no defined has_coe_to_sort nat instance

[Mario Carneiro]

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]

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