feat(Ico): initial implementation of intervals in nat [WIP]

[semorrison]

Some initial attempts at defining Ico (interval, closed-open), in nat, as a list, multiset, and finset.

There are many more lemmas to prove about these intervals (and the corresponding ones in int), but these are all I need so far for my "reindexing finset.sum" lemmas and tactics.

(And I think this stuff will be useful whatever our eventual design for big operators looks like.)

Please feel free to criticize, hack, or add to this branch!

[johoelzl]

(Note: I didn't try the proof myself)

I would suggest to prove first more general rules about Ico on lists:
n <= m <= k -> Ico n m ++ Ico m k = Ico n k
This also translates nicely to multiset and finset. On the other hand, I think all proofs you have in multiset should be there also for lists.

Then we can proof:

n <= l <= m ->
(Ico n m).filter (λ x, x < l) =
(Ico n l).filter (λ x, x < l) ++ (Ico l m).filter (λ x, x < l) =
(Ico n l).filter (λ x, x < l)

[johoelzl]

this holds more general for n >= m, also I would call it eq_nil_of_le

[semorrison]

Fixed, thanks.

[semorrison]

(Note: I didn't try the proof myself)

I would suggest to prove first more general rules about Ico on lists:
n <= m <= k -> Ico n m ++ Ico m k = Ico n k
This also translates nicely to multiset and finset. On the other hand, I think all proofs you have in multiset should be there also for lists.

Then we can proof:

n <= l <= m ->
(Ico n m).filter (λ x, x < l) =
(Ico n l).filter (λ x, x < l) ++ (Ico l m).filter (λ x, x < l) =
(Ico n l).filter (λ x, x < l)

Thanks for this. As it turned out I independently realised this was the way to go, and implemented this approach last night.