Stream: Mirror: Isabelle Users Mailing List

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


view this post on Zulip Email Gateway (Oct 15 2021 at 09:29):

From: Manuel Eberl <manuel@pruvisto.org>
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
Test.thy

view this post on Zulip Email Gateway (Oct 15 2021 at 14:52):

From: Manuel Eberl <manuel@pruvisto.org>
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

view this post on Zulip Email Gateway (Oct 15 2021 at 16:12):

From: Dmitriy Traytel <traytel@di.ku.dk>
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

view this post on Zulip Email Gateway (Oct 15 2021 at 16:35):

From: Manuel Eberl <manuel@pruvisto.org>
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]) auto

typedef 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

view this post on Zulip Email Gateway (Oct 15 2021 at 16:41):

From: Manuel Eberl <manuel@pruvisto.org>
NB: if I wrap the conjunction in the typedef of mynat into another
definition, everything works fine. So there seems to be some problem
with the conjunction.

Manuel

view this post on Zulip Email Gateway (Nov 12 2021 at 18:36):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,

I can confirm this since I backed this decision. Sorry for the late reply.

Florian
OpenPGP_signature


Last updated: Jul 15 2022 at 23:21 UTC