## Stream: new members

### Topic: n-sets

#### Alistair Tucker (Sep 21 2018 at 12:04):

Hi! I am trying to work with sets of a certain cardinality so I can prove some things by induction. I have defined

structure nset (n : nat) :=
(s : finset N)
(hn : card s ≤ n)


but it's a bit of a pain. Is there something like this already?

#### Kevin Buzzard (Sep 21 2018 at 12:09):

Instead of making new structures, I would be tempted to formalise the exact statement of the inductive hypothesis I wanted to use. Do you want a result of the form "(done for all sizes a < b implies done for size b) -> (done for all finsets)" or of the form "(done for empty finset) + (done for size n implies done for size n+1) -> (done for all finsets)?"

#### Kevin Buzzard (Sep 21 2018 at 12:12):

finset is a structure made up of a multiset and a proof of something about it, so it comes with a default inductive hypothesis finset.rec which is useless: "if you've proved it for all pairs consisting of a multiset and a proof of the relevant thing, you've proved it for all finsets!". Duh. But there's nothing stopping you proving other more useful recursors.

#### Alistair Tucker (Sep 21 2018 at 12:13):

Yes :)
I am using nat.rec_on to do the latter, but it incorporates a hypothesis that looks a lot like the former.

#### Kevin Buzzard (Sep 21 2018 at 12:20):

I am asking you if you can formalise the exact statement of what you want. The type. That's like making the level of the game. And then someone here will come along and formalise the proof, and it's like they solved the level. And some solutions will be more elegant than others. But you have to make the level first. You haven't said precisely what you want.

#### Kevin Buzzard (Sep 21 2018 at 12:21):

See my first message

#### Alistair Tucker (Sep 21 2018 at 12:24):

OK thanks. It's a bit complicated though. Perhaps this is the most relevant snippet

structure soln (α β : Type) [partial_order β] (n : nat) :=
(V : Π (s : nset n), set α)
(v : Π (s : nset n), Π (y : α), y ∈ V s → β)
(h : Π (t : nset n) (s : nset n) (hs : s.1 ⊆ t.1),
Π (y : α) (hy : y ∈ V s ∩ V t), v s y (and.left hy) ≤ v t y hy.right)


#### Kevin Buzzard (Sep 21 2018 at 12:42):

Your statement of the kind of induction you want should be a theorem.

#### Kevin Buzzard (Sep 21 2018 at 12:44):

Or even better a definition if you want recursion.

#### Kevin Buzzard (Sep 21 2018 at 12:44):

Hang on I'll try and knock one up.

#### Alistair Tucker (Sep 21 2018 at 12:45):

Hmm I have hoping to define V and v in the induction so it's not a theorem exactly

def solve (n : nat) : soln α β n :=
nat.rec_on n
(let V (s : nset 0) : set α := set.univ in
let v (s : nset 0) : Π (y : α), y ∈ V s → β := sorry in
let h (t : nset 0) (s : nset 0) (hs : s.1 ⊆ t.1) :
Π (y : α) (hy : y ∈ V s ∩ V t), v s y (and.left hy) ≤ v t y hy.right := sorry in
soln.mk V v h)
(λ (n : ℕ) (sol : soln α β n),
let f (t : nset (succ n)) (j : N) (hjt : j ∈ t.1) : set α :=
have h1 : card (erase t.1 j) = pred (card t.1), from card_erase_of_mem hjt,
have h2 : card (erase t.1 j) ≤ n, from eq.symm h1 ▸ pred_le_pred t.2,
let tnj := nset.mk (erase t.1 j) h2 in
λ (y : α), ∃ (hyV : y ∈ sol.V tnj), E (sol.v tnj y hyV) j > 0 in
let V (t : nset (succ n)) : set α := sup t.1 (λ j : N, f t j) in -- s.fold (⊔) ⊥ f
let v (s : nset (succ n)) : Π (y : α), y ∈ V s → β :=
sorry in
let h (t : nset (succ n)) (s : nset (succ n)) (hs : s.1 ⊆ t.1) :
Π (y : α) (hy : y ∈ V s ∩ V t), v s y (and.left hy) ≤ v t y hy.right := sorry in
soln.mk V v h)


#### Kevin Buzzard (Sep 21 2018 at 12:46):

Oh wow it's super-complicated. I don't even understand the question any more. I thought you were just asking how to do induction on the cardinality of a finset and I was trying to establish if you meant usual induction or strong induction.

#### Alistair Tucker (Sep 21 2018 at 12:49):

I have probably made it look more complicated than it is :) I should learn how to use tactics

#### Chris Hughes (Sep 21 2018 at 14:49):

You probably want something like finest.strong_induction

#### Alistair Tucker (Sep 21 2018 at 15:36):

You may be right. I guess I was thinking if I built it up one layer at a time then each element of a layer could use all the results of the previous layer without recalculating them. But I'm not sure it works like that. My first version was in Python where I was able to store those intermediate results explicitly.

Last updated: May 18 2021 at 17:44 UTC