# Library prosa.util.fixpoint

From mathcomp Require Import ssreflect ssrbool eqtype ssrfun ssrnat seq fintype bigop path.

Require Export prosa.util.rel.
Require Export prosa.util.list.
Require Export prosa.util.minmax.

# Fixpoint Search

This module provides some utilities for finding positive fixpoints of monotonic functions.

## Least Positive Fixpoint

Finds the least fixpoint of a monotonic function, between a start point s and a horizon h, given an amount of fuel.
Fixpoint find_fixpoint_from (f : nat nat) (x h fuel: nat): option nat :=
if fuel is S fuel' then
if f x == x then
Some x
else
if (f x) h then
find_fixpoint_from f (f x) h fuel'
else None
else None.

Given a horizon h and a monotonic function f, find the least positive fixpoint of f no larger than h, if any.
Definition find_fixpoint (f : nat nat) (h : nat) : option nat :=
find_fixpoint_from f 1 h h.

In the following, we show that the fixpoint search works as expected.
Section FixpointSearch.

Consider any function f ...
Variable f : nat nat.

... and any given horizon.
Variable h : nat.

We show that the result of find_fixpoint_from is indeed a fixpoint.
Using the above fact, we observe that the result of find_fixpoint is a fixpoint.
Corollary ffp_finds_fixpoint :
x : nat,
find_fixpoint f h = Some x
x = f x.

Next, we establish properties that rely on the monotonic properties of the function.
Section MonotonicFunction.

Suppose f is monotonically increasing ...
Hypothesis H_f_mono: monotone leq f.

... and not zero at 1.
Hypothesis F1: f 1 > 0.

Assuming the function is monotonic, there is no fixpoint between a and c, if f a = c.
Lemma no_fixpoint_skipped :
a c,
c = f a
b,
a b < c
b != f b.

It follows that find_fixpoint_from finds the least fixpoint larger than s.
Hence find_fixpoint finds the least positive fixpoint of f.
Furthermore, we observe that find_fixpoint_from finds positive fixpoints when provided with a positive starting point s.
Hence finds_fixpoint finds only positive fixpoints.
If find_fixpoint_from finds no fixpoint between s and h, there is none.
Hence, if find_fixpoint finds no positive fixpoint less than h, there is none.

## Maximal Fixpoint across a Search Space

Given a function taking two inputs and a search space for the first argument, find_max_fixpoint_of_seq finds the maximum fixpoint with regard to the second argument across the search space, but only if a fixpoint exists for each point in the search space.
Definition find_max_fixpoint_of_seq (f : nat nat nat)
(sp : seq nat) (h : nat) : option nat :=
let is_some opt := opt != None in
let fixpoints := [seq find_fixpoint (f s) h | s <- sp] in
let max := \max_(fp <- fixpoints | is_some fp) (odflt 0) fp in
if all is_some fixpoints then Some max else None.

We prove that the result of the find_max_fixpoint_of_seq is a fixpoint of the function for an element of the search space.
Furthermore, we show that the result is the maximum of all fixpoints, with regard to the search space.

## Search Space Defined by a Predicate

Consider a limit L ...
Variable L : nat.

... and any predicate P on numbers.
Variable P : pred nat.

We create a derive predicate that defines the search space as all values less than L that satisfy P.
This is used to create a corresponding sequence of points in the search space.
Let sp := [seq s <- (iota 0 L) | P s].

Based on this conversion, we define a function to find the maximum of all fixpoints within the search space.
Definition find_max_fixpoint (f : nat nat nat) (h : nat) :=
if (has P (iota 0 L)) then find_max_fixpoint_of_seq f sp h else None.

The result of find_max_fixpoint is a fixpoint of the function f for a an element of the search space.
Finally, we observe that there is no fixpoint in the search space larger than the result of find_maximum_fixpoint.