[isabelle] Confusing behaviour: free variables with the same name but different types

[T***@data61.csiro.au]

Hello Isabelle users,

I just found a strange behaviour in Isabelle/HOL using notes which allow to create to different free variables with different types but the same name. This is very confusing for a user which doesn't work with [[show_types]] (Which I think is mostly everyone). Here is a minimal example:

lemma
notes hyp = refl[where t=a]
shows "a = a"
apply (insert hyp)
subgoal by assumption
done

The notes introduces a free variable named "a" with schematic type "?'a1". Then shows introduces another free variable "a" with a fixed type " 'a ". If you do by (rule hyp) right after the shows, the schematic type will be unified with "'a" and from now on both variables will be the same (same name + same type ⟹ same variable). However if you add hyp to your premises and then use the subgoal command, all schematics (here only "?'a") are instantiated with fresh free variables (here " 'b "). Therefore, right after the subgoal command, your context is:

(a :: 'b) = (a :: 'b) ⟹ (a :: 'a) = (a :: 'a)

but without type annotations it looks like:

a = a ⟹ a = a

which one would expect to be solved by assumption. In practice, the variables are different and thus assumption fails.


If this is not considered as a bug, I think there should at least be either:

* a warning that two different variables with different types but same name have appeared in the context
* or an even simpler change: when two variables have the same name but different types, print the types in the pretty printer for those specific variables even when we are in a printing mode where types are hidden


In both cases the current type printing mode (when using [[show_types]]) assumes that such name conflicts cannot exist. The previous goal gets printed as

goal (1 subgoal):
1. a = a ⟹ a = a
variables:
a :: 'a
a :: 'b

which is not very informative about which "a" is which.


For extra information: This behaviour can also be obtained with the lemmas command:

lemmas hyp = refl[where t=a]
lemma
"a = a"
apply (insert hyp)
subgoal by assumption
done

it can also be obtained without subgoal by manually instantiating the type variable:

