Zulip Chat Archive

Stream: new members

Topic: working with finset and fintype


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 11 2020 at 08:41):

aha you didn't provide an expllicit basis, alright

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jun 11 2020 at 08:57):

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

view this post on Zulip 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

view this post on Zulip Jalex Stark (Jun 11 2020 at 13:24):

These theory pages are great

view this post on Zulip 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. )

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 11 2020 at 19:18):

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

view this post on Zulip Patrick Massot (Jun 11 2020 at 19:19):

These brackets refer to the binder of fintype.elems

view this post on Zulip Patrick Massot (Jun 11 2020 at 19:21):

See

#check @fintype.elems

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

#check @fintype'.elems

view this post on Zulip Patrick Massot (Jun 11 2020 at 19:22):

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

view this post on Zulip Patrick Massot (Jun 11 2020 at 19:22):

The default value changed recently.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 11 2020 at 19:39):

It's not meant to be odd.

view this post on Zulip 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 }

view this post on Zulip 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```

view this post on Zulip Kevin Buzzard (Jun 11 2020 at 21:53):

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

view this post on Zulip Mario Carneiro (Jun 11 2020 at 21:56):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jun 12 2020 at 00:02):

But sometimes, sadly, erw seems unavoidable.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Jun 12 2020 at 02:31):

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

view this post on Zulip Yakov Pechersky (Jun 12 2020 at 02:32):

Is it possible to trace which relations refl uses?

view this post on Zulip Mario Carneiro (Jun 12 2020 at 03:01):

anything with a @[refl] tag

view this post on Zulip Mario Carneiro (Jun 12 2020 at 03:01):

or are you asking something else?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jun 12 2020 at 03:46):

Oh, got it.

view this post on Zulip Yakov Pechersky (Jun 12 2020 at 04:00):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Bryan Gin-ge Chen (Jun 12 2020 at 04:08):

It does suggest looking at #print set.has_coe_to_sort.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jun 12 2020 at 04:33):

Perhaps simp instead of rw at that step?

view this post on Zulip 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

view this post on Zulip 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. :-)

view this post on Zulip Scott Morrison (Jun 12 2020 at 04:40):

Welcome to dependent type theory...

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jun 12 2020 at 04:46):

↥s is the subtype of elements of s

view this post on Zulip Mario Carneiro (Jun 12 2020 at 04:46):

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

view this post on Zulip Mario Carneiro (Jun 12 2020 at 04:46):

but you know this already?

view this post on Zulip Mario Carneiro (Jun 12 2020 at 04:47):

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

view this post on Zulip 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?

view this post on Zulip 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