Email Gateway (Aug 18 2022 at 13:50): Email Gateway (Aug 18 2022 at 13:50):From: Jens Doll <jd@cococo.de>
Wow, the theory covers 27 DIN A4 pages. Is there a way of decomposition
and plausification of the proof/theorems?
Jens
Email Gateway (Aug 18 2022 at 13:50):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
Hi Jens,
Wow, the theory covers 27 DIN A4 pages. Is there a way of
decomposition and plausification of the proof/theorems?
these theories are not mine. Larry Paulson wrote LFilter and Stephan
Merz LList2. I merely ported them such that they now use
Coinductive_List from HOL/Library instead of Induct/LList.
LFilter simply defines the filter functional for lazy lists.
A rough outline of LList2 is:
Lazy lists over an alphabet
There are various sets: "alllsts A" are all lists with elements from A,
"finlsts A" are only the finite lazy lists with elements from A.
"inflsts A" are the infinite ones, "fpslsts A" are non-empty, finite
llists, "poslsts A" are all non-empty llists.
Most lemmas in LList2 deal with these sets and how some functions on
lists behave w.r.t. these sets.
The recursion operator finlsts_rec for finite llists.
Some functions for llists:
ll2f somewhat models nth for llist, but returns an option: None if the
index exceeds the list.
ltake, ldrop, lset are their list-counterpart for llists
The prefix order on llist.
The set of all prefixes / suffixes / infinite suffixes of a list
Some safety and liveliness properties
For 2. to 6., numerous lemmas are proved about the various notions for
different combinations of the above types of llists over alphabets.
What Stephan Merz used these theories for, I do not know. Neither am I
sure that being focused on the various kinds of lazy lists over some
alphabet is the best way to work with lazy lists. Moreover, one might
question some design decisions (like ll2f returning an option, llength
being only defined for finite llists).
Andreas
Last updated: May 03 2024 at 12:27 UTC