Email Gateway (Aug 19 2022 at 15:56): Email Gateway (Aug 19 2022 at 15:56):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear all,
I currently have some trouble when trying to build code for types with invariants.
In principle, I have some
typedef foo = {b :: bar. P b} ...
and now want to construct some function which creates objects of type bar as follows:
setup_lifting type_definition_foo
lift_definition create_foo :: "bar => foo option" is "% b. if P b then Some b else None" ...
However, then I cannot create code for create_foo:
a simple
export_code create_foo in Haskell
fails.
Reading the manual on code-generation and "Data Refinement in Isabelle/HOL", I realized that
page 109 it is mentioned that for abstract type A and concrete type C one can
lift a function f :: C => (C)θ => C to a function f whose type should be A => (A)θ => A.
So does that mean that I won't be able to define my function create_foo as essentially it is
of type C => A?
Any help is appreciated,
Kind regards,
René
PS: Below you find a more detailed example
theory Test
imports
Main
begin
datatype test = A | B | C
typedef no_B = "{ t :: test. t ~= B}" by auto
setup_lifting type_definition_no_B
lift_definition get_test :: "no_B => test"
is "% x. x" .
lift_definition get_no_B :: "test => no_B option"
is "% t. if t = B then None else Some t"
by auto
export_code get_test in Haskell
(* works fine *)
export_code get_no_B in Haskell
(* No code equations for get_no_B *)
declare get_no_B.abs_eq[code]
export_code get_no_B in Haskell
(* Abstraction violation
(in code equation get_no_B ?x ≡
map_option Abs_no_B
(if equal_test_inst.equal_test ?x
B
then None else Some ?x)):
constant Abs_no_B *)
(* somehow the violation is just because the criterion seems to be purely
syntactic. Via the if-then-else it is guaranteed that the invariant of
no_B is satisfied ! *)
Email Gateway (Aug 19 2022 at 15:57):From: Wenda Li <wl302@cam.ac.uk>
Dear René,
This is not quite true, as you can define
lift_definition g:: "test => no_B "
is "% t. if t = B then A else t"
by auto
and the code generation works fine. In terms of
lift_definition get_no_B :: "test => no_B option"
is "% t. if t = B then None else Some t"
by auto
I think the problem is with
get_no_B.rep_eq: map_option Rep_no_B (get_no_B ?x) = (if ?x = B then
None else Some ?x)
An ideal code abstract equation for type no_B is of the form
Rep_no_B (f ...) = ...
so that code equations that preserve invariants of no_B could be derived
for f. Lemma get_no_B.rep_eq does not match such format, and I guess
that is why code generation fails for get_no_B (although in theory I
think we can still derive code equations in such cases). Experts on data
refinements should be able to comment more ;-)
Hope this helps,
Wenda
Email Gateway (Aug 19 2022 at 15:57):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear Wenda,
Reading the manual on code-generation and "Data Refinement in Isabelle/HOL", I realized that
page 109 it is mentioned that for abstract type A and concrete type C one can
lift a function f :: C => (C)? => C to a function f whose type should be A => (A)? => A.
So does that mean that I won't be able to define my function create_foo as essentially it is
of type C => A?This is not quite true, as you can define
lift_definition g:: "test => no_B "
is "% t. if t = B then A else t"
by autoand the code generation works fine. In terms of
lift_definition get_no_B :: "test => no_B option"
is "% t. if t = B then None else Some t"
by autoI think the problem is with
get_no_B.rep_eq: map_option Rep_no_B (get_no_B ?x) = (if ?x = B then None else Some ?x)
I fully agree.
An ideal code abstract equation for type no_B is of the form
Rep_no_B (f ...) = ...
so that code equations that preserve invariants of no_B could be derived for f. Lemma get_no_B.rep_eq does not match such format, and I guess that is why code generation fails for get_no_B (although in theory I think we can still derive code equations in such cases).
Again I agree, in principle the test ensures that no bad terms can walk below an Abs_no_B.
Experts on data refinements should be able to comment more ;-)
Hope this helps,
Definitely it was helpful, thanks a lot. Based on your definition of get_no_B I now could modify my code as follows to my original setting, which now is code-exportable.
datatype test = A | B | C
typedef no_B = "{ t :: test. t ~= B}" by auto
setup_lifting type_definition_no_B
lift_definition get_test :: "no_B => test"
is "% x. x" .
lift_definition get_no_B' :: "test => no_B"
is "% t. if t = B then A else t"
by auto
definition get_no_B :: "test => no_B option" where
"get_no_B t = (if t = B then None else Some (get_no_B' t))"
lemma get_no_B: "get_no_B t = Some no_b ==>
get_test no_b = t"
unfolding get_no_B_def
by (cases "t = B", simp_all, transfer, auto)
export_code get_test in Haskell
export_code get_no_B in Haskell
However, this solution has the small problem, that the test "t = B" is done in both
get_no_B and get_no_B'. In my real application this test "t = B" is a bit more complicated to
compute, so still the solution is not optimal. (The original definition of get_no_B only had
one test "t = B")
Cheers,
René
Email Gateway (Aug 19 2022 at 15:57):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi René,
You can avoid the duplicate test by lifting the invariant no_B to the type "no_B option".
To that end, you have to introduce another type constructor, say no_B_option (see below
for an adaptation of your example). The tricky bit is to get from no_B_option back to no_B
option. There, you must not use lifting in the result type; otherwise, the same problem
reoccurs. Here, I use a a case combinator, but your real use case might require something
else.
Hope this helps,
Andreas
datatype test = A | B | C
typedef no_B = "{ t :: test. t ~= B}" by auto
setup_lifting type_definition_no_B
lift_definition A_no_B :: "no_B" is A by simp
lift_definition C_no_B :: "no_B" is C by simp
typedef no_B_option = "{x. B ∉ set_option x}" by auto
setup_lifting type_definition_no_B_option
lift_definition get_no_B' :: "test ⇒ no_B_option"
is "λt . if t = B then None else Some t" by simp
lift_definition unpack_no_B_option :: "no_B_option ⇒ no_B option"
is "λx. (case x of None ⇒ None | Some A ⇒ Some A_no_B | Some C ⇒ Some C_no_B)" .
definition get_no_B :: "test ⇒ no_B option"
where "get_no_B t = unpack_no_B_option (get_no_B' t)"
export_code get_no_B
Email Gateway (Aug 19 2022 at 15:58):From: René Thiemann <rene.thiemann@uibk.ac.at>
Hi Andreas,
However, this solution has the small problem, that the test "t = B" is done in both
get_no_B and get_no_B'. In my real application this test "t = B" is a bit more complicated to
compute, so still the solution is not optimal. (The original definition of get_no_B only had
one test "t = B")
You can avoid the duplicate test by lifting the invariant no_B to the type "no_B option". To that end, you have to introduce another type constructor, say no_B_option (see below for an adaptation of your example). The tricky bit is to get from no_B_option back to no_B option. There, you must not use lifting in the result type; otherwise, the same problem reoccurs.
First of all, thanks for your hints.
Unfortunately I was not able to adapt your proposed solution to my case for the following reasons.
1) I do not see why in your solution there is only one test "t = B":
in get_noB' there definitely is one "t = B" test, and the second one is hidden in
unpack_no_B_option, where again you make a case analysis which seems similar to a "t = B" test,
i.e., here you have to choose the reason why the value is in no_B (whether it is the reason A or C)
2) I did not understand why the type-copy no_B_option should help at all: with A_no_B and C_no_B at hand you can
more easily and directly define
definition get_no_B :: "test => no_B option" where
"get_no_B t == if t = B then None else case t of A => Some A_no_B | C => Some C_no_B"
or even
definition get_no_B :: "test => no_B option" where
"get_no_B t == case t of A => Some A_no_B | B => None | C => Some C_no_B"
Here, I use a a case combinator, but your real use case might require something else.
3) Exactly. In my real case I have
typedef special_functions = "{ f :: nat => nat. P f}"
where P is some predicate of interest on functions. Here, I do not see how I can easily write functions similar to "A_no_B" or "C_no_B"
which always create objects of special_function type (without actually checking P).
This would then again lead to two invocations of checking P: one in the function corresponding to "A_no_B", and the other similar to get_no_B
with then checks whether it should return None or Some.
Cheers,
René
Email Gateway (Aug 19 2022 at 15:59):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi René,
On 30/09/14 15:14, René Thiemann wrote:
1) I do not see why in your solution there is only one test "t = B":
in get_noB' there definitely is one "t = B" test, and the second one is hidden in
unpack_no_B_option, where again you make a case analysis which seems similar to a "t = B" test,
i.e., here you have to choose the reason why the value is in no_B (whether it is the reason A or C)
That's right. I just thought that a case analysis is faster than a complicated predicate
test, but at second thought it does not buy you anything.
2) I did not understand why the type-copy no_B_option should help at all: with A_no_B and C_no_B at hand you can
more easily and directly definedefinition get_no_B :: "test => no_B option" where
"get_no_B t == if t = B then None else case t of A => Some A_no_B | C => Some C_no_B"or even
definition get_no_B :: "test => no_B option" where
"get_no_B t == case t of A => Some A_no_B | B => None | C => Some C_no_B"
The idea for the type copy comes from the paper on Data Refinement, as I have answered on
stackexchange some time ago:
However, this does not solve your problem with duplicate testing. In a follow-up thread,
Joachim describes a solution to avoid duplicate tests:
Best,
Andreas
Email Gateway (Aug 19 2022 at 16:16):From: René Thiemann <rene.thiemann@uibk.ac.at>
Hi Andreas,
thanks for this reference. Joachim's solution can perfectly be adapted to our application, and indeed now we also require only one test.
Cheers,
René
Last updated: Apr 19 2024 at 12:27 UTC