n-sets

Stream: new members

[Alistair Tucker]

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]

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]

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]

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]

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]

See my first message

[Alistair Tucker]

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]

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

[Kevin Buzzard]

Or even better a definition if you want recursion.

[Kevin Buzzard]

Hang on I'll try and knock one up.

[Alistair Tucker]

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]

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]

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

[Chris Hughes]

You probably want something like finest.strong_induction

[Alistair Tucker]

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.