Email Gateway (Jun 24 2022 at 15:52): Email Gateway (Jun 24 2022 at 15:52):From: Steven Obua <obua@practal.com>
There has been going on a lot of work on quotient types for Isabelle/HOL, but when trying to use it for my formalisation of Abstraction Logic in Isabelle/HOL (https://github.com/practal/AL-in-HOL <https://github.com/practal/AL-in-HOL/blob/main/Quotients.thy>), I couldn't, because my quotients would depend on values.
So I rolled my own theory (https://github.com/practal/AL-in-HOL/blob/main/Quotients.thy) based on HOL.Equiv-Relations, which adds a nice twist on top: It defines a new type
typedef 'a quotient = { r::'a rel. ∃ A. equiv A r }
which is similar to 'a set, but allows a custom equivalence relation for each individual set. This has the advantage that you can now introduce notation like
u /∈ q
u = v (mod q)
where u and v have type 'a, and q has type 'a quotient. You can furthermore easily build up new quotients from existing ones, for example the quotient
p /⇒ q
which has type ('a ⇒ 'b) quotient, given that p has type 'a quotient, and q has type 'b quotient. Then for the normal composition operator for example, the following theorem holds:
(◦) /∈ (q /⇒ r) /⇒ (p /⇒ q) /⇒ (p /⇒ r)
As another example, q /^ n represents the vectors of length n with elements in q, and has type ('a list) quotient, where q has type 'a quotient.
So this makes reasoning modulo an equivalence relation quite straightforward and convenient, and I am relying heavily on it now for my formalisation.
Now my question: Does anyone know of similar work in HOL? I've seen that this is known as "setoid" in constructive mathematics and type theory, but I see it rather as a practical way of working around the limitations of simple types in classical HOL: Instead of using 'a set for a formalisation, use 'a quotient instead. In that sense, is there other work out there in HOL following this approach?
Cheers,
Steven
Last updated: Apr 25 2024 at 20:15 UTC