Email Gateway (Aug 18 2022 at 14:17): Email Gateway (Aug 18 2022 at 14:17):From: Andrei Popescu <uuomul@yahoo.com>
Hello,
I have trouble understanding the following behavior of macros w.r.t.
polymorphism. Consider the following situation:
consts f :: "nat => 'a"
consts g :: "'a => nat"
lemma L1: fixes n::nat shows "g(f n) = undefined"
proof-
term f (* has type "nat => 'b" OK *)
term g (* has type "'b => nat" OK *)
(* So my understanding was that, inside this proof, 'b acts like a
fixed unspecified type. *)
term "g(f(n))" (* has type "nat" OK *)
let ?c = "g(f n)"
term "?c"
(* ?c is now "%TYPE. g (f n)" and has type "'b itself => nat" WHY? *)
let ?d = "(g::'b => nat)((f::nat => 'b) n)"
term ?d (* This did not work either *)
(* Neither does this: *)
have "?d _ = (g::'b => nat)((f::nat => 'b) n)" sorry
show ?thesis sorry
qed
But the following works as expected:
lemma L2 fixes n::nat
shows "(g::'b => nat)((f::nat => 'b) n) = undefined"
proof-
term "g(f(n))" (* has type "nat" OK *)
let ?d = "(g::'b => nat)((f::nat => 'b) n)"
term "?d" (* has type "nat" OK *)
show ?thesis sorry
qed
From outside, the two lemmas L1 and L2 are identical.
1) Why is it that macros seemingly take into consideration some
extra generality?
And what does this generality mean -- is it a form of universal
quantification over types?
2) What is the status difference between the type variable
'b from L1 (that was provided automatically) and the one from L2 (that
was declared explicitly)? Before encountering the above, I was
assuming there is no difference.
Thank you in advance for any explanations on this.
Andrei
Email Gateway (Aug 18 2022 at 14:17):From: Brian Huffman <brianh@cs.pdx.edu>
Hi Andrei,
If you turn on "Show Sorts" and "Show Consts", then you should be able
to see what is going on with your example.
On Thu, Nov 12, 2009 at 2:07 PM, Andrei Popescu <uuomul@yahoo.com> wrote:
Hello,
I have trouble understanding the following behavior of macros w.r.t.
polymorphism. Consider the following situation:consts f :: "nat => 'a"
consts g :: "'a => nat"lemma L1: fixes n::nat shows "g(f n) = undefined"
At this point, 'a is a fixed, unspecified type. The "f" in the goal
has type "nat => 'a" and the "g" in the goal has type "'a => nat". If
you have "Show Sorts" turned on, then the goal display will include a
line like "type variables: 'a :: type" telling you that 'a is a fixed
type.
proof-
term f (* has type "nat => 'b" OK *)
term g (* has type "'b => nat" OK *)
(* So my understanding was that, inside this proof, 'b acts like a
fixed unspecified type. *)
Here, Isabelle is telling you that terms f and g are polymorphic,
which it would usually denote with the types "nat => 'a" and "'a =>
nat", respectively. But since type variable 'a is already used,
Isabelle uses the next available free type variable, which is 'b.
term "g(f(n))" (* has type "nat" OK *)
let ?c = "g(f n)"
term "?c"
(* ?c is now "%TYPE. g (f n)" and has type "'b itself => nat" WHY? *)
The term "g(f(n))" has type "nat", but there is also a free variable
inside the term. The fully type-annotated term is
"(g::'b=>nat)((f::nat=>'b)(n::nat)) :: nat" (Remember that 'b here
indicates polymorphism; it is not a fixed type in this context.)
The extra parameter of type 'b itself is Isabelle's way of dealing
with this situation where term contains a free type variable that does
not appear in the term's type.
When defining a constant or abbreviation, all polymorphic type
variables in the term are required to appear in the type of the term.
For example, if you try the following definition command, Isabelle
will give you a "Specification depends on extra type variables" error:
definition c :: "nat => nat" where "c n = g (f n)"
When defining abbreviations with "let" inside a proof script, Isabelle
has a workaround for this restriction: It adds an extra parameter to
change the type from "nat" (which is not allowed since it doesn't
mention 'b) to "'b itself => nat" (which is OK).
let ?d = "(g::'b => nat)((f::nat => 'b) n)"
term ?d (* This did not work either *)
This means exactly the same thing as the previous definition of ?c.
If you had instead typed
let ?d = "(g::'a => nat)((f::nat => 'a) n)"
Then the extra TYPE parameter would disappear. Since 'a is a fixed
type variable in the proof context, it is OK to define an abbreviation
for a term mentioning 'a whose type doesn't mention 'a.
(* Neither does this: *)
have "?d _ = (g::'b => nat)((f::nat => 'b) n)" sorry
show ?thesis sorry
qedBut the following works as expected:
lemma L2 fixes n::nat
shows "(g::'b => nat)((f::nat => 'b) n) = undefined"
proof-
term "g(f(n))" (* has type "nat" OK *)
let ?d = "(g::'b => nat)((f::nat => 'b) n)"
term "?d" (* has type "nat" OK *)
show ?thesis sorry
qed
Yes, this one works because the type variable in term ?d and the type
variable in the goal are the same.
From outside, the two lemmas L1 and L2 are identical.
1) Why is it that macros seemingly take into consideration some
extra generality?
And what does this generality mean -- is it a form of universal
quantification over types?2) What is the status difference between the type variable
'b from L1 (that was provided automatically) and the one from L2 (that
was declared explicitly)? Before encountering the above, I was
assuming there is no difference.Thank you in advance for any explanations on this.
Andrei
I think the original source of all your confusion was with the "term
f" and "term g" commands inside the proof script. In these cases,
Isabelle does not assume that by "term f" you mean, "the type of f
as it appears in the goal".
Also, remember to use "Show Sorts" if you ever get confused about
which type variables are fixed in a proof.
Hope this helps,
Email Gateway (Aug 18 2022 at 14:18):From: Andrei Popescu <uuomul@yahoo.com>
Hello Brian,
Many thanks for the detailed answer -- this does clarify everything.
Last updated: Nov 21 2024 at 12:39 UTC