Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] using mono predicate


view this post on Zulip Email Gateway (Aug 18 2022 at 17:38):

From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello,

I have the following theory fragment:

theory test imports Main
begin

class test = lattice
begin

theorem test:
"f x = (x::'a) ==> mono f ==> f x = x"

When processing the theorem test I get the following error:

*** Type unification failed: Variable 'a::type not of sort order

The predicate mono is defined in class order and class lattice
extends the class order.

Best regards,

Viorel Preoteasa

view this post on Zulip Email Gateway (Aug 18 2022 at 17:38):

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Dear Viorel,

this is how the type error arises:
In the context order, mono has the type "'a :: type => 'b :: order => bool",
which is specified in the definition of mono in theory Orderings. The sort
constraint order on 'b is necessary such that the order operation are availabe
on the image type.

In your theorem test, you are in the locale context test, which is a sublocale
of order, i.e. mono has the polymorphic type "'a :: type => ?'b :: order =>
bool" where ?'b is free and 'a is bound.
The function f has type "'a :: type => 'a", i.e., mono's type must be
specialized such that ?'b becomes 'a. However, 'a is not known to be of sort
order, so this gives the type error.

I know of three approaches to your problem:

  1. State and prove your theorem test outside the context test, but with explicit
    sort constraints:

class test = lattice

theorem test: "f x = (x::'a :: test) ==> mono f ==> f x = x"

Alternatively, you can use the sort constraint "order" instead of "test".

This approach is suitable if

  1. Change the definition of class test such that 'a has the sort constraint
    order. The conditions are similar to 1., but now, everything in context test
    includes the sort constraint.

  2. Give up on type classes and do everything in locales. Then, you will have to
    define mono yourself in a locale for order morphisms and setup proof automation
    by yourself. The locale tutorial contains such an example with order
    homomorphisms. If you base your order morphism locale on the locale "order" that
    lives behind the type class "order", you get some automation from the type class
    "order" for free, but not everything (cf.
    https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-February/msg00132.html).
    You cannot have order morphisms as type class because they would involve
    multiple type variables, which Isabelle does not support.

Hope this helps,
Andreas

Viorel Preoteasa schrieb:

view this post on Zulip Email Gateway (Aug 18 2022 at 17:38):

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hello Viorel,

there is no direct way to enforce this. The easiest is to add a trivial
assumption which introduces the sort constraint, for example:

class test = lattices +
assumes "(a :: 'a :: order) = a"

The class command also accepts the constrains element that locales support, but
this seems to be without effect.

Andreas

Viorel Preoteasa schrieb:


Last updated: Mar 29 2024 at 08:18 UTC