Re: [isabelle] Problems with coercions



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 at 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 at 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Ã
>>>
>>>
>>
> 
> 


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.