How to deal with `match`?

Stream: general

[Zikang Yu]

I was trying to prove some basic facts about the following concept, namely, a partition induced by a finite set on a dense linear order without endpoints.

variable {n : ℕ} (f : Fin n → α) (hf : StrictMono f)
/--
Given `n` points `f 0, f 1, ..., f (n-1)`, this function generates a partition of `α`
into `2n + 1` sets. The points are assumed to be sorted.
The partition is `(-∞, f 0), {f 0}, (f 0, f 1), {f 1}, ..., {f (n-1)}, (f (n-1), ∞)`.
-/
noncomputable def points_to_partition :Set (Set α) :=
match n with
| 0 => {univ}
| n + 1 =>
  let singletons := ⋃ (i : Fin (n + 1)), {{f i}}
  let intervals_between := ⋃ (i : Fin n), {Ioo (f i.castSucc) (f (Fin.succ i))}
  let first_interval := {Iio (f 0)}
  let last_interval := {Ioi (f (Fin.last n))}
  singletons ∪ intervals_between ∪ first_interval ∪ last_interval

/--
Given a finite set of points `F`, this function induces a partition of `α` into
open intervals and singletons determined by the points in `F`.
-/
noncomputable def finset_to_partition (F : Finset α) : Set (Set α) :=
  let f := Finset.orderEmbOfFin F (rfl)
  points_to_partition f (OrderEmbedding.strictMono f)

It works actually qutie well. I've successfully proved that these functions do generate partitions, where the "partition" is implemented by IsPartition from Mathlib.Data.Setoid.Partition as a predicate for Set (Set α)

But then the problem arises when I try to prove the following lemma:

/-- If a finite set `A` is a subset of `B`, then the partition induced by `B`
    is a refinement of the partition induced by `A`. -/
lemma finset_to_partition_is_refinement_of_subset (A B : Finset α) (hAB : A ⊆ B) :
    ∀ d ∈ finset_to_partition B, ∃ c ∈ finset_to_partition A, d ⊆ c := by

The proof is quite direct. Just find some suitable set in finset_to_partition A for all four forms of d by analyzing the relationship between endpoints of d and A.

At first I tried to use cases h : B.card and hoped that the match expression in context would collapse automatically but it didn't happen. So I had to use split. But then several inaccessible variables were created, and included some heterogeneous equation like ⇑(B.orderEmbOfFin ⋯) ≍ f✝. Now I have no idea about what to do next.

The problem may be raised by the rfl tactic in the definition of finset_to_partition but I don't know how to fix it.

[Zikang Yu]

Now I've found a way to completely bypass this issue by simply adding some auxiliary lemmas, but I'm still confused about the heterogeneous equation and why it appears.

[Aaron Liu]

Zikang Yu said:

At first I tried to use cases h : B.card and hoped that the match expression in context would collapse automatically but it didn't happen. So I had to use split. But then several inaccessible variables were created, and included some heterogeneous equation like ⇑(B.orderEmbOfFin ⋯) ≍ f✝. Now I have no idea about what to do next.

I don't understand. Just continue the proof? It sounds like you had a proof in mind and gave up for since reason after splitting the match.

[Zikang Yu]

The split tactic made the context quite complicated with the following inaccessible variables:

x✝ : StrictMono ⇑(B.orderEmbOfFin ⋯)
n✝¹ : ℕ
f✝¹ : Fin n✝¹ → α
hf✝¹ : StrictMono f✝¹
n✝ : ℕ
f✝ : Fin (n✝ + 1) → α
hf✝ : StrictMono f✝
heq✝² : B.card = n✝.succ
heq✝¹ : ⇑(B.orderEmbOfFin ⋯) ≍ f✝
heq✝ : x✝ ≍ hf✝
hd : d ∈
  insert (Ioi (f✝ (Fin.last n✝)))
    (insert (Iio (f✝ 0)) ((range fun x ↦ {f✝ x}) ∪ range fun x ↦ Ioo (f✝ x.castSucc) (f✝ x.succ)))

And you can see that the actual function I need to access is f✝, which is heterogeneously equal to B.orderEmbOfFin. Even I exposed f✝ as f, I don't know how to prove that range f = B, which it should be.

