Library hydras.Prelude.Iterates

Open Scope nat_scope.
From Coq Require Import RelationClasses Relations Arith Max Lia.
From hydras Require Import Exp2.

From LibHyps Require Import LibHyps.
From hydras Require Import MoreLibHyps.
Ltac rename_hyp n th ::= rename_short n th.


Fixpoint iterate {A:Type}(f : A → A) (n: nat)(x:A) :=
  match n with
  | 0 ⇒ x
  | S p ⇒ f (iterate f p x)
  end.

Lemma iterate_comm {A: Type} f n (x:A)
  : iterate f n (f x) = f (iterate f n x).

Lemma iterate_compat {f : nat → nat}(n:nat)(x:nat):
  iterate f n x = nat_rec
                    (fun _ ⇒ nat → nat)
                    (fun x : nat ⇒ x)
                    (fun (_ : nat) (rec : nat → nat) (x : nat) ⇒ f (rec x))
                    n x.

Lemma iterate_compat2 {A} (f : A → A) n :
  ∀ x, iterate f n x = Nat.iter n f x.

Lemma iterate_compat3 f x n :
  iterate f n x = nat_rec (fun _ : nat ⇒ nat) x (fun _ y : nat ⇒ f y) n.

Definition strict_mono f := ∀ n p, n < p → f n < f p.

Definition dominates_from n g f := ∀ p, n ≤ p → f p < g p.

Definition fun_le f g := ∀ n:nat, f n ≤ g n.
Infix "<<=" := fun_le (at level 60).

Definition dominates g f := ∃ n : nat, dominates_from n g f .
Infix ">>" := dominates (at level 60).

Definition dominates_strong g f := {n : nat | dominates_from n g f}.
Infix ">>s" := dominates_strong (at level 60).


Lemma S_pred_rw (f : nat → nat) : S <<= f →
                                   ∀ x, S (Nat.pred (f x)) = f x.

Lemma fun_le_trans f g h : f <<= g → g <<= h → f <<= h.

Lemma mono_le f (Hf : strict_mono f) : ∀ n, n ≤ f n.

Lemma mono_injective f (Hf : strict_mono f) :
  ∀ n p , f n = f p → n = p.

Lemma mono_weak f (H: strict_mono f) :
  ∀ n p, n ≤ p → f n ≤ f p.

Lemma dominates_from_trans :
  ∀ f g h i j, dominates_from i g f →
                    dominates_from j h g →
                    dominates_from (Nat.max i j) h f .

Lemma dominates_trans f g h :
  dominates g f → dominates h g → dominates h f.

Lemma dominates_trans_strong : ∀ f g h,
    dominates_strong g f →
    dominates_strong h g →
    dominates_strong h f.

Lemma iterate_S_eqn {A:Type}(f : A → A) (n: nat)(x:A):
  iterate f (S n) x = f (iterate f n x).

Lemma iterate_S_eqn2 {A:Type}(f : A → A) (n: nat)(x:A):
  iterate f (S n) x = (iterate f n (f x)).

Lemma iterate_rw {A} {f : A → A} n :
  ∀ x, iterate f (S n) x = iterate f n (f x).

Lemma iterate_ext {A:Type}(f g: A → A) (H: ∀ x, f x = g x):
  ∀ n x, iterate f n x = iterate g n x.


Lemma iterate_le f (Hf : strict_mono f) :
  ∀ i j, i ≤ j → ∀ z, iterate f i z ≤ iterate f j z.

