## Stream: new members

### Topic: Pattern match on finset

#### Tage Johansson (Nov 02 2022 at 18:50):

Hello,

I know the topic is a bit vague, but I simply want to decide a proposition about a finite set. I'd like to pattern match on the set just as I'm used to pattern match on lists. I saw there is finset.induction_on, but I don't get it to work. Perhaps it expects a predicate and decidable is not a prop but a type. Anyway, here's (approximately) what I want to achieve:

def all_positive (p : finset ℕ)
: decidable (∀ x ∈ p, 0 < x) :=
by sorry


What would be the cleanest way to implement this?

Thanks,
Tage

#### Kyle Miller (Nov 02 2022 at 18:53):

There are already instances in mathlib for that, so you can do

def all_positive (p : finset ℕ)
: decidable (∀ x ∈ p, 0 < x) :=
infer_instance


#### Kyle Miller (Nov 02 2022 at 18:54):

But, just to check, are you sure you're wanting decidable here?

#### Kyle Miller (Nov 02 2022 at 18:56):

If you want to track down how mathlib does it, if you do

def all_positive (p : finset ℕ)
: decidable (∀ x ∈ p, 0 < x) :=
by apply_instance
#print all_positive


then you can see it uses docs#finset.decidable_dforall_finset

#### Tage Johansson (Nov 02 2022 at 18:57):

Thanks, but I just gave a simplified example. It wasn't ment to be solved by "cheating". Here what I actually want to achieve:

def weightlifting_subset (p : finset ℕ)
(w : ℕ)
: decidable (∃ (s : finset ℕ), s ⊆ p ∧ w = ∑ x in s, x) :=
by sorry




#### Tage Johansson (Nov 02 2022 at 18:59):

I want to split the proof/implementation into a case where p is empty and one case where p is a set with an inserted element.

#### Kyle Miller (Nov 02 2022 at 18:59):

Poking around a bit, it looks like the key is that since a finset is a kind of multiset, then you can use quotient.rec_on_subsingleton on that, which gives a list that you can compute with however you like. But you should look through how that's done.

#### Kyle Miller (Nov 02 2022 at 19:00):

To #xy this a bit, where is this decidable being used? I'm asking because you have a def rather than a class, which makes me wonder what you're up to.

#### Kyle Miller (Nov 02 2022 at 19:03):

Anyway, I'd still do this by "cheating" by using pre-existing instances wherever possible. (I switched to s.sum id, which is equivalent, just because I was in the middle of a random other Lean file)

def weightlifting_subset (p : finset ℕ)
(w : ℕ)
: decidable (∃ (s : finset ℕ), s ⊆ p ∧ w = s.sum id) :=
begin
apply decidable_of_iff (∃ (s : p.powerset), w = s.1.sum id),
simp,
end


#### Kyle Miller (Nov 02 2022 at 19:05):

The trick is that I knew there was a decidable instance for existentials over finite types.

#### Tage Johansson (Nov 02 2022 at 19:13):

Your solution seems to work, although I probably need some time to understand why. It feels all too magick!

But anyway. The problem is that I should create an algorithm that given a set of weights p and a total weight w, checks whether there exists a subset of p which sum is equal to w. Then I wanted to prove this algorithm being correct, and I thought I could do the computation and proof together by using decidable. But perhaps this isn't entirely correct?

#### Kyle Miller (Nov 02 2022 at 19:19):

The high-level reason this works is that there are already algorithms for this problem somewhere deep in mathlib, and we just needed to rewrite the Prop to help it see this. Whether that algorithm is any good is a different story! (I imagine it's one someone thought at least a little about runtime characteristics.)

#### Kyle Miller (Nov 02 2022 at 19:21):

I suppose it makes sense to use decidable this way. It can be easier to define an algorithm then prove it's correct, though if you can interleave the algorithm and proof that's fine too.

decidable is generally used as a typeclass, since it's used to synthesize decision procedures for propositions automatically. That way you can use a Prop as if it were a Bool inside programs.

#### Tage Johansson (Nov 02 2022 at 19:33):

Is there any way to get to know the instance used by decidable_of_iff?

#### Kyle Miller (Nov 02 2022 at 19:35):

It's not the best, but I might try doing #print weightlifting_subset and looking for something relevant

#### Kyle Miller (Nov 02 2022 at 19:37):

Another way is

set_option pp.implicit true
def weightlifting_subset (p : finset ℕ)
(w : ℕ)
: decidable (∃ (s : finset ℕ), s ⊆ p ∧ w = s.sum id) :=
begin
show_term { apply decidable_of_iff (∃ (s : p.powerset), w = s.1.sum id), },
simp,
end


and in the output I see fintype.decidable_exists_fintype ↥(p.powerset).

Last updated: Dec 20 2023 at 11:08 UTC