[Aaron Liu]

Well we can start be using rename_i to name all the variables

[Aaron Liu]

Oh Finset.orderEmbOfFin takes an equality argument

[Aaron Liu]

This should be a lot easier if we use that instead

[Aaron Liu]

Zikang Yu said:

And you can see that the actual function I need to access is f✝, which is heterogeneously equal to B.orderEmbOfFin. Even I exposed f✝ as f, I don't know how to prove that range f = B, which it should be.

My guess is that you can prove that range (B.orderEmbOfFin rfl) = B and then just grind will solve it (grind has been pretty good at solving my intractable casting goals)

[Zikang Yu]

range (B.orderEmbOfFin rfl) = B is actually trivial. The real problem is that the function in hd is not B.orderEmbOfFin but f✝. In summary, the very first thing to do is to connect d with B, i.e. , to handle heterogeneous equality.

[Aaron Liu]

What I mean is, first you should name f✝ something accessible, then prove that range (B.orderEmbOfFin rfl) = B, and if you have the proof in the context then grind will be able to do range f✝ = B.

[Zikang Yu]

Oh, I got it, and it works! Thanks for your advice. I have totally no idea about how grind tactic works well on such coercion. Nevertheless, it will still be too complicated to have so many variables in context, since there's still another finset_to_partition in goal to unfold.

[Jakub Nowak]

Try to post complete code, it makes it easier to help you. In this case you should've included:

import Mathlib

variable {α : Type*} [LinearOrder α]
open Set

You should've also included the partial proof that leads to the problematic context with match.

Does this help you?

import Mathlib

variable {α : Type*} [LinearOrder α]
open Set

/--
Given `n` points `f 0, f 1, ..., f (n-1)`, this function generates a partition of `α`
into `2n + 1` sets. The points are assumed to be sorted.
The partition is `(-∞, f 0), {f 0}, (f 0, f 1), {f 1}, ..., {f (n-1)}, (f (n-1), ∞)`.
-/
noncomputable def points_to_partition {n : ℕ} (f : Fin n → α) (hf : StrictMono f) : Set (Set α) :=
match n with
| 0 => {univ}
| n + 1 =>
  let singletons := ⋃ (i : Fin (n + 1)), {{f i}}
  let intervals_between := ⋃ (i : Fin n), {Ioo (f i.castSucc) (f (Fin.succ i))}
  let first_interval := {Iio (f 0)}
  let last_interval := {Ioi (f (Fin.last n))}
  singletons ∪ intervals_between ∪ first_interval ∪ last_interval

/--
Given a finite set of points `F`, this function induces a partition of `α` into
open intervals and singletons determined by the points in `F`.
-/
noncomputable def finset_to_partition (F : Finset α) : Set (Set α) :=
  let f := Finset.orderEmbOfFin F (rfl)
  points_to_partition f (OrderEmbedding.strictMono f)

/-- If a finite set `A` is a subset of `B`, then the partition induced by `B`
    is a refinement of the partition induced by `A`. -/
lemma finset_to_partition_is_refinement_of_subset (A B : Finset α) (hAB : A ⊆ B) :
    ∀ d ∈ finset_to_partition B, ∃ c ∈ finset_to_partition A, d ⊆ c := by
  intro d hd
  unfold finset_to_partition at hd
  unfold points_to_partition at hd
  cases h : B.card with
  | zero =>
    rw! [h] at hd
    simp at hd
    sorry
  | succ n =>
    rw! [h] at hd
    simp at hd
    obtain hd | hd | ⟨i, hd⟩ | ⟨i, hd⟩ := hd
    · sorry
    · sorry
    · sorry
    · sorry

If you're using cases with an expression, not a variable, Lean won't replace occurrences of that expression in context, so you have to use e.g. rw. In this case I had to use rw! instead.
Ah, sorry, cases actually does replaces expression. At least it tries. But it failed in this case, so you have to use rw! manually.
I'm not sure why

    rw! [h] at hd
    simp at hd

worked, but simp [*] at hd didn't. I'm guessing it has some problems with dependant types.