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

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.

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

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

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

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

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