Email Gateway (Aug 19 2022 at 09:19): Email Gateway (Aug 19 2022 at 09:19):From: Alessandro Coglio <coglio@kestrel.edu>
Hello,
Since a (non-empty) finite lattice is also complete, I would like to define
class finite_lattice = finite + lattice
and then prove
instance finite_lattice < complete_lattice
after giving suitable definitions for Inf/Sup/bot/top.
But apparently
instance A < B
requires A to have (at definition time) all the operators of B. Are
there "deep" reasons for this requirement, or could it be relaxed with
relative ease to allow the extra operators to be defined after A has
been defined and then used to show that A is a subclass of B?
Anyhow, given the current situation, one approach is to define
finite_lattice as above, define Inf/Sup/bot/top on finite_lattice, and
prove that finite_lattice is a sublocale of complete_lattice. In this
way, after proving that a type L has class finite_lattice, all the
operators and theorems of complete_lattice should be available for L.
The drawback of this approach is that L will not have class
complete_lattice, and so, for example, existing operations that take
complete_lattice arguments cannot be used on L.
Another approach is to define class finite_lattice to include
Inf/Sup/bot/top, along with assumptions that define these four operators
in terms of the existing operators of finite_lattice. In this way,
finite_lattice can be a subclass of complete_lattice. The drawback is
that proving that a type L has class finite_lattice will require more
work because of the extra operators and assumptions that must be
satisfied (but perhaps this work can be eased by proving and using
general lemmas that relate Inf/Sup/bot/top to inf and sup). Furthermore,
the approach seems (to me) methodologically less clean than the previous
one.
A third approach is to define
class finite_lattice = finite + complete_lattice
and avoid proving subclass relations altogether. The drawback is that
proving that a type L has class finite_lattice is even more work (but
again perhaps this work can be eased by suitable general lemmas). This
seems to be the approach taken in the library definition of class
complete_lattice, which includes bounded_lattice explicitly, even though
Inf and Sup suffice. Also, this approach seems (to me) methodologically
less clean than the previous two.
Does anybody have comments on the three approaches sketched above?
Relative pros and cons? Other approaches?
Thank you in advance!
smime.p7s
Email Gateway (Aug 19 2022 at 09:21):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Alessandro,
Since a (non-empty) finite lattice is also complete, I would like to
defineclass finite_lattice = finite + lattice
and then prove
instance finite_lattice < complete_lattice
after giving suitable definitions for Inf/Sup/bot/top.
But apparently
instance A < B
requires A to have (at definition time) all the operators of B. Are
there "deep" reasons for this requirement, or could it be relaxed with
relative ease to allow the extra operators to be defined after A has
been defined and then used to show that A is a subclass of B?
this is a well-known restriction of type classes. The short answer is,
no, this restriction cannot be lifted. This is the price you have to
pay to have operations and assumptions about them: in order for a
structure to be a complete lattice, it is not necessary that there exist
operations which satisfy its properties, but these operations must be
explicitly defined for that particular type.
Anyhow, given the current situation, one approach is to define
finite_lattice as above, define Inf/Sup/bot/top on finite_lattice
Such definitions would be rejected, since they violate the rules for
overloading: Inf/Sup/bot/top can only be instantiated on particular type
constructors, not (sort-constrained) type variables.
Another approach is to define class finite_lattice to include
Inf/Sup/bot/top, along with assumptions that define these four operators
in terms of the existing operators of finite_lattice. In this way,
finite_lattice can be a subclass of complete_lattice. The drawback is
that proving that a type L has class finite_lattice will require more
work because of the extra operators and assumptions that must be
satisfied (but perhaps this work can be eased by proving and using
general lemmas that relate Inf/Sup/bot/top to inf and sup). Furthermore,
the approach seems (to me) methodologically less clean than the previous
one.
IMHO it is the cleanest one you can achieve inside the current
infrastructure. E.g.
lemma finite_complete_lattice:
assumes Inf: "\<And>A. (Inf :: ('a::{Inf, Sup, bounded_lattice, finite}) set ⇒ 'a) A =
(if A = {} then top else Inf_fin A)"
assumes Sup: "\<And>A. (Sup :: ('a::{Inf, Sup, bounded_lattice, finite}) set ⇒ 'a) A =
(if A = {} then top else Sup_fin A)"
shows "OFCLASS('a::{Inf, Sup, bounded_lattice, finite}, complete_lattice_class)"
proof
A third approach is to define
class finite_lattice = finite + complete_lattice
and avoid proving subclass relations altogether. The drawback is that
proving that a type L has class finite_lattice is even more work (but
again perhaps this work can be eased by suitable general lemmas).
This does indeed save you nothing on instance proofs.
This
seems to be the approach taken in the library definition of class
complete_lattice, which includes bounded_lattice explicitly, even though
Inf and Sup suffice. Also, this approach seems (to me) methodologically
less clean than the previous two.
The issue is that class bot already demands assumptions on bot and thus
you cannot instantiate bot without actually proving these.
There have been two ideas around to lift this somehow:
Provide purely syntactic classes for operations without further
assumptions; this has a long tradition in isabelle (cf. plus, times,
zero etc.), but has the disadvantage that you can write down things
syntactically which do not obey properties you would expect naively
(i.e. "a + 0 = a" does not hold in general).
Build a fancy wrapper around instantiation in the spirit of Haskell
default class method definitions. Since this must also cover proofs, it
would be a tedious affair and maybe not worth doing it.
Cheers,
Florian
signature.asc
Last updated: Apr 19 2024 at 12:27 UTC