## Stream: new members

#### 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?

#### Johan Commelin (Nov 14 2019 at 19:04):

apply subtype.val_injective?

#### Johan Commelin (Nov 14 2019 at 19:05):

Sorry, that goes the wrong way round.

#### Bhavik Mehta (Nov 14 2019 at 19:05):

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

#### Johan Commelin (Nov 14 2019 at 19:06):

exact congr_arg subtype.val h_your_subtype.rec_assumption

#### Johan Commelin (Nov 14 2019 at 19:07):

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

Hmm, are you nesting subtypes?

#### Bhavik Mehta (Nov 14 2019 at 19:09):

I _think_ so, but subtypes are confusing me

#### Johan Commelin (Nov 14 2019 at 19:10):

What are you trying to do?

#### Johan Commelin (Nov 14 2019 at 19:10):

As in: bigger picture

#### Bhavik Mehta (Nov 14 2019 at 19:10):

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

#### Johan Commelin (Nov 14 2019 at 19:11):

That's generally a good idea :wink:

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


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

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

#### Bhavik Mehta (Nov 14 2019 at 19:20):

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

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

Kevin this is what happens when you only teach tactic mode

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

Hey I did get started with term mode

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

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

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

#### 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.

#### Bhavik Mehta (Nov 14 2019 at 19:25):

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

#### Bhavik Mehta (Nov 14 2019 at 19:25):

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

#### Bhavik Mehta (Nov 14 2019 at 19:26):

And this sort of thing is useful in enumerative combinatorics

#### Bhavik Mehta (Nov 14 2019 at 19:26):

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

#### Johan Commelin (Nov 14 2019 at 19:27):

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

#### 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)

#### Reid Barton (Nov 14 2019 at 19:34):

You used cases too much

#### Reid Barton (Nov 14 2019 at 19:34):

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

#### Reid Barton (Nov 14 2019 at 19:35):

Just use intro i, and fields of i

#### Reid Barton (Nov 14 2019 at 19:35):

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

#### Reid Barton (Nov 14 2019 at 19:36):

It's also then obviously not that trivial

#### Reid Barton (Nov 14 2019 at 19:36):

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

#### Bhavik Mehta (Nov 14 2019 at 19:36):

Yeah this part shouldn't be super trivial

Yeah exactly

#### Reid Barton (Nov 14 2019 at 19:37):

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

#### Bhavik Mehta (Nov 14 2019 at 19:37):

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

#### Bhavik Mehta (Nov 14 2019 at 19:37):

And also how to use cases to prove the property?

#### Reid Barton (Nov 14 2019 at 19:39):

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

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

#### 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)

#### Reid Barton (Nov 14 2019 at 19:41):

subtype.rec is case analysis on a subtype value

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

#### Bhavik Mehta (Nov 14 2019 at 19:50):

I think I see, thanks so much!

Last updated: May 18 2021 at 16:25 UTC