Zulip Chat Archive

Stream: new members

Topic: Lemmas about subtype.rec


view this post on Zulip Bhavik Mehta (Nov 14 2019 at 19:03):

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?

view this post on Zulip Johan Commelin (Nov 14 2019 at 19:04):

apply subtype.val_injective?

view this post on Zulip Johan Commelin (Nov 14 2019 at 19:05):

Sorry, that goes the wrong way round.

view this post on Zulip Bhavik Mehta (Nov 14 2019 at 19:05):

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

view this post on Zulip Johan Commelin (Nov 14 2019 at 19:06):

exact congr_arg subtype.val h_your_subtype.rec_assumption

view this post on Zulip Johan Commelin (Nov 14 2019 at 19:07):

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

Hmm, are you nesting subtypes?

view this post on Zulip Bhavik Mehta (Nov 14 2019 at 19:09):

I _think_ so, but subtypes are confusing me

view this post on Zulip Johan Commelin (Nov 14 2019 at 19:10):

What are you trying to do?

view this post on Zulip Johan Commelin (Nov 14 2019 at 19:10):

As in: bigger picture

view this post on Zulip Bhavik Mehta (Nov 14 2019 at 19:10):

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

view this post on Zulip Johan Commelin (Nov 14 2019 at 19:11):

That's generally a good idea :wink:

view this post on Zulip Bhavik Mehta (Nov 14 2019 at 19:15):

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}}

view this post on Zulip Johan Commelin (Nov 14 2019 at 19:19):

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

view this post on Zulip Bhavik Mehta (Nov 14 2019 at 19:20):

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

view this post on Zulip Bhavik Mehta (Nov 14 2019 at 19:20):

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

view this post on Zulip Reid Barton (Nov 14 2019 at 19:22):

Kevin this is what happens when you only teach tactic mode

view this post on Zulip Bhavik Mehta (Nov 14 2019 at 19:22):

Hey I did get started with term mode

view this post on Zulip Bhavik Mehta (Nov 14 2019 at 19:22):

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

view this post on Zulip Bhavik Mehta (Nov 14 2019 at 19:24):

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

view this post on Zulip Johan Commelin (Nov 14 2019 at 19:25):

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.

view this post on Zulip Bhavik Mehta (Nov 14 2019 at 19:25):

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

view this post on Zulip Bhavik Mehta (Nov 14 2019 at 19:25):

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

view this post on Zulip Bhavik Mehta (Nov 14 2019 at 19:26):

And this sort of thing is useful in enumerative combinatorics

view this post on Zulip Bhavik Mehta (Nov 14 2019 at 19:26):

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

view this post on Zulip Johan Commelin (Nov 14 2019 at 19:27):

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

view this post on Zulip Bhavik Mehta (Nov 14 2019 at 19:31):

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

view this post on Zulip Bhavik Mehta (Nov 14 2019 at 19:33):

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)

view this post on Zulip Reid Barton (Nov 14 2019 at 19:34):

You used cases too much

view this post on Zulip Reid Barton (Nov 14 2019 at 19:34):

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

view this post on Zulip Reid Barton (Nov 14 2019 at 19:35):

Just use intro i, and fields of i

view this post on Zulip Reid Barton (Nov 14 2019 at 19:35):

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

view this post on Zulip Reid Barton (Nov 14 2019 at 19:36):

It's also then obviously not that trivial

view this post on Zulip Reid Barton (Nov 14 2019 at 19:36):

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

view this post on Zulip Bhavik Mehta (Nov 14 2019 at 19:36):

Yeah this part shouldn't be super trivial

view this post on Zulip Bhavik Mehta (Nov 14 2019 at 19:36):

Yeah exactly

view this post on Zulip Reid Barton (Nov 14 2019 at 19:37):

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

view this post on Zulip Bhavik Mehta (Nov 14 2019 at 19:37):

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

view this post on Zulip Bhavik Mehta (Nov 14 2019 at 19:37):

And also how to use cases to prove the property?

view this post on Zulip Reid Barton (Nov 14 2019 at 19:39):

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

view this post on Zulip Reid Barton (Nov 14 2019 at 19:40):

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

view this post on Zulip Reid Barton (Nov 14 2019 at 19:40):

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

view this post on Zulip Reid Barton (Nov 14 2019 at 19:41):

subtype.rec is case analysis on a subtype value

view this post on Zulip Reid Barton (Nov 14 2019 at 19:44):

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

view this post on Zulip Bhavik Mehta (Nov 14 2019 at 19:50):

I think I see, thanks so much!


Last updated: May 18 2021 at 16:25 UTC