Return element of 'a::finite_lattice · Beginner Questions

But I am not sure how to work with an element of that type or how to even create such. Is that even possible?

Manuel Eberl (Aug 30 2022 at 12:41):

No, at least not like this. The order of the lattice comes from the type class and is thus fixed for any given type. What you can do is to define a type constructor dual that takes a type parameter 'a and then instantiates the type class with the order reversed. You also get morphisms to_dual :: 'a ⇒ 'a dual and from_dual :: 'a dual ⇒ 'a that map between the type's copy and the type itself. The to_dual sort of corresponds to the reverse_lattice you tried to define above.

This requires quite a bit of boilerplate to set up, but it's not that hard if you know what needs to be done. In fact, I think something like this should probably be put into HOL-Library (if it doesn't exist already).

typedef 'a dual = "UNIV :: 'a set"
  morphisms from_dual to_dual by blast

setup_lifting type_definition_dual


instantiation dual :: (ord) ord
begin

lift_definition less_eq_dual :: "'a dual ⇒ 'a dual ⇒ bool" is "(≥)" .
lift_definition less_dual :: "'a dual ⇒ 'a dual ⇒ bool" is "(>)" .

instance ..

end


instance dual :: (order) order
  by standard (transfer; force)+

instance dual :: (preorder) preorder
  by standard (transfer; force simp: less_le_not_le intro: order.trans)+

instance dual :: (linorder) linorder
  by standard (transfer; force)+


instantiation dual :: (sup) inf
begin
lift_definition inf_dual :: "'a dual ⇒ 'a dual ⇒ 'a dual" is sup .
instance ..
end

instance dual :: (semilattice_sup) semilattice_inf
  by standard (transfer; simp)+

instantiation dual :: (inf) sup
begin
lift_definition sup_dual :: "'a dual ⇒ 'a dual ⇒ 'a dual" is inf .
instance ..
end

instantiation dual :: (Sup) Inf
begin
lift_definition Inf_dual :: "'a dual set ⇒ 'a dual" is Sup .
instance ..
end

instantiation dual :: (Inf) Sup
begin
lift_definition Sup_dual :: "'a dual set ⇒ 'a dual" is Inf .
instance ..
end

instantiation dual :: (top) bot
begin
lift_definition bot_dual :: "'a dual" is top .
instance ..
end

instantiation dual :: (bot) top
begin
lift_definition top_dual :: "'a dual" is bot .
instance ..
end


instance dual :: (semilattice_inf) semilattice_sup
  by standard (transfer; simp)+

instance dual :: (lattice) lattice
  by standard

instance dual :: (distrib_lattice) distrib_lattice
  by standard (transfer; simp add: inf_sup_distrib1)

instance dual :: (complete_lattice) complete_lattice
  by standard (transfer; force intro: Sup_upper Inf_lower simp: Sup_le_iff le_Inf_iff; fail)+

instance dual :: (finite_lattice) finite_lattice
  by standard (transfer; simp; fail)+


lemma from_dual_le_iff [simp]: "from_dual x ≤ from_dual y ⟷ x ≥ y"
  by transfer auto

lemma from_dual_less_iff [simp]: "from_dual x < from_dual y ⟷ x > y"
  by transfer auto

lemma to_dual_le_iff [simp]: "to_dual x ≤ to_dual y ⟷ x ≥ y"
  by transfer auto

lemma to_dual_less_iff [simp]: "to_dual x < to_dual y ⟷ x > y"
  by transfer auto

waynee95 (Aug 30 2022 at 17:28):

@Manuel Eberl I already feared that it might be more involved to do that. How would I use to_dual?

datatype variance =
  Plus
  | Minus
  | PlusMinus

datatype ty =
  Base
  | Fun ty variance ty

The variances are used to specify the dependency of the values of a function on their arguments, e.g. Plus indicates a _monotonic_ dependency.

We can mathematically define the following constructions on complete lattices: inverse, flattening, product of lattices and creating the lattice of component-wise ordered monotonic functions between two lattices.

These constructions are then used to associate with each ty a complete lattice.

Stream: Beginner Questions

Topic: Return element of 'a::finite_lattice

waynee95 (Aug 30 2022 at 11:20):

Manuel Eberl (Aug 30 2022 at 12:41):

waynee95 (Aug 30 2022 at 17:28):