Lemmas about subtype.rec

Stream: new members

[Bhavik Mehta]

I have as assumption something of the form subtype.rec x1 t = subtype.rec x2 t, and my goal is x1 = x2, I'm struggling to see what to do next (the injection tactic didn't work), any suggestions?

[Johan Commelin]

apply subtype.val_injective?

[Johan Commelin]

Sorry, that goes the wrong way round.

[Bhavik Mehta]

That changes the goal to x1.val = x2.val

[Johan Commelin]

exact congr_arg subtype.val h_your_subtype.rec_assumption

[Johan Commelin]

That changes the goal to x1.val = x2.val

Hmm, are you nesting subtypes?

[Bhavik Mehta]

I _think_ so, but subtypes are confusing me

[Johan Commelin]

What are you trying to do?

[Johan Commelin]

As in: bigger picture

[Bhavik Mehta]

I think the easiest way to explain would be for me to paste my code here

[Johan Commelin]

That's generally a good idea :wink:

[Bhavik Mehta]

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

-- the type of those subsets of X which have cardinality r
@[reducible] def rset (r : ℕ) (X) [fintype X] := {x : finset X // x ∈ finset.powerset_len r (elems X)}

instance rset_fintype (r : ℕ) : fintype (rset r X) := finset.subtype.fintype _

def rset_mk {r : ℕ} (A : finset X) (H : card A = r) : rset r X :=
begin
  refine ⟨A, _⟩,
  rw mem_powerset_len,
  refine ⟨λ x _, complete x, H⟩,
end

def example1 : rset 4 (fin 9) := rset_mk {0,1,4,5} (by trivial)
def example2 : finset (rset 3 (fin 5)) :=
{rset_mk {0,1,2} (by trivial),
 rset_mk {0,1,3} (by trivial),
 rset_mk {0,2,3} (by trivial),
 rset_mk {0,2,4} (by trivial)
 }

#eval example1
#eval example2

@[reducible] instance {r : ℕ} : has_mem X (rset r X) := ⟨λ i A, i ∈ A.1⟩

#eval elems (rset 3 (fin 5))

def stretch {r : ℕ} (x : rset r X) (s : X) (s ∉ x) : rset (r+1) X :=
begin
  refine ⟨insert s (x.1), _⟩,
  rw mem_powerset_len,
  cases x with a b,
  rw mem_powerset_len at b,
  cases b,
  refine ⟨insert_subset.2 ⟨complete _, _⟩, _⟩,
    simpa,
  rw card_insert_of_not_mem H,
  congr,
  rw b_right,
end

def remove {r : ℕ} (x : rset r X) (s : X) (h : s ∈ x) : rset (r-1) X :=
begin
  refine ⟨erase (x.1) s, _⟩,
  rw mem_powerset_len,
  cases x with a b,
  split,
    intros t p,
    apply complete,
  rw card_erase_of_mem h,
  congr,
  rw mem_powerset_len at b,
  rw b.2,
  trivial,
end

theorem rset_card (r : ℕ) : card (rset r X) = nat.choose (card X) r :=
begin
  rw card_of_subtype (powerset_len r (elems X)) (λ _, iff.rfl),
  apply card_powerset_len
end

-- in maths notation, shadow 𝒜 = {A−{i} | A ∈ 𝒜, i ∈ A}
def shadow {r : ℕ} (𝒜 : finset (rset r X)) : finset (rset (r-1) X) :=
begin
  refine 𝒜.bind _,
  intro A,
  cases A,
  refine A_val.attach.map ⟨_, _⟩,
  -- I can use .image here, but since the function is injective I might as well prove it,
  -- it also might make writing mem_shadow easier
    rintro ⟨i, hi⟩,
    apply remove ⟨A_val, A_property⟩ i,
    exact hi,
  intros x1 x2 q,
  simp at q,
  apply subtype.val_injective,
  refine (congr_arg subtype.val _),
  sorry
end

#eval shadow example2 -- should be {{0,1}, {0,2}, {0,3}, {0,4}, {1,2}, {1,3}, {2,3}, {2,4}}

[Johan Commelin]

Ok... that's a whole bunch of code... could you give a bit of context please? What's your goal beyond this? Is this set theory? I know nothing about set theory

[Bhavik Mehta]

Yeah, sorry about that. It's combinatorics. I think the examples might help a little, but rset is the type of subsets with a given cardinality

[Bhavik Mehta]

Then shadow ought to be a function acting on a family of rsets

[Reid Barton]

Kevin this is what happens when you only teach tactic mode

[Bhavik Mehta]

Hey I did get started with term mode

[Bhavik Mehta]

But defining shadow seemed like such a pain in term mode that I switched to tactics

[Bhavik Mehta]

Hopefully the code is vaguely understandable, if not I'm happy to tidy it or explain what I'm trying to do

[Johan Commelin]

To be honest, I don't really follow what's going on. But that's mainly because I have no clue at all what kind of maths you are aiming for.

[Bhavik Mehta]

Right now, I'm trying to define what the shadow is

[Bhavik Mehta]

It should be a straightforward function on families of r-sets

[Bhavik Mehta]

And this sort of thing is useful in enumerative combinatorics

[Bhavik Mehta]

(But this is why I didn't start off by posting code)

[Johan Commelin]

I need more maths explanation. I have never heard of the shadow before.

[Bhavik Mehta]

https://leanprover.zulipchat.com/user_uploads/3121/wqVK3QJdaiHnYeYY76EY1AJ9/pasted_image.png

[Bhavik Mehta]

X^(r) corresponds to the type rset r X, and it's the collection of subsets of X with size r (we're taking X to be finite)

[Reid Barton]

You used cases too much

[Reid Barton]

It's better not to use rintro ⟨i, hi⟩, when constructing data

[Reid Barton]

Just use intro i, and fields of i

[Reid Barton]

Then you get a goal which doesn't involve this strange subtype.rec

[Reid Barton]

It's also then obviously not that trivial

[Reid Barton]

You need to prove if A - {x1} = A - {x2} then x1 = x2

[Bhavik Mehta]

Yeah this part shouldn't be super trivial

[Bhavik Mehta]

Yeah exactly

[Reid Barton]

The alternative is also to use cases in the proof of that property

[Bhavik Mehta]

Could you explain what subtype.rec is, and why using cases made it show up?

[Bhavik Mehta]

And also how to use cases to prove the property?

[Reid Barton]

The function you're passing to finset.map first does cases on its argument

[Reid Barton]

So you had better apply cases to the arguments also when you want to prove something about it, otherwise the function won't be able to reduce

[Reid Barton]

for example add cases x1, cases x2 after intros x1 x2 q (or use rintros there also)

[Reid Barton]

subtype.rec is case analysis on a subtype value

[Reid Barton]

If you apply subtype.rec to a variable, it's stuck. If you do case analysis on the variable then it becomes a constructor application, and then subtype.rec (subtype.mk _ _) _ can reduce

[Bhavik Mehta]

I think I see, thanks so much!