Email Gateway (Aug 23 2022 at 08:48): Email Gateway (Aug 23 2022 at 08:48):From: Tobias Nipkow <nipkow@in.tum.de>
Dear Jeremy,
I have added Manuel's function "successively" to the development version of the
Isabelle distribution. If you feel bored (some people do these days) you could
update your AFP entry to use "successively" instead of your "binrealchain".
Tobias
smime.p7s
Email Gateway (Aug 23 2022 at 08:48):From: Jasmin Blanchette via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Dear list,
Tobias wrote:
I have added Manuel's function "successively" to the development version of the Isabelle distribution. If you feel bored (some people do these days) you could update your AFP entry to use "successively" instead of your "binrealchain".
For the record, there's also "chain" in "$AFP/thys/Ordered_Resolution_Prover/Lazy_List_Chain.thy". There's no nil case though, and they're over lazy lists.
For us having no nil case was the natural thing: our processes always have a start state. I'd argue it's a better default in general. Chains are basically fences with n segments and n segment and n + 1 posts. The base case is naturally 0 segments and 1 post. The 0 segment, 0 post case is a weird case, just like 0 - 1 = 0 on natural numbers.
Jasmin
Email Gateway (Aug 23 2022 at 08:48):From: Tobias Nipkow <nipkow@in.tum.de>
Jasmin,
I view "successively" differently: it expresses a property of adjacent elements
of a list. In fact, I now wonder if this would have been a better starting point:
neighbors :: 'a list => ('a * 'a) set
Just like we have learned to use the "set" function to express properties of all
elements of a list.
Tobias
smime.p7s
Email Gateway (Aug 23 2022 at 08:49):From: Thomas Sewell <sewell@chalmers.se>
For what it's worth, I'd found it useful to define the transitive counterpart of
neighbours in another project, and show that sortedness, distinctness etc
can be defined in terms of that.
Cheers,
Thomas.
Email Gateway (Aug 23 2022 at 08:49):From: Jasmin Blanchette via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Tobias wrote:
Good points. Rethinking about it, there are definitely cases where my fence analogy doesn't hold; e.g. it's convenient for syntaxes like k_1 + ... + k_n to be defined as 0 if n = 0, and why not for chains as well. I guess my application was a bit special and not necessarily typical of what one would want as the default; just like lists by default support [] even though some applications don't want empty lists.
Jasmin
Email Gateway (Aug 23 2022 at 08:58):From: Manuel Eberl <eberlm@in.tum.de>
I recently came across a few list functions that might be of general
interest and I was wondering whether we should add them to HOL/List or
HOL-Library:
"successively R xs" holds iff the relation "R" holds for each pair of
successive elements in the list "xs":
inductive successively :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ bool" for P where
"successively P []"
| "successively P [x]"
| "P x y ⟹ successively P (y # xs) ⟹ successively P (x # y # xs)"
Another possible name would be something like "chain" or "chain_rel".
In analogy to "remdups"/""distinct_adj", one can define
definition distinct_adj where
"distinct_adj = successively (≠)"
Lastly, and probably of less general interest, I have functions "rle"
and "unrle" that perform run-length encoding and -decoding (and build on
"distinct_adj"). Perhaps this is one for HOL-Library? It's a bit small
for the AFP.
Notably, "remdups_adj = map fst ∘ rle", and unlike "remdups_adj", rle is
easily invertible and fulfils some nice properties, which makes proving
things about it much easier. For instance, contrast the somewhat awkward
characterisation "remdups_adj_altdef" that we currently have in HOL/List
with the following more concise one:
lemma remdups_adj_eq_iff:
"(remdups_adj xs = ys) ⟷
distinct_adj ys ∧
(∃ns. length ns = length ys ∧
0 ∉ set ns ∧
unrle (zip ys ns) = xs)"
In total, I have the following amount of material on each of these:
successively: 90 lines
distinct_adj: 50 lines
RLE: 200 lines
Cheers,
Manuel
Email Gateway (Aug 23 2022 at 08:58):From: Tobias Nipkow <nipkow@in.tum.de>
On 20/04/2020 13:57, Manuel Eberl wrote:
I recently came across a few list functions that might be of general
interest and I was wondering whether we should add them to HOL/List or
HOL-Library:"successively R xs" holds iff the relation "R" holds for each pair of
successive elements in the list "xs":inductive successively :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ bool" for P where
"successively P []"
| "successively P [x]"
| "P x y ⟹ successively P (y # xs) ⟹ successively P (x # y # xs)"Another possible name would be something like "chain" or "chain_rel".
See List:
fun sorted_wrt :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ bool" where
"sorted_wrt P [] = True" |
"sorted_wrt P (x # ys) = ((∀y ∈ set ys. P x y) ∧ sorted_wrt P ys)"
In analogy to "remdups"/""distinct_adj", one can define
definition distinct_adj where
"distinct_adj = successively (≠)"
I am happy to add that to List.
Lastly, and probably of less general interest, I have functions "rle"
and "unrle" that perform run-length encoding and -decoding (and build on
"distinct_adj"). Perhaps this is one for HOL-Library? It's a bit small
for the AFP.
Yes, HOL-Library.
Tobias
Notably, "remdups_adj = map fst ∘ rle", and unlike "remdups_adj", rle is
easily invertible and fulfils some nice properties, which makes proving
things about it much easier. For instance, contrast the somewhat awkward
characterisation "remdups_adj_altdef" that we currently have in HOL/List
with the following more concise one:lemma remdups_adj_eq_iff:
"(remdups_adj xs = ys) ⟷
distinct_adj ys ∧
(∃ns. length ns = length ys ∧
0 ∉ set ns ∧
unrle (zip ys ns) = xs)"In total, I have the following amount of material on each of these:
successively: 90 lines
distinct_adj: 50 lines
RLE: 200 linesCheers,
Manuel
Email Gateway (Aug 23 2022 at 08:59):From: Manuel Eberl <eberlm@in.tum.de>
See List:
fun sorted_wrt :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ bool" where
"sorted_wrt P [] = True" |
"sorted_wrt P (x # ys) = ((∀y ∈ set ys. P x y) ∧ sorted_wrt P ys)"
That is not the same!
The two only coincide if the given relation is transitive. In
particular, "sorted_wrt (≠)" is equivalent to "distinct", whereas
"successively (≠)" is equivalent to "distinct_adj".
I am happy to add that to List.
I'll send the files to you then. Or I can merge it myself. Whichever you
prefer.
Manuel
Email Gateway (Aug 23 2022 at 08:59):From: Tobias Nipkow <nipkow@in.tum.de>
On 20/04/2020 17:45, Manuel Eberl wrote:
See List:
fun sorted_wrt :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ bool" where
"sorted_wrt P [] = True" |
"sorted_wrt P (x # ys) = ((∀y ∈ set ys. P x y) ∧ sorted_wrt P ys)"That is not the same!
Indeed they are not. So far we always seem to have gotten away with this one.
(Although I recall Christian Sternagel also used the non-transitive version for
some sorting proofs) Your distinct_adj is a good example where the other one is
useful. I would call it something like "chain_list" because there is already a
"chain" on sets. Possibly "chainp_list" in analogy with "chain"/"chainp".
The two only coincide if the given relation is transitive. In
particular, "sorted_wrt (≠)" is equivalent to "distinct", whereas
"successively (≠)" is equivalent to "distinct_adj".I am happy to add that to List.
I'll send the files to you then. Or I can merge it myself. Whichever you
prefer.
Please send me the files.
Tobias
Manuel
Email Gateway (Aug 23 2022 at 08:59):From: Jeremy Sylvestre <jsylvest@ualberta.ca>
I have something similar in one of my AFP submissions. See
subsubsection ‹Binary relation chains›
at
https://www.isa-afp.org/browser_info/current/AFP/Buildings/Prelim.html
Cheers,
Jeremy S.
Last updated: Apr 30 2024 at 08:19 UTC