# Zulip Chat Archive

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