Zulip Chat Archive

Stream: Is there code for X?

Topic: infinite sequence


view this post on Zulip Chase Norman (Oct 18 2020 at 07:59):

I have a function of type X → X and I want to create some representation of the infinite sequence starting from one element of X through the repeated application of the function.
I intend to prove that there is a duplicate element in the list since X is a fintype and then create a finite sublist between those two elements.
What constructs, if any, would exist to make this sort of thing easier? I've seen seq, but I'm not sure how to make it apply to my situation. Thanks!

view this post on Zulip Floris van Doorn (Oct 18 2020 at 08:07):

The infinite sequence is defined by docs#stream.iterate (note: stream α is just ℕ → α). I don't know how much lemmas about it are useful for you.

view this post on Zulip Floris van Doorn (Oct 18 2020 at 08:09):

The duplicate element should come from an cardinality argument. You want that a function from nat into a fintype is not injective...

view this post on Zulip Floris van Doorn (Oct 18 2020 at 08:10):

Searching for not_injective_nat_fintype gave docs#not_injective_infinite_fintype.

view this post on Zulip Floris van Doorn (Oct 18 2020 at 08:13):

Then the finite sublist can be created in different ways, depending on what you exactly want to do with that list. If you want to make sure you get a minimal list back (with no more duplicates), docs#nat.find will be useful at some point.

view this post on Zulip Chase Norman (Oct 18 2020 at 08:19):

Thanks so much for your response! Right now I have a statement (in a proof) that for ∀ (x : X), ∃ (y : X), useful_property x y, do you have any ideas on how to construct the associated function to create the stream?

view this post on Zulip Floris van Doorn (Oct 18 2020 at 08:23):

It will be something like λ x, classical.some (my_lemma x) (and the property can be proven by λ x, classical.some_spec (my_lemma x)).

(if you are in the middle of a proof you can do this with the tactic tactic#choose, but it is often better to separate things out in separate definitions/lemmas).

view this post on Zulip Kenny Lau (Oct 18 2020 at 09:18):

there's also nat.iterate notated as f ^[n]

view this post on Zulip Yury G. Kudryashov (Oct 18 2020 at 12:18):

And there is docs#function.is_periodic_pt

view this post on Zulip Yury G. Kudryashov (Oct 18 2020 at 12:19):

This file doesn't have a theorem [fintype α] (f : α → α) : periodic_pts f = univ yet. Feel free to PR it.


Last updated: May 16 2021 at 05:21 UTC