Library Coq.ZArith.Zmisc


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_nat (n:nat) (A:Set) (f:A -> A) (x:A) {struct n} : A :=

  match n with

    | O => x

    | S n' => f (iter_nat n' A f x)

  end.




Fixpoint iter_pos (n:positive) (A:Set) (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:Set) (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_plus :

  forall (n m:nat) (A:Set) (f:A -> A) (x:A),

    iter_nat (n + m) A f x = iter_nat n A f (iter_nat m A f x).

Proof.

  simple induction n;

    [ simpl in |- *; auto with arith

      | intros; simpl in |- *; apply f_equal with (f := f); apply H ].

Qed.




Theorem iter_nat_of_P :

  forall (p:positive) (A:Set) (f:A -> A) (x:A),

    iter_pos p A f x = iter_nat (nat_of_P p) A f x.

Proof.

  intro n; induction n as [p H| p H| ];

    [ intros; simpl in |- *; rewrite (H A f x);

      rewrite (H A f (iter_nat (nat_of_P p) A f x)); 

        rewrite (ZL6 p); symmetry  in |- *; apply f_equal with (f := f);

          apply iter_nat_plus

      | intros; unfold nat_of_P in |- *; simpl in |- *; rewrite (H A f x);

        rewrite (H A f (iter_nat (nat_of_P p) A f x)); 

          rewrite (ZL6 p); symmetry  in |- *; apply iter_nat_plus

      | simpl in |- *; auto with arith ].

Qed.




Theorem iter_pos_plus :

  forall (p q:positive) (A:Set) (f:A -> A) (x:A),

    iter_pos (p + q) A f x = iter_pos p A f (iter_pos q A f x).

Proof.

  intros n m; intros.

  rewrite (iter_nat_of_P m A f x).

  rewrite (iter_nat_of_P n A f (iter_nat (nat_of_P m) A f x)).

  rewrite (iter_nat_of_P (n + m) A f x).

  rewrite (nat_of_P_plus_morphism n m).

  apply iter_nat_plus.

Qed.

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:Set) (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).

Proof.

  simple induction n; intros;

    [ trivial with arith

      | simpl in |- *; apply H0 with (x := iter_nat n0 A f x); apply H;

        trivial with arith ].

Qed.




Theorem iter_pos_invariant :

  forall (p:positive) (A:Set) (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).

Proof.

  intros; rewrite iter_nat_of_P; apply iter_nat_invariant; trivial with arith.

Qed.