Library prosa.classic.util.fixedpoint

Require Import prosa.classic.util.tactics prosa.classic.util.induction.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

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.
  Proof.
    movee. elim: n. rewrite leqn0. by move/eqP<-.
    moven IH. rewrite leq_eqVlt; case/orP; first by move/eqP<-.
    move/IH ⇒ /= IHe. by rewrite -!IHe.
  Qed.

  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.
  Proof.
    intros f x0 x1 x2 LE MIN MON.
    revert LE; revert x2; rewrite leq_as_delta; intros delta.
    induction x1; try rewrite add0n.
    {
      induction delta; first by apply leqnn.
      apply leq_trans with (n := iter delta f x0); first by done.
      clear IHdelta.
      induction delta; first by done.
      {
        rewrite 2!iterS; apply MON.
        apply IHdelta.
      }
    }
    {
      rewrite iterS -addn1 -addnA [1 + delta]addnC addnA addn1 iterS.
      by apply MON, IHx1.
    }
  Qed.

  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).
  Proof.
    intros T f le x0 x1 REFL TRANS MIN MON.
    generalize dependent x0.
    induction x1; first by ins; apply (MIN 1).
    by ins; apply MON; [by apply MIN | by apply IHx1].
  Qed.

  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).
  Proof.
    intros T f le x0 x1 x2 REFL TRANS LE MON MIN.
    revert LE; revert x2; rewrite leq_as_delta; intros delta.
    induction delta; first by rewrite addn0; apply REFL.
    apply (TRANS) with (y := iter (x1 + delta) f x0);
      first by apply IHdelta.
    by rewrite addnS; apply fun_mon_iter_mon_helper.
  Qed.

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.
    Proof.
      induction max_steps.
      {
        by ins; simpl; destruct (x0 == f x0); left.
      }
      {
        intros x0; simpl.
        destruct (x0 == f x0) eqn:EQ1;
          first by right; x0; split; last by apply/eqP.
        by destruct (IHmax_steps (f x0)) as [NONE | FOUND].
      }
    Qed.

    (* 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.
    Proof.
      induction max_steps; first by done.
      intros x0 x SOME P P0 ALL.
      move: SOME; simpl.
      case EQ: (_ == _).
      {
        move: EQ ⇒ /eqP EQ.
        caseSAME; subst.
        by rewrite EQ; apply ALL.
      }
      {
        intros SOME; clear EQ.
        apply (IHmax_steps (f x0) x SOME P); first by apply ALL.
        by apply ALL.
      }
    Qed.

  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.
    Proof.
      induction max_steps; first by done.
      {
        intros x0 x1 x SOME MIN BOT; simpl in SOME.
        destruct (x1 == f x1) eqn:EQ1;
          first by inversion SOME; subst.
        apply IHmax_steps with (x0 := x0) in SOME; first by done.
        - by apply (@H_transitive x1).
        - by apply H_monotone.
      }
    Qed.

    Lemma iter_fixpoint_ge_bottom:
       max_steps x0 x,
        iter_fixpoint max_steps x0 = Some x
        R x0 (f x0)
        R x0 x.
    Proof.
      intros max_steps x0 x SOME BOT.
      by apply iter_fixpoint_ge_min with (max_steps := max_steps) (x1 := x0).
    Qed.

  End RelationLemmas.

End Iteration.