Lemma iterate_lt f (Hf : strict_mono f)(Hf': fun_le S f):
  ∀ i j, i < j → ∀ z, iterate f i z < iterate f j z.

Lemma iterate_lt_from f k:
   strict_mono f →
    ( ∀ n, k ≤ n → n < f n) →
    ∀ i j : nat, i < j →
                       ∀ z : nat, k ≤ z →
                                       iterate f i z < iterate f j z.


Lemma iterate_le_n_Sn (f: nat → nat):
  (∀ x, x ≤ f x) →
  ∀ n x, iterate f n x ≤ iterate f (S n) x.
Lemma iterate_le_np_le (f: nat → nat):
  (∀ x, (x ≤ f x)%nat) →
  ∀ n p x, (n ≤ p → iterate f n x ≤ iterate f p x)%nat.

Lemma iterate_mono2 (f: nat → nat):
  (∀ x y, x ≤ y → f x ≤ f y)%nat →
  ∀ n x y, (x ≤ y → iterate f n x ≤ iterate f n y)%nat.

Lemma iterate_mono f (Hf : strict_mono f) (Hf' : S <<= f):
  ∀ n, strict_mono (iterate f n).

Lemma iterate_ge : ∀ f , S <<= f →
                              ∀ j n, j ≤ iterate f n j.

Lemma iterate_Sge f j : S <<= f → S <<= iterate f (S j).

Lemma iterate_ge' : ∀ f, id <<= f →
                               ∀ n j, 0 < n → j ≤ iterate f n j.

Lemma iterate_ge'' f : id <<= f → strict_mono f → ∀ i k,
      k ≤ Nat.pred (iterate (fun z ⇒ S (f z)) (S i) k).

Lemma strict_mono_iterate_S f :
  strict_mono f → id <<= f →
  ∀ i, strict_mono
               (fun k ⇒ Nat.pred (iterate (fun z ⇒ S (f z)) (S i) k)).

Lemma iterate_mono_1 (f g: nat → nat) (k:nat) (Hf: strict_mono f)
      (Hf' : S <<= f)
      (H : ∀ n, k ≤ n → f n ≤ g n) :
  ∀ i n, k ≤ n → iterate f i n ≤ iterate g i n.

Lemma iterate_dom_prop :
  ∀ f g i (Hgt : S <<= f)
         (Hm : strict_mono f) (Hm': strict_mono g),
    dominates_from i g f →
    ∀ k, 0 < k → dominates_from i (iterate g k) (iterate f k).

Lemma dominates_from_le i j g f : i ≤ j →
                                   dominates_from i g f →
                                   dominates_from j g f .

Lemma smono_Sle f : f 0 ≠ 0 → strict_mono f → S <<= f.

Lemma iterate_ext2 {A:Type} (f g : (A → A) → A → A)
      (h i : A→A) : (∀ x, h x = i x) →
                     (∀ h' i', (∀ x, h' x = i' x) →
                                     ∀ x, f h' x = g i' x) →
                     ∀ n x, iterate f n h x = iterate g n i x.

Lemma iterate2_mono (f : (nat→nat)->(nat→nat)):
   (∀ g, strict_mono g → S <<= g → strict_mono (f g))->
   (∀ g, strict_mono g → S <<= g → S <<= (f g))->
   ∀ k g x y, strict_mono g → S <<= g →
                     (x < y)%nat →
                     (iterate f k g x < iterate f k g y)%nat.

Lemma iterate2_mono_weak (f : (nat→nat)->(nat→nat)):
   (∀ g, strict_mono g → S <<= g → strict_mono (f g))->
   (∀ g, strict_mono g → S <<= g → S <<= (f g))->
   ∀ k g x y, strict_mono g → S <<= g →
                     (x ≤ y)%nat →
                     (iterate f k g x ≤ iterate f k g y)%nat.

Lemma iterate2_mono3 (phi : (nat→nat)->(nat→nat)) :
  (∀ g, strict_mono g → S <<= g →
             strict_mono (phi g) ∧ S <<= phi g)->
  (∀ (f g : nat → nat), strict_mono f → S <<= f →
                              strict_mono g → S <<= g →
                              ((∀ x, f x ≤ g x) →
                               ∀ x, phi f x ≤ phi g x)) →
  ∀ g h, strict_mono g → S <<= g → strict_mono h → S <<= h →
             (∀ x, g x ≤ h x) →
  ∀ k x y, x ≤ y →
                 iterate phi k g x ≤ iterate phi k h y.

Lemma iterate2_mono2 (phi psi : (nat→nat)->(nat→nat)):
  (∀ g, strict_mono g → S <<= g → strict_mono (phi g))->
  (∀ g, strict_mono g → S <<= g → S <<= (phi g))->
  (∀ g, strict_mono g → S <<= g → strict_mono (psi g))->
  (∀ g, strict_mono g → S <<= g → S <<= (psi g))->
  (∀ g x, strict_mono g → fun_le S g → phi g x ≤ psi g x) →
  (∀ f g, strict_mono f → strict_mono g → S <<= f → S <<= g →
               (∀ x, f x ≤ g x) → (∀ x, psi f x ≤ psi g x)) →
  ∀ k g x y, strict_mono g → S <<= g →
                    (x ≤ y)%nat →
                    (iterate phi k g x ≤ iterate psi k g y)%nat.

Lemma exp2_ge_S : S <<= exp2.

Lemma exp2_mono : strict_mono exp2.

Lemma exp2_mono_weak : ∀ n p, n≤ p → exp2 n ≤ exp2 p.

Lemma exp2_as_iterate n : exp2 n = iterate (fun i ⇒ 2 × i)%nat n 1.

Definition hyper_exp2 k := iterate exp2 k 1.

Lemma hyper_exp2_S : ∀ n, hyper_exp2 (S n) = exp2 (hyper_exp2 n).

Lemma iterate_ge_from : ∀ f i, dominates_from i f id →
                               ∀ j, i ≤ j →
                                          ∀ n,
                                            j ≤ iterate f n j.

Lemma dominates_iterate :
  ∀ i f,
    dominates_from i f id →
    strict_mono f →
    ∀ n,
      {j:nat | i ≤ j ∧ dominates_from j (iterate f (S n)) id}.

Corollary iterate_gt_diag' :
  ∀ i f,
    dominates_from i f id →
    strict_mono f →
    ∀ n, 0 < n →
              {j:nat | i≤ j ∧ dominates_from j (iterate f n) id}.

Corollary iterate_ge_diag' :
  ∀ i f,
    dominates_from i f id→
    strict_mono f →
    ∀ n,
      {j:nat | i≤ j ∧ ∀ k, j≤ k → k ≤ iterate f n k}.