Email Gateway (Aug 19 2022 at 08:18): Email Gateway (Aug 19 2022 at 08:18):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Hi all,
I must miss something obvious, I can't get a simple sample class
instatiation working, and that's many hours I try to guess, but failed,
thus this message.
Here is the sample:
class cls1 =
fixes
cls1_x :: "'a" and
cls1_f :: "'a ⇒ 'a" and
cls1_g :: "nat ⇒ 'a"
assumes
cls1_fg_prop: "(cls1_f (cls1_g 0)) = (cls1_g 0)"
fun f :: "int ⇒ int" where
"f i = i"
fun g :: "nat ⇒ int" where
"g n = (int n)"
instantiation int :: cls1
begin
definition df: "cls1_f n = f n"
definition dg: "cls1_g n = g n"
instance proof
have "cls1_f 0 = f 0" unfolding df by simp -- #1
have "cls1_g 0 = g 0" unfolding dg by simp -- #2
have "f (g 0) = g 0" by simp -- #3
then show "cls1_f (cls1_g 0) = cls1_g 0" -- #4
unfolding df and dg by simp
qed
end
Cls1 is just for testing, it does not pretend to be useful in any way. F
and g, are supposed to play the role of cls1_f and cls1_g, respectively.
In the instantiation, putting the cursor on Show, which is underlined in
red, Isabelle insist on complaining:
Local statement will fail to refine any pending goal
Failed attempt to solve goal by exported rule:
cls1_f (cls1_g 0) = cls1_g 0
However, putting the cursor right after Instance Proof, Isabelle says:
proof (state): step 1
goal (1 subgoal):
1. cls1_f (cls1_g 0) = cls1_g 0
… which is exactly what's in the expression to be shown.
Line #1 and #2 are for testing, after this failure, and both are OK.
Hovering the cursor above cls1_f and cls1_g in line #1 and #2, says they
are cls1_class.cls1_f and cls1_class.cls1_g, which makes Isabelle's
complains even less clear to me.
Line #3 is OK too.
So what's wrong? Must be obvious, but honestly, I completely miss it.
P.S. By the way, what's the name of the default proof method Isabelle uses
in Instance Proof? Does not seems to be unfold_classes (as there is an
unfold_locales method) or any similar names I've tested.
Email Gateway (Aug 19 2022 at 08:18):From: Lars Noschinski <noschinl@in.tum.de>
I haven't looked at your problem in detail, but this sounds like a type problem. Try "using [show_types]" before the failing proof step. "show_sorts" and "show_consts" might also be useful.
Email Gateway (Aug 19 2022 at 08:19):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Am 14.08.2012 um 05:34 schrieb Lars Noschinski:
I haven't looked at your problem in detail, but this sounds like a type problem. Try "using [show_types]"
Or rather "using [[show_types]]", with two layers of brackets.
before the failing proof step. "show_sorts" and "show_consts" might also be useful.
Jasmin
Email Gateway (Aug 19 2022 at 08:19):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
At least, I've found an answer to this one. That's intro_classes; thus,
“instance proof” do the same as “instance proof intro_classes”.
Email Gateway (Aug 19 2022 at 08:19):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
After Lars Noschinski's suggestion, I added (already posted, but never
shown up in the thread, so I'm re‑posting it)
declare [[show_types]]
declare [[show_consts]]
declare [[show_sorts]]
… before the Instantiation
Moving the cursor after “instance proof”, the Output pan of
jEdit/Isabelle, shows this:
proof (state): step 1
goal (1 subgoal):
1. cls1_f (cls1_g (0∷nat)) = cls1_g (0∷nat)
constants:
TYPE(int) :: int itself
cls1_class :: int itself ⇒ prop
prop :: prop ⇒ prop
0∷nat :: nat
cls1_g :: nat ⇒ int
cls1_f :: int ⇒ int
op = :: int ⇒ int ⇒ bool
Trueprop :: bool ⇒ prop
op ⟹ :: prop ⇒ prop ⇒ prop
Types seems correctly applied/inferred. I attempted to replace
then show "(cls1_f (cls1_g 0)) = (cls1_g 0)"
with
then show "(cls1_f (cls1_g (0::nat))) = (cls1_g (0::nat))"
… but this solved nothing.
At this stage, as I have no idea, I wonder if it's me who is missing
something, or else if my assumption that this should be OK is right, and
so, that this would be an error from Isabelle. This would not be proving
something which is wrong, but failing to allow to prove something which is
right; which in turn is not the worst, but annoying. That doubts are
blocking for me (I can't avoid thinking about this topic).
Email Gateway (Aug 19 2022 at 08:19):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Yannick,
without having really tried, I guess that the type of these definitions
is too general; try something like "cls1_f n = (f n :: int)".
Florian
signature.asc
Email Gateway (Aug 19 2022 at 08:19):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Florian, thanks for your reply,
I tried to add type annotations everywhere I could, which gave:
class cls1 =
fixes
cls1_x :: "'a" and
cls1_f :: "'a ⇒ 'a" and
cls1_g :: "nat ⇒ 'a"
assumes
cls1_fg_prop: "(cls1_f (cls1_g (0::nat))) = (cls1_g (0::nat))"
fun f :: "int ⇒ int" where
"f (i::int) = (i::int)"
fun g :: "nat ⇒ int" where
"g (n::nat) = (int (n::nat))"
declare [[show_types]] -- Testing
declare [[show_consts]] -- Testing
declare [[show_sorts]] -- Testing
instantiation int :: cls1
begin
definition df: "(cls1_f (i::int)) = (f (i::int))"
definition dg: "(cls1_g (n::nat)) = (g (n::nat))"
instance proof
have "(cls1_f (0::int)) = (f (0::int))" using df by simp -- Testing
have "(cls1_g (0::nat)) = (g (0::nat))" using dg by simp -- Testing
have "(f (g (0::nat))) = (g (0::nat))" by simp
then show "(cls1_f (cls1_g (0::nat))) = (cls1_g (0::nat))"
using df and dg by simp
qed
end
The result is the same. May be that's finally a bug, or else don't see why
it can't unify the expression to be shown with the pending goal.
By the way, is there a recommended way to submit bug reports (if that's
really one) about Isabelle?
I wondered if this could be due to the absence of a universal
quantification in the pending goal, but Isabelle is OK with this in other
context, and there's no variables to Fix here. I will try something
similar with a Locale, as a Class has similarities with a Locale, to see
if it ends with the same.
Email Gateway (Aug 19 2022 at 08:19):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
class cls1 =
fixes
cls1_x :: "'a" and
cls1_f :: "'a ⇒ 'a" and
cls1_g :: "nat ⇒ 'a"
assumes
cls1_fg_prop: "(cls1_f (cls1_g (0::nat))) = (cls1_g (0::nat))"
…
then show "(cls1_f (cls1_g (0::nat))) = (cls1_g (0::nat))"
using df and dg by simp
you don't have a type constraint on the result type here, e.g.
then show "(cls1_f (cls1_g (0::nat)) :: int) = (cls1_g (0::nat))"
If this does not help, please boil down your example to something
simpler until it work, and post the last non-working version.
Florian
signature.asc
Email Gateway (Aug 19 2022 at 08:20):From: Makarius <makarius@sketis.net>
On Thu, 16 Aug 2012, Yannick Duchêne (Hibou57) wrote:
I tried to add type annotations everywhere I could, which gave:
class cls1 =
fixes
cls1_x :: "'a" and
cls1_f :: "'a ⇒ 'a" and
cls1_g :: "nat ⇒ 'a"
assumes
cls1_fg_prop: "(cls1_f (cls1_g (0::nat))) = (cls1_g (0::nat))"fun f :: "int ⇒ int" where
"f (i::int) = (i::int)"fun g :: "nat ⇒ int" where
"g (n::nat) = (int (n::nat))"declare [[show_types]] -- Testing
declare [[show_consts]] -- Testing
declare [[show_sorts]] -- Testinginstantiation int :: cls1
begin
definition df: "(cls1_f (i::int)) = (f (i::int))"
definition dg: "(cls1_g (n::nat)) = (g (n::nat))"
instance proof
have "(cls1_f (0::int)) = (f (0::int))" using df by simp -- Testing
have "(cls1_g (0::nat)) = (g (0::nat))" using dg by simp -- Testing
have "(f (g (0::nat))) = (g (0::nat))" by simp
then show "(cls1_f (cls1_g (0::nat))) = (cls1_g (0::nat))"
using df and dg by simp
qed
end
Try this one:
show "(cls1_f (cls1_g (0::nat) :: int)) = (cls1_g (0::nat))"
^^^^^^
The Prover IDE helped to expose the type of cls1_f and cls2_g in the text,
using CTRL/COMMAND hover.
The result is the same. May be that's finally a bug, or else don't see
why it can't unify the expression to be shown with the pending goal.By the way, is there a recommended way to submit bug reports (if that's
really one) about Isabelle?
As a rule of thumb there are hardly any bugs, only unexpected behaviour,
and that is best discussed on the mailing list.
Makarius
Email Gateway (Aug 19 2022 at 08:20):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
On Thu, 16 Aug 2012 16:44:43 +0200, Makarius <makarius@sketis.net> wrote:
Try this one:
show "(cls1_f (cls1_g (0::nat) :: int)) = (cls1_g (0::nat))"
^^^^^^
And yes, this solves the unification! (Makarius is a genius :-P )
Any of this three ones do:
then show "(cls1_f (cls1_g 0)) = ((cls1_g 0) :: int)"
then show "((cls1_f (cls1_g 0)) :: int) = (cls1_g 0)"
then show "(cls1_f ((cls1_g 0) :: int)) = (cls1_g 0)"
The Prover IDE helped to expose the type of cls1_f and cls2_g in the
text,
using CTRL/COMMAND hover.
I often use it, but well, missed that. I did it again, and for cls1_f it
says “'a::cls1 ⇒ 'a::cls1”, and for cls1_f it says “'nat ⇒ 'a::cls1”.
So the type inference did not applied (while I was so much sure it did),
and I have to understand why. What could have been the way to solve the
type inference as I expected it to be? I see only one:
definition df: "(cls1_f i) = (f i)"
definition dg: "(cls1_g n) = (g n)"
May be because that's just definitions? So I tried to replace the above
with:
fun cls1_f :: "int ⇒ int"
where "(cls1_f i) = (f i)"
fun cls1_g :: "nat ⇒ int"
where "(cls1_g n) = (g n)"
Now ctrl/command + mouse‑hovering on cls1_f and cls1_g in:
then show "(cls1_f (cls1_g 0)) = (cls1_g 0)" by simp
… shows type inference applies in this case, as it says “int ⇒ int” and
“nat ⇒ int”. But unification does not works for another reason; it now
complains instead:
Local statement will fail to refine any pending goal
Failed attempt to solve goal by exported rule:
local.cls1_f (local.cls1_g (0∷nat)) = local.cls1_g (0∷nat)
while before it was complaining:
Local statement will fail to refine any pending goal
Failed attempt to solve goal by exported rule:
cls1_f (cls1_g (0∷nat)) = cls1_g (0∷nat)
The difference is the “local.” prefix.
Another attempt with:
abbreviation "(cls1_f i) ≡ (f i)"
abbreviation "(cls1_g n) ≡ (g n)"
… ends into the same similar issue as with Definition, but even worst, as
adding a type annotation does not solve anything now.
Conclusion so far: Definition (and Abbreviation) do not provides hints for
type inference, even if the Definition provides type annotations, and
using fun/function, which provides hints for type inference, is not OK, as
this create a plain new entity (of the same name, but still another
entity), which cannot be unified with the expected one.
These are things to keep in mind about Isar.
Now to come back to an above comment I've made, which is “I often use it,
but well, missed that” (talking about ctrl/command + mouse‑hovering over
an item), may be an idea: show_types/consts/sorts, could still display
something even when there is error to display. The Output pan did not show
anything, as there was an error message instead, which replaced report
messages. If both have been displayed together, may be I won't have missed
it, as what's always displayed is less likely to be missed as I did.
By the way, is there a recommended way to submit bug reports (if that's
really one) about Isabelle?As a rule of thumb there are hardly any bugs, only unexpected behaviour,
I believe the same (thus my doubts), and surprised myself to come to the
bug hypothesis.
and that is best discussed on the mailing list.
OK
Email Gateway (Aug 19 2022 at 08:20):From: Makarius <makarius@sketis.net>
On Thu, 16 Aug 2012, Yannick Duchêne (Hibou57) wrote:
Try this one:
show "(cls1_f (cls1_g (0::nat) :: int)) = (cls1_g (0::nat))"
^^^^^^
Any of this three ones do:then show "(cls1_f (cls1_g 0)) = ((cls1_g 0) :: int)"
then show "((cls1_f (cls1_g 0)) :: int) = (cls1_g 0)"
then show "(cls1_f ((cls1_g 0) :: int)) = (cls1_g 0)"
Yes. In this context the argument type of cls1_g is always nat, so there
is no need for that constraint.
The Prover IDE helped to expose the type of cls1_f and cls2_g in the text,
using CTRL/COMMAND hover.I often use it, but well, missed that. I did it again, and for cls1_f it says
“'a::cls1 ⇒ 'a::cls1”, and for cls1_f it says “'nat ⇒ 'a::cls1”.So the type inference did not applied (while I was so much sure it did),
and I have to understand why.
There is something like a standard portfolio of getting confused with type
inference. I will try harder next time to provide some visual clues in
the Prover IDE markup about such situations, so that errors are easier to
understand, or avoided in the first place.
What could have been the way to solve the type
inference as I expected it to be? I see only one:definition df: "(cls1_f i) = (f i)"
definition dg: "(cls1_g n) = (g n)"May be because that's just definitions? So I tried to replace the above with:
fun cls1_f :: "int ⇒ int"
where "(cls1_f i) = (f i)"fun cls1_g :: "nat ⇒ int"
where "(cls1_g n) = (g n)"
There is no fundamental difference of 'definition' vs. 'fun', only an
accidental one: 'definition' (like 'abbreviation') allows a short form
where the defined entity is not explicitly bound but just mentioned in the
proper place on the LHS of the defining equation. You can call that
feature a bug, but I usually use neither of these meaningless words. It
is just a convenience to write short definitions, even if it can lead to
slightly different situations concerning type-inference.
So what happens here is that
definition df: "(cls1_f i) = (f i)"
refers to a particilar instance of the overloaded constant cls1_f for type
int, because that is special in the instantiation context. The context is
also responsible for exchanging that instance internally with a formal
parameter cls1_f_int that needs to be defined here for the sake of the
instantiation. The 'print_context' command right after 'instantiation'
tells that story in extreme brevity.
So here is the fun version of your example:
class cls1 =
fixes cls1_x :: "'a"
and cls1_f :: "'a ⇒ 'a"
and cls1_g :: "nat ⇒ 'a"
assumes cls1_fg_prop: "(cls1_f (cls1_g 0)) = (cls1_g 0)"
fun f :: "int ⇒ int" where "f i = i"
fun g :: "nat ⇒ int" where "g n = (int n)"
instantiation int :: cls1
begin
print_context
fun cls1_f_int where "cls1_f_int n = f n"
fun cls1_g_int where "cls1_g_int n = g n"
instance
proof
have "cls1_f 0 = f 0" by simp
have "cls1_g 0 = g 0" by simp
have "f (g 0) = g 0" by simp
then show "cls1_f (cls1_g 0 :: int) = cls1_g 0" by simp
qed
end
Another obvious improvement of the Prover IDE would be to turn the
print_context above into some kind of template for the consecutive text.
Now ctrl/command + mouse‑hovering on cls1_f and cls1_g in:
then show "(cls1_f (cls1_g 0)) = (cls1_g 0)" by simp
… shows type inference applies in this case, as it says “int ⇒ int” and “nat
⇒ int”. But unification does not works for another reason; it now complains
instead:Local statement will fail to refine any pending goal
Failed attempt to solve goal by exported rule:
local.cls1_f (local.cls1_g (0∷nat)) = local.cls1_g (0∷nat)while before it was complaining:
Local statement will fail to refine any pending goal
Failed attempt to solve goal by exported rule:
cls1_f (cls1_g (0∷nat)) = cls1_g (0∷nat)The difference is the “local.” prefix.
You've just fallen on you nose by defining unrelated cls1_f and cls2_g.
See the fun clauses above, with cls1_f_int and cls2_g_int.
Another attempt with:
abbreviation "(cls1_f i) ≡ (f i)"
abbreviation "(cls1_g n) ≡ (g n)"… ends into the same similar issue as with Definition, but even worst,
as adding a type annotation does not solve anything now.
Another trap here. This is how it works:
abbreviation (input) f :: "int ⇒ int" where "f i ≡ i"
abbreviation (input) g :: "nat ⇒ int" where "g n ≡ (int n)"
Abbreviations try to be smart folding back by default, but the first line
can do that indefinitely, so an attempt to print something integer will
loop later on.
Makarius
Email Gateway (Aug 19 2022 at 08:20):From: Makarius <makarius@sketis.net>
This is just an area that is not fully covered by the Prover IDE markup
yet. Just for Isabelle2012 I managed to get the inferred types into the
annotations of the source text in the succesful case, which used to be an
open problem for many years. The error case still needs to be refined in
that respect, and then everyone will rightly take that for granted, so one
needs to move further on to exhibit even more in the theory source.
Makarius
Email Gateway (Aug 19 2022 at 08:20):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
The case is in the practical way solved, but something still holds
mysterious things. With or without the “::int” annotation, at the
beginning of the proof, there was this:
proof (state): step 1
goal (1 subgoal):
1. cls1_f (cls1_g (0∷nat)) = cls1_g (0∷nat)
constants:
[…]
cls1_g :: nat ⇒ int
cls1_f :: int ⇒ int
[…]
Types are correctly inferred at the beginning, but later forgotten? That's
strange. I will stay with this for now, but wish to understand it deeper a
later time.
Email Gateway (Aug 19 2022 at 08:20):From: Makarius <makarius@sketis.net>
This is because there is no formal syntactic relationship between the goal
state in the background and the Isar proof body in the foreground that is
meant to address it (fix/assume/show clause). This principle allows to
generalize what you are drafting in the proof text on the spot, without
having your nose directly on the goal.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC