Library rt.util.fixedpoint

Require Import rt.util.tactics rt.util.induction.

Section FixedPoint.

  Lemma iter_fix T (F : T → T) x k n :
    iter k F x = iter k.+1 F x →
    k ≤ n →
    iter n F x = iter n.+1 F x.

  Lemma fun_mon_iter_mon :
    ∀ (f: nat → nat) x0 x1 x2,
      x1 ≤ x2 →
      f x0 ≥ x0 →
      (∀ x1 x2, x1 ≤ x2 → f x1 ≤ f x2) →
      iter x1 f x0 ≤ iter x2 f x0.

  Lemma fun_mon_iter_mon_helper :
    ∀ T (f: T → T) (le: rel T) x0 x1,
      reflexive le →
      transitive le →
      (∀ x2, le x0 (iter x2 f x0)) →
      (∀ x1 x2, le x0 x1 → le x1 x2 → le (f x1) (f x2)) →
      le (iter x1 f x0) (iter x1.+1 f x0).

  Lemma fun_mon_iter_mon_generic :
    ∀ T (f: T → T) (le: rel T) x0 x1 x2,
      reflexive le →
      transitive le →
      x1 ≤ x2 →
      (∀ x1 x2, le x0 x1 → le x1 x2 → le (f x1) (f x2)) →
      (∀ x2 : nat, le x0 (iter x2 f x0)) →
      le (iter x1 f x0) (iter x2 f x0).

End FixedPoint.

(* In this section, we define some properties of relations
   that are important for fixed-point iterations. *)
Section Relations.

  Context {T: Type}.
  Variable R: rel T.
  Variable f: T → T.

  Definition monotone (R: rel T) :=
    ∀ x y, R x y → R (f x) (f y).

End Relations.

(* In this section we define a fixed-point iteration function
   that stops as soon as it finds the solution. If no solution
   is found, the function returns None. *)
Section Iteration.

  Context {T : eqType}.
  Variable f: T → T.

  Fixpoint iter_fixpoint max_steps (x: T) :=
    if max_steps is step.+1 then
      let x' := f x in
        if x == x' then
          Some x
        else iter_fixpoint step x'
    else None.

  Section BasicLemmas.

    (* We prove that iter_fixpoint either returns either None
       or Some y, where y is a fixed point. *)
    Lemma iter_fixpoint_cases :
      ∀ max_steps x0,
        iter_fixpoint max_steps x0 = None ∨
        ∃ y,
          iter_fixpoint max_steps x0 = Some y ∧
          y = f y.

    (* We also show that any inductive property P is propagated
       through the fixed-point iteration. *)
    Lemma iter_fixpoint_ind:
      ∀ max_steps x0 x,
        iter_fixpoint max_steps x0 = Some x →
        ∀ P,
          P x0 →
          (∀ x, P x → P (f x)) →
          P x.

  End BasicLemmas.

  Section RelationLemmas.

    Variable R: rel T.
    Hypothesis H_reflexive: reflexive R.
    Hypothesis H_transitive: transitive R.
    Hypothesis H_monotone: monotone f R.

    Lemma iter_fixpoint_ge_min:
      ∀ max_steps x0 x1 x,
        iter_fixpoint max_steps x1 = Some x →
        R x0 x1 →
        R x1 (f x1) →
        R x0 x.

    Lemma iter_fixpoint_ge_bottom:
      ∀ max_steps x0 x,
        iter_fixpoint max_steps x0 = Some x →
        R x0 (f x0) →
        R x0 x.

  End RelationLemmas.

End Iteration.