Instance hypotheses in instance parameter

Stream: lean4

[Aaron Liu]

I'm working on making docs#RelHom.instFintype more efficient. I've decided that the best way to state it has a typeclass parameter [∀ a b [Decidable (a = b)], Decidable (s a b)]. Unfortunately, synthesis is not aware of the [Decidable (a = b)] instance while synthesizing Decidable (s a b). Is there another way I can do this?

[Eric Wieser]

What do you mean by efficient?

[Aaron Liu]

faster to #eval and #reduce

[Eric Wieser]

What are you trying to achieve with that argument?

[Aaron Liu]

I have an instance [Fintype V] [Fintype α] [DecidableEq V] [DecidableRel G.Adj] : Fintype (G.Coloring α) in which I would like to reuse this code without requiring [DecidableEq α]

[Eric Wieser]

Do you have a mwe?

[Aaron Liu]

Is this sufficient?

class Foo where

instance instFoo [∀ p [Decidable p], Decidable p] : Foo where

-- fails
#synth Foo

-- what I expect to be synthesized
#check @instFoo fun (p : Prop) [inst : Decidable p] => inst

[Aaron Liu]

btw this is for #22919

[Eric Wieser]

I don't understand how you intend to use [∀ p [Decidable p], Decidable p] in the implementation of instFoo

[Eric Wieser]

(and obviously that example is too contrived)

[Aaron Liu]

Ok, do you want the actual code?

[Aaron Liu]

Here's what I have

import Mathlib

attribute [-instance] SimpleGraph.instFintypeColoring

--- Mathlib/Data/Fintype/Pi ---

private def finHomFintype {n m} {r : Fin n → Fin n → Prop} {s : Fin m → Fin m → Prop}
    [DecidableRel r] [DecidableRel s] : Fintype (r →r s) :=
  sorry

instance RelHom.instFintype_1 {α β} {r : α → α → Prop} {s : β → β → Prop}
    [Fintype α] [Fintype β] [DecidableEq α] [DecidableRel r]
    [∀ a b [Decidable (a = b)], Decidable (s a b)] :
    Fintype (r →r s) :=
  (Fintype.truncFinBijection β).recOnSubsingleton fun ⟨b, hb⟩ ↦
    (Fintype.truncEquivFin α).recOnSubsingleton fun a ↦
      haveI : ∀ x y, Decidable (b x = b y) := fun x y =>
        decidable_of_iff (x = y) hb.injective.eq_iff.symm
      haveI : DecidableRel (b ⁻¹'o s) := fun x y =>
        inferInstanceAs (Decidable (s (b x) (b y)))
      ⟨(@Finset.univ _ finHomFintype).map ⟨fun (f : a.symm ⁻¹'o r →r b ⁻¹'o s) => sorry, sorry⟩, sorry⟩

--- Mathlib/Combinatorics/SimpleGraph/Basic ---

instance Top.adjDecidable {V} (v w : V) [Decidable (v = w)] : Decidable ((⊤ : SimpleGraph V).Adj v w) :=
  inferInstanceAs <| Decidable (v ≠ w)

--- Mathlib/Combinatorics/SimpleGraph/Coloring ---

instance SimpleGraph.instFintypeColoring_1 {V α} (G : SimpleGraph V) [Fintype V] [Fintype α]
    [DecidableEq V] [DecidableRel G.Adj] : Fintype (G.Coloring α) :=
  inferInstance

[Eric Wieser]

What's the issue with adding [DecidableEq β] here?

[Eric Wieser]

Most of the time when someone says "constructively finite" they mean [DecidableEq β] [Fintype β] anyway

[Aaron Liu]

I prefer to not have it if possible

[Aaron Liu]

And I hope to also reuse this for RelEmbedding.instFintype

[Aaron Liu]

A very fun Fintype that doesn't have DecidableEq is Prop

[Aaron Liu]

I guess for now I'll just have a primed version? Or will that create diamonds

[Eric Wieser]

Aaron Liu said:

And I hope to also reuse this for RelEmbedding.instFintype

Do you have this in a branch anywhere? @Harry Richman asked about this at ICERM today

[Aaron Liu]

Eric Wieser said:

Aaron Liu said:

And I hope to also reuse this for RelEmbedding.instFintype

Do you have this in a branch anywhere? Harry Richman asked about this at ICERM today

I haven't written it yet

[Eric Wieser]

My inclination for now is to split your PR into "add the computable instance" and a follow up "weaken the decidable hypothesis"

[Eric Wieser]

I'm happy to do the split and solve the conflicts