Tricky recursive proof

Stream: maths

[Bhavik Mehta]

TL;DR: An abstracted version of my problem is here, I'd like to prove the theorem at the bottom and I can't seem to make any serious progress.
A bit more detail on the problem: we're interested in families 𝒜 of subsets of X={1,...,n} (and each subset has size r) and we'd like to minimise a packing-like quantity: the size of its shadow. (The definitions of these things shouldn't matter for this; the types are in the link above, and the actual definitions are here, if they're needed. I think I've put all the necessary lemmas in the abstracted version though.)
The goal is to prove that among families of a fixed size, the minimum size of shadow is attained at a particular family (I'll call this C). To do this, we apply "compressions": applying a compression keeps the family the same size and (weakly) decreases the size of its shadow (under certain conditions), and makes the family look a little bit more like C. (Compressions are also idempotent)
What are these conditions? Compressing using the (fin)sets (U,V) (where |U| = |V|) will decrease the size of the shadow of 𝒜 if 𝒜 is already compressed with respect to every pair (U₁,V₁) such that |U₁| < |U| (again, |U₁|=|V₁|).
Also, applying a (U,V) compression strictly decreases a particular quantity which I've called the c_measure.
Putting all this together, we get the following lemma

lemma compression_improved (U V : finset X) (𝒜 : finset (finset X)) (h₁ : gamma U V)
  (h₂ : ∀ U₁ V₁, gamma U₁ V₁ ∧ U₁.card < U.card → is_compressed U₁ V₁ 𝒜) (h₃ : ¬ is_compressed U V 𝒜):
  c_measure (compress_family U V 𝒜) < c_measure 𝒜 ∧ (compress_family U V 𝒜).card = 𝒜.card ∧ (∂ compress_family U V 𝒜).card ≤ (∂𝒜).card := sorry

(gamma is a relation which essentially says it's worthwhile to compress using this pair - one of the things in gamma is that |U|=|V|) (∂ is notation for the shadow).
I'll state also the theorem I'd like to prove from this:

theorem kruskal_katona_helper (𝒜 : finset (finset X)) :
  ∃ (ℬ : finset (finset X)), 𝒜.card = ℬ.card ∧ (∂ℬ).card ≤ (∂𝒜).card ∧ (∀ U V, gamma U V → is_compressed U V ℬ) :=

(I'll prove later that ℬ satisfying the last condition means that it is exactly C, but this will do for now.)
The maths proof looks something like this. Set 𝒜_0 = 𝒜, and we'll construct a (finite) sequence 𝒜_n. If 𝒜_k is already compressed with respect to all (U,V) in gamma, stop. If not, choose (U,V) in gamma such that 𝒜_k isn't (U,V)-compressed, with |U| minimal, and set 𝒜_(k+1) to be the (U,V)-compression of 𝒜_k. This process terminates, since the c_measure is strictly decreasing (and it's always a natural number). Then set ℬ as the final element of this sequence, and we're done.

This doesn't seem too hard, but I'm pretty muddled on how to prove this in lean. Actually constructing the sequence seems wrong - I'd have to prove that it'll terminate and it's not clear how (I'd kinda like something like Haskell's unfoldr, maybe?). There's the stuff about well founded relations, but I only get stuff about the compression being better if |U| was picked carefully. It's also not immediate that if you (U,V)-compress, then (U',V')-compress then you're still (U,V)-compressed, so inducting on the size of |U| wouldn't work either. Any help appreciated

[Reid Barton]

It sounds like you want to use (strong?) induction on whatever c_measure is

[Bhavik Mehta]

I couldn't get that to work because of the thing I mention in the last paragraph - we've got to choose |U| minimal at each stage

[Reid Barton]

As far as I can see, that is a separate concern

[Reid Barton]

Unless there is some detail I'm missing. When you construct your sequence, do you need anything about the previous A_k (other than it came from A by some sequence of compressions)?

[Reid Barton]

It looks like you should be able to prove the following statement by induction on n : nat: if A is any family with c_measure A = n, then ...

[Bhavik Mehta]

Ah I see - yeah I could construct the sequence without the fact that the previous compressions were chosen carefully, but how would I prove anything about the sequence?

[Reid Barton]

Don't actually construct the sequence

[Bhavik Mehta]

Sure, I'd construct the thing I want to be B using strong induction, but even then how would I prove things about the result?

[Reid Barton]

Well, for example, if n = 0, then you would learn that there can't be any U V for which A is not compressed

[Reid Barton]

More generally, either (what I wrote above) or there exists A' obtained by applying some compression with a smaller c_measure, and then apply the inductive hypothesis to A'

[Reid Barton]

Sure, I'd construct the thing I want to be B using strong induction, but even then how would I prove things about the result?

Oh I see. This is not quite what I was suggesting.
Instead modify the statement of kruskal_katona_helper to (n : nat) (A : finset (finset X)) (hn : c_measure A = n) : ...

[Reid Barton]

Try to apply a compression step, if there's none you can apply, use A as B, else you get A' with smaller c_measure, apply the induction hypothesis and use its B as B.

[Bhavik Mehta]

This makes sense, thanks!

[Bhavik Mehta]

I'll give it a go now

[Reid Barton]

In that case, the fancier but basically equivalent way is to prove kruskal_katona_helper directly by well-founded induction on the order induced by c_measure

[Bhavik Mehta]

I think I see where I got stuck - I was trying to use the well-founded fixpoint and getting myself confused

[Reid Barton]

We often naturally express proofs like this as a construction but sometimes it can be more convenient to reformulate the proof to avoid the construction for the purpose of formalization

[Bhavik Mehta]

Yeah I realised construction wasn't the right way to do this in lean but I couldn't get what the right way was

[Bhavik Mehta]

Separating out the minimality of |U| as a concern from c_measure was a key point I missed though

[Bhavik Mehta]

I've got the line by_cases (∃ U V, gamma U V ∧ ¬ is_compressed U V A),, and it doesn't like this because the type of the expression isn't decidable - I can use classical logic but it doesn't seem right to just assert locally that the expression I want is decidable. Instead, U and V range over a finite set, not being compressed is definitely decidable and gamma looks like ∃ (HU : U ≠ ∅), ∃ (HV : V ≠ ∅), {decidable stuff using HU and HV} as argument, so this thing should be decidable... How can I show this? I've found the definition of decidable and decidable_rel, but it seems like there should be some lemmas to help me out

[Bhavik Mehta]

And now I'm getting deterministic timeouts on a small file...

[Kevin Buzzard]

That can be because you've made a slip and unification can be going crazy with the wrong idea about something instead of failing quickly

[Kevin Buzzard]

Accidentally coercing an int to a nat used to cause timeouts

[Bhavik Mehta]

Is there a neat way to get the argmin of a function on a finset?

[Bhavik Mehta]

That can be because you've made a slip and unification can be going crazy with the wrong idea about something instead of failing quickly

Any suggestions on where the slip is here?

import data.finset
import data.fintype

open fintype
open finset

variable {n : ℕ}
local notation `X` := fin n

def gamma : rel (finset X) (finset X) := (λ U V, ∃ (HU : U ≠ ∅), ∃ (HV : V ≠ ∅), disjoint U V ∧ finset.card U = finset.card V ∧ max' U HU < max' V HV)

instance thing (U V : finset X) : decidable (gamma U V) :=
begin
  rw gamma,
  dsimp,
  exact @exists_prop_decidable _ _ _ _,
end

[Bhavik Mehta]

(got it!)

[Bhavik Mehta]

Got this lemma done! Thanks so much Reid

[Reid Barton]

what was the issue with the code above, out of curiosity?

[Bhavik Mehta]

There wasn't an instance of decidable (disjoint U V), and so typeclass resolution failed for one of the hypotheses of exists_prop_decidable

[Bhavik Mehta]

Adding that instance in (I'll PR it to mathlib soon) made it work