Email Gateway (Aug 19 2022 at 08:44): Email Gateway (Aug 19 2022 at 08:44):From: John Munroe <munddr@gmail.com>
Hi,
I'm trying to define a new type which is essentially a set of 3 pairs.
Two objects of that type are equal iff 2 of the pairs are equal. I
have a few questions:
1) If I declare that type using 'typedecl' then how do I express that
it's essentially a set of 3 pairs? 'type_synonym' doesn't seem to be
appropriate since the existing equality on sets of pairs conflicts
with my notion of equality.
2) Even if I declare a new type, does my notion of equality conflict
with any of the existing lemmas, creating a contradiction? Equality is
polymorphic, so I should be able to define it whichever way I want,
right?
Thanks a lot for your time in advance.
John
Email Gateway (Aug 19 2022 at 08:44):From: John Wickerson <jpw48@cam.ac.uk>
Hi John,
I don't think that's a good notion of equality, because it's not transitive.
{(1,2);(3,4);(5,6)} = {(1,2);(3,4);(7,8)} = {(1,2);(5,6);(7,8)}
but
{(1,2);(3,4);(5,6)} =/= {(1,2);(5,6);(7,8)}
Best wishes,
John
Email Gateway (Aug 19 2022 at 08:44):From: John Wickerson <jpw48@cam.ac.uk>
Sorry, I messed up my counterexample. I meant:
{(1,2);(3,4);(5,6)} = {(1,2);(3,4);(7,8)} = {(1,2);(9,10);(7,8)}
but
{(1,2);(3,4);(5,6)} =/= {(1,2);(9,10);(7,8)}
John
Email Gateway (Aug 19 2022 at 08:45):From: Elsa L Gunter <egunter@illinois.edu>
Dear John,
Equality is not something you get to define. It already exists, at
all types already introduce and those yet to be formally introduced.
Polymorphism doesn't mean you get to define it at each type whatever way
you please. It means that is has been defined, or otherwise introduced,
in a way that is uniform at all types. Among other things, it is a
relation satisfying
HOL.subst: [|?s = ?t; ?P ?s |] ==> ?P ?t
no matter what type ?s and ?t have.
If you create a new type (which is what I'm guessing you really want to
do), then two elements in the new type are equal iff their
representations in the underlying model are equal. I don't quite
understand the definition of the type you are trying to create, but it
sounds to me like you really want to have an underlying model that
starts with (some collection of) sets of something (pairs?) and that you
then want to define an equivalence relation on those sets, and then your
model would be (some of) the equivalence classes.
---Elsa
Last updated: Apr 27 2024 at 04:17 UTC