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