subtype as a fintype

Stream: Is there code for X?

[Vincent Beffara]

Do we have this?

instance fintype.subtype' (α : Type) [fintype α] (p : α → Prop) [decidable_pred p] :
  fintype {x // p x} :=
fintype.subtype (finset.filter p finset.univ)
  (λ x, by simp only [finset.mem_filter, finset.mem_univ, true_and])

It is not found by apply_instance...

[Yaël Dillies]

docs#subtype.fintype :wink:

[Vincent Beffara]

Ah ...

[Vincent Beffara]

So why doesn't apply_instance find it?

[Eric Rodriguez]

decidable_pred is why

[Vincent Beffara]

by apply_instance fails and by apply subtype.fintype works in my use case, so lean is able to infer what p is and figure out that it is decidable, but still needs the hint? (I'm still lost with the typeclass system.)

[Yaël Dillies]

This works for me

import data.fintype.basic

instance fintype.subtype' (α : Type) [fintype α] (p : α → Prop) [decidable_pred p] :
  fintype {x // p x} :=
by apply_instance

[Adam Topaz]

Add open_locale classical to your file to activate math mode

[Vincent Beffara]

structure edge (α : Type) (r : α → α → Prop) := (x y : α) (adj : r x y)

noncomputable instance titi (α : Type) [fintype α] (r : α → α → Prop) :
  fintype (edge α r) :=
begin
    let f : edge α r → α × α := λ e, (e.x, e.y), apply fintype.of_injective f,
    rintros ⟨x₁,y₁,h₁⟩ ⟨x₂,y₂,h₂⟩, simp only [prod.mk.inj_iff], exact id
end

def good (α β : Type) (r : α → α → Prop) (f : α → β): Type :=
{e : edge α r // f e.x ≠ f e.y}

noncomputable instance toto (α β : Type) (r : α → α → Prop) (f : α → β)
    [decidable_rel r] [fintype α] [decidable_eq β] :
  fintype (good α β r f) := by apply_instance

noncomputable instance toto' (α β : Type) (r : α → α → Prop) (f : α → β)
    [decidable_rel r] [fintype α] [decidable_eq β] :
  fintype (good α β r f) := by apply subtype.fintype

The first instance fails, the second one succeeds

[Yaël Dillies]

I suspect this is because of the (ir)reducibility of good. In that case you probably want to move the instance over by hand.

[Vincent Beffara]

Ah, right, marking good as @[reducible] makes it work. Slowly learning :grinning:

[Yaël Dillies]

To reassure you, this is a pretty technical issue!