## Stream: new members

### Topic: Defining a function by or.elim

#### Bhavik Mehta (Nov 22 2019 at 04:19):

I'm trying to define a function which has the hypothesis r ≤ n, and it's defined differently if r = n compared to r < n, but or.elim doesn't work since the result isn't a Prop, any help appreciated. (Simplified example - the definition of rset shouldn't matter at all, but it has type rset : ℕ → Π (X : Type u_2) [_inst_3 : fintype X], Type u_2):

constant f1 (r : ℕ) (A : finset (finset X)) : finset (rset r X)
constant f2 {r : ℕ} (B : finset (rset (r+1) X)) : finset (rset r X)

def decompose {n : ℕ} (𝒜 : finset (finset X)) (r : ℕ) (hr2 : r ≤ n) : finset (rset r X) :=
or.elim (lt_or_eq_of_le hr2) _ _

-- I want decompose A n _ = f1 n A
--    and decompose A r _ = (f1 r A) ∪ f2 (decompose A (r+1) _)


#### Bhavik Mehta (Nov 22 2019 at 04:20):

If then else doesn't work for me, since in the then part I lose the proof that r = n, which I need to make it typecheck

#### Bhavik Mehta (Nov 22 2019 at 04:21):

Ooh dite looks about right...

#### Kevin Buzzard (Nov 22 2019 at 07:01):

Indeed dite is or elimination into type. I remember the day this dawned on me :-)

#### Patrick Massot (Nov 22 2019 at 08:58):

Let's also repeat that you can write if ... then ... else... also keeping the assumption, using if h : ... then ... else ....

#### Bhavik Mehta (Nov 22 2019 at 11:43):

I'm struggling with this definition still - there seems to be a couple of factors making this awkward... It's kind of defined inductively downward, starting from r=n and going down to r=0. So I'm trying first to define a flipped version, with k = n-r:

def decompose' {n : ℕ} (A : finset (finset X)) : Π (k : ℕ), k ≤ n → finset (rset (n-k) X)
| 0 _ := f1 n A
| (k+1) hk := f1 _ A ∪ (f2 (decompose' k _))


but I'm getting the error

type mismatch at application
f2 (decompose' k ?m_1)
term
decompose' k ?m_1
has type
finset (rset (n - k) X)
but is expected to have type
finset (rset (n - (k + 1) + 1) X)


Now I'd usually just use rw to sort this out - but I'd have to go into tactic mode for that first and it might be awkward to prove things about this definition then. I can't get ▸ to work either, it gives some confusing messages about motives.

Alternatively I'd be interested if this definition could be given downwards instead - the things I tried didn't work...

#### Edward Ayers (Nov 22 2019 at 12:47):

I feel like doing a cast in the above definition is unavoidable since (n-k) != (n - (k+1) + 1)  when n=k, which is fine because hk : k+1 <= n but still requires reasoning.

#### Simon Hudon (Nov 22 2019 at 12:49):

That's true and that suggests to me that your types are overly dependent. You might want to separate them into types that you don't have to rewrite so much and a proposition on those types that adds the nuances that you now encode with dependent types.

#### Edward Ayers (Nov 22 2019 at 12:50):

It's pretty disheartening that dependent types seem to cause more problems than they solve in situations like this.

#### Edward Ayers (Nov 22 2019 at 12:53):

You might be able to write it out as upward induction by using wf induction with the size being n - r.

#### Marc Huisinga (Nov 22 2019 at 12:55):

is this really an issue with dependent types, though?
i feel like carrying around an invariant everywhere you go like rset seems to do is rarely the right thing to do anyways because you always need to ensure that it is maintained.

#### Marc Huisinga (Nov 22 2019 at 12:58):

this is usually easy when you already have a full interface that maintains the invariant for you (e.g. as is the case for finset) but even then it can be cumbersome if you need to work harder in order to use the interface (e.g. mapping over a finset requires injectivity)

#### Simon Hudon (Nov 22 2019 at 13:01):

this is usually easy when you already have a full interface that maintains the invariant for you (e.g. as is the case for finset)

Even in this case, a lot of the reasoning is encapsulated in the multiset module. This api is carefully layered, separating invariants and maintaining them when it is convenient and relevant.

but even then it can be cumbersome if you need to work harder in order to use the interface (e.g. mapping over a finset requires injectivity)

welll ... finset has image which does not require infectivity. Some apis aren't great to work with but I think this one does a great job.

#### Kevin Buzzard (Nov 22 2019 at 13:06):

I would attempt to show you how to fix the issue in this case but there are so many undefined variables that I can't cut and paste easily :-/

#### Marc Huisinga (Nov 22 2019 at 13:06):

welll ... finset has image which does not require infectivity. Some apis aren't great to work with but I think this one does a great job.

i agree!

#### Marc Huisinga (Nov 22 2019 at 13:08):

i did not know about image. finset is definitely not a good example to choose (edit: for me quibbling about it being hard to maintain invariants).

#### Bhavik Mehta (Nov 22 2019 at 13:13):

You might be able to write it out as upward induction by using wf induction with the size being n - r.

Yeah, this was the idea of the flipped version with k = n-r

#### Bhavik Mehta (Nov 22 2019 at 13:14):

I would attempt to show you how to fix the issue in this case but there are so many undefined variables that I can't cut and paste easily :-/

I hoped giving f1 and f2 as constants would help copy-pasting, but I'll abstract a bit more

#### Simon Hudon (Nov 22 2019 at 13:14):

i did not know about image. finset is definetly not a good example to choose.

I actually really like the examples of finset and finmap for API designed because of how carefully layered they are. They also show two different directions. finset is an invariant layered on top of a quotient. In a way, finmap is also an invariant on top of a quotient also because it's defined in terms of multimap but most useful lemmas relate finmap to alist and makes the design upside down: a quotient on top of an invariant.

#### Bhavik Mehta (Nov 22 2019 at 13:17):

import data.finset
import data.fintype

variables {X : Type*}
variables [fintype X] [decidable_eq X]
variables {r : ℕ}

constant rset (r : ℕ) (X) [fintype X] : Type
constant f1 (r : ℕ) (A : finset (finset X)) : finset (rset r X)
constant f2 {r : ℕ} (B : finset (rset (r+1) X)) : finset (rset r X)

def decompose' {n : ℕ} (A : finset (finset X)) : Π (k : ℕ), k ≤ n → finset (rset (n-k) X)
| 0 _ := f1 n A
| (k+1) hk := f1 _ A ∪ (f2 (decompose' k _))

-- I want decompose A n _ = f1 n A
--    and decompose A r _ = (f1 r A) ∪ f2 (decompose A (r+1) _)
-- so I'm using decompose A r = decompose' A (n-r)


This should be copy-paste-able

#### Simon Hudon (Nov 22 2019 at 13:20):

What is the definition of rset?

#### Bhavik Mehta (Nov 22 2019 at 13:21):

Other attempt which also doesn't work:

def decompose {n : ℕ} : Π (A : finset (finset X)) (r : ℕ), r ≤ n → finset (rset r X) :=


#### Simon Hudon (Nov 22 2019 at 13:45):

The alternative, as @Edward Ayers noted is to use cast but this is only pushing the problem further down the line. When you use your definition for rewriting, you're going to find that you have cast popping up in inconvenient locations.

#### Bhavik Mehta (Nov 22 2019 at 13:45):

So you're suggesting to change the types of f1 and f2 as well?

#### Bhavik Mehta (Nov 22 2019 at 13:46):

If possible I'd really prefer not to change the type of f2, it's kind of fundamental to the problem at hand

#### Simon Hudon (Nov 22 2019 at 13:46):

Yes or at least provide a version without the rset.

Oh!

#### Bhavik Mehta (Nov 22 2019 at 13:46):

I see, and provide a lemma saying that if the source has the restricted type then the target does too

#### Simon Hudon (Nov 22 2019 at 13:47):

f2 looks a bit more challenging to change than f1 but I can't say for sure. I don't have the definition

That's right

#### Bhavik Mehta (Nov 22 2019 at 13:49):

Changing this is gonna mean changing a lot of stuff :(

#### Bhavik Mehta (Nov 22 2019 at 13:49):

(the details are here: https://github.com/b-mehta/lean-experiments/blob/master/src/kruskal_katona.lean#L155. f2 is the same as shadow)

#### Bhavik Mehta (Nov 22 2019 at 13:51):

But I think I see the general design principle here: definitions and functions shouldn't have restricted types, and we instead move the restrictions to the lemmas about our definitions and functions. Is this about right?

#### Simon Hudon (Nov 22 2019 at 13:54):

That's a bit oversimplified. One time the restrictions are helpful is when the constraints don't change much throughout your formula. A take away lesson I'd rather give is: understand the ups and down of intrinsic invariant (dependent types and subtypes) versus extrinsic constraints and consider using one when the other is leading to painful proofs

#### Bhavik Mehta (Nov 22 2019 at 13:58):

I think the restrictions are helpful in my case, then - the proofs using f2 weren't particularly painful

#### Kevin Buzzard (Nov 22 2019 at 13:59):

I would attempt to show you how to fix the issue in this case but there are so many undefined variables that I can't cut and paste easily :-/

I can't do it :-/. Here are my efforts:

import data.finset
import data.fintype
import tactic.omega tactic.linarith

variables {X : Type*}
variables [fintype X] [decidable_eq X]
variables {r : ℕ}

constant rset (r : ℕ) (X) [fintype X] : Type
constant f1 (r : ℕ) (A : finset (finset X)) : finset (rset r X)
constant f2 {r : ℕ} (B : finset (rset (r+1) X)) : finset (rset r X)

instance foo (Y : Type) : has_union (finset Y) := sorry

def stupid (n k : ℕ) (h : n - k = n - (k + 1) + 1) :
finset (rset (n - k) X) → finset (rset (n - (k + 1) + 1) X) :=
λ t, by rwa h at t

noncomputable def decompose' {n : ℕ} (A : finset (finset X)) : Π (k : ℕ), k ≤ n → finset (rset (n-k) X)
| 0 _ := f1 n A
| (k+1) hk := f1 _ A ∪ (
have h : n - k = n - (k + 1) + 1 := begin clear decompose' _inst_1 _inst_2 A, omega, end, -- ??
--    (f2 (stupid _ _ h (decompose' k (le_trans (nat.le_succ k) hk) : finset (rset (n - k) X)) : finset (rset (n - (k + 1) + 1) X))))
let temp := (decompose' k (le_trans (nat.le_succ k) hk) : finset (rset (n - k) X)) in
@f2 X _inst_1 _inst_2 (n - (k + 1)) ((h ▸ temp : finset (rset (n - (k + 1) + 1) X))))


The commented out line works fine but involves a stupid function. Without it I'm surprised I can't get the stupid triangle to work and I'm also surprised that omega wouldn't work without a lot of coaxing. I still have a lot to learn :-/

#### Bhavik Mehta (Nov 22 2019 at 14:00):

noncomputable! But this thing should be computable

#### Kevin Buzzard (Nov 22 2019 at 14:01):

Is that because of the instance I added? I couldn't get union to work

#### Rob Lewis (Nov 22 2019 at 14:01):

@Kevin Buzzard Are you using a recent mathlib? Seul fixed some of the issues with coaxing omega last month.

#### Kevin Buzzard (Nov 22 2019 at 14:02):

I hope so because I just submitted a PR

#### Bhavik Mehta (Nov 22 2019 at 14:02):

Oh the union should work without an instance I think

#### Bhavik Mehta (Nov 22 2019 at 14:03):

Sorry I think that's my fault

#### Bhavik Mehta (Nov 22 2019 at 14:07):

Okay yeah that was my fault, since I abstracted away what rset was, it couldn't automatically derive decidable_eq for it, and so finset (rset _ _) didn't have has_union

#### Bhavik Mehta (Nov 22 2019 at 14:07):

Changing the constant rset line to:
def rset (r : ℕ) (X) [fintype X] := {x : finset X // x ∈ finset.powerset_len r (fintype.elems X)} should make has_union work

#### Reid Barton (Nov 22 2019 at 15:07):

@Kevin Buzzard The stupid triangle only works to rewrite inside a Prop

#### Reid Barton (Nov 22 2019 at 15:14):

@Bhavik Mehta I think the easiest approach is to define something along the lines of

def rset.cast {X : Type} {r r' : ℕ} (h : r = r') (A : rset r X) : rset r' X :=
⟨A.val, h ▸ A.property⟩


and use it where you need to "fix" the size of an rset

#### Reid Barton (Nov 22 2019 at 15:15):

If you use rw, or equivalently cast/eq.rec, you'll be in for a world of pain later when you want to get out the actual finset.

#### Reid Barton (Nov 22 2019 at 15:15):

By the way, writing x ∈ finset.powerset_len r (fintype.elems X) as the property rather than x.card = r looks rather awkward to me.

#### Reid Barton (Nov 22 2019 at 15:18):

Bhavik Mehta I think the easiest approach is to define something along the lines of

def rset.cast {X : Type} {r r' : ℕ} (h : r = r') (A : rset r X) : rset r' X :=
⟨A.val, h ▸ A.property⟩


and use it where you need to "fix" the size of an rset

Oh, this is what Kevin called a "stupid function"--but sometimes the stupid approach is the best?

#### Kevin Buzzard (Nov 22 2019 at 15:21):

I think Reid's definition looks better than mine because he's only using eq.rec in Prop land

#### Reid Barton (Nov 22 2019 at 15:29):

Oh yes, the definition is different

#### Kevin Buzzard (Nov 22 2019 at 15:31):

This is not the first time I've seen this issue and I should perhaps have been wise enough by now to come up with Reid's definition. @Bhavik Mehta I once wrote such a function when working with quotient groups -- I needed a map from $G/H$ to $G/K$ when I had a proof that $H=K$ and I did it in the same way that Reid suggested above.

#### Bhavik Mehta (Nov 23 2019 at 13:50):

Bhavik Mehta I think the easiest approach is to define something along the lines of

def rset.cast {X : Type} {r r' : ℕ} (h : r = r') (A : rset r X) : rset r' X :=
⟨A.val, h ▸ A.property⟩


and use it where you need to "fix" the size of an rset

I like this, thanks!

#### Bhavik Mehta (Nov 23 2019 at 13:51):

By the way, writing x ∈ finset.powerset_len r (fintype.elems X) as the property rather than x.card = r looks rather awkward to me.

Ah this is a good point...

#### Bhavik Mehta (Nov 23 2019 at 13:52):

I'd made rset_mk (A : finset X) (H : finset.card A = r) : rset r X  instead to get around this, but your way is a lot cleaner

#### Bhavik Mehta (Dec 04 2019 at 16:20):

@Simon Hudon @Reid Barton I finally got around to rewriting everything with your suggestions, and managed to finish the main proof this was for! This was very instructive, thanks both

Last updated: Dec 20 2023 at 11:08 UTC