Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problems with coercions

Email Gateway (Aug 22 2022 at 16:10):

From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi Akihisa,

On 3 Oct 2017, at 17:58, Yamada, Akihisa <Akihisa.Yamada@uibk.ac.at> wrote:

Dear Dmitriy,

thanks for the explanation. If it sees "sr :: real" in the lemma statement but not in the proof, why does the following fail?

lemma "{x. cmod x = sr} = range (op * sr)"
proof -
show "{x. cmod x = (sr :: real)} = range (op * (sr::real))"
oops

It is the other way round: the show statement yields "sr :: real" annotations (since sr is fixed in the context). In the lemma statement "sr" is just a free type variable and its precise type is the result of type inference.

If I further annotate the lemma statement, it will work.

Anyway, if it's not a surprising outcome of the design, I'll be surprised by the design.

I guess you are not surprised that the following fails (fortunately):

lemma
"f x = x"
proof -
define f :: "'a ⇒ 'a" where "f = id"
show "f x = x" unfolding f_def by simp
qed

This example demonstrates that parsing in Isabelle is heavily context-dependent. You can not expect the same string to always evaluate to the same result. Admittedly, in your example the context modification happens implicitly (by fixing the free variables of a lemma in the context), while here the define is quite explicit.

From the point of view of coercion inference, there is absolutely no way to view the two different input terms as the same.

Cheers,
Dmitriy

Cheers,
Akihisa

On 3 Oct 2017, at 13:39, Dmitriy Traytel <traytel@inf.ethz.ch> wrote:

Hi René,

interesting observation, but not really surprising.

After parsing (and inserting coercions into) the lemma statement, sr gets declared in the context (as a real). Coercion inference must respect such declarations. To do so, instead of a free variable sr, it will now see "sr :: real". I.e., the term that the constraint inference sees at "show" is not the same as the one at "lemma". This influences the internal constraint solving and affects the end result in this case.

A workaround is to fix the type of sr in the context using the long goal format, before the lemma's statement is parsed.

Cheers,
Dmitriy

On 3 Oct 2017, at 12:41, Thiemann, Rene <Rene.Thiemann@uibk.ac.at> wrote:

Dear All,

consider the following theory

theory Test
imports HOL.Complex
begin

lemma "{x. cmod x = sr} = range (op * sr)"
proof -
show "{x. cmod x = sr} = range (op * sr)"
(* failed to refine any pending goal *)
text ‹proof line is parsed as @{term "{x. cmod (complex_of_real x) = sr} = range (op * sr)"}›
text ‹goal is parsed as @{term "{x. cmod x = sr} = range (op * (complex_of_real sr))"}›
oops

end

Here, the same formula is parsed differently in the lemma-statement and in the proof,
which at least I found quite confusing.

The effect appears in both Isabelle 2017-RC3 as well as in c90fb8bee1dd.

Cheers,
René

Email Gateway (Aug 22 2022 at 16:11):

From: "Yamada, Akihisa" <Akihisa.Yamada@uibk.ac.at>
Dear Dmitriy,

thanks for the explanation. If it sees "sr :: real" in the lemma statement but not in the proof, why does the following fail?

lemma "{x. cmod x = sr} = range (op * sr)"
proof -
show "{x. cmod x = (sr :: real)} = range (op * (sr::real))"
oops

If I further annotate the lemma statement, it will work.

Anyway, if it's not a surprising outcome of the design, I'll be surprised by the design.

Cheers,
Akihisa

Email Gateway (Aug 22 2022 at 16:11):

From: "Yamada, Akihisa" <Akihisa.Yamada@uibk.ac.at>
Dear Dmitriy,

It is the other way round: the show statement yields "sr :: real" annotations (since sr is fixed in the context). In the lemma statement "sr" is just a free type variable and its precise type is the result of type inference.

ah, I see. So if I understand correctly, coercion is performed before
the type inference, and its behavior will change when types are inferred.

I guess you are not surprised that the following fails (fortunately):

lemma
"f x = x"
proof -
define f :: "'a ⇒ 'a" where "f = id"
show "f x = x" unfolding f_def by simp
qed

