Email Gateway (Aug 22 2022 at 20:51): Email Gateway (Aug 22 2022 at 20:51):From: Makarius <makarius@sketis.net>
On 29/11/2019 13:51, Yakoub Nemouchi wrote:
What I tried to point out in the the other topic thread is the following:
Isabelle= Functional programming + HOL + PIDE (including PIDE document
model and PIDE protcol)
Of course PIDE is part of the core Isabelle concepts, and you always need to
be open for further inclusions. Thus you better say "Isabelle = A + B + C +
..." with the literal dots.
What I am saying in the other thread is: It is odd that in the same proof
context we have the same visual semantics, ie. the blue color, to a free
variable with two different types!My question on how relaxed or restricted Isabelle system is! Hides the
following: Is it the case that PIDE visual semantics which decides about
the kind of Isabelle's type system at the very end?
Isabelle is both relaxed and restricted in many ways. Sometimes too relaxed
and/or too restricted, which can lead to confusing situations. PIDE provides
extra visual clues to sort this out, but it is also approximative.
To return to the initial question: here is a perfectly normal Isar proof text
where a locally fixed variable occurs with different types.
theory Scratch
imports Main
begin
notepad
begin
fix x
{ have "(x::nat) = x" .. }
moreover
{ have "(x::int) = x" .. }
ultimately have True
apply - ML_val ‹Thm.add_frees (#goal @{Isar.goal}) []›
apply (rule TrueI)
done
end
end
The ML snippet is merely for illustration: it shows how proper tool
implementations work with variables, such they don't break down just because
this legal but unusual situation happens: the two occurrences of x are distinct.
(Side remark: I keep ignoring the anonymous dummy, so I can't say about the
other thread.)
Makarius
Email Gateway (Aug 22 2022 at 21:03):From: Yakoub Nemouchi <y.nemouchi@gmail.com>
Dear list,
I ended up with a free variable X with two different types within the same
proof goal:
For example:
F (X:::: ('d, 'c) my_type)==> G (X:: ('b, 'a) my_type)
Is that an expected type inference behavior from Isabelle?
Best wishes,
Yakoub.
Email Gateway (Aug 22 2022 at 21:03):From: Peter Lammich <lammich@in.tum.de>
Hi Yakoub,
while this is legal in the (low-level) kernel (vars are identified by
name AND type), it's definitely going to cause some trouble in higher
level tools. I don't think this is intended to happen (unless you have
done something really odd on ML-level).
Can you give a (small) example how to produce this goal?
Email Gateway (Aug 22 2022 at 21:03):From: Makarius <makarius@sketis.net>
In principle, the observation is correct, but the spin is too strong
towards a genuine problem.
Variables with the same name and different types are normal, they can
occur occasionally and most tools should be able to cope with them.
In practice such situations are very rare, so one could get the
impression that this should not happen at all.
BTW "The ML-level of Isabelle" was discontinued approx. 20 years ago; it
is time to get rid of this misleading terminology.
Makarius
Email Gateway (Aug 22 2022 at 21:03):From: Yakoub Nemouchi <y.nemouchi@gmail.com>
Hi Peter,
I think your observation is correct. It is a high level tool, ie. Eisbach,
which helped me to reveal this odd type inference.
At the very end it is my Eisbach script which did something odd. however it
is odd that Isabelle did not deny this odd type inference and allowed it to
happen.
Can you give a (small) example how to produce this goal?
The main idea is to automate splitting rules using an Eisbach script, for
example:
lemma X_SPLIT:
assumes "Q (X)"
obtains Y where X = P (Y)
proof<>
My Eisbach script looks like the following:
SCRIPT 1: ((match conclusion in ‹my_pattern_matching (X) for X ⇒
‹succeed›), rule ACTION_SPLITTER[where X=X])
This caused the problem, since the X after the Eisbach "sequential
composition" is not anymore the one bounded by the "for".
The correction was :
SCRIPT 2: ((match conclusion in ‹my_pattern_matching (X) for X ⇒ ‹rule
ACTION_SPLITTER[where X=X]›))
When using SCRIPT 2 the odd type inference does not happen.
Now the remaining questions are:
Is it the responsibility of Isabelle to deny such a type inference?
Are bounded variables with "for" within an Eisbach script have a larger
scope than the expected one?
Best wishes,
Yakoub
Email Gateway (Aug 22 2022 at 21:03):From: Yakoub Nemouchi <y.nemouchi@gmail.com>
Hi Makarius,
I think your comment is correct in the sense that it is a high level tool,
ie Eisbach, which does not cope with this!
However, this use case reveals an interesting question:
How much is restricted or how much is relaxed Isabelle's type system?
As an active member of this thread I already know your opinion which is
"Isabelle is not HOL nor HOL4. So things in Isabelle may behave
slightly differently."
I admit that I do not have a strong background in type inference, however,
just using my intuition, this use case reveals an odd type inference to me.
I will leave type inference experts to comment on that.
Best wishes,
Yakoub.
Email Gateway (Aug 22 2022 at 21:03):From: Yakoub Nemouchi <y.nemouchi@gmail.com>
Sorry, any occurrence of ACTION_SPLITTER should be replaced by X_SPLIT
within SCRIPT 1 and SCRIPT 2.
Email Gateway (Aug 22 2022 at 21:03):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear Yakoub Nemouchi/All,
I would like to mention that I started a similar thread (but with a
slightly different context) several months ago:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-July/msg00066.html.
The thread had three follow-ups.
Thank you
Email Gateway (Aug 22 2022 at 21:03):From: Yakoub Nemouchi <y.nemouchi@gmail.com>
Hi,
Thank you for the pointer. Indeed, it is related.
What I tried to point out in the the other topic thread is the following:
Isabelle= Functional programming + HOL + PIDE (including PIDE document
model and PIDE protcol)
After using Isabelle for the several years I came to the conclusion that
PIDE is not just a feature it is a part of Isabelle's logic anyways.
I know that some people will think that it is crazy, but this is the
reality in some sens. PIDE actually add a visual semantics that helps
Isabelle users to understand better their logical formulas.
The users get very hooked to this visual semantics, Blue variable, Dark
Blue variables, Green variables, Orange variables, etc...
What I am saying in the other thread is: It is odd that in the same proof
context we have the same visual semantics, ie. the blue color, to a free
variable with two different types!
My question on how relaxed or restricted Isabelle system is! Hides the
following: Is it the case that PIDE visual semantics which decides about
the kind of Isabelle's type system at the very end?
Best wishes,
Yakoub.
Email Gateway (Aug 22 2022 at 21:04):From: Makarius <makarius@sketis.net>
This thread is still pending. Can you please post a self-contained example
with Eisbach where the unexpected behaviour happens?
I would like to see if this is really just unexpected to end-users or if
Eisbach (or one of its supporting proof methods) treats variables with the
same name but different types incorrectly.
Makarius
Email Gateway (Aug 22 2022 at 21:05):From: Yakoub Nemouchi <y.nemouchi@gmail.com>
Hi Makrius,
You can see the example in the sequel. In SCRIPT 1 there are: a red X and a
blue X.
In SCRIPT 1, the blue X is fixed with the Eisbach keyword "for". The red X
is not fixed.
For this reason the application of SCRIPT 1 on a proof context, that have
the same pattern matching in the conclusion, leads to 2 variables with
same name and different types.
The application of SCRIPT 2 on a proof context, that have the same pattern
matching in the conclusion, leads to the expected behavior since the X
fixed by "for" is the same used by the rule.
It looks like that on Eisbach level the red X and the blue X have the same
visual semantics, ie. they are both blue.
Therefore, a user can easily think it is the same variable. Especially if
the Eisbach script is a bit long and complicated.
Namely, Either Eisbach brakes PIDE feature, which usually add a visual
semantics to distinguish both variable in the document model,
or the visual semantics added by PIDE uses a color that a human eye can not
capture easily.
(I do not know why this topic thread was divided to two bits, which
confused me. I do not know where to reply.
I will reply to your example you provided in the other bit of this topic
thread. I have a suggestion for PIDE that I will share with you.)
Eample*
lemma X_SPLIT:
assumes "Q (X)"
obtains Y where X = P (Y)
proof<>
My Eisbach script looks like the following:
SCRIPT 1: ((match conclusion in ‹my_pattern_matching (X) for X ⇒
‹succeed›), rule X_SPLIT[where X=X])
This caused the problem, since the X after the Eisbach "sequential
composition" is not anymore the one bounded by the "for".
The correction was :
SCRIPT 2: ((match conclusion in ‹my_pattern_matching (X) for X ⇒ ‹rule
X_SPLIT[where X=X]›))
Best wishes,
Yakoub.
Email Gateway (Aug 22 2022 at 21:05):From: Makarius <makarius@sketis.net>
I have difficulties to assemble this into a working example, and after trying
long enough it is likely to be something else than your application.
Can you produce a full .thy file where such a situation that you describe happens?
Makarius
Email Gateway (Aug 22 2022 at 21:05):From: Yakoub Nemouchi <y.nemouchi@gmail.com>
Hi Makarius,
Attached is the .thy file.
Best wishes,
Yakoub
Scratch.thy
Email Gateway (Aug 22 2022 at 21:06):From: Yakoub Nemouchi <y.nemouchi@gmail.com>
If the two occurrences of X are distinct then the pretty printer should add
a visual semantics to distinguish them.
But adding such a visual semantics will end with the following question:
+
Blue is for free variables.
Green is for bounded variables.
Orange is for fixed variables.
?DarkBlue is for meta variables.
the new visual semantics is for what? Namely, what is the mapping of this
situation in the logic.
Best wishes,
Yakoub.
Email Gateway (Aug 22 2022 at 21:13):From: Yakoub Nemouchi <y.nemouchi@gmail.com>
Hi list,
This topic is still pending!
Yakoub,
Email Gateway (Aug 22 2022 at 21:14):From: Yakoub Nemouchi <y.nemouchi@gmail.com>
Hi list,
This topic is still pending too!
Yakoub.
Last updated: Apr 24 2024 at 12:33 UTC