How to reason about Fin type

Stream: new members

[Ching-Tsun Chou]

I want to prove the following theorem:

open Fintype Finset Set

noncomputable section

variable (α : Type*) [Fintype α] [DecidableEq α]

def initSeg (n : ℕ) : Finset (Fin (card α + 1)) := { i | (i : ℕ) < n }

theorem init_seg_last (n : ℕ) (h0 : 0 < n) (h1 : n < card α + 1) :
    (initSeg α n).toSet \ {(n : Fin (card α + 1)) - 1} = initSeg α (n - 1) := by
  ext i
  simp [initSeg]
  sorry

I don't know how to finish the proof. In particular, I don't know how to deal with the equality i = ↑n - 1, which is an equality in the type Fin (card α + 1) while the reset of the goal is about ℕ. How do I move between Fin (card α + 1) and ℕ?

Also, I wonder if it is possible to avoid the long type cast in the singleton expression. I tried ↑ n but Lean fails to type-check it.

[Zhang Qinchuan]

You can use docs#Fin.val_eq_val to move between Fin m and ℕ.

[Vlad Tsyrklevich]

import Mathlib
open Fintype Finset Set

noncomputable section

variable (α : Type*) [Fintype α] [DecidableEq α]

def initSeg (n : ℕ) : Finset (Fin (card α + 1)) := { i | (i : ℕ) < n }

theorem init_seg_last (n : ℕ) (h0 : 0 < n) (h1 : n < card α + 1) :
    (initSeg α n).toSet \ {(n : Fin (card α + 1)) - 1} = initSeg α (n - 1) := by
  ext i
  simp [initSeg]
  rw [← Nat.cast_pred h0]
  rw [Fin.mk_eq_mk]
  rw [Fin.val_natCast]
  rw [Nat.mod_eq_of_lt (by omega)]
  omega

I suspect you're forcing too many casts and there is a simpler design here that would be easier to reason about, but it's not clear to me what you're trying to do.

[Chris Wong]

Fin (card + 1) is an interesting construction. What are you trying to model with it? Permutations?

[Chris Wong]

If all you want to do is add an element, then docs#Optional (or its friends docs#WithTop and docs#WithBot) are cleaner

[Vlad Tsyrklevich]

  rw [← Nat.cast_pred h0]
  rw [@Fin.natCast_def]
  rw [@Fin.eq_mk_iff_val_eq]
  rw [Nat.mod_eq_of_lt (by omega)]

is a sequence you could have found just using consecutive rw?, the rewrites I used above aren't discoverable that way

[Aaron Liu]

Chris Wong said:

If all you want to do is add an element, then docs#Optional (or its friends docs#WithTop and docs#WithBot) are cleaner

Do you mean docs#Option

[Ching-Tsun Chou]

