Re: [isabelle] Problems with coercions



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

> 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.