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



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.

On 2021-07-17 16:53, Tobias Nipkow wrote:
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

On 17/07/2021 10:57, Florian Haftmann wrote:
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 at 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





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