# Zulip Chat Archive

## Stream: new members

### Topic: finsets, decidable_mem, and filter

#### Bryan Gin-ge Chen (Sep 11 2018 at 04:04):

I have a filter on a finset (of finsets) that I want to construct and for some reason I'm stubbornly trying to do it constructively. Here's a stripped down version of what I have (which is part of some stuff on matroids):

import data.finset variables {α : Type*} [decidable_eq α] (G : finset (finset α)) -- copied from init.logic variable p : Prop lemma dec_not [decidable p] : decidable (¬p) := if hp : p then is_false (absurd hp) else is_true hp def is_in (S : finset α) (G : finset (finset α)) : Prop := S ∈ G def is_out (S : finset α) (G : finset (finset α)) : Prop := ¬ S ∈ G lemma is_out_iff_not_in (S : finset α) (G : finset (finset α)) : is_out S G ↔ ¬ is_in S G := by unfold is_in is_out; simp instance decidable_in (S : finset α) (G : finset (finset α)) : decidable (is_in S G) := finset.decidable_mem S G /- failed to generate bytecode for 'decidable_out' code generation failed, VM does not have code for 'dec_not' ... ??? -/ instance decidable_out (S : finset α) (G : finset (finset α)) : decidable (is_out S G) := begin rw is_out_iff_not_in, exact dec_not (is_in S G) end def is_min_out (x : finset α) (G :finset (finset α)) : Prop := is_out x G ∧ (∀ y, y ⊂ x → is_in y G) def min_out (G : finset (finset α)) (F : finset α): finset (finset α) := (finset.powerset F).filter (λ x, is_min_out x G)

First, you can see how in proving `decidable_out`

, I used `dec_not`

, a lemma which is copied from an instance from lean's `init.logic`

. Is there a way of just convincing the elaborator to figure this out for me?

Second, what does the weird warning message by `decidable_out`

mean?

Third and finally, is it even possible to construct an instance of `decidable_pred`

for `is_min_out`

so that I can define `min_out`

constructively? What if I assume a little bit more about α? Do I need to figure out how to use `data.equiv.encodable`

or something?

Thanks again!

#### Mario Carneiro (Sep 11 2018 at 04:19):

First, you can see how in proving decidable_out, I used dec_not, a lemma which is copied from an instance from lean's init.logic. Is there a way of just convincing the elaborator to figure this out for me?

As you say, this is already in core lean, under the (autogenerated) name `not.decidable`

. The elaborator will infer it automatically in most places, but if you need to trigger typeclass inference manually use the tactic `apply_instance`

.

Second, what does the weird warning message by decidable_out mean?

`lemma`

s and `theorem`

s don't generate code in the VM. This means that you should basically always mark any inhabitant of a Type as a `def`

not a `lemma`

, or else you will get these strange error messages when you use the `def`

-that-isn't.

#### Mario Carneiro (Sep 11 2018 at 04:20):

I'm not sure why you are redefining all these symbols. You are just making typeclass inference harder for no reason

#### Mario Carneiro (Sep 11 2018 at 04:31):

def is_min_out (x : finset α) (G : finset (finset α)) : Prop := x ∉ G ∧ (∀ y, y ⊂ x → y ∈ G) instance (x : finset α) (G : finset (finset α)) : decidable (is_min_out x G) := decidable_of_iff (x ∉ G ∧ ∀ y ∈ (finset.powerset x).erase x, y ∈ G) begin simp [is_min_out, (⊂), finset.ssubset_iff], refine and_congr iff.rfl (forall_congr $ λ y, _), refine ⟨λ H h₁ h₂, H (mt _ h₂) h₁, λ H h₁ h₂, H h₂ (mt _ h₁)⟩, { rintro rfl, refl }, { exact finset.subset.antisymm h₂ } end

#### Bryan Gin-ge Chen (Sep 11 2018 at 04:37):

Thanks so much Mario!

I'm not sure why you are redefining all these symbols. You are just making typeclass inference harder for no reason

The honest reason is that I don't know any better. What precisely should I be avoiding?

#### Bryan Gin-ge Chen (Sep 11 2018 at 04:38):

Oh, you mean just the names `is_in`

and `is_out`

. Those are artifacts of my making a MWE; in reality, there's a structure that I have to pull the finset from.

Last updated: May 08 2021 at 09:11 UTC