Zulip Chat Archive

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!

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.

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...

Floris van Doorn (Oct 18 2020 at 08:10):

Searching for not_injective_nat_fintype gave docs#not_injective_infinite_fintype.

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.

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?

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).