Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Turning intervals into lists: upt and upto


view this post on Zulip Email Gateway (Jul 16 2021 at 08:58):

From: Manuel Eberl <eberlm@in.tum.de>
I just stumbled across this while talking to Katharina Kreuzer.

Currently, we have two notions of making a list from an interval of numbers:

[a..b], which desugars to "upto a b" with "upto :: int => int => int"

[a..<b], which desugars to "upt a b" with "upt :: nat => nat => nat"

Clearly, this is confusing and I suspect that it is a historic accident.
I think we should clean this up.

What one would like to have, in my opinion, is four notations [a..b],
[a<..b], [a..<b], [a<..<b] to mirror the same notation on sets.

The question is: how do we implement this properly? Haskell does it with
an "Enum" type class that has "succ"/"pred" operations. A "succ" would
be enough for us, but to implement the above operations one would
additionally need to assume that {a..b} is finite for any a, b. And, in
the specification of succ, one would have to figure out what to do if
there is no successor (e.g. in finite types).

Any ideas/comments?

Manuel
smime.p7s

view this post on Zulip Email Gateway (Jul 16 2021 at 09:23):

From: Peter Lammich <lammich@in.tum.de>
Hi,

shouldn't linearly ordered and countable be enough to define the succ
operation, e.g. as succ x = LEAST y. x<y.

One could leave succ undefined if there is no successor.

view this post on Zulip Email Gateway (Jul 16 2021 at 09:27):

From: Manuel Eberl <eberlm@in.tum.de>
Define yes, but we'd still need it to be a typeclass argument because we
also need implementations of it. "Least" is not executable.

"countable + linorder" is not enough though because e.g. "enat" does not
work. [0..∞] is not a finite list. You could define "succ", but not
"pred". (So on the dual of "enat" you could not define "succ").

Manuel
smime.p7s

view this post on Zulip Email Gateway (Jul 16 2021 at 09:41):

From: Tobias Nipkow <nipkow@in.tum.de>
This is not a accident but by design. For the types nat in int is exactly what
you want. I do not see any advantage in having all 4 notations because on nat
and int we have +1 and -1. On the contrary, you have to provide multiple
versions of each lemma. This may not seem too bad for the lemmas in the list
library, but it gets worse for user provided lemmas where you would have much
more of a choice how to formulate them. The analogy with set intervals is
misleading because they are often used for real numbers where having 4 different
intervals does make sense.

I always like to balance ease of notation and proof automation.

I would have no objection against generalising [_.._] to some type class.

If you really want to improve the situation, you could iron out a different
problem. This is a defining equation and simp rule:

"[i..<(Suc j)] = (if i ≤ j then [i..<j] @ [j] else [])"

Unfortunately it leads to lists where elements are appended at the end, but many
functions consume lists from the front. Thus this simp rule is frequently
removed. Something like the following one should work better (I hope):

"[i..<j] = (if i < j then i # [Suc i..<j] else [])"

Tobias
smime.p7s

view this post on Zulip Email Gateway (Jul 17 2021 at 08:57):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,

I always like to balance ease of notation and proof automation.

I would have no objection against generalising [_.._] to some type class.

5 years ago I posted sth. on the mailing list:
https://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg06715.html

I think it is still a valid starting point for further discussion.

If you really want to improve the situation, you could iron out a
different problem. This is a defining equation and simp rule:

"[i..<(Suc j)] = (if i ≤ j then [i..<j] @ [j] else [])"

Unfortunately it leads to lists where elements are appended at the end,
but many functions consume lists from the front. Thus this simp rule is
frequently removed. Something like the following one should work better
(I hope):

"[i..<j] = (if i < j then i # [Suc i..<j] else [])"

I agree with the observation that the default simp rule above obstructs
proofs that would require unfolding from the lower bound rather than the
upper bound. But the alternative formulation has no syntactic circuit
breaker like Suc and would hence unfold infinitely. Maybe a conditional
formulation would help:

‹i < j ==> [i..<j] = i # [Suc i..<j]›

But this all would require further thinking.

Cheers,
Florian
OpenPGP_signature

view this post on Zulip Email Gateway (Jul 17 2021 at 15:53):

From: Tobias Nipkow <nipkow@in.tum.de>
Yes, "[i..<j] = (if i < j then i # [Suc i..<j] else [])" does not terminate
(hence my "something like") and two conditional rules are probably the best
option. But updating the proofs could be daunting...

Tobias
smime.p7s

view this post on Zulip Email Gateway (Jul 19 2021 at 08:47):

From: Thomas Sewell <tals4@cam.ac.uk>
I've worked with upt a bit, and I generally override the default
simplification direction for the reasons mentioned already.

Often it's useful to work with an upt+map variant, for instance:
"i < j ⟹ upt i j = i # map Suc (upt i (j - 1))"

The above will work with an induction on j, assuming the map is
compatible with what you're doing. The library already contains
map_upt_Suc for cases where the map was explicitly present.

Anyway, my points is, while there might be a lot of proofs about upt,
many of them might manually set the rewrite/simp pattern, and might
need less maintenance.

I note that a grep for 'del:.*upt.simps' in the l4.verified
repository gives me 160+ hits. That might be daunting or not.

Best regards,
Thomas.


Last updated: Sep 25 2021 at 09:17 UTC