Library prosa.util.fixpoint

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

Require Export prosa.util.rel.
Require Export prosa.util.list.
Require Export prosa.util.option.
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.

  Lemma ffpf_finds_fixpoint :
    ∀ s x fuel: nat,
      find_fixpoint_from f s h fuel = Some x →
      x = f x.

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.

    Lemma ffpf_finds_least_fixpoint :
      ∀ y s fuel,
        find_fixpoint_from f s h fuel = Some y →
        ∀ x,
          s ≤ x < y →
          x != f x.

Hence find_fixpoint finds the least positive fixpoint of f.

    Corollary ffp_finds_least_fixpoint :
      ∀ x y,
        0 < x < y →
        find_fixpoint f h = Some y →
        x != f x.

Furthermore, we observe that find_fixpoint_from finds positive fixpoints when provided with a positive starting point s.

  Lemma ffpf_finds_positive_fixpoint :
    ∀ s fuel x,
      Some x = find_fixpoint_from f s h fuel →
      0 < s →
      0 < x.

Hence finds_fixpoint finds only positive fixpoints.

    Lemma ffp_finds_positive_fixpoint :
      ∀ x,
        Some x = find_fixpoint f h →
        0 < x.

If find_fixpoint_from finds no fixpoint between s and h, there is none.

    Lemma ffpf_finds_none :
      ∀ s fuel,
        s ≤ f s →
        fuel ≥ h - s →
        find_fixpoint_from f s h fuel = None →
        ∀ x,
          s ≤ x < h →
          x != f x.

Hence, if find_fixpoint finds no positive fixpoint less than h, there is none.

    Lemma ffp_finds_none :
      find_fixpoint f h = None →
        ∀ x,
        0 < x < h →
        x != f x.

  End MonotonicFunction.

End FixpointSearch.

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 ) unwrap 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.

Lemma fmfs_finds_fixpoint :
  ∀ (f : nat → nat → nat) (sp : seq nat) (h x : nat),
    ~~ nilp sp →
    find_max_fixpoint_of_seq f sp h = Some x →
    exists2 a , a \in sp & x = f a x.

Furthermore, we show that the result is the maximum of all fixpoints, with regard to the search space.

Lemma fmfs_is_maximum :
  ∀ (f : nat → nat → nat) (sp : seq nat) (h s r: nat),
    Some r = find_max_fixpoint_of_seq f sp h →
    s \in sp →
    exists2 v ,
      Some v = find_fixpoint (f s) h & r ≥ v.

Search Space Defined by a Predicate

Section PredicateSearchSpace.

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.

Let is_in_search_space A := (A < L ) && P A.

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.

  Corollary fmf_finds_fixpoint :
    ∀ (f : nat → nat → nat) (h x: nat),
      find_max_fixpoint f h = Some x →
      exists2 a , is_in_search_space a & x = f a x.

Finally, we observe that there is no fixpoint in the search space larger than the result of find_maximum_fixpoint.

  Corollary fmf_is_maximum :
    ∀ {f : nat → nat → nat} {h s r: nat},
      Some r = find_max_fixpoint f h →
      is_in_search_space s →
        exists2 v , Some v = find_fixpoint (f s) h & r ≥ v.

End PredicateSearchSpace.