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

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.