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