Email Gateway (Aug 19 2022 at 13:43): Email Gateway (Aug 19 2022 at 13:43):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear BNF experts,
I am trying to convert my manual definitions of primitively corecursive functions to use
primcorec. Unfortunately, I am having trouble as soon as my codatatype uses nested
recursion. Here's a minimal example. It runs with Isabelle2013-2, but the problem is the
same with a recent development version such as e872d196a73b. I want to define map_bar'
with primcorec, but primcorec rejects my attempt below with "Invalid map function in
"map_foo'". So, how should I write my definition of map_bar'?
datatype_new ('a, 'c, 'e) foo = A 'a | B "'c => 'e"
primrec_new map_foo' ::
"('a => 'b) => ('d => 'c) => ('e => 'f)
=> ('a, 'c, 'e) foo => ('b, 'd, 'f) foo"
where
"map_foo' f h k (A x) = A (f x)"
| "map_foo' f h k (B c) = B (map_fun h k c)"
codatatype ('a, 'c) bar = Bar "('a, 'c, ('a, 'c) bar) foo"
definition map_bar' :: "('a => 'b) => ('d => 'c) => ('a, 'c) bar => ('b, 'd) bar"
where "map_bar' f h = bar_unfold (map_foo' f h id o un_Bar)" (* works *)
primcorec map_bar' :: "('a => 'b) => ('d => 'c) => ('a, 'c) bar => ('b, 'd) bar"
where "un_Bar (map_bar' f h r) = map_foo' f h (map_bar' f h) (un_Bar r)"
(* invalid map function map_foo' *)
Here's some background info on what I am trying to achieve. The type variable 'c in foo is
dead, so map_foo as generated by datatype_new does not take a parameter for 'c. The
quotient and lifting packages, however, expect a map function that take one parameters for
each type variable. That's why I want to define map_foo' and map_bar'.
Best,
Andreas
Email Gateway (Aug 19 2022 at 13:43):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Andreas,
So, how should I write my definition of map_bar'?
Try
primcorec map_bar' :: "('a => 'b) => ('d => 'c) => ('a, 'c) bar => ('b, 'd) bar" where
"un_Bar (map_bar' f h r) = map_foo id (map_bar' f h) ((map_foo' f h id \<circ> un_Bar) r)"
I arrived at it by looking at the characteristic theorem
thm bar.unfold[of "map_foo' f h id o un_Bar" for f h, folded map_bar'_def]
associated with your definition
definition map_bar' :: "('a => 'b) => ('d => 'c) => ('a, 'c) bar => ('b, 'd) bar"
where "map_bar' f h = bar_unfold (map_foo' f h id o un_Bar)" (* works *)
I'm sorry if this is a bit tedious each time. If this is a major hurdle for you, we might look into ways to make "primcorec" work more smoothly for such cases. Do you think it would make sense if the BNF package always defined the "map" function in the way you suggest?
Cheers,
Jasmin
Email Gateway (Aug 19 2022 at 13:43):From: Dmitriy Traytel <traytel@in.tum.de>
The corecursive call to map_bar' is only allowed to be applied either
directly of through the map function of foo (the one generated by the
package, not your custom map_foo'). The solution is to modify the
"abstract state" (here "un_Bar r") before applying the corecursive call.
To obtain your original equations you will need a few helper lemmas
(relating map_foo and map_foo').
primcorec map_bar' :: "('a => 'b) => ('d => 'c) => ('a, 'c) bar => ('b,
'd) bar"
where "un_Bar (map_bar' f h r) = map_foo f (map_bar' f h) (map_foo' id h
id (un_Bar r))"
lemma map_foo_map_foo': "map_foo f k foo = map_foo' f id k foo"
by (induct foo) auto
lemma map_foo'_comp[simp]:
"map_foo' f h k (map_foo' f' h' k' foo) = map_foo' (f o f') (h' o h)
(k o k') foo"
by (induct foo) (auto simp: map_fun.compositionality o_def)
lemma map_bar': "un_Bar (map_bar' f h r) = map_foo' f h (map_bar' f h)
(un_Bar r)"
by (auto simp: map_foo_map_foo')
Dmitriy
Email Gateway (Aug 19 2022 at 13:43):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Jasmin and Dmitriy,
Thanks for the quick replies. Jasmin's description of how he found the decomposition into
map functions and state transformation helped me to solve the next few definitions.
Do you think it would make sense if the BNF package always defined the "map" function
in the way you suggest?
It would certainly have saved me some work it the BNF package did not omit the dead
variables in the map function (I have also generalised the relator, so that would be the
next thing). But I need them only for the lifting package, I have not yet used them in
other cases. So, if there will be some integration of BNF and lifting, then that's
definitely worth thinking about; otherwise, I suggest that we need more evidence of this
being useful before someone starts to implement special cases for dead type variables.
I'm sorry if this is a bit tedious each time. If this is a major hurdle for you, we
might look into ways to make "primcorec" work more smoothly for such cases.
It is (not yet) obvious to me how I have to decompose the transformations such that
primcorec accepts them. In fact, I am already stuck again.
codatatype 'a foobar = AA 'a | BB "bool => 'a foobar"
primcorec fbind :: "'a foobar => ('a => 'b foobar) => 'b foobar"
where "fbind f g = (if is_AA f then g (un_AA f) else BB (%b. fbind (un_BB f b) g))"
datatype_new ('a, 'c, 'e) foo = A 'a | B "'c => 'e"
codatatype ('a, 'c) bar = Bar "('a, 'c, ('a, 'c) bar) foo foobar"
definition bbind :: "('a, 'c) bar => ('a => ('b, 'c) bar) => ('b, 'c) bar"
where
"bbind r f =
corec_bar (%r. fbind (un_Bar r) (%foo. case foo of A x =>
map_foobar (map_foo id Inl) (un_Bar (f x))
| B c => AA (B (%input. Inr (c input))))) r"
The functions fbind and bbind are monadic bind operations for the two codatatypes.
Following your suggestions, I thought that I transform the foobar first into
"bar + (bar * ('a => bar)) foo foobar" and then in the map functions, the Inl part stops
the corecursion and the right continues. The following attempt raises an exception that
says something about Inr () (but there are no unit types anywhere in my spec ???).
*** exception TERM raised (line 366 of "~~/src/HOL/Tools/hologic.ML"):
*** mk_split: bad body type
*** Inr ()
*** At command "primcorec"
primcorec bbind :: "('a, 'c) bar => ('a => ('b, 'c) bar) => ('b, 'c) bar"
where
"un_Bar (bbind r f) =
map_foobar (map_foo id (case_sum id (split bbind)))
(fbind (un_Bar r)
(case_foo
(map_foobar (map_foo id Inl) o un_Bar o f)
(%c. AA (B (%i. Inr (c i, f))))))"
Next, I tried to eta-expand split as follows, but in vain. This time, I am puzzled about
the "Inr (r, f)" in the prod_case. Where does that come from?
primcorec bbind :: "('a, 'c) bar => ('a => ('b, 'c) bar) => ('b, 'c) bar"
where
"un_Bar (bbind r f) =
map_foobar (map_foo id (%z. case z of Inl r => r | Inr (r, f) => bbind r f))
(fbind (un_Bar r)
(case_foo
(map_foobar (map_foo id Inl) o un_Bar o f)
(%c. AA (B (%i. Inr (c i, f))))))"
*** primcorec error:
*** Type unification failed: Clash of types "_ + _" and "(_, _) bar"
*** Type error in application: incompatible operand type
*** Operator: sum_case (%r. r) ::
*** (('a, 'c) bar * ('a => ('b, 'c) bar) => ('b, 'c) bar)
*** => ('b, 'c) bar + ('a, 'c) bar * ('a => ('b, 'c) bar) => ('b, 'c) bar
*** Operand: %a. case a of (r, f) => Inr (r, f) ::
*** ('a, 'c) bar * ('a => ('b, 'c) bar)
*** => ('b, 'c) bar + ('a, 'c) bar * ('a => ('b, 'c) bar)
*** At command "primcorec"
Could you please help me once more?
Andreas
Email Gateway (Aug 19 2022 at 13:44):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Andreas,
It would certainly have saved me some work it the BNF package did not omit the dead variables in the map function (I have also generalised the relator, so that would be the next thing). But I need them only for the lifting package, I have not yet used them in other cases. So, if there will be some integration of BNF and lifting, then that's definitely worth thinking about; otherwise, I suggest that we need more evidence of this being useful before someone starts to implement special cases for dead type variables.
It occurred to me that it might be cleaner if you define a map function that affects only the deads and then use function composition with the BNF-generated "map" to obtain the map function you need for Lifting. (Whether this actually improves things or makes your life more miserable is an open question, admittedly.)
Now to your actual problem:
codatatype 'a foobar = AA 'a | BB "bool => 'a foobar"
primcorec fbind :: "'a foobar => ('a => 'b foobar) => 'b foobar"
where "fbind f g = (if is_AA f then g (un_AA f) else BB (%b. fbind (un_BB f b) g))"datatype_new ('a, 'c, 'e) foo = A 'a | B "'c => 'e"
codatatype ('a, 'c) bar = Bar "('a, 'c, ('a, 'c) bar) foo foobar"
[...] The following attempt raises an exception that says something about Inr () (but there are no unit types anywhere in my spec ???).
*** exception TERM raised (line 366 of "~~/src/HOL/Tools/hologic.ML"):
*** mk_split: bad body type
*** Inr ()
*** At command "primcorec"primcorec bbind :: "('a, 'c) bar => ('a => ('b, 'c) bar) => ('b, 'c) bar"
where
"un_Bar (bbind r f) =
map_foobar (map_foo id (case_sum id (split bbind)))
(fbind (un_Bar r)
(case_foo
(map_foobar (map_foo id Inl) o un_Bar o f)
(%c. AA (B (%i. Inr (c i, f))))))"
This is currently not supported, because "sum" is an old-style datatype and "primrec" can only deal with new-style "case"s. (It wouldn't be hard to hard-code something for sums and products on our side, though.)
With the repository version: If you make sure that changes 1401434a7e83, f09037306f25, 3d2c97392e25, and 5ebf832b58a1 are applied, and you define your own sum "datatype_new" (or "codatatype" if you are so inclined), both the above example and the example below will work. (In fact, the naming "case_sum" in your example suggests that you are using a new-style datatype, if it's not a typo.)
Considering that we have 340 working instances of "primcorec" in Isabelle, the AFP, and a semi-private repository [], I'm amazed that you managed to produce an example that triggered so many bugs at once. The combination of "split" not followed by a lambda + a case inside a map function argument was simply toxic. I hope you feel slightly guilty for shaming us [*] publicly like that. ;)
All right: Thanks for your patience and for taking the time to file in the bug report!
Cheers,
Jasmin
[*] https://bitbucket.org/traytel/co-rec
[**] or rather: me. I can't even blame Lorenz or Dmitriy; all the bugs were clearly mine.
Email Gateway (Aug 19 2022 at 13:44):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Jasmin,
This is currently not supported, because "sum" is an old-style datatype and "primrec" can only deal with new-style "case"s. (It wouldn't be hard to hard-code something for sums and products on our side, though.)
It would be nice if such basic type constructors like sum and product work with
prim(co)rec. I tried to register sum with wrap_free_constructors, but that did not work.
I now have a local sum type as a temporary workaround.
locale sum_datatype_new begin
datatype_new ('a, 'b) sum = Inl 'a | Inr 'b
end
context begin
interpretation sum_datatype_new .
primcorec bbind ...
end
(In fact, the naming "case_sum" in your example suggests that you are using a new-style
datatype, if it's not a typo.)
True, I am hooked on the repository version again. But as I had the same problems in
Isabelle2013-2, I thought that I post this on isabelle-users for documentation.
I hope you feel slightly guilty for shaming us [**] publicly like that. ;)
All right: Thanks for your patience and for taking the time to file in the bug report!
I did not consider this a bug report. I was simply desperate because nothing worked and I
thought that I had still not understood how nested corecursion works map functions.
Thanks for fixing all this.
Andreas
Email Gateway (Aug 19 2022 at 13:44):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Andreas,
Am 06.02.2014 um 09:44 schrieb Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>:
It would be nice if such basic type constructors like sum and product work with prim(co)rec. I tried to register sum with wrap_free_constructors, but that did not work.
Did you specify selectors? Currently (and unfortunately), the tactics behind "primcorec" require types with "sel_split" theorems, which are generated only for types with selectors and discriminators.
I now have a local sum type as a temporary workaround.
I'll see what I can do. In fact, there's a lot that can and will be done at some point or another, including having us enrich the structure of "list", "option", "sum", and "prod". Today these are BNFs and free constructor types without selectors and discriminators. The next steps are (1) free constructor types with selectors and discriminators; (2) new-style datatypes (either using "datatype_new" or a forthcoming "wrap_datatype_new" command, depending on the type). The latter would allow things like nested-to-mutual recursion through lists.
All right: Thanks for your patience and for taking the time to file in the bug report!
I did not consider this a bug report. I was simply desperate because nothing worked and I thought that I had still not understood how nested corecursion works map functions.
To me, any report of one of my tools spitting out an exception is a bug report. Even though we know that "primcorec" messaging is not finished; see e.g.
Cheers,
Jasmin
Email Gateway (Aug 19 2022 at 13:44):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Jasmin,
I tried the following in Isabelle/8a53ee72e595.
wrap_free_constructors
[Inl, Inr]
case_sum
[is_Inl, is_Inr]
[[projl], [projr]]
sorry
primcorec bbind :: "('a, 'c) bar => ('a => ('b, 'c) bar) => ('b, 'c) bar"
where
"un_Bar (bbind r f) =
map_foobar (map_foo id (case_sum id (split bbind)))
(fbind (un_Bar r)
(case_foo
(map_foobar (map_foo id Inl) o un_Bar o f)
(%c. AA (B (%i. Inr (c i, f))))))"
It results in the following exception:
*** exception TERM raised (line 366 of "~~/src/HOL/Tools/hologic.ML"):
*** mk_split: bad body type
*** Inr ()
*** At command "primcorec"
Best,
Andreas
Email Gateway (Aug 19 2022 at 13:45):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Andreas,
Ah, that one was easy to fix (a87e49f4336d). Incidentally, looking at 062aa11e98e1 in conjunction with a87e49f4336d suggests that some Isabelle developers are like monkeys in front of typewriters.
Cheers,
Jasmin
Email Gateway (Aug 19 2022 at 13:45):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Jasmin,
Thanks, my example now also works with wrap_free_constructors. Maybe the
wrap_free_constructors declaration could be moved to Sum_Type?
Incidentally, looking at 062aa11e98e1 in conjunction with a87e49f4336d suggests that
some Isabelle developers are like monkeys in front of typewriters.
Unfortunately, the DUP exception is back in Isabelle/b5b64d9d1002 as the following example
shows (AFP/3daf6a41c65b).
theory Scratch imports
"$AFP/Coinductive/Coinductive_Nat"
"~~/src/HOL/Probability/Probability"
begin
*** exception DUP "Extended_Nat.enat" raised (line 374 of "General/table.ML")
*** At command "theory"
Happy debugging,
Andreas
Email Gateway (Aug 19 2022 at 13:45):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Andreas,
Thanks, my example now also works with wrap_free_constructors. Maybe the wrap_free_constructors declaration could be moved to Sum_Type?
Yesterday I gave it a try and failed (having "rep_datatype" and "wrap_free_constructors" in the same theory file introduces its own set of problems), but now I realized that if I put "wrap_free_constructors" before "rep_datatype" and use the "rep_compat" option, things work smoothly. Then the problem is that the entry gets overwritten, but more on this below...
Incidentally, looking at 062aa11e98e1 in conjunction with a87e49f4336d suggests that some Isabelle developers are like monkeys in front of typewriters.
Unfortunately, the DUP exception is back in Isabelle/b5b64d9d1002 as the following example shows (AFP/3daf6a41c65b).theory Scratch imports
"$AFP/Coinductive/Coinductive_Nat"
"~~/src/HOL/Probability/Probability"
begin*** exception DUP "Extended_Nat.enat" raised (line 374 of "General/table.ML")
*** At command "theory"Happy debugging,
Ah, I can already see what's going on: "Coinductive_Nat" redefines the "Ctr_Sugar" entry for "nat", whereas "Probability" doesn't. Merge then has to choose between two different entries and can't make up its mind.
So there are two problems:
Overwriting an entry is not harmless -- cf. the discussion above, but also after "Coinductive_Nat" all the tools that are based on the "Ctr_Sugar" entry for "nat" (and that includes "function" and some simprocs) won't know about the inductive view.
The "DUP" exception.
I'll start by simply reverting yesterday's change that causes the "DUP". Then I'll see how easy it is to generalize the data structure (and modify its clients) so that it can store multiple entries for a given key.
As usual, thanks for your report and patience with us mere mortals (or monkeys),
Cheers,
Jasmin
Email Gateway (Aug 19 2022 at 13:45):From: Johannes Hölzl <hoelzl@in.tum.de>
Hm, in this particular case the fix is to move most parts of
Coinductive_Nat to HOL/Library/Extended_Nat. I think we should even
change the definition of enat to use codatatype enat = eZero | eSuc
(epred: enat)
PS: This could be another nice (in the sky) feature for (co)datatype:
codatatype enat = (0::zero) | eSuc (epred: enat)
and automatically have all your rules etc about 0 instead of Zero :-)
Of course this would only work for syntactic typeclasses.
Email Gateway (Aug 19 2022 at 13:45):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Sure, you guys do what you want. ;)
But the "DUP" is a general issue, and we had to address it.
For the record: A "DUP" exception might still arise in odd cases where two theories independently register ctr sugar for the same type in a different way and then merge. Perhaps we should simply do like others do, namely "Symtab.merge (K true)", in which case the "canonical" order of imports decides who wins.
This is one reason why I'm slightly attacted to the possibility of having several ctr sugar records. On the other hand, some applications might not be able to cope with this gracefully and will have to pick a winner anyway...
Jasmin
Last updated: Apr 24 2024 at 20:16 UTC