Defining a function by or.elim

Stream: new members

[Bhavik Mehta]

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]

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]

Ooh dite looks about right...

[Kevin Buzzard]

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

[Patrick Massot]

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

[Bhavik Mehta]

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]

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]

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]

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

[Edward Ayers]

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

[Marc Huisinga]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

What is the definition of rset?

[Bhavik Mehta]

Other attempt which also doesn't work:

def decompose {n : ℕ} : Π (A : finset (finset X)) (r : ℕ), r ≤ n → finset (rset r X) :=
λ A r hr, dite (r=n) (λ _, f1 r A) $
  assume k : ¬(r = n),
  have k2 : r < n, from lt_of_le_of_ne ‹r ≤ n› k,
  (f1 r 𝒜) ∪ f2 (decompose _ _ _)

[Bhavik Mehta]

I don't believe it should matter for this, but

@[reducible] def rset (r : ℕ) (X) [fintype X] := {x : finset X // x ∈ finset.powerset_len r (elems X)}

I've got ~300 lines of other stuff using this definition which work nicely together

[Kevin Buzzard]

oh sorry! I missed the earlier part of the discussion

[Simon Hudon]

What if you broke down this definition into two parts:

constant f1 (A : finset (finset X)) : finset (finset X)
constant f2 (B : finset (finset X)) : finset (finset X)

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

lemma decompose_powerset_len {n : ℕ} (A : finset (finset X)) (k : ℕ) (hk : k ≤ n) (x : finset X) :
   x ∈ decompose A k hk → x ∈ powerset_len (n - k) (elems X) := /- put proof here -/

def decompose {n : ℕ} (A : finset (finset X)) (k : ℕ) (hk : k ≤ n) : finset (rset (n-k) X)
(decompose' A k hk).attach.image $ λ ⟨x,hx⟩, ⟨x,decompose_powerset_len A k hk x hx⟩

[Simon Hudon]

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]

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

[Bhavik Mehta]

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]

Yes or at least provide a version without the rset.

[Bhavik Mehta]

Oh!

[Bhavik Mehta]

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

[Simon Hudon]

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

[Simon Hudon]

That's right

[Bhavik Mehta]

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

[Bhavik Mehta]

(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]

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]

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]

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

[Kevin Buzzard]

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]

noncomputable! But this thing should be computable

[Kevin Buzzard]

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

[Rob Lewis]

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

[Kevin Buzzard]

I hope so because I just submitted a PR

[Bhavik Mehta]

Oh the union should work without an instance I think

[Bhavik Mehta]

Sorry I think that's my fault

[Bhavik Mehta]

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]

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]

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

[Reid Barton]

@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]

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]

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]

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]

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

[Reid Barton]

Oh yes, the definition is different

[Kevin Buzzard]

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]

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]

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]

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]

@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