fintype for functions

Stream: general

[Thorsten Altenkirch]

Is there an instance of fintype that shows that

instance (α β : Type*) [fintype α] [fintype β] : fintype (α → β)

If not, maybe there is some advice how to prove it?

[Eric Rodriguez]

docs#pi.fintype

[Kyle Miller]

It needs decidable equality on the domain to construct that fintype.

[Kyle Miller]

One trick for finding these instances from within Lean when you're not sure of the decidability assumptions is this:

open_locale classical
noncomputable def foo (α β : Type*) [fintype α] [fintype β] : fintype (α → β) := by apply_instance
#print foo
-- ... pi.fintype

[Thorsten Altenkirch]

Actually what we really want to show is

structure decPow(A : Type 1) : Type 2 :=
  (pred : A → Prop)
  [decP : decidable_pred pred]

instance finpow (A : Type 1) [fintype A][decidable_eq A] : fintype (decPow A) := sorry

(How can we use universes better here?) We can show this by using pi.fintype and showing that decPow is the same as A -> Bool but maybe there is a better way?

[Eric Wieser]

Does @[derive fintype] work?

[Thorsten Altenkirch]

Eric Wieser said:

Does @[derive fintype] work?

Like

structure decPow(A : Type 1) : Type 2 :=
  (pred : A → Prop)
  [decP : decidable_pred pred]
  @[derive fintype]

seems to work?

[Eric Wieser]

It goes before not after

[Eric Wieser]

But it won't work here

[Thorsten Altenkirch]

Ok now I see. failed to find a derive handler for 'fintype'

[Eric Wieser]

import tactic.derive_fintype

[Thorsten Altenkirch]

Ah ok then I get failed to synthesize type class instance for

[Eric Wieser]

But like I said, it won't work anyway. by tactic.mk_fintype_instance also fails

[Eric Wieser]

Thorsten Altenkirch said:

We can show this by using pi.fintype and showing that decPow is the same as A -> Bool but maybe there is a better way?

this sounds like a good strategy to me. I think the equivalence with A -> Bool is worth having anyway

[Thorsten Altenkirch]

Do we actually need the equivalence? It seems we should only need one direction. Namely that the is an injection from DecProp A to A -> Bool. I guess there is a fintype instance for this?

[Eric Wieser]

Thorsten Altenkirch said:

(How can we use universes better here?)

Let lean deal with it

structure decPow (A : Type*) :=
(pred : A → Prop)
[decP : decidable_pred pred]

as it turns out, there's no need for a universe bump

[Eric Wieser]

Arguably you should make the equivalence anyway since it's true

[Eric Wieser]

docs#fintype.of_surjective is what you're after

[Eric Wieser]

Although you might run into trouble since that needs decidable equality of your structure

[Kyle Miller]

I'm not sure you can make decPow be a computable fintype -- is that ok?

[Thorsten Altenkirch]

Eric Wieser said:

Although you might run into trouble since that needs decidable equality of your structure

Yes, but we need this anyway.

[Kyle Miller]

Here's a noncomputable one:

import topology.separation

open_locale classical

structure decPow (A : Type 1) : Type 2 :=
  (pred : A → Prop)
  [decP : decidable_pred pred]

-- ideally this could be generated automatically using a `mk_equiv` attribute, like `mk_iff`
def decPow_equiv (A) : decPow A ≃ (Σ (p : A → Prop), decidable_pred p) :=
{ to_fun := λ o, ⟨o.pred, o.decP⟩,
  inv_fun := λ e, @decPow.mk _ e.1 e.2,
  left_inv := by { intro, cases x, refl, },
  right_inv := by { intro, cases x, refl, } }

noncomputable instance finpow (A : Type 1) [fintype A] : fintype (decPow A) :=
fintype.of_equiv _ (decPow_equiv A).symm

[Kyle Miller]

The issue is that you can't enumerate decidable p unless you have a proof or disproof of p.

[Eric Wieser]

I disagree, it's computable

[Eric Wieser]

import data.fintype.basic

structure decPow (A : Type*) :=
(pred : A → Prop)
[decP : decidable_pred pred]

attribute [instance] decPow.decP

instance finpow (A : Type 1) [fintype A] [decidable_eq A] : fintype (decPow A) :=
fintype.of_equiv (A → bool) $
  { to_fun := λ p, ⟨λ a, p a⟩,
    inv_fun := λ A i, A.pred i,
    left_inv := sorry,
    right_inv := sorry }

