How to calculate the number of graphs or trees?

Stream: maths

[Brisal]

Hello! I want to use Fintype.card to count the number of trees in given condition. But I found I have to add the condition of dec_adj so that it makes T.degree hold and prove the instance of Fintype tree first. Can this work? Or maybe there exists other methods to formalize it ?

import Mathlib

structure tree where
  T : SimpleGraph (Fin 5)
  is_tree : T.IsTree
  dec_adj : DecidableRel T.Adj
  deg_T :
    T.degree ⟨0, by decide⟩ = 3

example : Fintype.card (tree) = _ := by
  sorry

instance : Fintype tree := sorry

[Kenny Lau]

there's no point using Fintype here because none of this is computable, so you should prove a Finite instance, for which you would want to prove that tree.T is injective, and then use Finite.of_injective

[Kenny Lau]

if you want the Fintype anyway you can afterwards do Fintype.ofFinite

[Aaron Liu]

Kenny Lau said:

there's no point using Fintype here because none of this is computable

really

[Aaron Liu]

what do you mean by that

[Kenny Lau]

ah, sorry, the map to SimpleGraph has noncomputable image, but if you add the dec_adj then it is computable

[Aaron Liu]

I don't think SimpleGraph carries any data

[Kenny Lau]

so instead of using just the injection tree.T, combine it with tree.dec_adj

[Kenny Lau]

Aaron Liu said:

I don't think SimpleGraph carries any data

I mean, I'm just saying that Set Unit has no decidable equality, essentially