## Stream: maths

### Topic: Tricky recursive proof

#### Bhavik Mehta (Dec 15 2019 at 04:15):

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 (Dec 15 2019 at 04:19):

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

#### Bhavik Mehta (Dec 15 2019 at 04:19):

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 (Dec 15 2019 at 04:22):

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

#### Reid Barton (Dec 15 2019 at 04:23):

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 (Dec 15 2019 at 04:24):

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 (Dec 15 2019 at 04:24):

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 (Dec 15 2019 at 04:25):

Don't actually construct the sequence

#### Bhavik Mehta (Dec 15 2019 at 04:26):

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 (Dec 15 2019 at 04:27):

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 (Dec 15 2019 at 04:28):

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 (Dec 15 2019 at 04:30):

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 (Dec 15 2019 at 04:31):

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 (Dec 15 2019 at 04:31):

This makes sense, thanks!

#### Bhavik Mehta (Dec 15 2019 at 04:32):

I'll give it a go now

#### Reid Barton (Dec 15 2019 at 04:32):

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 (Dec 15 2019 at 04:34):

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

#### Reid Barton (Dec 15 2019 at 04:35):

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 (Dec 15 2019 at 04:36):

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 (Dec 15 2019 at 04:36):

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

#### Bhavik Mehta (Dec 15 2019 at 04:51):

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 (Dec 15 2019 at 05:00):

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

#### Kevin Buzzard (Dec 15 2019 at 10:25):

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 (Dec 15 2019 at 10:26):

Accidentally coercing an int to a nat used to cause timeouts

#### Bhavik Mehta (Dec 15 2019 at 14:46):

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

#### Bhavik Mehta (Dec 15 2019 at 15:18):

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


(got it!)

#### Bhavik Mehta (Dec 15 2019 at 16:08):

Got this lemma done! Thanks so much Reid

#### Reid Barton (Dec 15 2019 at 16:08):

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

#### Bhavik Mehta (Dec 15 2019 at 16:27):

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 (Dec 15 2019 at 16:27):

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

Last updated: May 06 2021 at 18:20 UTC