# Library Coq.ZArith.Zmisc

Require Import Wf_nat.
Require Import BinInt.
Require Import Zcompare.
Require Import Zorder.
Require Import Bool.
Open Local Scope Z_scope.

Iterators

nth iteration of the function f

Fixpoint iter_pos (n:positive) (A:Type) (f:A -> A) (x:A) : A :=
match n with
| xH => f x
| xO n' => iter_pos n' A f (iter_pos n' A f x)
| xI n' => f (iter_pos n' A f (iter_pos n' A f x))
end.

Definition iter (n:Z) (A:Type) (f:A -> A) (x:A) :=
match n with
| Z0 => x
| Zpos p => iter_pos p A f x
| Zneg p => x
end.

Theorem iter_nat_of_P :
forall (p:positive) (A:Type) (f:A -> A) (x:A),
iter_pos p A f x = iter_nat (nat_of_P p) A f x.

Lemma iter_nat_of_Z : forall n A f x, 0 <= n ->
iter n A f x = iter_nat (Zabs_nat n) A f x.

Theorem iter_pos_plus :
forall (p q:positive) (A:Type) (f:A -> A) (x:A),
iter_pos (p + q) A f x = iter_pos p A f (iter_pos q A f x).

Preservation of invariants : if f : A->A preserves the invariant Inv, then the iterates of f also preserve it.

Theorem iter_nat_invariant :
forall (n:nat) (A:Type) (f:A -> A) (Inv:A -> Prop),
(forall x:A, Inv x -> Inv (f x)) ->
forall x:A, Inv x -> Inv (iter_nat n A f x).

Theorem iter_pos_invariant :
forall (p:positive) (A:Type) (f:A -> A) (Inv:A -> Prop),
(forall x:A, Inv x -> Inv (f x)) ->
forall x:A, Inv x -> Inv (iter_pos p A f x).