*To*: "Yamada, Akihisa" <Akihisa.Yamada at uibk.ac.at>*Subject*: Re: [isabelle] Problems with coercions*From*: Dmitriy Traytel <traytel at inf.ethz.ch>*Date*: Wed, 4 Oct 2017 15:17:28 +0200*Cc*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>, "Thiemann, Rene" <Rene.Thiemann at uibk.ac.at>*In-reply-to*: <3EAF25C69DA0E54B82B05574F64E9DEA9C2F779F@XMBX1.uibk.ac.at>*References*: <763020B0-6928-4F48-BDDE-FE7FDDF142F4@exchange.uibk.ac.at> <C18A86EE-7E2A-47F5-B7A4-A456E0AC7879@inf.ethz.ch> <F5C65C76-C00A-4BA8-BF71-070C1953ACD7@uibk.ac.at> <8D3066D5-CB2D-40DC-8539-09D26101E403@inf.ethz.ch> <3EAF25C69DA0E54B82B05574F64E9DEA9C2F779F@XMBX1.uibk.ac.at>

Hi Akihisa, > On 4 Oct 2017, at 12:31, Yamada, Akihisa <Akihisa.Yamada at 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)

**References**:**[isabelle] Problems with coercions***From:*Thiemann, Rene

**Re: [isabelle] Problems with coercions***From:*Dmitriy Traytel

**Re: [isabelle] Problems with coercions***From:*Yamada, Akihisa

**Re: [isabelle] Problems with coercions***From:*Dmitriy Traytel

**Re: [isabelle] Problems with coercions***From:*Yamada, Akihisa

- Previous by Date: Re: [isabelle] Problems with coercions
- Next by Date: Re: [isabelle] Calling Isabelle tools without exiting
- Previous by Thread: Re: [isabelle] Problems with coercions
- Next by Thread: [isabelle] Isabelle2017-RC3 and Sledgehammer
- Cl-isabelle-users October 2017 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list