Re: [isabelle] Code generation for typedefs with an invariant



Hi Manuel,

lift_definition already implements your workaround. Try:

context notes[[typedef_overloaded]] begin
lift_definition (code_dt) my_complicated_computation' :: "nat ⇒ good_nat list" is my_complicated_computation
  using my_complicated_computation_good by (auto simp: list.pred_set)
end

(The context is only needed because your typedef is overloaded. If you 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 but decided against as it would significantly increase the trusted code base (which now would need to take map functions into account).

Dmitriy


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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.