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