Email Gateway (Aug 22 2022 at 11:28): Email Gateway (Aug 22 2022 at 11:28):From: noam neer <noamneer@gmail.com>
so far in my experiments Isabelle was able to infer types correctly, and
even to place conversion functions when necessary (such as 'real' to
convert nats and ints to reals when necessary.) but in the following
example,
declare [[show_types]]
lemma
"(n::real)>0 ==> floor(n) = n"
oops
instead of adding 'real' around the 'floor' I got the output
goal (1 subgoal):
1. (0∷real) < real n ==> ⌊real n⌋ = n
variables:
n :: int
the type inference went against an explicit type constraint 'n::real'. this
was very surprising, since I expected that if Isabelle thinks it can't
satisfy the constraint it'd issue an error message. I was able to get what
I wanted by changing the lemma to
lemma
"n>0 ==> floor(n) = (n::real)"
but I'd like to know in general at what situations can type constraints be
ignored, and if there's a way to get a clear message when it happens.
Email Gateway (Aug 22 2022 at 11:29):From: Lars Hupel <hupel@in.tum.de>
Hello,
the system decidedly did not go against the explicit type constraint.
However, it applied the coercion _inside_ the type constraint.
A type constraint inside a term can be attached to any term, not just
variables. To illustrate the point, your annotation could also be written
as "(n)::real". The system is free to apply a coercion inside the
parentheses.
I reckon you want the variable "n" to be of type "real". In that case, use
a "fixes" declaration:
lemma
fixes n :: real
shows "n>0 ==> floor(n) = n"
oops
I admit that it is somewhat unintuitive that the outer syntax "::" has a
different meaning than the inner syntax "::".
Cheers
Lars
Email Gateway (Aug 22 2022 at 11:30):From: Larry Paulson <lp15@cam.ac.uk>
I just want to stress this point: “fixes” is a much better way to constrain the type of a variable. It can also make your theorem statements more legible, even in cases where type inference does the right thing.
Larry
Last updated: Apr 26 2024 at 20:16 UTC