*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Code generation for typedefs with an invariant*From*: Manuel Eberl <manuel at pruvisto.org>*Date*: Fri, 15 Oct 2021 18:41:11 +0200*Authentication-results*: cam.ac.uk; iprev=pass (smtprelay01.ispgateway.de) smtp.remote-ip=80.67.18.13; spf=none smtp.mailfrom=pruvisto.org; arc=none*In-reply-to*: <b8bd5792-cbe6-edf4-0ef3-bb5dbe876fbd@pruvisto.org>*References*: <796951f0-49fc-a0f0-1324-3a0b0ee2ed8d@uibk.ac.at> <6817a65e-dd1f-385f-7ac7-4a54265f1319@pruvisto.org> <1dd5589b-2bfd-bd11-14f8-2ad52761dfec@pruvisto.org> <D52B3CA3-E621-4918-B399-26B3223CDCD6@di.ku.dk> <b8bd5792-cbe6-edf4-0ef3-bb5dbe876fbd@pruvisto.org>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:91.0) Gecko/20100101 Thunderbird/91.2.0

Manuel On 15/10/2021 18:34, Manuel Eberl wrote:

Interesting, thanks!Unfortunately, there seems to be a problem with the implementation.Consider e.g. this example:typedef mynat = "{n::nat. n > 0 ∧ even n}" by (rule exI[of _ 2]) autotypedef foo = "{(a :: nat,bs :: (nat × nat) list). ∀b∈set bs. fst b >0 ∧ even (fst b)}"by (rule exI[of _ "(0, [])"]) auto setup_lifting type_definition_foo setup_lifting type_definition_mynat lift_definition (code_dt) bar :: "foo ⇒ (mynat × nat) list" is snd by (force simp: list.pred_set) This gives me a "tactic failed". Manuel On 15/10/2021 18:11, Dmitriy Traytel wrote:Hi Manuel, lift_definition already implements your workaround. Try: context notes[[typedef_overloaded]] beginlift_definition (code_dt) my_complicated_computation' :: "nat ⇒good_nat list" is my_complicated_computationusing my_complicated_computation_good by (auto simp: list.pred_set) end(The context is only needed because your typedef is overloaded. Ifyou have a concrete non-overloaded definition for good you can drop it.)This is documented in Ondra's PhD thesis(https://www21.in.tum.de/~kuncar/documents/kuncar-phdthesis.pdf,Section 6.4) and in isar-ref (page 282 for the Isabelle2021 edition).IIRC, Ondra had also considered extending the code generator butdecided against as it would significantly increase the trusted codebase (which now would need to take map functions into account).DmitriyOn 15 Oct 2021, at 16:52, Manuel Eberl <manuel at pruvisto.org> wrote: Small addition: another application of this is to make a "safe" constructor for types with invariants that returns "None" if the given value does not fulfil the invariant, e.g.: mk_pos_nat :: nat ⇒ good_nat option mk_pos_nat n = (if good_nat n then Some (Abs_good_nat n) else None) One can do this with an auxiliary function that returns a default value instead of None, but then you have to check the condition twice. The best possible solution I see here is if "code abstype" could handle not only equations of the form "projection (fun_with_invariant x y z) = …" but relations involving "canonical" relators on types. In the above case, one would then not have a code equation but a code relation: rel_fun (=) (rel_option pcr_good_nat) (λn. if good n then Some n else None) mk_good_nat Similarly, the function in my last email have the following relations: rel_fun (=) (list_all2 pcr_good_nat) my_complicated_computation my_complicated_computation' The actual generated code should of course be: mk_pos_nat n = (if good_nat n then Some (Abs_good_nat n) else None my_complicated_computation' xs = map Abs_good_nat (my_complicated_computation xs) Which is exactly the m_complicated_computation' that comes out of the lift_definition anyway (and I imagine there's a one-to-one correspondence between the map operations in the def lemma and the relators in the transfer lemma). So, not sure – is there some fundamental problem with implementation something like this in the code generator? Manuel On 14/10/2021 21:31, Manuel Eberl wrote:Hello, I have a typedef of the form typedef good_nat = "{n::nat. good n}" and I have an executable function that produces a "nat list" where I have proven that all entries are good. How can I lift that to an *executable* function that produces a "good_nat list" instead? The way I see it, the usual approach of doing a "code abstype" and specifying the code equation in terms of some projection out of the "type with invariant" to "type without invariant" doesn't work here because I have lists of these things. I do have a workaround involving a second typedef for intermediate results, but it is very boilerplatey and I'd be happy to know if there is something easier. See attachment for all the details. Thanks, Manuel

**References**:**[isabelle] Fwd: Code generation for typedefs with an invariant***From:*Manuel Eberl

**Re: [isabelle] Fwd: Code generation for typedefs with an invariant***From:*Manuel Eberl

**Re: [isabelle] Code generation for typedefs with an invariant***From:*Dmitriy Traytel

**Re: [isabelle] Code generation for typedefs with an invariant***From:*Manuel Eberl

- Previous by Date: Re: [isabelle] Code generation for typedefs with an invariant
- Next by Date: [isabelle] New in the AFP: Verified Quadratic Virtual Substitution for Real Arithmetic
- Previous by Thread: Re: [isabelle] Code generation for typedefs with an invariant
- Next by Thread: [isabelle] New in the AFP: Verified Quadratic Virtual Substitution for Real Arithmetic
- Cl-isabelle-users October 2021 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