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):
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 beA -> bool
rather than tacking on the decidability assumption, seeing asdecidable_pred
amounts to a way to liftA -> Prop
toA -> 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