Re: [isabelle] Problems with coercions



Hi Akihisa,

> On 3 Oct 2017, at 17:58, Yamada, Akihisa <Akihisa.Yamada at 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 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.