Condense a Generator Function

Here we introduce functionality that allows to condense repeated function calls according to a certain mapper. By that, we mean that if the generator produces a new value that is the same as the previous one under the mapper function, then the value is skipped.

def Function.condense_generator {α : Type u} {β : Type v} [DecidableEq α] (generator : β → β) (mapper : β → α) (different_value_exists : ∀ (b : β), ∃ (n : Nat), mapper (repeat_fun generator n b) ≠ mapper b) (b : β) : β

We condense a generator function by skipping the values that yield the same value under a mapper function. To knwo that this terminates, we need a proof that eventually we will obtain a new value. Internally the recursion is implemented using an auxiliary function, which requires a slightly stronger proof but we can simply derive that one from the weaker claim given to this function.

Equations

• Function.condense_generator generator mapper different_value_exists b = Function.condense_generator_weak✝ generator mapper ⋯ b

theorem Function.condense_generator_of_next_eq {α : Type u} {β : Type v} [DecidableEq α] {generator : β → β} {mapper : β → α} {different_value_exists : ∀ (b : β), ∃ (n : Nat), mapper (repeat_fun generator n b) ≠ mapper b} {b : β} : mapper (generator b) = mapper b → condense_generator generator mapper different_value_exists b = condense_generator generator mapper different_value_exists (generator b)

This unfolds the branch of the recursive definition where the values of the current and the next value are the same. In this case the next value is skipped.

theorem Function.condense_generator_eq_generator_of_ne {α : Type u} {β : Type v} [DecidableEq α] {generator : β → β} {mapper : β → α} {different_value_exists : ∀ (b : β), ∃ (n : Nat), mapper (repeat_fun generator n b) ≠ mapper b} (b : β) : mapper (generator b) ≠ mapper b → condense_generator generator mapper different_value_exists b = generator b

This unfolds the branch of the recursive definition where the values of the current and the next value are not the same. In this case the condense_generator yields the same value as the original generator.

theorem Function.condense_generator_next_ne {α : Type u} {β : Type v} [DecidableEq α] {generator : β → β} {mapper : β → α} {different_value_exists : ∀ (b : β), ∃ (n : Nat), mapper (repeat_fun generator n b) ≠ mapper b} (b : β) : mapper (condense_generator generator mapper different_value_exists b) ≠ mapper b

The next value produced by condense_generator is guaranteed to be different from the current one under the mapper function.

theorem Function.condense_generator_eq_repeat_generator {α : Type u} {β : Type v} [DecidableEq α] (generator : β → β) (mapper : β → α) (different_value_exists : ∀ (b : β), ∃ (n : Nat), mapper (repeat_fun generator n b) ≠ mapper b) (b : β) : ∃ (n : Nat), condense_generator generator mapper different_value_exists b = repeat_fun generator n b

Each value produced by condense_generator can be obtain from a suitable number of repetitions of the original generator. Note that this is true for the produced "carrier" value of the generator and not just for the value under the mapper function. The result simply holds since condense_generator is only skipping value from the generator but it cannot produce anything which would not eventually be produced by the generator as well.