# Zulip Chat Archive

## Stream: new members

### Topic: Type decidable_eq

#### Chase Norman (Jan 07 2023 at 04:06):

I am looking to prove ‘decidable_eq’ for a structure like this for the purpose of program verification:

`structure graph := (V : Type) (f : fintype V) (d : decidable_eq V) (w : V → V → ℤ) `

It has become clear that this graph does not satisfy `decidable_eq`

because `Type`

does not satisfy `decidable_eq`

. I would like to have different graphs of different types. Is there some subtype of `Type`

that I should use that has decidable equality? And how would I go about proving decidable equality of the resulting ‘graph’ type?

#### Mario Carneiro (Jan 07 2023 at 04:12):

you should move `V`

to a parameter

#### Mario Carneiro (Jan 07 2023 at 04:13):

also probably `[fintype V] [decidable_eq V]`

#### Chase Norman (Jan 07 2023 at 04:15):

How might you place multiple `graph`

instances with different `V`

in the same `list`

, for instance? @Mario Carneiro

#### Chase Norman (Jan 07 2023 at 04:17):

It is actually my intention that the node type `V`

is compared when two graphs are compared. However, since `Type`

does not have decidable equality, it seems that I will need to choose a subtype.

#### Mario Carneiro (Jan 07 2023 at 04:32):

In general, you can't do this because different types can't be compared. (#xy ?) For an enumerated list or schema of types, you can do it by having an inductive type (with decidable equality) giving the schema, and then an evaluation function which gives the type for one representative in order to put a graph structure on it

Last updated: Dec 20 2023 at 11:08 UTC