Iterate.v

From Tealeaves Require Import Tactics.Prelude.

(* Iterate an endofunction <<n>> times *)

(** * Iterating Functions *)
(**********************************************************************)
Fixpoint iterate (n : nat) {A : Type} (f : A -> A) :=
  match n with
  | 0 => @id A
  | S n' => iterate n' f ∘ f
  end.

(** ** Rewriting Rules *)
(**********************************************************************)
Lemma iterate_rw0 : forall {A : Type} (f : A -> A),
    iterate 0 f = id.forall (A : Type) (f : A -> A), iterate 0 f = id
Proof.forall (A : Type) (f : A -> A), iterate 0 f = id
  reflexivity.
Qed.

Lemma iterate_rw1 : forall (n : nat) {A : Type} (f : A -> A),
    iterate (S n) f = (iterate n f) ∘ f.forall (n : nat) (A : Type) (f : A -> A),
iterate (S n) f = iterate n f ∘ f
Proof.forall (n : nat) (A : Type) (f : A -> A),
iterate (S n) f = iterate n f ∘ f
  intros.n: nat
A: Type
f: A -> A
iterate (S n) f = iterate n f ∘ f
  cbn.n: nat
A: Type
f: A -> A
iterate n f ∘ f = iterate n f ∘ f
  reflexivity.
Qed.

Lemma iterate_rw2 : forall (n : nat) {A : Type} (f : A -> A),
    iterate (S n) f = f ∘ (iterate n f).forall (n : nat) (A : Type) (f : A -> A),
iterate (S n) f = f ∘ iterate n f
Proof.forall (n : nat) (A : Type) (f : A -> A),
iterate (S n) f = f ∘ iterate n f
  intros.n: nat
A: Type
f: A -> A
iterate (S n) f = f ∘ iterate n f
  cbn.n: nat
A: Type
f: A -> A
iterate n f ∘ f = f ∘ iterate n f
  induction n.A: Type
f: A -> A
iterate 0 f ∘ f = f ∘ iterate 0 f
n: nat
A: Type
f: A -> A
IHn: iterate n f ∘ f = f ∘ iterate n f
iterate (S n) f ∘ f = f ∘ iterate (S n) f
  +A: Type
f: A -> A
iterate 0 f ∘ f = f ∘ iterate 0 f reflexivity.
  +n: nat
A: Type
f: A -> A
IHn: iterate n f ∘ f = f ∘ iterate n f
iterate (S n) f ∘ f = f ∘ iterate (S n) f rewrite iterate_rw1.n: nat
A: Type
f: A -> A
IHn: iterate n f ∘ f = f ∘ iterate n f
iterate n f ∘ f ∘ f = f ∘ (iterate n f ∘ f)
    reassociate <- on right.n: nat
A: Type
f: A -> A
IHn: iterate n f ∘ f = f ∘ iterate n f
iterate n f ∘ f ∘ f = f ∘ iterate n f ∘ f
    rewrite <- IHn.n: nat
A: Type
f: A -> A
IHn: iterate n f ∘ f = f ∘ iterate n f
iterate n f ∘ f ∘ f = iterate n f ∘ f ∘ f
    reflexivity.
Qed.

Lemma iterate_rw0A : forall {A : Type} (f : A -> A) a,
    iterate 0 f a = a.forall (A : Type) (f : A -> A) (a : A),
iterate 0 f a = a
Proof.forall (A : Type) (f : A -> A) (a : A),
iterate 0 f a = a
  reflexivity.
Qed.

Lemma iterate_rw1A : forall (n : nat) {A : Type} (f : A -> A) a,
    iterate (S n) f a = (iterate n f) (f a).forall (n : nat) (A : Type) (f : A -> A) (a : A),
iterate (S n) f a = iterate n f (f a)
Proof.forall (n : nat) (A : Type) (f : A -> A) (a : A),
iterate (S n) f a = iterate n f (f a)
  reflexivity.
Qed.


Lemma iterate_rw2A : forall (n : nat) {A : Type} (f : A -> A) a,
    iterate (S n) f a = f (iterate n f a).forall (n : nat) (A : Type) (f : A -> A) (a : A),
iterate (S n) f a = f (iterate n f a)
Proof.forall (n : nat) (A : Type) (f : A -> A) (a : A),
iterate (S n) f a = f (iterate n f a)
  intros.n: nat
A: Type
f: A -> A
a: A
iterate (S n) f a = f (iterate n f a)
  compose near a on right.n: nat
A: Type
f: A -> A
a: A
iterate (S n) f a = (f ∘ iterate n f) a
  rewrite iterate_rw2.n: nat
A: Type
f: A -> A
a: A
(f ∘ iterate n f) a = (f ∘ iterate n f) a
  reflexivity.
Qed.