[isabelle-dev] {0::nat..<n} = {..<n}

[Florian Haftmann]

Hello Andreas,

> AFAIU {..<n} wouldn't protect against negative integers and might
> deliver wrong positive.
> AFAIK the questionif 0 is part of natural numbers is disputed. Was there
> some solution in recent years?
> Depending on that {1..<n} might be an option too in some cases.

each value (term) in Isabelle/HOL has a type, and a type can be thought
of as a fixed (non-empty) set of values.  In this thread we have solely
talked about the type ‹nat› which corresponds to the natural numbers
including zero.

Cheers,
	Florian

> 
> Cheers,
> Andreas
> 
> On 05.07.2016 08:38, Tobias Nipkow wrote:
>> Florian,
>>
>> The whole setup has grown over time and initially I may have preferred
>> {..<n} just like you did. I would welcome your proposed changes.
>>
>> I agree, sums look nicer with {..<n}, but look at the bright side:
>> {0..<n} clearly shows that the set/sum is bounded, something that is
>> otherwise implicit in the type.
>>
>> Tobias
>>
>> On 04/07/2016 21:00, Florian Haftmann wrote:
>>>> The problem with {..<n} on nat is that you need multiple versions of
>>>> every lemma involving {m..<n} on nat. Hence I discourage the use of
>>>> {..<n} on nat. If you add ‹{0..<n} = {..<n}› it will solve many but not
>>>> all problems: not all proof methods invoke simp all the time.
>>>>
>>>> I consider {..<n} on nat an anomaly that should be avoided because one
>>>> gains very little by using it. One could even think aout replacing
>>>> it by
>>>> {0..<n} upon parsing.
>>>
>>> OK, then {0..<n} is the canonical representative.  And, as I did not
>>> realize before, rules concerning {0..<?n} are obviously equally simple
>>> to state as rules concerning {..<?n}, particulary induction on the upper
>>> bound.
>>>
>>> However then I suggest to add a few lemmas to emphasize that
>>> decision, e.g.
>>>
>>> lemma lessThan_atLeast0:
>>>   fixes n :: nat
>>>   shows "{..<n} = {0..<n}"
>>>   by (simp add: atLeast0LessThan)
>>>
>>> lemma atMost_atLeast0:
>>>   fixes n :: nat
>>>   shows "{..n} = {0..n}"
>>>   by (simp add: atLeast0AtMost)
>>>
>>> Currently, only their symmetrics are present, but not these, which would
>>> suggest that {..<n} is the canonical form.
>>>
>>> Similarly for ‹{0..<Suc n} = insert n {0..n}› vs. ‹{..<Suc n} = insert n
>>> {..n}›
>>>
>>> What remains a little bit unsatisfactory is the printing of sums and
>>> products:
>>>
>>> term "setsum (\<lambda>n. n ^ 3) {0..<m::nat}" -- \<open>\<Sum>n =
>>> 0..<m. n ^ 3\<close>
>>> term "setsum (\<lambda>n. n ^ 3) {..<m::nat}" -- \<open>\<Sum>n<m. n ^
>>> 3\<close>
>>> term "setsum (\<lambda>n. n ^ 3) {0..m::nat}" -- \<open>\<Sum>n = 0..m.
>>> n ^ 3\<close>
>>> term "setsum (\<lambda>n. n ^ 3) {..m::nat}" -- \<open>\<Sum>n\<le>m. n
>>> ^ 3\<close>
>>>
>>> Here the non-canonical forms are superior to read, but I think we can
>>> live with that.
>>>
>>> Since I have currently laid hands-on on that matter, I would offer to
>>> add lessThan_atLeast0, atMost_atLeast0 and ‹{0..<Suc n} = insert n
>>> {0..n}› to the distribution.  I would also polish one or two definitions
>>> in Binomial.thy which currently involve the non-canonical forms.
>>>
>>> Maybe lessThan_atLeast0 and atMost_atLeast0 are suitable candidates for
>>> default simp rules also then.
>>>
>>> Cheers,
>>>     Florian
>>>
>>>>> obviously on natural numbers ‹{0..<n} = {..<n}› holds, and the right
>>>>> hand side is also more convenient to work with (no preconditions on m
>>>>> being less or equal n etc.). But for historic reasons, ‹{0..<n}› is
>>>>> still the preferred variant in many theorems, cf. ‹find_theorems
>>>>> "{0::nat..<_}"›.
>>>>>
>>>>> I'm tempted to say that these occurrences should be normalized to
>>>>> ‹{..<n}› and ‹{0..<n} = {..<n}› be added as default simp rule, but I
>>>>> leave it to experts on intervals to judge.
>>
>>
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160705/d1dda30b/attachment.sig>