Email Gateway (Aug 22 2022 at 10:19): Email Gateway (Aug 22 2022 at 10:19):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear all,
The simps_of_case conversion function does not seem to like records. Consider the
following minimal example:
record foo = foo :: nat
definition f :: "foo ⇒ nat × nat ⇒ nat"
where "f s xy = (case xy of (x, y) ⇒ foo s + x + y)"
simps_of_case f_def
In this example, simps_of_case raises an exception THM, because unification of "TERM _"
and "⟦?Q ⟷ ?P; ?Q⟧ ⟹ ?P" has failed in line 315 in drule.ML. This error occurs only if one
of the parameters of the function is a record.
Is this a general limitation of simps_of_case?
Background on my use case: I want to a function with many cases. Using fun with nested
pattern matching is too slow because the internal splitting procedure creates several
hundred disambiguiations and the internal constructions then take too long. However, it
works nicely with a case expression on the right hand side. So I'd like to get the simp
rules back with simps_of_case. Any suggestions on this are welcome.
Best,
Andreas
Email Gateway (Aug 22 2022 at 10:20):From: Lars Noschinski <noschinl@in.tum.de>
The problem is that "#splits o Ctr_Sugar.ctr_sugar_of ctxt" returns
Drule.dummy_thm for records, which has not the expected format for a
split rule.
See http://isabelle.in.tum.de/testboard/Isabelle/rev/ccafd7d193e7 for a
patch which ignores these rules.
-- Lars
Email Gateway (Aug 22 2022 at 10:21):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Lars, Andreas,
Lars wrote:
This immediately points to a workaround for Andreas:
free_constructors foo_ext for foo_ext
by (erule foo.cases_scheme) (rule foo.ext_inject)
will update the “Ctr_Sugar” entry for your record type so that it works with “simps_of_case”.
This of course raises the question of whether we can/should integrate records better with the emerging “free constructor” architecture. This is mostly an engineering or design issue. Records and datatypes have some obvious conceptual overlap: A plain (non-extended) record is like a nonrecursive single-constructor datatype. Also, for extended records, there is no single constant that acts as a constructor, so the “free constructor” architecture would have to be extended to cope with that. Hence, right now we do the minimum automatically and let users invoke “free_constructors” if they want to go further. If this is too much of an annoyance, we could at least derive the split rule automatically from “foo.cases_scheme".
Jasmin
Email Gateway (Aug 22 2022 at 10:23):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Jasmin and Lars,
Thanks for your input. After Lars' explanations, I found another workaround, namely
explicitly listing the relevant split rules using (splits: ...).
Of course, I'd appreciate a better integration of record with the other packages. This
would, e.g., allow to pattern-match on records in function definitions, as in
record foo = foo :: nat
record bar = foo + bar :: int
free_constructors foo_ext for foo_ext by (fact foo.cases_scheme foo.ext_inject)+
free_constructors bar_ext for bar_ext by (meson bar.ext_surjective)(fact bar.ext_inject)
fun f :: "'a bar_scheme ⇒ int" where "f (|foo = x, bar = y, … = z|) = int x + y"
Though, I do not see why the free constructor architecture would have to be extended. An
extended extensible record like 'a bar_scheme just abbreviates "'a bar_ext foo_ext" and
the functions foo_ext and bar_ext can serve as constructors for foo_ext and bar_ext,
respectively. That is, we just have nested types with free constructors. What am I missing?
Unfortunately, the record package is still completely unlocalised. That's probably the
bigger hurdle.
Cheers,
Andreas
Email Gateway (Aug 22 2022 at 10:24):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Andreas,
Though, I do not see why the free constructor architecture would have to be extended. An extended extensible record like 'a bar_scheme just abbreviates "'a bar_ext foo_ext" and the functions foo_ext and bar_ext can serve as constructors for foo_ext and bar_ext, respectively. That is, we just have nested types with free constructors. What am I missing?
Some of the architecture doesn’t like complex types like “‘a bar_ext foo_ext” — e.g. lookup is performed on a type name. That’s the main problem IIRC. It might be easy to fix. I thought there was also an issue with the “bar_ext” constant being an abbreviation, but I apparently remembered this wrong.
Another worry I have is just the naming and wealth of theorems. Automatically performing what you do when you manually do “free_constructors” yields quite a few theorems coming from two worlds. It seems like the prefixes keep things apart, e.g. “foo.splits” (generated by record) vs. “foo_ext.splits” (generated by “free_constructors”) — but the situation is still not entirely satisfactory IMO. Hence, I would rather tread carefully here, and perhaps wait one more iteration of Isabelle and new datatypes before doing more “reforms”.
I’m also not sure all infrastructure will be equally happy to have two views on records — the records one and the “ctr_sugar” one (which has largely displaced the old datatype one here and there). This is a minor issue that can be addressed one tool at a time (Nitpick, Quickcheck, etc.), but it might require some weeks before all problems have been identified and solved.
Finally, this would enable the datatype plugins on records — generation of a size function etc. Again, this is not completely impact-free, if nothing else on the number of theorems/constants/etc. generated and hence on the performance of the prover. This is another reason why I’m inclined to wait.
All this having been said, I believe that records belong in “ctr_sugar” and that the convenience of having them in there by default would be appreciated by many users. If anybody is willing to jump in and make it happen faster than I’m likely going to, they’re welcome. ;)
Unfortunately, the record package is still completely unlocalised. That's probably the bigger hurdle.
I think that’s fine as far as “Ctr_Sugar” goes, thanks to the “generic data” abstraction. “Ctr_Sugar” can also deal with old-style datatypes, after all.
Cheers,
Jasmin
Last updated: Nov 21 2024 at 12:39 UTC