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) {struct n} : 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.
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).