*To*: Wenda Li <wl302 at cam.ac.uk>, "Thiemann, Rene" <Rene.Thiemann at uibk.ac.at>*Subject*: Re: [isabelle] computation_check with "let ... in ..."*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Thu, 22 Feb 2018 10:14:26 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <D23B635A-1E38-41C3-AA88-3FC6C9EE6498@cam.ac.uk>*Organization*: TU Munich*References*: <38FEDE48-C960-4469-9B49-2B4835965C03@cam.ac.uk> <ABD88AD5-5361-49F4-B09A-D31E89C9593E@uibk.ac.at> <D23B635A-1E38-41C3-AA88-3FC6C9EE6498@cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.6.0

Dear Wenda, a generic solution to the abstraction issue would be a preprocessor transforming abstractions into expressions in combinatorial logic. There is an implementation of this in meson: ML ‹ Meson_Clausify.introduce_combinators_in_cterm @{context} @{cterm "let (k::int) = 42 * 7 in k + k * 1705 - k ^ 2"} › Unfortunately, following the comments in the code, the implementation seems suboptimal. I would appreciate if someone would use this as a base to provide a generic preprocessor in Pure; this could then be an official part of computations. Cheers, Florian Am 21.02.2018 um 15:19 schrieb Wenda Li: > Dear René, > > Thanks for your prompt reply and detailed explanation, which did clarify some of my confusions. > > Eliminating occurrences of “let … in …” when pre-prossessing is of course a viable way, but my main motivation for this “let … in …” expression is possible gain in performance: suppose we want to prove the following proposition > > lemma "let x::int poly= smult 2 [:1,2:] in [:2,3:] * x * x = [:8, 44, 80, 48:]” > > through evaluation. If we can directly evaluate "let x::int poly= smult 2 [:1,2:] in [:2,3:] * x * x = [:8, 44, 80, 48:]” in SML, we probably need to do the “smult” operation only once. However, with the “let” expression unfolded, what we need to evaluate is instead > > [:2, 3:] * smult 2 [:1, 2:] * smult 2 [:1, 2:] = [:8, 44, 80, 48:] > > , with which I guess the “smult” operation will be carried out twice. > > To sum up, my main purpose of “let … in …” is to eliminate repeated computations, and I hope to achieve this in the computation_check setups. > > Many thanks, > Wenda > >> On 21 Feb 2018, at 08:33, Thiemann, Rene <Rene.Thiemann at uibk.ac.at> wrote: >> >> Dear Wenda, >> >> one might be tempted to just add “Let" to the list of constants. However, >> this still won’t work since your input term contains an abstraction: >> >> Let [:2,3:] (% x. [:1,2:] * x = [:2, 7, 6:]) >> >> And according to the code-generator manual (codegen.pdf), abstractions are not supported: >> >> From the documentation: >> 6.5 Pitfalls concerning input terms >> >> No abstractions. Only constants and applications are admissible as input; abstractions are not possible. In theory, the compilation schema could be extended to cover abstractions also, but this would increase the trusted code base. If abstractions are required, they can always be eliminated by a dedicated preprocessing step, e.g. using combinatorial logic. >> >> >> So your unfolding of the “Let” constant is precisely such a required preprocessing step to get rid of the abstraction in this example. >> >> With best regards, >> René >> >> >> >>> Am 20.02.2018 um 22:00 schrieb Wenda Li <wl302 at cam.ac.uk>: >>> >>> Dear code generation experts, >>> >>> I was wondering how can we computation_check a term with the form “let … in …”. Here is a small example: given a proposition that can be proved by evalutaion (i.e., by eval or by by code_simp), >>> >>> lemma "let x ::int poly= [:2,3:] in [:1,2:] * x = [:2, 7, 6:]” >>> >>> I want to solve it using the computation_check mechanic. If I unfold the “let” constant first, the proposition can be proved like the following: >>> >>> ML ‹ >>> val holds = @{computation_check terms: >>> Trueprop >>> "times::int poly ⇒ _" >>> "HOL.equal ::int poly ⇒ _" >>> "0 :: int poly" >>> "pCons :: int ⇒ _" >>> "0 :: int" "1 :: int" >>> Code_Target_Int.positive datatypes:num >>> }; >>> › >>> >>> lemma "let x::int poly= [:2,3:] in [:1,2:] * x = [:2, 7, 6:]" >>> unfolding Let_def >>> apply (tactic ‹ >>> CONVERSION (holds @{context}) 1 >>> ›) >>> by (rule TrueI) >>> >>> However, without the unfolding (i.e., remove “unfolding Let_def”), "apply (tactic ‹CONVERSION (holds@{context}) 1›)” will get stuck. I am not sure if there is any other constant I should add to “@{computation_check terms: >>> ... >>> };" >>> to make the CONVERSION work. >>> >>> Thanks in advance, >>> Wenda >>> >> > -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**References**:**[isabelle] computation_check with "let ... in ..."***From:*Wenda Li

**Re: [isabelle] computation_check with "let ... in ..."***From:*Thiemann, Rene

**Re: [isabelle] computation_check with "let ... in ..."***From:*Wenda Li

- Previous by Date: Re: [isabelle] OpenTheory import for Isabelle
- Next by Date: Re: [isabelle] imp_program replace more bindings by let
- Previous by Thread: Re: [isabelle] computation_check with "let ... in ..."
- Next by Thread: [isabelle] VerifyThis 2018: Call for Problems and First Announcement
- Cl-isabelle-users February 2018 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