[Kyle Miller]

Ah, right, ok

[Kyle Miller]

At that point, I think it would be better to define pred to be A -> bool rather than tacking on the decidability assumption, seeing as decidable_pred amounts to a way to lift A -> Prop to A -> bool.

[Eric Wieser]

@Kyle Miller, can you add imports to your example?

[Kyle Miller]

Sure, it's a silly one (import topology.separation) just because of the file I happened to be in.

[Eric Wieser]

Weird, I can't reproduce your code any more

[Kyle Miller]

I accidentally had open_locale classical too.

[Eric Wieser]

Perhaps mathlib should have

def equiv.sigma_decidable_pred {α : Type*} : (Σ (p : α → Prop), decidable_pred p) ≃ (α → bool) :=
{ to_fun := λ A i, @to_bool (A.1 i) (A.2 i),
  inv_fun := λ p, ⟨λ a, p a, by apply_instance⟩,
  left_inv := sorry,
  right_inv := λ p, funext $ λ i, bool.to_bool_coe _ }

[Eric Wieser]

The proof of the sorry escapes me

[Kyle Miller]

@Eric Wieser Got it:

lemma foo (p q : Prop) (h : p ↔ q) (x : decidable p) (y : decidable q) : x == y :=
begin
  have := propext h,
  unfreezingI { cases this, },
  simp,
end

@[simps]
def equiv.sigma_decidable_pred {α : Type*} : (Σ (p : α → Prop), decidable_pred p) ≃ (α → bool) :=
{ to_fun := λ A i, by { haveI := A.2, exact A.1 i},
  inv_fun := λ p, ⟨λ i, p i, by apply_instance⟩,
  left_inv := λ A, begin cases A, resetI, simp, ext, refl, intros i i' h, cases h, dsimp,
    apply foo,
    simp,
 end,
  right_inv := λ p, funext $ λ i, bool.to_bool_coe _ }

(I also changed to_fun to use a coercion, but that's immaterial.)

[Kyle Miller]

I guess decidable is one of those rare types where you can deduce parameters are equal from heterogeneous equality of terms.

[Eric Wieser]

Can you prove that?

[Mario Carneiro]

you can prove it by "cases" on p and q

[Mario Carneiro]

that is, p = true \/ p = false

[Mario Carneiro]

actually maybe not; even if you know decidable true = decidable false I don't think you can deduce a contradiction

[Mario Carneiro]

because both types are singletons

[Eric Rodriguez]

def equiv.sigma_decidable_pred {α : Type*} : (Σ (p : α → Prop), decidable_pred p) ≃ (α → bool) :=
{ to_fun := λ A i, @to_bool (A.1 i) (A.2 i),
  inv_fun := λ p, ⟨λ a, p a, by apply_instance⟩,
  left_inv := λ p, sigma.ext (by simp) $ subsingleton.helim (by simp) _ _,
  right_inv := λ p, funext $ λ i, bool.to_bool_coe _ }

maybe is a bit clearer

[Eric Rodriguez]

I think foo is a weaker version of docs#subsingleton.helim, actually

[Thorsten Altenkirch]

Kyle Miller said:

At that point, I think it would be better to define pred to be A -> bool rather than tacking on the decidability assumption, seeing as decidable_pred amounts to a way to lift A -> Prop to A -> bool.

Yes, we thought of this. However, I want to use this in a lecture and it is easy to just use Prop for reasoning and to show separately that decidable predicates are the same as booleans. This is needed in the construction of the power automaton.

[Kyle Miller]

Eric Wieser said:

Can you prove that?

Sometimes Lean lets me too easily turn off the part of my brain that informs me about what I'm actually doing. I interpreted foo as if it were its converse when I said that.

[Quanwen Chen]

Eric Wieser said:

Although you might run into trouble since that needs decidable equality of your structure

Given the equivalence of (Σ (p : α → Prop), decidable_pred p) ≃ (α → bool), do we have a convenient way to show the decidable equality of Σ (p : α → Prop), decidable_pred p?

[Eric Wieser]

Yes, you can use equiv.sigma_decidable_pred.symm.surjective.forall\2 or similar

[Quanwen Chen]

Figured out that equiv.decidable_eq equiv.sigma_decidable_pred could solve the problem.