Zulip Chat Archive

Stream: new members

Topic: n-sets


view this post on Zulip 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?

view this post on Zulip 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)?"

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Sep 21 2018 at 12:21):

See my first message

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Sep 21 2018 at 12:42):

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

view this post on Zulip Kevin Buzzard (Sep 21 2018 at 12:44):

Or even better a definition if you want recursion.

view this post on Zulip Kevin Buzzard (Sep 21 2018 at 12:44):

Hang on I'll try and knock one up.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Chris Hughes (Sep 21 2018 at 14:49):

You probably want something like finest.strong_induction

view this post on Zulip 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