Zulip Chat Archive

Stream: general

Topic: fintype for functions


Thorsten Altenkirch (Jul 28 2022 at 16:24):

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 (Jul 28 2022 at 16:25):

docs#pi.fintype

Kyle Miller (Jul 28 2022 at 16:26):

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

Kyle Miller (Jul 28 2022 at 16:28):

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 (Jul 28 2022 at 16:39):

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 (Jul 28 2022 at 16:42):

Does @[derive fintype] work?

Thorsten Altenkirch (Jul 28 2022 at 16:46):

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 (Jul 28 2022 at 16:47):

It goes before not after

Eric Wieser (Jul 28 2022 at 16:48):

But it won't work here

Thorsten Altenkirch (Jul 28 2022 at 16:49):

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

Eric Wieser (Jul 28 2022 at 16:49):

import tactic.derive_fintype

Thorsten Altenkirch (Jul 28 2022 at 16:50):

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

Eric Wieser (Jul 28 2022 at 16:50):

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

Eric Wieser (Jul 28 2022 at 16:51):

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 (Jul 28 2022 at 16:52):

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 (Jul 28 2022 at 16:53):

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 (Jul 28 2022 at 16:54):

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

Eric Wieser (Jul 28 2022 at 16:54):

docs#fintype.of_surjective is what you're after

Eric Wieser (Jul 28 2022 at 16:55):

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

Kyle Miller (Jul 28 2022 at 16:55):

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

Thorsten Altenkirch (Jul 28 2022 at 16:56):

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 (Jul 28 2022 at 16:56):

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 (Jul 28 2022 at 16:57):

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

Eric Wieser (Jul 28 2022 at 16:58):

I disagree, it's computable

Eric Wieser (Jul 28 2022 at 16:58):

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 (Jul 28 2022 at 16:58):

Ah, right, ok

Kyle Miller (Jul 28 2022 at 16:59):

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 (Jul 28 2022 at 17:00):

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

Kyle Miller (Jul 28 2022 at 17:01):

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

Eric Wieser (Jul 28 2022 at 17:01):

Weird, I can't reproduce your code any more

Kyle Miller (Jul 28 2022 at 17:02):

I accidentally had open_locale classical too.

Eric Wieser (Jul 28 2022 at 17:05):

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 (Jul 28 2022 at 17:12):

The proof of the sorry escapes me

Kyle Miller (Jul 28 2022 at 17:23):

@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 (Jul 28 2022 at 17:26):

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

Eric Wieser (Jul 28 2022 at 17:28):

Can you prove that?

Mario Carneiro (Jul 28 2022 at 17:28):

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

Mario Carneiro (Jul 28 2022 at 17:28):

that is, p = true \/ p = false

Mario Carneiro (Jul 28 2022 at 17:29):

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

Mario Carneiro (Jul 28 2022 at 17:30):

because both types are singletons

Eric Rodriguez (Jul 28 2022 at 17:31):

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 (Jul 28 2022 at 17:32):

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

Thorsten Altenkirch (Jul 28 2022 at 17:33):

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 (Jul 28 2022 at 17:39):

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 (Aug 03 2022 at 09:23):

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 (Aug 03 2022 at 09:24):

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

Quanwen Chen (Aug 03 2022 at 09:38):

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


Last updated: Dec 20 2023 at 11:08 UTC