lemmas hyp = refl[where t=a]
lemma
"a = a"
apply (insert hyp[where 'a = int)
by assumption


Thank you for y

[Makarius]

Post by T***@data61.csiro.au
lemma
notes hyp = refl[where t=a]
shows "a = a"
apply (insert hyp)
subgoal by assumption
done
(a :: 'b) = (a :: 'b) ⟹ (a :: 'a) = (a :: 'a)
a = a ⟹ a = a
which one would expect to be solved by assumption. In practice, the variables are different and thus assumption fails.

Such things can happen: Isabelle is a very complex system with many
implicit conveniences, but in rare situations it is possible to shoot
oneself into the foot.

Incidents like above occur approx. every 2 years on this mailing list,
which I would consider very rare.

Post by T***@data61.csiro.au
* a warning that two different variables with different types but same name have appeared in the context
* or an even simpler change: when two variables have the same name but different types, print the types in the pretty printer for those specific variables even when we are in a printing mode where types are hidden

Nothing of this is as simple as it might seem on the surface. After some
decades with this inherent challenge, we are already at a local minimum
of potential confusion.

Post by T***@data61.csiro.au
lemmas hyp = refl[where t=a]

Note that "a" is out-of-scope here, and bad things are to be expected
later on.

In current Isabelle2018-RC3 the above command is even rejected. Such
tightening of the system usually causes other problems elsewhere, and I
am actually surprised that nobody has complained about it in the past
weeks of testing Isabelle2018 release candidates.


Makarius

[Lars-Henrik Eriksson]

Post by Makarius

Post by T***@data61.csiro.au
[...]
a = a ⟹ a = a
which one would expect to be solved by assumption. In practice, the variables are different and thus assumption fails.

Such things can happen: Isabelle is a very complex system with many
implicit conveniences, but in rare situations it is possible to shoot
oneself into the foot.
Incidents like above occur approx. every 2 years on this mailing list,
which I would consider very rare.

Post by T***@data61.csiro.au
* a warning that two different variables with different types but same name have appeared in the context
* or an even simpler change: when two variables have the same name but different types, print the types in the pretty printer for those specific variables even when we are in a printing mode where types are hidden

Nothing of this is as simple as it might seem on the surface. After some
decades with this inherent challenge, we are already at a local minimum
of potential confusion.

This kind of thing happens frequently to me. I do use [[show_types]] to figure things out when I suspect this is the problem but it would still help considerably if Isabelle could provide some kind of heuristic that could warn the user.

Lars-Henrik Eriksson









När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/om-uu/dataskydd-personuppgifter/

[Makarius]

Post by Lars-Henrik Eriksson
This kind of thing happens frequently to me. I do use [[show_types]] to figure things out when I suspect this is the problem but it would still help considerably if Isabelle could provide some kind of heuristic that could warn the user.

Can you illustrate it by typical examples?

Everything shown on this thread so far was quite a-typical in the use of
contexts (lack of explicit declarations, 'notes' in odd places etc.).


Makarius

[Lars-Henrik Eriksson]

Post by Makarius

Post by Lars-Henrik Eriksson
This kind of thing happens frequently to me. I do use [[show_types]] to figure things out when I suspect this is the problem but it would still help considerably if Isabelle could provide some kind of heuristic that could warn the user.

Can you illustrate it by typical examples?
Everything shown on this thread so far was quite a-typical in the use of
contexts (lack of explicit declarations, 'notes' in odd places etc.).

I work with bounded sets (HOL/Cardinals/Bounded_Set.thy). Isabelle can not always infer the bounding type. A typical proof would look like this:

lemma Act_in_tau_steps: "bmember (tAct τ x) (map_bset (tau_steps_Tree x) (Abs_bset UNIV::nat set['idx]))"
proof -
have "Suc 0 ∈ set_bset (Abs_bset UNIV::nat set['idx])"
by auto
then have "bmember (tau_steps_Tree x (Suc 0)) (map_bset (tau_steps_Tree x) (Abs_bset UNIV::nat set['idx]))"
by (metis bmember.rep_eq imageI map_bset.rep_eq)
then show ?thesis
by simp
qed

All three type annotations are necessary. In this particular case it is pretty clear where type annotations are likely to be needed, but there are cases which are not so clear (sorry, I can't dig one up right now). Also, I don't want to include unnecessary type annotations as they clutter up the proof.

Lars-Henrik Eriksson









När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/om-uu/dataskydd-personuppgifter/

[Makarius]

Post by Lars-Henrik Eriksson

Post by Makarius

Post by Lars-Henrik Eriksson
This kind of thing happens frequently to me. I do use [[show_types]] to figure things out when I suspect this is the problem but it would still help considerably if Isabelle could provide some kind of heuristic that could warn the user.

Can you illustrate it by typical examples?
Everything shown on this thread so far was quite a-typical in the use of
contexts (lack of explicit declarations, 'notes' in odd places etc.).

lemma Act_in_tau_steps: "bmember (tAct τ x) (map_bset (tau_steps_Tree x) (Abs_bset UNIV::nat set['idx]))"

That is a slightly different problem. The examples at the start of this
thread were about free (undeclared) variables, but here it is about
polymorphic constants.

The logic can handle both variables and constants of the same name and
different types: they are just different formal entities. In contrast,
the higher concepts of abstract syntax and type-checking within a local
context ensure that variables always coincide on their types, as long as
the name is equal. For constants this is not done: it is normal to have
different type instances of the same constant family in the same context
(e.g. the equality constant).

More precisely, the built-in Hindley-Milner type inference for Isar
proof texts connects the types of sub-expressions via locally fixed term
variables from the context, but connecting via constants alone does not
work. For example:

notepad
begin
fix a b c d
{ have "a + b = c + d" sorry ― ‹type ‹'a›› }
{
have 1: "a + b = 0" sorry ― ‹type ‹'a››
have 2: "0 = c + d" sorry ― ‹type ‹'b››
thm trans [OF 1 2] ― ‹fails›
}
end


Makarius

[Lars-Henrik Eriksson]

Post by Makarius
That is a slightly different problem. The examples at the start of this
thread were about free (undeclared) variables, but here it is about
polymorphic constants.

Yes, there is a difference but the two problems have the common issue that expressions that "look" identical are in fact not.

Lars-Henrik Eriksson









När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/om-uu/dataskydd-personuppgifter/