Finitely many strings of length ≤ n?

Stream: Is there code for X?

[Jacob Weightman]

I just wrapped up a proof about a string rewriting system that makes use of the pigeonhole principle and the fact that there are finitely many short strings. I have the following definition of "short strings," and the corresponding hole in my proof:

variable {α : Type u} [Inhabited α][Fintype α]

def ShortList (α : Type u) (n : ℕ) :=
  { l : List α // l.length ≤ n }

instance ShortList.fintype [Fintype α] {n : ℕ} : Fintype (ShortList α n) :=
  -- There are finitely many List α of length i, by induction:
  -- zero => there is exactly one empty string, [].
  -- succ i => prefix each of the finitely many List α of length i with each of the finitely many
  --           elements of α. There are #a * #(ShortList α i) of these.
  -- The strings of length ≤ n is the union of strings of length i ≤ n. Since there are finitely
  -- many strings of length i, and the union of finite sets is finite, there are also finitely many
  -- strings of length ≤ n. ∎
  sorry

My initial searching of Mathlib didn't turn up anything quite like what I was looking for, but I thought I'd ask here before I spent time reinventing the wheel. Is there something like this already?

[Robin Arnez]

Your ShortList is List.Vector and in fact there is an instance for Fintype of it!

variable {α : Type u} [Inhabited α][Fintype α]

abbrev ShortList (α : Type u) (n : ℕ) := List.Vector α n

instance ShortList.fintype [Fintype α] {n : ℕ} : Fintype (ShortList α n) :=
  inferInstance

[Edward van de Meent]

Robin Arnez said:

Your ShortList is List.Vector and in fact there is an instance for Fintype of it!

not quite. List.Vector is lists of a certain length, while it seems ShortList is meant to refer to lists of a certain length or below

[Robin Arnez]

Oh I missed that detail

[Robin Arnez]

Then perhaps you'd actually want to do this yourself

[Robin Arnez]

or actually this works:

abbrev ShortList (α : Type u) (n : ℕ) := (i : Fin (n + 1)) ×' List.Vector α i.val

instance ShortList.fintype [Fintype α] {n : ℕ} : Fintype (ShortList α n) :=
  inferInstance

[Edward van de Meent]

actually, you don't need PSigma here, just Sigma works

[Edward van de Meent]

and i imagine that the subtype definition has better definitional equality, so it will probably be easier to get the Fintype instance from proving an equivalence between the sigmatype and the subtype

[Robin Arnez]

Yeah, right, for some reason I thought × was Prod and ×' was Sigma lol. And yeah, an equiv is probably what you want, shouldn't be too hard though.

[Edward van de Meent]

(× works for both Prod and Sigma)

[Robin Arnez]

(yeah I'm aware)

[Kyle Miller]

(i : Fin (n + 1)) × List.Vector α i seems fine to me

[Edward van de Meent]

it is prone to getting into dependent type hell tho

[Violeta Hernández]

Maybe you instead just want to build an equivalence between {l // l.length ≤ n} and the sigma type?

[Chris Wong]

Since nobody's brought it up yet, docs#Fintype.ofEquiv

[Edward van de Meent]

Edward van de Meent said:

so it will probably be easier to get the Fintype instance from proving an equivalence between the sigmatype and the subtype

that was what i was attempting to hint at here

[Jacob Weightman]

Okay, I haven't done much practical Lean work with dependent product types, but it isn't quite obvious to me how to change my proof to work with them — "dependent type hell" seems like an apt description. I've also tried building the equivalence suggested by @Violeta Hernández, but run into a similar problem. Maybe someone could give me a pointer on how to finish this proof?

def ShortList (α : Type u) (n : ℕ) :=
  { l : List α // l.length ≤ n }

abbrev ShortList' (α : Type u) (n : ℕ) := (i : Fin (n + 1)) × List.Vector α i

def ShortList_iso (α : Type u) (n : ℕ) : ShortList' α n ≃ ShortList α n :=
  let toFun (l : ShortList' α n) : ShortList α n :=
    let ⟨i, v⟩ := l
    have π : v.val.length ≤ n := by
      simp; rw [← Nat.lt_succ]; exact i.isLt
    ⟨v.val, π⟩
  let fromFun (l : ShortList α n) : ShortList' α n :=
    let len : Fin (n + 1) := l.val.length
    have π : l.val.length = len := by
      simp [len]; rw [Nat.mod_eq_of_lt]; rw[Nat.lt_succ]; exact l.property
    ⟨l.val.length, ⟨l.val, π⟩⟩
  have π₁ : Function.LeftInverse fromFun toFun := by
    intro l; simp [toFun, fromFun]
    induction' l with a b
    simp
    -- rw [← eq_cast_iff_heq]
    -- rfl
    -- #check eq_cast_iff_heq
    sorry
  have π₂ : Function.RightInverse fromFun toFun := by
    intro l; simp [toFun, fromFun]
  ⟨toFun, fromFun, π₁, π₂⟩

instance ShortList'.fintype [Fintype α] {n : ℕ} : Fintype (ShortList' α n) :=
  inferInstance

instance ShortList.fintype [Fintype α] {n : ℕ} : Fintype (ShortList α n) :=
  Fintype.ofEquiv _ (ShortList_iso α n)

Here's the context at the point of the sorry:

α✝ : Type u
inst✝¹ : Inhabited α✝
inst✝ : Fintype α✝
T : TagSystem α✝
α : Type u
n : ℕ
toFun : ShortList' α n → ShortList α n := fun l ↦
  match l with
  | ⟨i, v⟩ =>
    let_fun π := ⋯;
    ⟨↑v, π⟩
fromFun : ShortList α n → ShortList' α n := fun l ↦
  let len := ↑(↑l).length;
  let_fun π := ⋯;
  ⟨↑(↑l).length, ⟨↑l, π⟩⟩
a : Fin (n + 1)
b : List.Vector α ↑a
⊢ HEq ⟨↑b, ⋯⟩ b

I haven't encountered heterogeneous equality before, and my familiarity with casting is quite lacking. This has me at a loss for how to prove that. At this point, I'm also not really convinced that pulling in this heavy machinery simplifies the proof at all, which makes me feel like I must be missing something. Could any of you kind folks help me bridge this gap?

[Violeta Hernández]

Currently AFK so can't help much with the proof, but perhaps you want to prove a more general equivalence? Namely for f : b -> a and p : a -> Prop, {x // p (f x)} is equivalent to {a // p a} ×' {x // f x = a}.

[Violeta Hernández]

Your specific case is f = length and p x = x ≤ n

[Violeta Hernández]

(in fact, maybe this already exists?)

[Violeta Hernández]

I mention this because I've realized this result would also be useful to me!

[Bhavik Mehta]

Note docs#List.finite_length_le exists

[Kyle Miller]

(@Jacob Weightman It's worth evaluating whether you need Fintype in your argument for some reason, or if Finite suffices — if it's for proofs, it's usually the right choice. docs#Fintype.ofFinite is one of the ways to temporarily get a Fintype instance in the middle of a proof if you really need it.)

[Matt Diamond]

yeah, if Finite suffices then the proof is literally just (List.finite_length_le α n).to_subtype, as @Bhavik Mehta pointed out

[Violeta Hernández]

That's a shame, I do think the Fintype instance could still be useful.

[Aaron Liu]

Why does ext work better than simp here?

import Mathlib

def ShortList (α : Type u) (n : ℕ) :=
  { l : List α // l.length ≤ n }

abbrev ShortList' (α : Type u) (n : ℕ) := (i : Fin (n + 1)) × List.Vector α i

def ShortList_iso (α : Type u) (n : ℕ) : ShortList' α n ≃ ShortList α n where
  toFun a := ⟨a.snd.toList, a.snd.toList_length.symm ▸ a.fst.is_le⟩
  invFun b := ⟨⟨b.val.length, Nat.lt_add_one_of_le b.prop⟩, ⟨b.val, rfl⟩⟩
  left_inv a := by
    ext i j
    · simp
    · simp [List.Vector.toList]
  right_inv b := rfl

instance ShortList'.fintype [Fintype α] {n : ℕ} : Fintype (ShortList' α n) :=
  inferInstance

instance ShortList.fintype [Fintype α] {n : ℕ} : Fintype (ShortList α n) :=
  Fintype.ofEquiv _ (ShortList_iso α n)

[Violeta Hernández]

Here's the proof I was talking about:

import Mathlib

variable {α β : Type*}

def preimageEquiv (f : β → α) (p : α → Prop) :
    {x // p (f x)} ≃ (a : {a // p a}) ×' f ⁻¹' {a.1} where
  toFun x := ⟨⟨f x.1, x.2⟩, ⟨x.1, rfl⟩⟩
  invFun x := ⟨x.2, by convert x.1.2; exact x.2.2⟩
  left_inv x := by simp
  right_inv x := by
    have : f x.2 = x.1 := x.2.2
    ext
    · simpa
    · simp

instance (n : ℕ) [Fintype α] : Fintype { l : List α // l.length ≤ n } :=
  let _ : Fintype { a // a ≤ n } :=
    Fintype.ofFinset (p := Set.Iic n) (Finset.Iic n) (by simp)
  let _ : Fintype ((a : { a // a ≤ n }) ×' ↑(List.length ⁻¹' {↑a})) :=
    inferInstanceAs (Fintype ((a : { a // a ≤ n }) ×' List.Vector α a))
  Fintype.ofEquiv _ (preimageEquiv List.length (· ≤ n)).symm

[Violeta Hernández]

(there's probably some better way to get the Fintype { a // a ≤ n } instance)

[Kyle Miller]

Violeta Hernández said:

That's a shame, I do think the Fintype instance could still be useful.

There's nothing about this that means that there couldn't also be a Fintype instance. I'd suggest adding it to the same file with the Set.Finite lemmas.

Finite instances don't suffice for Fintype instances, since the Fintype instance needs a real Fintype instance for the element type to be computationally useful.

[Violeta Hernández]

Aaron Liu said:

Why does ext work better than simp here?

I think simp has an easier time applying after some of the dependent type theory hell is dispatched via docs#PSigma.ext.

[Violeta Hernández]

At some point I think I wanted this exact Fintype instance for my Rubik's cube project, so I'd be glad if we could PR that alongside the Finite instance.

[Kyle Miller]

The pattern can be (1) define the Fintype instance and (2) make use of Fintype.ofFinite to apply the instance for the Finite instance.

This was done a lot in the core Finite instances, which, at least at some point, were defined in terms of corresponding Fintype instances.

[Jacob Weightman]

Wow, if only I'd found List.finite_length_le before! Finite is definitely sufficient to apply the relevant pigeonhole principle theorems. I ended up with this very economical code:

def ShortList (α : Type u) (n : ℕ) :=
  { l : List α // l.length ≤ n }

instance ShortList.finite {α : Type u}{n : ℕ} [Finite α] : Finite (ShortList α n) :=
  List.finite_length_le α n

Thanks so much for all the good discussion, I definitely learned some new things!

[Matt Diamond]

you might want to write it as (List.finite_length_le α n).to_subtype to avoid things breaking if the definition of Set.Finite changes (this is what people mean when they talk about "defeq abuse"), but it's also not a big deal, especially for a personal project