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

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 [])"


On 16/07/2021 10:57, Manuel Eberl wrote:
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?


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.