Library Coq.ZArith.Zmisc
Iterators
nth iteration of the function f
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).