Pattern match on `finset`

Stream: new members

[Tage Johansson]

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]

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]

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

[Kyle Miller]

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]

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]

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]

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]

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]

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]

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

[Tage Johansson]

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]

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]

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]

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

[Kyle Miller]

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

[Kyle Miller]

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).