Email Gateway (Aug 22 2022 at 13:22): Email Gateway (Aug 22 2022 at 13:22):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear experts of the lifting package,
I wonder whether I can automate certain liftings with the Lifting package. Concretely,
suppose I have a function foo and I want to lift it to a type of state transformers:
datatype ('s, 'm) stateT = StateT (run_state: "'s => 'm")
context fixes foo :: "('a => 'm) => 'm" begin
definition foo_state :: "('a => ('s, 'm) stateT) => ('s, 'm) stateT"
where "foo_state f = StateT (%s. foo (%a. run_state (f a) s))"
end
Can I (somehow) use lift_definition to define foo_state? I am thinking of something like
the following:
setup_lifting ...
lift_definition foo_state :: "('a => ('s, 'm) stateT) => ('s, 'm) stateT" is foo
Unfortunately, I have no idea what theorem provide to setup_lifting to make this work. I
tried with the obvious one
type_definition run_state StateT UNIV
but that did not work. Any ideas?
Best,
Andreas
Email Gateway (Aug 22 2022 at 13:22):From: Peter Lammich <lammich@in.tum.de>
Hi Andreas,
Cant you just define an abbreviation "lift", and define foo_state = lift foo ?
Peter
\-------- Originalnachricht --------
Email Gateway (Aug 22 2022 at 13:22):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Peter,
The function foo is just an example. I want to do this for several other functions, each
of which has its own type. So I'd need a new abbreviation of each of them?
(And I would also like to do this for a bunch of other transformers, not just state, but
I'm hoping that I get enough insights from this example to generalise it to the others.)
Cheers,
Andreas
Email Gateway (Aug 22 2022 at 13:22):From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi Andreas,
This obviously does not work, since with the above type_definition lift_definition expects you to tell what to do with the state ’s. The following works.
datatype ('s, 'm) stateT = StateT (run_state: "'s => 'm")
context fixes foo :: "('a => 'm) => 'm" begin
lemma typedef_stateT: "type_definition run_state StateT UNIV"
by unfold_locales auto
setup_lifting typedef_stateT
lift_definition foo_state :: "('a => ('s, 'm) stateT) => ('s, 'm) stateT" is
"λf s. foo (λa. f a s)" .
end
So you can automatically insert the morphisms StateT and run_state, but I don’t think you can come up with a type_definition that hides the threading through of the state ’s from the user.
Dmitriy
Email Gateway (Aug 22 2022 at 13:22):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Dmitriy,
It would be the point of using lift_definition to relieve the user from figuring out how
to pass the state through. Unfortunately, it looks as if you were right.
No theorem of the form "type_definition Rep Abs X" will work, because it would state that
the new type is isomorphic to the set X. But ('s, 'm) stateT has much more elements than
'm (unless 's is a singleton type), so there cannot be such an isomorphic subset.
For the same reason of cardinality, no theorem "Quotient R Abs Rep T" can do the job,
either. Still, it feels as if some automation should be possible, as I myself found all
the lifted versions of constants by "type-directed programming".
Andreas
Email Gateway (Aug 22 2022 at 13:23):From: Ognjen Maric <ognjen.maric@gmail.com>
I don't know if it helps your use case, but there should still be an
isomorphism if 's is finite and 'm is infinite. At least in ZF, you can
prove from the axiom of choice that every infinite set A is equipotent
to the Cartesian product A x A - in fact, the two are equivalent by a
theorem of Tarski. I don't know if the same holds in HOL.
Ognjen
Email Gateway (Aug 22 2022 at 13:23):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Ognjen,
Equipotence of A and A * A for infinite A also holds in HOL. But in general, my state
space 's is infinite :-(.
Thanks for the suggestion,
Andreas
Last updated: Apr 26 2024 at 12:28 UTC