Problems with deriving noncomputable instances

Stream: new members

[Egor Morozov]

Here is my setup. I'm sorry for a long piece of code but I could not reproduce with a smaller mwe.

import Mathlib

structure WDigraph (V R : Type*) [CommSemiring R] where
  weight : V → V → R

universe u v

variable {V : Type u}
variable {R : Type v} [CommSemiring R]
variable (G : WDigraph V R)

namespace WDigraph

def Adj (u v : V) : Prop := G.weight u v ≠ 0

inductive Walk : V → V → Type u
  | nil {u : V} : Walk u u
  | cons {u v w : V} (h : G.Adj u v) (p : Walk v w) : Walk u w
  deriving DecidableEq

class IsWeaklyLocallyFinite : Prop where
  fin_walks : ∀ (u v : V), Finite (G.Walk u v)

instance {u v : V} [h : IsWeaklyLocallyFinite G] : Finite (G.Walk u v) :=
  h.fin_walks u v

noncomputable instance {u v : V} [IsWeaklyLocallyFinite G] :
  Fintype (G.Walk u v) := Fintype.ofFinite _

variable [IsWeaklyLocallyFinite G]
variable {n : ℕ} (A B : Fin n → V)

suppress_compilation
structure path_system {n : ℕ} [IsWeaklyLocallyFinite G] (A B : Fin n → V) where
  σ : Equiv.Perm (Fin n)
  path : (i : Fin n) → G.Walk (A i) (B (σ i))
  deriving Fintype
unsuppress_compilation

(I'm working on the formalization of Gessel-Lindström-Viennot lemma if someone is interested.)
Now I have two questions
Question #1: why

#synth Fintype (path_system G A B)

fails?
Question #2: why I cannot delete [IsWeaklyLocallyFinite G] from the definition of path_system?
Also, if there are some thoughts on how to do better what I'm trying to do here, it would be nice too.

[Kevin Buzzard]

I can't comment on the mathematics, but the answer to Q1 seems to be this:

suppress_compilation
whatsnew in -- I added this
structure path_system {n : ℕ} [IsWeaklyLocallyFinite G] (A B : Fin n → V) where
  σ : Equiv.Perm (Fin n)
  path : (i : Fin n) → G.Walk (A i) (B (σ i))
  deriving Fintype
unsuppress_compilation

and then searching for Fintype in the output, gives us this:

def WDigraph.instFintypePath_system.{u_1, u_2} : {V : Type u_1} →
  {R : Type u_2} →
    {inst : CommSemiring R} →
      {G : WDigraph V R} →
        {n : ℕ} →
          {inst_1 : G.IsWeaklyLocallyFinite} →
            {A B : Fin n → V} → [Fintype V] → [Fintype R] → Fintype (G.path_system A B) :=
[blah]

so that's the instance you want to fire, and then trying to make it fire explicitly with

example : Fintype (path_system G A B) := WDigraph.instFintypePath_system

gives the error

failed to synthesize
  Fintype V

so deriving Fintype has made the instance under a finiteness assumption on V which you don't seem to be assuming.

And the answer to Q2 seems to be that deriving Fintype cannot figure out how to prove finiteness without this assumption on G.

Remember that deriving Fintype is just a dumb algorithm. If you are able to prove finiteness statements under weaker assumptions than those required by the dumb algorithm then you can just supply these arguments explicitly with

instance <your assumptions here> : Fintype (path_system G A B) := <your proof here>

and then #synth should work.

[Egor Morozov]

So deriving Fintype can add new assumptions to the context and say that everything is ok? And this fact becomes clear only when you really try to synthesize an instance... This looks very strange for me.
Concerning Q2, it is true that deriving Fintype needs [IsWeaklyLocallyFinite G] here but the latter is added to the context by variable [IsWeaklyLocallyFinite G] above. So this mechanism doesn't work with structure? I tried to do the same with def many times and it was fine.

[Egor Morozov]

Okay, I see that deriving Fintype does not work here. Now I'm trying to define an instance directly. I guess I need something like a type equivalence path_system G A B ≃ (σ : Equiv.Perm (Fin n)) × ((i : Fin n) → G.Walk (A i) (B (σ i))). I wonder if there is a way to extract it directly from structure? Of course, it is not difficult to define it manually as well but it looks a bit awkward.

[Egor Morozov]

Finally I came up with this

namespace path_system

variable {n : ℕ} (A B : Fin n → V)

def to_prod (P : path_system G A B) :
  (σ : Equiv.Perm (Fin n)) × ((i : Fin n) → G.Walk (A i) (B (σ i))) :=
  ⟨P.σ, P.path⟩

def from_prod (P : (σ : Equiv.Perm (Fin n)) × ((i : Fin n) →
  G.Walk (A i) (B (σ i)))) : path_system G A B := ⟨P.1, P.2⟩

def equiv_to_prod : (σ : Equiv.Perm (Fin n)) × ((i : Fin n) →
  G.Walk (A i) (B (σ i))) ≃ path_system G A B :=
  { toFun := from_prod G A B,
    invFun := to_prod G A B,
    left_inv := by
      intro _
      simp only [to_prod, from_prod]
    right_inv := by
      intro _
      simp only [to_prod, from_prod]
  }

instance : Finite (path_system G A B) := Finite.of_equiv _ (equiv_to_prod G A B)

noncomputable instance : Fintype (path_system G A B) := Fintype.ofFinite _

Well, at least it works, although I'm not sure there is not a lot of redundant code here.