# Library rt.util.fixedpoint

Require Import rt.util.tactics rt.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 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.
}
}
{
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.