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).