Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] setup_lifting - "no relator for the type" warning


view this post on Zulip Email Gateway (Aug 19 2022 at 09:39):

From: John Wickerson <jpw48@cam.ac.uk>
Dear Isabelle,

My attempt to make a typedef for finite sets ...

typedef 'a fset = "{A :: 'a set . finite A }"
by (rule exI[of _ "{}"], auto)

setup_lifting type_definition_fset

... results in the following warning message.

Generation of a parametrized correspondence relation failed.
Reason: No relator for the type "Set.set" found.

Could somebody kindly tell me how I can address this? Thanks.

john

view this post on Zulip Email Gateway (Aug 19 2022 at 09:39):

From: Ondřej Kunčar <kuncar@in.tum.de>
The relator for sets is defined in ~~/src/HOL/Library/Quotient_Set.
Including this file should remove the warning.

The warning is currently not really harmful because parametrized
correspondence relations are not used in Isabelle2013. I didn't include
other improvements of the Lifting package that depends on them to the
coming release. Maybe in the next release this will come into play.

Ondrej

view this post on Zulip Email Gateway (Aug 19 2022 at 09:40):

From: John Wickerson <jpw48@cam.ac.uk>
Thanks Ondrej.

Continuing my attempt to make a typedef for finite sets, I've managed to lift definitions like "union" from sets to finite sets. I'm now trying to lift "big union" from sets of sets to finite sets of finite sets, but this turns out to be less trivial. Could somebody kindly advise on how to do this proof?

Below is my complete .thy file.

Thanks very much,
john

------8<--------

theory J_Finite_Set imports
Main
"~~/src/HOL/Library/Quotient_Set"
begin

typedef 'a fset = "{A :: 'a set . finite A }"
by (rule exI[of _ "{}"], auto)

setup_lifting type_definition_fset

lift_definition
union_fset :: "'a fset ⇒ 'a fset ⇒ 'a fset"
is "union :: 'a set ⇒ 'a set ⇒ 'a set"
by simp

lift_definition
Union_fset :: "('a fset) fset ⇒ 'a fset"
is "Union :: 'a set set ⇒ 'a set"
(* not worked out how to prove this yet *)
sorry

end

------8<--------

view this post on Zulip Email Gateway (Aug 19 2022 at 09:40):

From: Ondřej Kunčar <kuncar@in.tum.de>
You might want to take a look to ~~/src/HOL/Quotient_Examples/Lift_DList
and ~~/src/HOL/Quotient_Examples/Lift_FSet.

You can find two operations using nested types there
concat :: "'a dlist dlist => 'a dlist (it uses typedef)
fconcat :: "'a fset fset => 'a fset" (it uses quotient)
and also corresponding proofs.

I think the example with 'a dlist is more suitable for what you are
doing in your formalization because 'a dlist is defined as a typedef.

Ondrej

view this post on Zulip Email Gateway (Aug 19 2022 at 09:40):

From: John Wickerson <jpw48@cam.ac.uk>
Thanks again, Ondrej.

I have one further question on this topic, which can be summarised as "How can I make the transfer method work properly inside a context?".

In more detail: suppose I'm working inside a context that gives me the assumption "P f" for some fixed f. I write a lemma involving f, and begin the proof by applying the transfer method. The transfer method generalises f, and thus loses the fact that P holds for it.

I find that I can survive, just about, by inserting "P f" before applying the transfer method. But this feels rather unscalable.

All of this is explained in further detail in the following theory file.

Best wishes,
John

---------8<----------

theory Scratch imports
Main
"~~/src/HOL/Library/Quotient_Set"
begin

locale always_true =
fixes f :: "'a ⇒ bool"
assumes always_true: "f x = True"
begin end

typedef 'a fset = "{A :: 'a set . finite A }"
by (rule exI[of _ "{}"], auto)

setup_lifting type_definition_fset

lift_definition
fset_member :: "'a ⇒ 'a fset ⇒ bool" (infix "|∈|" 50)
is "op ∈" by simp

context always_true begin

lemma "a |∈| A ⟹ f a"
apply transfer
oops

lemma "a |∈| A ⟹ f a"
apply (insert always_true)
apply transfer
apply auto
done

end

end

---------8<----------

view this post on Zulip Email Gateway (Aug 19 2022 at 09:40):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi John,

With the option fixing, you can tell transfer not to generalize certain
variables:

apply(transfer fixing: f)

Hope this helps,
Andreas

view this post on Zulip Email Gateway (Aug 19 2022 at 09:40):

From: Ondřej Kunčar <kuncar@in.tum.de>
Just citing from The Isabelle/Isar Reference Manual:
Goals are generalized over all free variables by default; this is
necessary for variables whose types change, but can be overridden for
specific variables with e.g. transfer fixing: x y z.

Ondrej

view this post on Zulip Email Gateway (Aug 19 2022 at 09:41):

From: Makarius <makarius@sketis.net>
I've occasionally seen this from a distance, but did not look more closely
(and right now I am also busy with the Isabelle2013 release).

Historically, the treatment of Free variables as arbitrary might stem from
the original HOL4 version of the quotient mechanism by Peter Homeier, when
it was ported to Isabelle/HOL for the first time. But Isabelle has a
clear notion of "fixed variable" within a context, which act as local
constants by default. So the above exception declaration via "fixing"
looks more like a hot fix.

A more standard way in Isabelle is to leave things as fixed as they are
already in the context, unless the users says differenly by augmenting the
"eigen context" of some language element. The "ind_cases" proof method is
an example for that, it uses the "for" syntax for that. (The same "for"
notation helped out in many conceptually difficult situations in locale
expressions some years ago.)

Makarius


Last updated: Mar 29 2024 at 08:18 UTC