Email Gateway (Aug 22 2022 at 14:29): Email Gateway (Aug 22 2022 at 14:29):From: Mark Wassell <mpwassell@gmail.com>
Hello Andreas and Isabelle list,
Thank you for your help with my last question. I have a follow up question:
I would like to be able to generate code for inductive predicates that have
clauses with variable number of premises that mention the inductive
predicate being defined.
A simple case:
datatype D =
DSingle nat | DMany "nat list"
inductive S :: "D ⇒ D ⇒ bool" where
"S (DSingle x) (DSingle x)" |
"List.list_all (λ(x,y). S (DSingle x) (DSingle y)) (zip xs ys) ⟹ S (DMany
xs) (DMany ys)"
For this I would like to generate a function S_i_o. Intuitively this should
be possible.
However the mode inference for S is only passing i->i->bool as a valid
mode. My rough understanding of how mode inference works (for example from
"Turning inductive into equational specifications") indicates i->o->bool is
consistent. However I can see that the appearance of 'zip xs ys' is mixing
known data (the xs) with unknown data (ys). Also its possible that
List.list_all is being considered as a side condition where, I believe, all
variables need to be known.
So my question is this: Why doesn't it infer i->o->bool where according to
the mode inference rules it should?
One solution is to by-pass this completely and define the predicate as:
inductive S' :: "D ⇒ D ⇒ bool" where
"S' (DSingle x) (DSingle x)" |
"S' (DMany []) (DMany [])" |
"S' (DMany xs) (DMany ys) ==> S' (DSingle x) (DSingle y) ==> S' (DMany
(x#xs)) (DMany (y#ys))"
However I would like to see if it can be made to work without doing this.
I have also tried to define a version of list_all as an inductive predicate
and also a list_all_pair, as in
inductive T :: "D ⇒ D ⇒ bool" where
"T (DSingle x) (DSingle x)" |
"list_all_pair (λx y. T (DSingle x) (DSingle y)) xs ys ⟹ T (DMany xs)
(DMany ys)"
but without too much success. I could have missed something though.
Cheers
Mark
Email Gateway (Aug 22 2022 at 14:29):From: Johannes Hölzl <hoelzl@in.tum.de>
Dear Mark,
There is already
list_all2 :: "('a ⇒ 'b ⇒ bool) ⇒ 'a list ⇒ 'b list ⇒ bool"
I'm not sure if this has the right setup.
But be aware that there is a difference btw
(1) list_all (%(x, y). P x y) (zip xs ys) and
(2) list_all2 P xs ys
While (1) allows xs and ys to have different length, and P only needs
to hold on the smaller length, (2) enforces that both lists have the
same length.
Email Gateway (Aug 22 2022 at 14:30):From: Tobias Nipkow <nipkow@in.tum.de>
The predicate compiller cannot invert arbitrary functions or expressions, that
would be magic. You need to be explicit about how ys is computed from xs. Your
current specification is not even a function, for any xs, my suitable ys exist
because zip will truncate longer ys's. You have to phrase your precondition in
terms of relations that have the right mode (or via functions that compute the
ys's, but that will not be possible because that involves S again. However,
there is the predefined predicate
listrel1p :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ 'a list ⇒ bool"
for exactly this purpose in List.thy. You could now write
listrel1p (λ(x,y). S (DSingle x) (DSingle y)) xs ys
That should be executable. In the end, you should formulate the precondition in
the most abstract style (eg via quantifiers) and prove the listrel1p version as
a consequence for code generation.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 14:30):From: Mark Wassell <mpwassell@gmail.com>
Tobias and Johannes, thank you for your responses.
Unfortunately I haven't had much success today using List.list_all2 or
listrel1p.
I am a little puzzled as to how these were going to work as mode inference
would have needed to 'pass though' these functions to make use of the mode
information for S (DSingle x) (DSingle y) occurrence inside the function.
I am thinking that I might need to have an equivalent of List.list_all2
defined as an inductive predicate so that mode information for this can be
used in the mode inference of S.
For example:
inductive list_all2_ind :: "('a ⇒ 'b ⇒ bool) ⇒ 'a list ⇒ 'b list ⇒ bool"
where
"list_all2_ind P [] []" |
"list_all2_ind P xs ys ⟹ P x y ⟹ list_all2_ind P (x#xs) (y#ys)"
When I do code_pred for list_all2_ind it does tell me that the mode
(i -> o -> bool) -> i -> o -> bool is consistent (the elimination rule for
this being called list_all2_ind_FioB_i_o).
Cheers
Mark
Email Gateway (Aug 22 2022 at 14:30):From: Tobias Nipkow <nipkow@in.tum.de>
Your solution should work. I though listrel1p was set up like that, but it is
slightly different.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 14:40):From: Mark Wassell <mpwassell@gmail.com>
Hi,
Thank you for your help. If I add the following to the end of your
Listall2.thy
datatype D =
DSingle nat | DMany "nat list"
inductive S :: "D ⇒ D ⇒ bool" where
"S (DSingle x) (DSingle (x+1))" |
"list_all2 (λx y. S (DSingle x) (DSingle y)) xs ys ⟹ S (DMany xs) (DMany
ys)"
code_pred [show_steps, show_mode_inference, show_invalid_clauses] S .
I don't get the mode of (i->o->bool) which is the one that I am after. I
see in the output that (o => i => bool) => o => i => bool is inferred for
list_all2 however clause 2 of S violates i->o->bool.
Is it ok to use the predicate that I am defining in the occurrence of
list_all2? I am passing to list_all2 the function (λx y. S (DSingle x)
(DSingle y))
I am also getting the following at the end of the output:
exception Fail raised (line 74 of "~~/src/HOL/Tools/Predicate_
Compile/predicate_compile_proof.ML"): prove_param: No valid parameter term.
Cheers
Mark
Email Gateway (Aug 22 2022 at 14:45):From: Lukas Bulwahn <lukas.bulwahn@gmail.com>
Dear Mark,
For higher-order predicates, we only allow single variables or
constants as higher-order arguments.
This might be mentioned in the ITP 2009 paper, and this certainly
should be mentioned in my diploma thesis.
I could reformulate your inductive predicate as follows:
datatype D =
DSingle nat | DMany "nat list"
inductive S_aux :: "nat ⇒ nat ⇒ bool"
and S :: "D ⇒ D ⇒ bool" where
"S (DSingle x) (DSingle y) ⟹ S_aux x y" |
"S (DSingle x) (DSingle (x+1))" |
"list_all2 S_aux xs ys ⟹ S (DMany xs) (DMany ys)"
code_pred [show_steps, show_mode_inference, show_invalid_clauses] S .
thm S.equation
So you can either use this definition and derive your introduction
rules from that, or you define it with your definition, introduce the
S_aux constant with the first introduction rule, and then derive the
introduction rules from my definition and annotate them with
code_pred_intro,
For code generation, you can then unfold the S_aux_i_o constant in the
S_i_o equation and you will get a recursive equation for S_i_o that
lazily enumerates all solutions.
Logically, there is no difference between your and my definition of S;
technically, the automatically derived induction rule probably looks
different, and hence, one definition might be better suited than the
other (but that's something you must find out).
Lukas
Email Gateway (Aug 22 2022 at 14:46):From: Lukas Bulwahn <lukas.bulwahn@gmail.com>
Dear Mark,
Tobias pointed out to me that list_all2 actually existed long before
the new datatype package, which just happens to define the constant
now automatically as it is the natural relator for lists.
As I found out by a more precise look at the history, Tobias defined
the list_all2 constant already in January 2000, i.e., in changeset
8115:c802042066e8 [1]. So the reason that there is no setup for
list_all2 is probably due to the fact that I did not come across an
example for the predicate compiler that uses list_all2 in 2009-2012;
even though Andreas Lochbihler and I used the predicate compiler
heavily for making the Jinja with threads semantics executable.
I have put it on my todo list to add the setup for list_all2 for the
predicate compiler in HOL-Main; it will happen eventually.
[1] http://isabelle.in.tum.de/repos/isabelle/rev/c802042066e8
Lukas
Email Gateway (Aug 22 2022 at 14:49):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Mark and Lukas,
I did use list_all2 in JinjaThreads a lot, and the setup is already there. It's just not
in List.thy, but in ~~/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy.
Andreas
Last updated: Apr 25 2024 at 16:19 UTC