finsets, decidable_mem, and filter

Stream: new members

[Bryan Gin-ge Chen]

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.encodableor something?

Thanks again!

[Mario Carneiro]

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?

lemmas and theorems 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]

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

[Mario Carneiro]

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]

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]

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.