Email Gateway (Aug 19 2022 at 11:58): Email Gateway (Aug 19 2022 at 11:58):From: Christoph LANGE <math.semantic.web@gmail.com>
Dear Isabelle power-users or developers,
I have made a very strange observation about reasoning with transitive
chains.
In
https://github.com/formare/auctions/tree/master/isabelle/Auction/Sandbox
you can find some "minimal" examples in Chain_Bug_*.thy. OK, I could
have stripped them down to an even more minimal form, but instead I
chose to provide the Chain_Bug_*.diff files, which point out the minimal
differences between the different *.thy files.
The problem is that I have a chain
have "X = Y" sorry
also have "Y = Z" sorry
finally have "X = Z" .
Y internally involves parameterised types – I'm not sure of the
terminology, but I mean something like "'a set". If I choose not to
make these types explicit I get a warning "Introduced fixed type
variable(s)" (see Chain_Bug_3_warn.thy), but otherwise everything works
fine. I don't have a type theory background but kind of
intuitively/superficially understand this warning. But is it a bad
thing not to provide explicit type annotations in such a situation?
When I add type annotations inside Y (to arrive at
Chain_Bug_4_fails.thy), I somehow manage to break the transitive chain,
as pointed out by Chain_Bug_adding_type_annotation_breaks_it.diff.
I can, however, use the same reasoning structure outside of a proof, in
a notepad that seems to have the same context. Chain_Bug_2_works.thy
shows such a notepad;
Chain_Bug_putting_into_lemma_context_breaks_it.diff points out the
difference from Chain_Bug_4_fails.thy.
Whether I put the structure into a lemma, or use it to justify a proof
step, makes, as expected, no difference. Chain_Bug_1_fails shows the
same thing in a proof step; Chain_Bug_using_for_proof_breaks_it.diff
shows the difference from Chain_Bug_2_works.thy, where the structure
occurs on top level.
I will for now omit the type annotations and ignore the warning, but I
would be happier if I understood what's wrong.
Cheers, and thanks in advance,
Christoph
Email Gateway (Aug 19 2022 at 11:58):From: Manuel Eberl <eberlm@in.tum.de>
On 09/07/2013 05:21 PM, Christoph LANGE wrote:
Y internally involves parameterised types – I'm not sure of the
terminology, but I mean something like "'a set".
This is called polymorphism, and it is indeed the cause of your problem
here. Isabelle uses a somewhat restricted form of polymorphism based on
schematic types variables, if I remember correctly, and that can
sometimes lead to some headaches.
My personal motto in matters such as these is: When in doubt, annotate
everything with type variables.
To illustrate, you can switch on unification tracing. Unification is, in
the context of types, the process of finding instantiations for type
variables so that one type matches another and tracing it can give you
more information about type errors such as this one. In your case, in
the last step, where you do
finally show "{{} = injections {} Y" .
the unification trace says
The following types do not unify:
('a × 'b) set set ⇒ ('a × 'b) set set ⇒ bool
('c × 'b) set set ⇒ ('c × 'b) set set ⇒ bool
The first line is the type of your calculation. The second line is the
type of your goal. If my interpretation of this output is correct,
Isabelle has introduced a new, fresh type variable 'c for the left-hand
part of your relation instead of the existing 'a. You need to force it
to use the existing 'a, by writing, for example:
finally show "{{} :: ('a×'b) set} = injections {} Y" .
…and it works.
About this warning, the warning is of a similar kind, I think it is not
prudent to ignore it in most cases. It means that you have a variable
with a polymorphic type that cannot be determined automatically, so
Isabelle will use some fresh type variable for the schematic type
variables in it. This can lead to problems, especially when you have
several of these variables in the same context and they depend on one
another in some fashion, for instance:
notepad
begin
fix A and B assume "A = {}" and "B = {}"
have "A = B"
end
This leads to a type error, because A is assigned the type 'a set and B
is assigned the type 'b set, because Isabelle cannot, from the
assumptions, determine that A and B must have the same type – indeed,
they don't have to – so it gives them two different types, which is more
general. In this case, we would have to fix both A and B to the type 'a
set, and then everything would work. And this is precisely the reason
why we get the warning:
Cheers,
Manuel
When I add type annotations inside Y (to arrive at
Chain_Bug_4_fails.thy), I somehow manage to break the transitive chain,
as pointed out by Chain_Bug_adding_type_annotation_breaks_it.diff.I can, however, use the same reasoning structure outside of a proof, in
a notepad that seems to have the same context. Chain_Bug_2_works.thy
shows such a notepad;
Chain_Bug_putting_into_lemma_context_breaks_it.diff points out the
difference from Chain_Bug_4_fails.thy.Whether I put the structure into a lemma, or use it to justify a proof
step, makes, as expected, no difference. Chain_Bug_1_fails shows the
same thing in a proof step; Chain_Bug_using_for_proof_breaks_it.diff
shows the difference from Chain_Bug_2_works.thy, where the structure
occurs on top level.I will for now omit the type annotations and ignore the warning, but I
would be happier if I understood what's wrong.Cheers, and thanks in advance,
Christoph
Email Gateway (Aug 19 2022 at 11:58):From: Lars Noschinski <noschinl@in.tum.de>
If you get this warning, it does not mean per se that you are doing something wrong. It is just that introducing new toe variables often means that the proposition you are stating is not what you intended (it often occurs if you fix some variables and than five some statement about these variables, which don't constrain the type to one occurring already in your lemma).
Christoph LANGE <math.semantic.web@gmail.com> schrieb:
Email Gateway (Aug 19 2022 at 11:58):From: Christoph LANGE <math.semantic.web@gmail.com>
2013-09-07 18:04 Manuel Eberl:
My personal motto in matters such as these is: When in doubt, annotate
everything with type variables.
OK, thanks, I figured out a way of doing this. I had to make a few mroe
explicit annotations, at the top level of the proof of which I wanted to
prove one step by the transitive chain I mentioned.
To illustrate, you can switch on unification tracing.
I don't know how to do this in jEdit. Does the conclusion of this
thread
(https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-June/thread.html)
still hold, i.e. that it is not possible in jEdit?
Cheers,
Christoph
Email Gateway (Aug 19 2022 at 11:59):From: Lars Noschinski <noschinl@in.tum.de>
You can switch on unification traces via some ML command:
ML {* trace_unify_fail:= true*}
However, you need to be aware that this is a global setting, I.e. it affects the whole Isabelle session, not just the commands coming after it. You need to switch it off explicitly by seeing the value to false again.
Christoph LANGE <math.semantic.web@gmail.com> schrieb:
Last updated: Apr 24 2024 at 12:33 UTC