Working with ```cast``` and ```HEq```

Stream: lean4

[Sophie Morel]

Okay, so I'm not sure that I'm approaching this the right way... The original problem that I'm trying to solve is proving the following lemma:

import Mathlib.Data.Set.Finite

example (n : ℕ) :
    Set.Finite {p : (k : ℕ) × (l : ℕ) × {s : Finset (Fin (k + l)) // s.card = l} |
    p.1 < n ∧ p.2.1 < n} := by sorry

I was able to write a proof, here it is:

import Mathlib.Data.Set.Finite

open Set in
example (n : ℕ) :
    Set.Finite {p : (k : ℕ) × (l : ℕ) × {s : Finset (Fin (k + l)) // s.card = l} |
    p.1 < n ∧ p.2.1 < n} := by
  set s := {p : (k : ℕ) × (l : ℕ) × {s : Finset (Fin (k + l)) // s.card = l} |
      p.1 < n ∧ p.2.1 < n}
  rw [Set.finite_def]
  apply Nonempty.intro
  set g : s → (k : Finset.range n) × (l : Finset.range n) ×
        {s : Finset (Fin (k + l)) | s.card = l} := (fun p =>
          ⟨⟨p.1.1, Finset.mem_range.mpr p.2.1⟩, ⟨p.1.2.1, Finset.mem_range.mpr p.2.2⟩, p.1.2.2⟩)
  set h : (k : Finset.range n) × (l : Finset.range n) ×
        {s : Finset (Fin (k + l)) | s.card = l} → s :=
        fun p => by refine ⟨⟨p.1, p.2.1, p.2.2⟩, ?_⟩
                    simp only [coe_setOf, mem_setOf_eq]
                    exact ⟨Finset.mem_range.mp p.1.property, Finset.mem_range.mp p.2.1.property⟩
  have h1 : ∀ x, h (g x) = x := by
        intro ⟨p, hp⟩
        simp only [coe_setOf, mem_setOf_eq, Sigma.eta]
  have h2 : ∀ x, g (h x) = x := by
        intro ⟨k, l, t⟩
        simp only [coe_setOf, mem_setOf_eq, id_eq]
  set e : s ≃ (k : Finset.range n) × (l : Finset.range n) ×
        {s : Finset (Fin (k + l)) | s.card = l} :=
        {toFun := g
         invFun := h
         left_inv := h1
         right_inv := h2}
  apply Fintype.ofEquiv _ e.symm

However, it a bit clunky, and I have several similar results to prove (but not similar enough to have an obvious common generalizations: the difference is that there are more or less factors in the product).

So I though that the best would be to have a result saying "if I have a map with a finite image and finite fibers, then its domain is finite", or something slightly more general. This was easy, here it is:

import Mathlib.Data.Set.Finite

theorem Set.Finite.of_finite_image_of_finite_fibers {α : Type*} {β : Type*} {s : Set α}
    {f : α → β} (hfin1 : Set.Finite (f '' s)) (hfin2 : ∀ y ∈ f '' s, Set.Finite (f ⁻¹' {y})) :
    Set.Finite s :=
  Set.Finite.subset (Set.Finite.biUnion hfin1 hfin2) (fun x hx ↦ Set.mem_biUnion
  (Set.mem_image_of_mem f hx) (by rw [Set.mem_preimage, Set.mem_singleton_iff]))

But I ran into trouble when trying to apply it to my example. First I defined the function, the obvious idea is projection on the first two factors, here it is:

def f : (k : ℕ) × (l : ℕ) × {s : Finset (Fin (k + l)) // s.card = l} → ℕ × ℕ := fun p ↦ ⟨p.1, p.2.1⟩

Okay, now I need to prove that the fibers of f are finie. So the most obvious is to define an injective map g from the fiber at (k,l) into Finset (Fin (k + l)), because that last thing is certainly finite. Here is the map g, already I am starting to struggle:

def g (k l : ℕ) : f ⁻¹' {⟨k, l⟩} → Finset (Fin (k + l)) :=
          fun x ↦ by have h := Prod.eq_iff_fst_eq_snd_eq.mp
                       (Set.mem_singleton_iff.mp (Set.mem_preimage.mp x.2))
                     simp only at h
                     refine cast ?_ x.1.2.2.1
                     simp_rw [← h.1, ← h.2, f]

Now I just need to prove that g is injective, except I can't seem to do it. I am battling expressions full of cast and HEq and I don't really know what to do. I can show you how I started, but very quickly I start going round in circles:

example (k l : ℕ) : Function.Injective (g k l) := by
  intro x y
  have hx := Prod.eq_iff_fst_eq_snd_eq.mp (Set.mem_singleton_iff.mp (Set.mem_preimage.mp x.2))
  have hy := Prod.eq_iff_fst_eq_snd_eq.mp (Set.mem_singleton_iff.mp (Set.mem_preimage.mp y.2))
  unfold f at hx hy
  simp only at hx hy
  intro h
  ext
  · rw [hx.1, hy.1]
  · apply heq_of_cast_eq

And so on...

[Sophie Morel]

I understand that of the problems is that, if even if, say, I know that n = m, then this does not mean that Fin n = Fin m and I need to use cast in order to move elements between these types. But that doesn't tell me how to use this strange cast function...

[Yaël Dillies]

Certainly m = n implies Fin m = Fin n! What you mean is that the typechecker doesn't know they are equal unless you actually substitute the m = n equality.

[Yaël Dillies]

Do you know about tactic#subst ?

[Sophie Morel]

I certainly don't know about that tactic. Let me check it out, thanks !

[Sophie Morel]

(Equality is complicated.)

[Kyle Miller]

Going back to the beginning, I think this would be easiest rewriting it as a product involving set products, and it's a product of finite sets.

[Kyle Miller]

Oh, oops, missed the dependence when reading it quickly.

[Sophie Morel]

Yeah, I'm in a noob but I'm not that much of a noob. :sweat_smile:

[Sophie Morel]

Okay, I can't really make subst work yet but also I have to go to bed because I have to catch a train super early tomorrow, so I'll think more about it and be back later.

[Kyle Miller]

I have to go, but this is what I'd use:

theorem foo {n : ℕ} :
    {p : (q : (ℕ × ℕ)) × {s : Finset (Fin (q.1 + q.2)) // s.card = q.2} |
      p.1.1 < n ∧ p.1.2 < n} =
      Finset.sigma (Finset.range n ×ˢ Finset.range n) (fun q =>
        (Finset.univ : Finset ({s : Finset (Fin (q.1 + q.2)) // s.card = q.2}))) := by
    ext ⟨k, l⟩
    simp

[Kyle Miller]

That establishes Set.Finite for a related set, and then your theorem then is about reassociating that dependent product.

[Kyle Miller]

(@Yaël Dillies would you know if there's at least an equivalence to reassociate this dependent product?

[Yaël Dillies]

To get the dependent type outside of the subtype?

[Sophie Morel]

Kyle Miller said:

I have to go, but this is what I'd use:

theorem foo {n : ℕ} :
    {p : (q : (ℕ × ℕ)) × {s : Finset (Fin (q.1 + q.2)) // s.card = q.2} |
      p.1.1 < n ∧ p.1.2 < n} =
      Finset.sigma (Finset.range n ×ˢ Finset.range n) (fun q =>
        (Finset.univ : Finset ({s : Finset (Fin (q.1 + q.2)) // s.card = q.2}))) := by
    ext ⟨k, l⟩
    simp

(Yes, I'm back. Only for a few minutes :fingers_crossed:, I wanted to check something in my code.)
Interesting, thanks ! I've been wondering about reassociating the dependent product myself, it seemed that it would make my life easier.

I wanted to check what I did in the original proof: I construct an equivalence with (k : Finset.range n) × (l : Finset.range n) × {s : Finset (Fin (k + l)) | s.card = l}, and then poof, Lean knows that that one is finite ! (I know its PSigma.fintype working its magic in the background, but still, magic.) So maybe another way to go would be to make the construction of the equivalence more efficient... Okay, I'm really going to bed now, I swear.

[Kyle Miller]

@Sophie Morel I realized right when I had to go that there's a more direct way to do this. It's still the same idea, write down a Finset expression that calculates the correct thing:

example (n : ℕ) :
    Set.Finite {p : (k : ℕ) × (l : ℕ) × {s : Finset (Fin (k + l)) // s.card = l} |
    p.1 < n ∧ p.2.1 < n} := by
  convert_to Set.Finite ((Finset.range n).sigma fun k =>
    (Finset.range n).sigma fun l =>
      (Finset.univ : Finset ({s : Finset (Fin (k + l)) // s.card = l}))).toSet
  · ext ⟨k, l, s⟩
    simp
  apply Finset.finite_toSet

[Kyle Miller]

I used convert_to rather than write a separate lemma that gives an equality of the sets.

[Terence Tao]

Perhaps it might be easier to work with an equivalent set such as {(k,l,s) : ℕ × ℕ × (Finset ℕ) | s ⊆ Finset.range (k+l) ∧ s.card = l ∧ k ∈ Finset.range n ∧ l ∈ Finset.range n} throughout, to avoid dependent types entirely? Note that this (up to coercions) is a subset of (Finset.range n) × (Finset.range n) × Finset (Finset.range (2*n)) so is manifestly finite.

[Sophie Morel]

Terence Tao said:

Perhaps it might be easier to work with an equivalent set such as {(k,l,s) : ℕ × ℕ × (Finset ℕ) | s ⊆ Finset.range (k+l) ∧ s.card = l ∧ k ∈ Finset.range n ∧ l ∈ Finset.range n} throughout, to avoid dependent types entirely? Note that this (up to coercions) is a subset of (Finset.range n) × (Finset.range n) × Finset (Finset.range (2*n)) so is manifestly finite.

The thing is that I can't choose what I am working with unless I do some rewriting of already existing mathlib code, or unless I duplicate some work. These are from the calculation of the power series of f(x + y) from that of f(x), I am proving that the new power series converges without any completeness assumptions if the original power series was finite. If I'm trying to minimize the amount of pain for myself, not rewriting all the technical lemmas there seems like a good option !

[Sophie Morel]

Kyle Miller said:

Sophie Morel I realized right when I had to go that there's a more direct way to do this. It's still the same idea, write down a Finset expression that calculates the correct thing:

example (n : ℕ) :
    Set.Finite {p : (k : ℕ) × (l : ℕ) × {s : Finset (Fin (k + l)) // s.card = l} |
    p.1 < n ∧ p.2.1 < n} := by
  convert_to Set.Finite ((Finset.range n).sigma fun k =>
    (Finset.range n).sigma fun l =>
      (Finset.univ : Finset ({s : Finset (Fin (k + l)) // s.card = l}))).toSet
  · ext ⟨k, l, s⟩
    simp
  apply Finset.finite_toSet

Great, thank you !

Is there a list of super-cool secret Lean4 tactics somewhere, with their documentation ? It seems that every time I ask a question, somebody answers "oh, you don't know the frobnicate tactic, that's exactly the thing for this situation". Meanwhile I was struggling the other day to find the documentation of rewrite. :sweat_smile:
(ETA: I did figure it out, I just need to hover over the tactic name in vscode and a handy documentation pop ups. And here I was trying to find it in the mathlib documentation...)

[Yaël Dillies]

Yes, mathlib documentation for tactics has disappeared in the port. This is something we're aware of but nobody fixed it yet.

[Sophie Morel]

Well, I've been examining Kyle's proof and it's pretty cool. I definitely have to learn more about convert and convert_to, because it seems like something I could have used in the past. (I've finally learned how to use calc instead of piling 13 levels of le_trans and lt_of_lt_and_le etc, and I'm cursing myself for not taking the time to learn earlier.)

[Sophie Morel]

Yaël Dillies said:

Yes, mathlib documentation for tactics has disappeared in the port. This is something we're aware of but nobody fixed it yet.

Ah, that explains why I have a much harder time finding it now, it's not there ! :laughing: It's reassuring in a way, because I felt like I had become very stupid all of a sudden.

[Riccardo Brasca]

Sophie Morel said:

Kyle Miller said:

Sophie Morel I realized right when I had to go that there's a more direct way to do this. It's still the same idea, write down a Finset expression that calculates the correct thing:

example (n : ℕ) :
    Set.Finite {p : (k : ℕ) × (l : ℕ) × {s : Finset (Fin (k + l)) // s.card = l} |
    p.1 < n ∧ p.2.1 < n} := by
  convert_to Set.Finite ((Finset.range n).sigma fun k =>
    (Finset.range n).sigma fun l =>
      (Finset.univ : Finset ({s : Finset (Fin (k + l)) // s.card = l}))).toSet
  · ext ⟨k, l, s⟩
    simp
  apply Finset.finite_toSet

Great, thank you !

Is there a list of super-cool secret Lean4 tactics somewhere, with their documentation ? It seems that every time I ask a question, somebody answers "oh, you don't know the frobnicate tactic, that's exactly the thing for this situation". Meanwhile I was struggling the other day to find the documentation of rewrite. :sweat_smile:
(ETA: I did figure it out, I just need to hover over the tactic name in vscode and a handy documentation pop ups. And here I was trying to find it in the mathlib documentation...)

You can have a look here. It is just a copy paste of the official documentation, but at least it is a list of tactics.

[Sophie Morel]

Thank you!
Hahaha, I've been playing with convert and this thing is freaking dark magic!

[Kyle Miller]

@Sophie Morel One of the things you can do with it is use to handle "wrong" Fintype and DecidableEq instances. If exact fails just because of differences in such instances, convert should succeed. (If it doesn't, ping me!)

Other related tactics are:

• congr! if the goal is an iff, eq, heq, or any other reflexive relation, and you want to reduce to the case of showing that corresponding sub-expressions are equal. (convert/convert_to are implemented using it)
• congrm is similar, but you can provide a pattern with placeholders, where the placeholders are in positions where you want a new sub-goal
• gcongr is for "generalized congruence," which can handle relations like inequalities, vs equalities/iffs in the previous tactics. It is more opinionated about doing what makes sense in context.
• apply_fun can handle applying a function at an equality hypothesis or, if it's injective, at the goal. It's not super related, but it's also got something to do with applying congruence lemmas so I'll include it.

[Sophie Morel]

Thank you for the list of useful tactics ! Even for the ones I already knew, you have just taught me about new ways to use them.