Definitely not, because everyone sees that `define f' will define f. I
hope not all Isabelle users have to understand the behavior of coercion
mechanism...

Cheers,
Akihisa

This example demonstrates that parsing in Isabelle is heavily context-dependent. You can not expect the same string to always evaluate to the same result. Admittedly, in your example the context modification happens implicitly (by fixing the free variables of a lemma in the context), while here the define is quite explicit.

From the point of view of coercion inference, there is absolutely no way to view the two different input terms as the same.

Cheers,
Dmitriy

Cheers,
Akihisa

On 3 Oct 2017, at 13:39, Dmitriy Traytel <traytel@inf.ethz.ch> wrote:

Hi René,

interesting observation, but not really surprising.

After parsing (and inserting coercions into) the lemma statement, sr gets declared in the context (as a real). Coercion inference must respect such declarations. To do so, instead of a free variable sr, it will now see "sr :: real". I.e., the term that the constraint inference sees at "show" is not the same as the one at "lemma". This influences the internal constraint solving and affects the end result in this case.

A workaround is to fix the type of sr in the context using the long goal format, before the lemma's statement is parsed.

Cheers,
Dmitriy

On 3 Oct 2017, at 12:41, Thiemann, Rene <Rene.Thiemann@uibk.ac.at> wrote:

Dear All,

consider the following theory

theory Test
imports HOL.Complex
begin

lemma "{x. cmod x = sr} = range (op * sr)"
proof -
show "{x. cmod x = sr} = range (op * sr)"
(* failed to refine any pending goal *)
text ‹proof line is parsed as @{term "{x. cmod (complex_of_real x) = sr} = range (op * sr)"}›
text ‹goal is parsed as @{term "{x. cmod x = sr} = range (op * (complex_of_real sr))"}›
oops

end

Here, the same formula is parsed differently in the lemma-statement and in the proof,
which at least I found quite confusing.

The effect appears in both Isabelle 2017-RC3 as well as in c90fb8bee1dd.

Cheers,
René

Email Gateway (Aug 22 2022 at 16:11):

From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi Akihisa,

On 4 Oct 2017, at 12:31, Yamada, Akihisa <Akihisa.Yamada@uibk.ac.at> wrote:

Dear Dmitriy,

It is the other way round: the show statement yields "sr :: real" annotations (since sr is fixed in the context). In the lemma statement "sr" is just a free type variable and its precise type is the result of type inference.

ah, I see. So if I understand correctly, coercion is performed before
the type inference, and its behavior will change when types are inferred.

Chapter 3 of the implementation manual (isabelle doc implementation) gives a high-level overview of how type checking/inference work in Isabelle. Coercion inference is implemented as a "check phase" and runs quite early in the stack of check phases. (Most check phases assume their input to be well-typed, while the coercion inference tries to repairs badly-typed terms. For well-typed terms, coercion inference behaves as plain Hindley-Milner type inference.)

I guess you are not surprised that the following fails (fortunately):

lemma
"f x = x"
proof -
define f :: "'a ⇒ 'a" where "f = id"
show "f x = x" unfolding f_def by simp
qed

Definitely not, because everyone sees that `define f' will define f. I
hope not all Isabelle users have to understand the behavior of coercion
mechanism…

I'd say all users of coercions (not equal to all Isabelle users) need to understand what they are "buying into" by using coercions:

• coercion inference will not modify type-correct terms
• for not type-correct terms it will try to repair them using the coercions it knows
• in case there are different ways to repair a term, one way will be chosen (the choice depends on the input term*)

The potential ambiguity makes it necessary to carefully inspect the terms and if needed to manually adjust them by adding type annotations or coercion functions.

Cheers,
Dmitriy

[*] To be very precise: the input term that coercion inference receives when the user writes a string s in the context ctxt is:

s
|> Syntax.parse_term ctxt
|> singleton (snd o Proof_Context.prepare_sorts ctxt)
|> singleton (fst o Type_Infer_Context.prepare_positions ctxt)
|> singleton (snd o Type_Infer_Context.prepare ctxt)

Email Gateway (Aug 22 2022 at 16:17):

From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear All,

consider the following theory

theory Test
imports HOL.Complex
begin

lemma "{x. cmod x = sr} = range (op * sr)"
proof -
show "{x. cmod x = sr} = range (op * sr)"
(* failed to refine any pending goal *)
text ‹proof line is parsed as @{term "{x. cmod (complex_of_real x) = sr} = range (op * sr)"}›
text ‹goal is parsed as @{term "{x. cmod x = sr} = range (op * (complex_of_real sr))"}›
oops

end

Here, the same formula is parsed differently in the lemma-statement and in the proof,
which at least I found quite confusing.

The effect appears in both Isabelle 2017-RC3 as well as in c90fb8bee1dd.

Cheers,
René

Email Gateway (Aug 22 2022 at 16:18):

From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi René,

interesting observation, but not really surprising.

After parsing (and inserting coercions into) the lemma statement, sr gets declared in the context (as a real). Coercion inference must respect such declarations. To do so, instead of a free variable sr, it will now see "sr :: real". I.e., the term that the constraint inference sees at "show" is not the same as the one at "lemma". This influences the internal constraint solving and affects the end result in this case.

A workaround is to fix the type of sr in the context using the long goal format, before the lemma's statement is parsed.

Cheers,
Dmitriy

Last updated: Nov 21 2024 at 12:39 UTC