Thanks to all! I now understand better how to work with Fin. I did not know about the omega tactic. None of the introductory books (https://leanprover-community.github.io/learn.html) mentions it. I tried linarith and it did not work.

[Ching-Tsun Chou]

Yes, I am trying to prove some rather trivial cardinality theorems about permutations, modeled as a bijective map from a finite set to an initial segment of ℕ (whence the use of Fin). Man, that has proved much harder and generated much more code than I expected. (Unfortunately, I can't use the existing permsOfFinset because I need my notion of permutations to have some special properties.) I'm beginning to wonder whether it has been a mistake to have used Finset and Fin. Perhaps I should have just used Set and ℕ. Perhaps stating and proving finiteness explictly is less an evil than the type-casting hell I'm in.

[Chris Wong]

Aaron Liu said:

Chris Wong said:

If all you want to do is add an element, then docs#Optional (or its friends docs#WithTop and docs#WithBot) are cleaner

Do you mean docs#Option

Yes, that's what I get for typing on my phone :laughing:

[Chris Wong]

@Ching-Tsun Chou I'm curious about what the special properties are. A lot of theory is built upon Equiv.Perm, in particular Cayley's theorem, so I think it's worth trying to use it.

Fintype.card strips away information about the original elements, then Fin adds them back. So it feels like a roundabout way of using the original elements directly.

Another tip is, for induction on naturals, it's easier to talk about n + 1 than n - 1, 0 < n, because you can simplify the former without side conditions.

[Ching-Tsun Chou]

@Chris Wong I'll describe what I want to prove below. I'll use the informal set-theoretic language.

Let's call a bijective map from a finite set A to the set {0, 1, ..., (#A-1)} a numbering. (Perhaps "ordering" is a better name, but that word has been used for other things in Lean.). For B ⊂ A, we say a numbering has B as a prefix if B's elements are ordered before the elements of A \ B in the numbering. Then I want to prove two things:
(1) There are exactly #B.factoral * (#A - #B).factorial numberings with prefix B.
(2) For B ⊂ A and B' ⊂ A, if any numbering has both B and B' as prefixes, then either B ⊂ B' or B' ⊂ B.
I don't know how to make the existing notions of permutations in mathlib to have properties (1) and (2), especially (2).

[Chris Wong]

Oh that makes sense!

One thing that comes to mind is that a bijection from a set to Fin n can be represented as a List of length n. I wonder if that's useful.

[Chris Wong]

(docs#FinEnum.ofNodupList)

[Philippe Duchon]

Ching-Tsun Chou said:

Let's call a bijective map from a finite set A to the set {0, 1, ..., (#A-1)} a numbering. (Perhaps "ordering" is a better name, but that word has been used for other things in Lean.).

Is "enumeration" already used for something else? It would seem to me to be a natural name for this. Or maybe an enumeration would be the inverse - a bijection from some Fin n to A.

I have not tried to do anything with the notion, but this looks like a topic I would be interested in. I would say remaining in the world of (Lean) bijections should be more comfortable than going to lists: "a occurs before b" can then be expressed by comparing images (or preimages, depending on the definition) of a and b. Notably, your point (2) seems like it would not be too hard this way (but I'm still a real beginner, despite having been going through many tutorials for most of a year).

[Ching-Tsun Chou]

@Philippe Duchon , the following is the precise definitions I am using. Note that the codomain of PreNumbering α has a cardinality one bigger than its domain. This provides me with a natural default value 0 which I can use in the definition setNumbering even when α is an empty type. It also explains why I did not use the reverse direction of the bijective map: there is no obvious way to pick a default element of α without invoking choice and assuming α is nonempty. An alternative is to define PreNumbering := Fin (card α) → Option αand use Option.none as the default. Perhaps that is worth a try, but it is not clear how that would impact the proofs of properties I want. My guess is that it won't simplifies things. (For example, it is not obvious what s should be replaced with in the expression BijOn f s (initSeg α s.card), since Option operates on a type, not on a set.)

variable (α : Type*) [Fintype α] [DecidableEq α]

def initSeg (n : ℕ) : Finset (Fin (card α + 1)) := { i | (i : ℕ) < n }

abbrev PreNumbering := α → Fin (card α + 1)

def setNumbering (s : Finset α) : Finset (PreNumbering α) :=
  { f | BijOn f s (initSeg α s.card) ∧ ∀ a ∈ sᶜ, (f a : ℕ) = 0 }

[Ching-Tsun Chou]

BTW, it took me almost 200 lines of Lean to prove the painfully obvious fact that (setNumbering α s).card = s.card.factorial. I proved it by induction on s.card. I would very much like to know if this result can be derived from some existing result about permutations in mathlib in a shorter manner. I thought a lot about it, but couldn't think of any easy way.

[Philippe Duchon]

Not sure why you want to avoid using the cardinality of \alpha, and real bijections. Is there a problem with bijections between empty types? (It looks like Mathlib already has a lot on bijections between finite types, and by using not-quite-bijections you are making your life harder?)

[Ching-Tsun Chou]

Note that α is just the carrier type. The objects we really want to reason about are sets over α and over other types constructed from α. For example, we want to be able to talk about the numberings over a set s ∈ Finset α and prove that there are s.card.factorial of them. If we use bijections on the type α, what do you do with the elements of sᶜ (the complement of s in α)? You need to "fix" them somehow so that they don't add to the cardinality of the numberings.

[Aaron Liu]

You could have a function out of s instead.
You could remove α entirely and only reason about s (make it a type on its own).
You could quotient the functions by equality on s (not recommended).
You could use docs#PFun (partial functions) and have a predicate on the domain (also not recommended).

[Ching-Tsun Chou]

I think you should read the previous discussion in this thread.

[Matt Diamond]

This may be naive but why not represent a numbering as Fin s.card ≃ s?

(Also, isn't this the kind of thing where you could transfer the order from Fin to the set and then talk about lower sets, etc.?)

[Aaron Liu]

Here's one of my suggestions (number 2):

import Mathlib

variable (α : Type*) [Fintype α]

@[reducible] def Numbering := α ≃ Fin (Fintype.card α)

variable {α} {β : Type*} [Fintype β] (i : α ↪ β) (a : Numbering α) (b : Numbering β)

def IsPrefix := ∀ u : α, b (i u) < Fintype.card α

instance : Decidable (IsPrefix i b) := by
  unfold IsPrefix
  infer_instance

theorem card_univ_filter_isPrefix [DecidableEq β] :
    ((Finset.univ : Finset (Numbering β)).filter (IsPrefix i)).card =
    (Fintype.card α).factorial * (Fintype.card β - Fintype.card α).factorial := by
  classical
  sorry

EDIT: I misread the definition of "prefix" (naively assumed it meant one permutation was a docs#List.IsPrefix of the other)

[Ching-Tsun Chou]

@Aaron Liu , I would like to see you complete the proof of the theorem card_univ_filter_isPrefix you stated above and state and prove the property (2) that I wanted in an earlier message in this thread (#new members > How to reason about Fin type @ 💬 ).

[Chris Wong]

This formulation proves property (2), but I'm not sure if it extends to (1)

import Mathlib

class Numbered (α : Type*) extends Fintype α where
  numbering' : α ≃ Fin (Fintype.card α)

def numbering {α} [Numbered α] : α ≃ Fin (Fintype.card α) := Numbered.numbering'

variable {α : Type*} [Numbered α]

def IsPrefix (s : Finset α) := ∀ x, x ∈ s ↔ numbering x < s.card

theorem meow {s t : Finset α} (hs : IsPrefix s) (ht : IsPrefix t) : s ⊆ t ∨ t ⊆ s := by
  wlog hst : s.card ≤ t.card generalizing s t
  · symm
    exact this ht hs (by omega)
  left
  rw [Finset.subset_iff]
  intro x hx
  rw [hs x] at hx
  rw [ht x]
  omega

[Ching-Tsun Chou]

@Chris Wong , your formulation is basically what I started with (see below). I could easily prove property (2) as well. But then I realized that I didn't know how to prove property (1). The natural idea is to observe that a numbering of A with prefix B ⊂ A is equivalent to a numbering of B followed by a numbering of A \ B. This means that it is not sufficient to talk about only the numberings of the carrier type α. We need to be able to talk about the numbering of any subset of α as well. Then it is just a short step to the formulation I ultimately used (see above #new members > How to reason about Fin type @ 💬 ).

def Numbering := α ≃ Fin (card α)

instance : Fintype (Numbering α) := Equiv.instFintype

theorem numbering_card : card (Numbering α) = (card α).factorial := by
  exact Fintype.card_equiv (Fintype.equivFinOfCardEq rfl)

def setPrefix (s : Finset α) : Finset (Numbering α) :=
  { p : Numbering α | ∀ a : α, a ∈ s ↔ p.toFun a < s.card }

theorem set_prefix_subset {s t : Finset α} {p : Numbering α} (h_s : p ∈ setPrefix α s) (h_t : p ∈ setPrefix α t)
    (h_st : s.card ≤ t.card) : s ⊆ t := by
  intro a h_as
  simp [setPrefix] at h_s h_t
  exact (h_t a).mpr (lt_of_le_of_lt' h_st ((h_s a).mp h_as))

theorem set_prefix_card (s : Finset α) :
    (setPrefix α s).card = s.card.factorial * (card α - s.card).factorial := by
  sorry

[Chris Wong]

I got the same idea but implemented it differently. I think that if we instead write the equivalence directly, then the cardinality will fall out of the RHS.

import Mathlib

@[reducible]
def Numbering (α : Type*) [Fintype α] := α ≃ Fin (Fintype.card α)

@[reducible]
def NumberingOn (s : Finset α) := {x // x ∈ s} ≃ Fin s.card

variable {α : Type*} [Fintype α] [DecidableEq α]

def IsPrefix (s : Finset α) (f : Numbering α) :=
  ∀ x, x ∈ s ↔ f x < s.card

def woof {s : Finset α} : {f // IsPrefix s f} ≃ NumberingOn s × NumberingOn sᶜ where
  toFun := fun ⟨f, hf⟩ ↦
    ({
      toFun := fun ⟨x, hx⟩ ↦ ⟨f x, by rwa [← hf x]⟩
      invFun := fun ⟨n, hn⟩ ↦ ⟨f.symm ⟨n, by have := s.card_le_univ; omega⟩, by rw [hf]; simpa⟩
      left_inv := by rintro ⟨x, hx⟩; simp
      right_inv := by rintro ⟨n, hn⟩; simp
    },
    {
      toFun := fun ⟨x, hx⟩ ↦ ⟨f x - s.card, by
        rw [s.mem_compl, hf] at hx
        rw [s.card_compl]
        exact Nat.sub_lt_sub_right (by omega) (by omega)
      ⟩
      invFun := fun ⟨n, hn⟩ ↦ ⟨f.symm ⟨n + s.card, by rw [s.card_compl] at hn; omega⟩, by rw [s.mem_compl, hf]; simp⟩
      left_inv := by
        rintro ⟨x, hx⟩
        rw [s.mem_compl, hf, not_lt] at hx
        simp [Nat.sub_add_cancel hx]
      right_inv := by rintro ⟨n, hn⟩; simp
    })
  invFun := fun (g, g') ↦ ⟨
    {
      toFun := fun x ↦
        if hx : x ∈ s then
          g ⟨x, hx⟩ |>.castLE s.card_le_univ
        else
          g' ⟨x, by simpa⟩ |>.addNat s.card |>.cast (by simp)
      invFun := fun ⟨n, hn⟩ ↦
        if hn' : n < s.card then
          g.symm ⟨n, hn'⟩
        else
          g'.symm ⟨n - s.card, by rw [s.card_compl]; omega⟩
      left_inv := by intro x; by_cases hx : x ∈ s <;> simp [hx]
      right_inv := by
        rintro ⟨n, hn⟩
        by_cases hn' : n < s.card
        · simp [hn']
        · simp [hn']
          split_ifs
          · rename_i h
            have : ∀ x, ↑(g'.symm x) ∉ s := by
              intro x
              simp only [← Finset.mem_compl, Finset.coe_mem]
            exact this _ h |>.elim
          · simp [Nat.sub_add_cancel (not_lt.mp hn')]
    },
    by
      intro x
      constructor
      · intro hx
        simp [hx]
      · by_cases hx : x ∈ s <;> simp [hx]
  ⟩
  left_inv := by
    rintro ⟨f, hf⟩
    ext x
    by_cases hx : x ∈ s
    · simp [hx]
    · rw [hf, not_lt] at hx
      simp [hx]
  right_inv := by
    rintro ⟨g, g'⟩
    simp
    constructor
    · ext x
      simp
    · ext x
      rcases x with ⟨x, hx⟩
      rw [Finset.mem_compl] at hx
      simp [hx]

theorem pyon {s : Finset α} {f : Numbering α} {hf : IsPrefix s f} :
    Fintype.card (NumberingOn s × NumberingOn sᶜ) = s.card.factorial * (Fintype.card α - s.card).factorial := by
  have (hn, hn') := woof ⟨f, hf⟩
  simp only [NumberingOn, Fintype.card_prod]
  rw [Fintype.card_equiv hn, Fintype.card_equiv hn']
  simp

[Ching-Tsun Chou]

@Chris Wong, if your last formulation can be fully fleshed out, it is definitely the right way to go. At one point I actually tried to prove a version of your theorem woof, but was not able to get rid of many type checking errors. I must have made some bad choices in my definitions. Also, nesting equivalence inside equivalence made my head spin. So I gave up on this approach, probably prematurely in retrospect. I'll give it another try to see if I can get it to work.

[Chris Wong]

Great! This is the first time I've written a nested equiv, too :laughing:

BTW, I had some spare time so I completed my proof (edited into the message above). It can definitely be cleaned up (lots of non-terminal simps) but now we know that this definition works.

[Jasper Ganten]

Sort of related - I just read the documentation on Fintype
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Fintype/Basic.html#Fintype
and how the property of a Fintype is proven by constructing a Finset from the elements of the type and then prove that all elements of the type are in the Finset.

So far - so good. But what I struggle to grasp is where this logic would fail if the type was not finite.
I got from the documentation that a the Finset is just the superset containing all the finite sets containing the type, but how does the ∈ here: complete (x : α) : x ∈ elems not just acces the finite set in the Finset which contains alpha? I don't get any smarter reading the documentation on the element definition.
Thanks :)

[Aaron Liu]

It is the case that ∀ (n : Nat), ∃ (f : Finset Nat), n ∈ f (take f := {n}), but it is not the case that ∃ (f : Finset Nat), ∀ (n : Nat), n ∈ f (f would need to contain infinitely many elements).
To construct a Fintype Nat, you need one Finset Nat which contains all Nats. This is impossible.

[Ruben Van de Velde]

Note that complete (x : α) : x ∈ elems means complete : ∀ (x : α), x ∈ elems

[Ruben Van de Velde]

So the Fintype structure contains a specific Finset elems, and a proof that all elements are in that specific elems

[Jasper Ganten]

Thanks a lot, got it!
My mistake in reasoning was to take the ∈ to 'literal' - this now makes much more sense.