Email Gateway (Aug 19 2022 at 13:46): Email Gateway (Aug 19 2022 at 13:46):From: Gottfried Barrow <igbi@gmx.com>
No one cares I'm sure, but, for closure, I didn't put in the condition
that the elements be in NNeg, where I guess I should have used P instead
of NNeg.
Email Gateway (Aug 19 2022 at 13:46):From: Gottfried Barrow <igbi@gmx.com>
I'm no expert on algebra, and the number of classes in Groups and Rings
is dizzying, but I guess I would try to put these typedef
positive/non-negative types lower down. I don't know any of the
ramifications of these types, other than the operations need to be closed.
typedef 'a ordered_ab_group_add_NN = "{x::'a::ordered_ab_group_add. x >=
0}"
by(auto)
typedef 'a ordered_ring_NN = "{x::'a::ordered_ring. x >= 0}"
by(auto)
typedef 'a linordered_idom_Pos = "{x::'a::linordered_idom. x > 0}"
proof-
have "1 : {x::'a. 0 < x}" by(auto) thus ?thesis by(blast) qed
So I wanted to do a little test to see if -(-1) would be of these
types, because experimenting with that might tell me if this is a loser
idea. I couldn't do that without doing the required lifting.
That's why I don't try to implement any this by myself right now. It's
because when I look at something like fset, I see that a lot of work
went into making it work.
Also, if I was proving theorems about x::nat when it gets coerced to
int, I don't know if that's the same thing as proving theorems about
(x::int) >= 0. I would want to know if I was getting locked into
something.
But, a type for the positive and non-negative members of a group or ring
could also be used in datatypes.
Regards,
GB
Email Gateway (Aug 19 2022 at 13:46):From: Gottfried Barrow <igbi@gmx.com>
(*NOTE: The "exception TYPE raised" error shown below might be of
interest to someone.)
The value of trying to get fancy can be the tangents. The
setup_lifting command works if typedef uses type rat, but not if
typedef uses 'a::linordered_idom. It has nothing specifically to do
with linordered_idom. A test case I made using 'a::finite does the
same thing.
So with a typedef based on rat, I can start down the lifting road:
typedef ratN = "{x::rat. x >= 0}"
by(auto)
declare [[coercion Rep_ratN]]
setup_lifting type_definition_ratN
instantiation ratN :: zero
begin
lift_definition zero_ratN :: ratN is "0::rat" ..
instance ..
end
theorem "(0::ratN) + x = (x::rat)"
by(transfer, simp)
But, if I want to use 'a::linordered_idom, I have to do it the
non-lifting, definitional way, because of the "exception TYPE raised"
error shown below:
typedef 'a loidN = "{x::('a::linordered_idom). x >= 0}"
by(auto)
declare Abs_loidN_inverse [simp add]
setup_lifting type_definition_loidN
(*
exception TYPE raised (line 246 of "term.ML"):
dest_Type
'f::linordered_idom
*)
instantiation loidN :: (linordered_idom) zero
begin
definition zero_loidN :: "'a loidN" where
"0 = Abs_loidN 0"
declare zero_loidN_def [simp add]
instance ..
end
theorem "Rep_loidN(0::'a loidN) + x = (x::'a::linordered_idom)"
by(simp)
Regards,
GB
Email Gateway (Aug 19 2022 at 13:46):From: Ondřej Kunčar <kuncar@in.tum.de>
For example me. Your type definition uses as a raw type a type variable.
The new code in lifting that deals with parametricity assumes that the
raw type is always a type constructor. I'll take a look at it.
Ondrej
Email Gateway (Aug 19 2022 at 13:47):From: Gottfried Barrow <igbi@gmx.com>
Ondrej,
Thanks. I use 'a::linordered_idom option as a workaround, as shown below.
NOTE for anyone: I can't get subtype coercion in the Rep direction, as
show below. If someone can tell me whether I can or can't do that, I'd
appreciate it.
typedef ('a::linordered_idom) loidOpt = "{x::'a option. x ~= None & the
x >= 0}"
by(auto)
(* The Rep declares don't return an error, but have no affect on
coercions. *)
(*
declare [[coercion Rep_loidOpt]]
declare [[coercion "Rep_loidOpt::rat loidOpt => rat option"]]
term "(x::rat loidOpt) = Some (y::rat)"
*)
(Going the Abs direction works, but it's not the subtyping I need.)
declare [[coercion Abs_loidOpt]]
term "(x::rat loidOpt) = Some (y::rat)"
term "(x::'a::linordered_idom loidOpt) = Some (y::'a::linordered_idom)"
(I tried messing with coercion_map, but it didn't help.)
fun MAPloidOpt :: "('a::linordered_idom => 'b::linordered_idom) => 'a
loidOpt => 'b loidOpt" where
"MAPloidOpt f q = Abs_loidOpt(Some(f (the(Rep_loidOpt q))))"
declare [[coercion_map MAPloidOpt]]
Email Gateway (Aug 19 2022 at 13:47):From: Dmitriy Traytel <traytel@in.tum.de>
Am 10.02.2014 14:38, schrieb Gottfried Barrow:
On 2/9/2014 4:40 PM, Ondřej Kunčar wrote:
On 02/09/2014 05:28 PM, Gottfried Barrow wrote:
(*NOTE: The "exception TYPE raised" error shown below might be of
interest to someone.)For example me. Your type definition uses as a raw type a type
variable. The new code in lifting that deals with parametricity
assumes that the raw type is always a type constructor. I'll take a
look at it.Ondrej,
Thanks. I use
'a::linordered_idom optionas a workaround, as shown
below.NOTE for anyone: I can't get subtype coercion in the Rep direction, as
show below. If someone can tell me whether I can or can't do that, I'd
appreciate it.
Hi Gottfried,
there are two different algorithms in charge of inserting coercions:
(1) A complete (=if a term can be coerced it will be coerced) for
structural subtyping (a.k.a. global coercion insertion in error
messages), where only coercions between base types (i.e., nullary type
constructors such as nat, int, real) are allowed. Map functions are used
to lift those coercions between base types to more complex types (e.g,
nat list or int option). In this "structural" setting, there might be a
coercion from "nat list" to "int list" (given a coercion from nat to int
and a map function for list), but never a coercion from "nat list" to
"int option".
(2) An incomplete (Coq-style) algorithm for non-structual coercions
(e.g. one from "nat list" to "int option"). This is called local
coercion insertion in error messages.
typedef ('a::linordered_idom) loidOpt = "{x::'a option. x ~= None &
the x >= 0}"
by(auto)(* The Rep declares don't return an error, but have no affect on
coercions. *)
(*
declare [[coercion Rep_loidOpt]]
declare [[coercion "Rep_loidOpt::rat loidOpt => rat option"]]term "(x::rat loidOpt) = Some (y::rat)"
*)
This is out of scope for (1). The incompleteness of (2) is visible on
your example, which only will not insert coercions in the first argument
of equality (and of other polymorphic functions). It would have worked
if you had reversed the equation:
term " Some (y::rat) = (x::rat loidOpt)"
Dmitriy
Email Gateway (Aug 19 2022 at 13:48):From: Gottfried Barrow <igbi@gmx.com>
Dmitriy
Thanks. It's fortunate I didn't switch the order, or in the future it
could have been, "I thought I remember that this worked."
If Ondrej accommodates, the problem I show next won't be an issue, but
below, I show how I can coerce to rat, but not to 'a::linordered_idom.
And thanks for the explanation. Guessing here, from what you said and
what Ondrej said, the error below is because the coercion needs a type
constructor, and 'a::linordered_idom is only a type variable.
Are there such things as 0-ary type constructor variables, that I can
put in place of 'a? With show_sorts, I never see the type/sort of
nat or int.
(source with error)
typedef ('a::linordered_idom) loidOpt = "{x::'a option. x ~= None & the
x >= 0}"
by(auto)
declare [[coercion Rep_loidOpt]]
definition the_Rep_loidOpt :: "'a::linordered_idom loidOpt => 'a" where
"the_Rep_loidOpt x = the(Rep_loidOpt x)"
declare [[coercion "the_Rep_loidOpt::rat loidOpt => rat"]]
term "(y::rat) = (x::rat loidOpt)"
declare [[coercion the_Rep_loidOpt]]
(*
Bad type for a coercion:
the_Rep_loidOpt :: ?'a::linordered_idom loidOpt => ?'a::linordered_idom
*)
Thanks again,
GB
Email Gateway (Aug 19 2022 at 13:48):From: Dmitriy Traytel <traytel@in.tum.de>
Am 10.02.2014 17:27, schrieb Gottfried Barrow:
On 2/10/2014 8:15 AM, Dmitriy Traytel wrote:
This is out of scope for (1). The incompleteness of (2) is visible on
your example, which only will not insert coercions in the first
argument of equality (and of other polymorphic functions). It would
have worked if you had reversed the equation:term " Some (y::rat) = (x::rat loidOpt)"
DmitriyThanks. It's fortunate I didn't switch the order, or in the future it
could have been, "I thought I remember that this worked."If Ondrej accommodates, the problem I show next won't be an issue, but
below, I show how I can coerce torat, but not to
'a::linordered_idom.And thanks for the explanation. Guessing here, from what you said and
what Ondrej said, the error below is because the coercion needs a type
constructor, and'a::linordered_idomis only a type variable.
Exactly. In principle this could be supported in the incomplete
algorithm (2), but it isn't yet (and I will not promise anything ;-) ).
Are there such things as 0-ary type constructor variables, that I can
put in place of'a? Withshow_sorts, I never see the type/sort of
natorint.
There is no such thing.
Dmitriy
Email Gateway (Aug 19 2022 at 13:49):From: Ondřej Kunčar <kuncar@in.tum.de>
The problem is addressed in 6ea67a791108.
Just a side note: I am not sure if linordered_idom is the best choice
because I fear you cannot prove that your type 'a loidN is again in
linordered_idom (usual problems with minus). Which I believe, you would
like to do.
Best,
Ondrej
Email Gateway (Aug 19 2022 at 13:50):From: Gottfried Barrow <igbi@gmx.com>
Ondrej,
Thanks a lot. I'll have to wait for summertime. Fortunately, it took
you, like, two days, instead of one. Otherwise, I might not have learned
about Lifting_Option.thy, and using it as a template for the lifting
setup I did.
I can get confused by the complexities of type classes, coercion, and
the many algebra type classes, but the context is a generalization of this:
(1) one function,
(2) the type variable sort must have the properties of int
(linordered_idom),
(3) but the function must work with nat, even though nat does not have
the required properties of linordered_idom.
The short story, according to what I currently understand, is that
coercion is the magic for there to be that one function, and auto
coercion is the magic to make it notationally convenient.
There's more I don't know than do know, but I worked up the example
below to show what I think I know, about what I think I want. Thanks
again for the magic. --GB.
(******************)
(* id_loid: It must work with nat and int, and generalizations of nat
and int.*)
(******************)
definition id_loid :: "'a::linordered_idom => 'a" where
"id_loid x = x"
(******************)
(* Works with nat, int, and linordered_idom, but not with
linordered_semidom.*)
(******************)
value "id_loid (x::int)" (x::int)
value "id_loid (x::nat)" (coerced to int)
value "id_loid (x::'a::linordered_idom)" (x::'a::linordered_idom)
term "id_loid (x::'a::linordered_semidom)"
(*
ERROR: Type unification failed: Variable 'a::linordered_semidom not of sort
linordered_idom
*)
(******************)
(* As nat is to int, loidNNeg is to linordered_idom. Coercion is the
magic.*)
(******************)
typedef 'a loidNNeg = "{x::'a::linordered_idom. x >= 0}"
by(auto)
term "id_loid (Rep_loidNNeg(x::'a::linordered_idom loidNNeg))"
value "id_loid (Rep_loidNNeg(x::'a::linordered_idom loidNNeg))"
(******************)
(*My subtype is supposed to model the natural numbers, so I try to
narrow down
the sort of the type class variable to linordered_semidom, and then
use it
in the function id_loid, but it doesn't work.*)
(******************)
typedef 'a losdNNeg = "{x::'a::linordered_semidom. x >= 0}"
by(auto)
term "id_loid (Rep_losdNNeg(x::'a::linordered_semidom losdNNeg))"
(*
ERROR: Type unification failed: Variable 'a::linordered_semidom not of sort
linordered_idom
*)
(******************)
(*It didn't work, so whatever I'm confused about, it's not that. I want
to check
that linordered_semidom accomodates nat. I can't depend on a type error
to know when I've exceed the properties of nat, because it will get
coerced to
int when I do. I have to look at the output panel to see if it got
coerced with
value.
It looks like linordered_semidom may be the maximum properties.*)
(******************)
definition id_losr :: "'a::linordered_semidom => 'a" where
"id_losr x = x"
term "id_losr (x::nat)" (x::nat)
value "id_losr (x::nat)" (x::nat)
(******************)
(*Well, okay, I don't let the lack of knowledge keep me from blindly
trying to
do things, because the magic kicks in many times. Am I making things too
complex? I don't know. If I start with linordered_semidom, there has to
be some
kind of coercion function, but I can't use the same x on both sides, as
below.*)
(******************)
definition losd_to_loid :: "'a::linordered_semidom =>
'b::linordered_idom option" where
"losd_to_loid x = Some x"
(******************)
(*
The thing for me to pursue is whether I can define any of these typedefs
in the
context of the type class linordered_idom.
Thanks to explanations by Andreas Lochbihler about locales, I was
sorting out
the difference between global and locale polymorhpic functions, and how the
inference engine will interpret the sort of any type variable as broadly as
possible. That can result in a 'b variable appearing in a type class
context,
when a global function is used.
Yes, there are many thing to confuse a Pure novice, and a HOL novice,
too. But
error messages can be educational, such as that a type class variable name
must be 'a, which is related to the fact that type classes can only have one
type variable, and related to what I said in the last paragraph.
class tester =
fixes tester :: 'b
Error: No type variable other than 'a allowed in class specification
*)
(******************)
(*
Now, I try to define the typedef in a linordered_idom context.
*)
context linordered_idom
begin
typedef 'a loidNNeg = "{x::'a::linordered_idom. x >= 0}"
end
(*
ERROR: Sort constraint linordered_idom inconsistent with default type
for type
variable "'a". The error(s) above occurred in typedef "loidNNeg"
*)
(*
The Wizard is talking to me. What is the Wizard saying? I suppose he's
saying
something similar to what Andreas Lochbihler was trying to tell me
months ago.
That the linordered_idom type variable sort has been specified broadly, as
'a::type, and here I am trying to put restrictions on it.
There is value in being able to experiment with software, except when the
software is running on the primary server of a large, worldwide
corporation.
*)
Email Gateway (Aug 19 2022 at 13:50):From: Gottfried Barrow <igbi@gmx.com>
To work with the repository, I was thinking I'd have to do something
complex, but then I just downloaded the 2 changeset files and built the
image. Also, thanks for the heads up on minus causing problems. That
may not be applicable here, but I'm sure it'll come up in the future.
Dude expressions are applicable, and possibly Fabian Cancellera
analogies, or maybe not, as I tend to confuse Czechoslovakia with the
Swiss domain .ch, but we can say that the power of the lifting package
can be compared to the size of André Greipel's thighs. As to the speed
with which I instantiated my type as linordered_semidom, we can say
that is comparable to the speed of Marcel Kittel.
There actually would have been a big snag, except for a recent tip by
Andreas Lochbihler, to not use ==> in a structured proof, but to use
assume. A proof goal was going all crazy when I would prove the step
using ==>.
The numeral type class is also important, by Florain Haftmann and Brian
Huffman. I haven't figured it out yet, but I know not to let my simp
rules interfere with letting it do its job.
Having a set of constants for a number system is a big reason why one
traditionally has to resort to using integers, rational numbers, and
real numbers. It's rather radical to have a set of constants, the
numerals, that are both abstract, due to polymorphism, but yet can be
used concretely. If I never have to use the real numbers or rational
numbers, because I can figure out how to get by with the numerals,
that'll be fine with me.
Regards,
GB
Last updated: Apr 24 2024 at 20:16 UTC