From mathcomp Require Import ssreflect ssrbool eqtype ssrfun ssrnat seq fintype bigop path.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]

Require Export prosa.util.rel.
Require Export prosa.util.list.
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
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 :
    forall s x fuel: nat,
      find_fixpoint_from f s h fuel = Some x ->
      x = f x.
f: nat -> nat
h: nat
forall s x fuel : nat,
find_fixpoint_from f s h fuel = Some x -> x = f x
  Proof.
f: nat -> nat
h: nat
forall s x fuel : nat,
find_fixpoint_from f s h fuel = Some x -> x = f x
    move=> s x fuel.
f: nat -> nat
h, s, x, fuel: nat
find_fixpoint_from f s h fuel = Some x -> x = f x
    elim: fuel s => // fuel' IH s'.
f: nat -> nat
h, x, fuel': nat
IH: forall s : nat,
find_fixpoint_from f s h fuel' = Some x ->
x = f x
s': nat
find_fixpoint_from f s' h fuel'.+1 = Some x -> x = f x
    rewrite /find_fixpoint_from.
f: nat -> nat
h, x, fuel': nat
IH: forall s : nat,
find_fixpoint_from f s h fuel' = Some x ->
x = f x
s': nat
(if f s' == s'
 then Some s'
 else
  if f s' <= h
  then
   (fix find_fixpoint_from
      (f : nat -> nat) (x h fuel : nat) {struct fuel} :
        option nat :=
      match fuel with
      | 0 => None
      | fuel'.+1 =>
          if f x == x
          then Some x
          else
           if f x <= h
           then find_fixpoint_from f (f x) h fuel'
           else None
      end) f (f s') h fuel'
  else None) = Some x -> x = f x
    case: (eqVneq (f s') s') => [F [] <- // | _].
f: nat -> nat
h, x, fuel': nat
IH: forall s : nat,
find_fixpoint_from f s h fuel' = Some x ->
x = f x
s': nat
(if f s' <= h
 then
  (fix find_fixpoint_from
     (f : nat -> nat) (x h fuel : nat) {struct fuel} :
       option nat :=
     match fuel with
     | 0 => None
     | fuel'.+1 =>
         if f x == x
         then Some x
         else
          if f x <= h
          then find_fixpoint_from f (f x) h fuel'
          else None
     end) f (f s') h fuel'
 else None) = Some x -> x = f x
    rewrite -/find_fixpoint_from.
f: nat -> nat
h, x, fuel': nat
IH: forall s : nat,
find_fixpoint_from f s h fuel' = Some x ->
x = f x
s': nat
(if f s' <= h
 then find_fixpoint_from f (f s') h fuel'
 else None) = Some x -> x = f x
    by case: (f s' <= h).
  Qed.

  (** Using the above fact, we observe that the result of [find_fixpoint] is a
      fixpoint. *)
  Corollary ffp_finds_fixpoint :
    forall x : nat,
      find_fixpoint f h = Some x ->
      x = f x.
f: nat -> nat
h: nat
forall x : nat, find_fixpoint f h = Some x -> x = f x
  Proof.
f: nat -> nat
h: nat
forall x : nat, find_fixpoint f h = Some x -> x = f x by move=> x FOUND; apply: ffpf_finds_fixpoint FOUND. Qed.

  (** 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 :
      forall a c,
        c = f a ->
        forall b,
          a <= b < c ->
          b != f b.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
forall a c : nat,
c = f a -> forall b : nat, a <= b < c -> b != f b
    Proof.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
forall a c : nat,
c = f a -> forall b : nat, a <= b < c -> b != f b
      move=> a c EQ b /andP[LEQ LT].
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
a, c: nat
EQ: c = f a
b: nat
LEQ: a <= b
LT: b < c
b != f b
      move: (H_f_mono a b LEQ) => MONO.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
a, c: nat
EQ: c = f a
b: nat
LEQ: a <= b
LT: b < c
MONO: f a <= f b
b != f b
      by lia.
    Qed.

    (** It follows that [find_fixpoint_from] finds the least fixpoint larger
        than [s]. *)
    Lemma ffpf_finds_least_fixpoint :
      forall y s fuel,
        find_fixpoint_from f s h fuel = Some y ->
        forall x,
          s <= x < y ->
          x != f x.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
forall y s fuel : nat,
find_fixpoint_from f s h fuel = Some y ->
forall x : nat, s <= x < y -> x != f x
    Proof.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
forall y s fuel : nat,
find_fixpoint_from f s h fuel = Some y ->
forall x : nat, s <= x < y -> x != f x
      move=> y s fuel.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
y, s, fuel: nat
find_fixpoint_from f s h fuel = Some y ->
forall x : nat, s <= x < y -> x != f x
      elim: fuel s => // fuel' IH s FFP x /andP[LEQx LT].
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
y, fuel': nat
IH: forall s : nat,
find_fixpoint_from f s h fuel' = Some y ->
forall x : nat, s <= x < y -> x != f x
s: nat
FFP: find_fixpoint_from f s h fuel'.+1 = Some y
x: nat
LEQx: s <= x
LT: x < y
x != f x
      move: FFP; rewrite /find_fixpoint_from.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
y, fuel': nat
IH: forall s : nat,
find_fixpoint_from f s h fuel' = Some y ->
forall x : nat, s <= x < y -> x != f x
s, x: nat
LEQx: s <= x
LT: x < y
(if f s == s
 then Some s
 else
  if f s <= h
  then
   (fix find_fixpoint_from
      (f : nat -> nat) (x h fuel : nat) {struct fuel} :
        option nat :=
      match fuel with
      | 0 => None
      | fuel'.+1 =>
          if f x == x
          then Some x
          else
           if f x <= h
           then find_fixpoint_from f (f x) h fuel'
           else None
      end) f (f s) h fuel'
  else None) = Some y -> x != f x
      case: (eqVneq (f s) s);
        first by move=> EQ []; lia.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
y, fuel': nat
IH: forall s : nat,
find_fixpoint_from f s h fuel' = Some y ->
forall x : nat, s <= x < y -> x != f x
s, x: nat
LEQx: s <= x
LT: x < y
f s != s ->
(if f s <= h
 then
  (fix find_fixpoint_from
     (f : nat -> nat) (x h fuel : nat) {struct fuel} :
       option nat :=
     match fuel with
     | 0 => None
     | fuel'.+1 =>
         if f x == x
         then Some x
         else
          if f x <= h
          then find_fixpoint_from f (f x) h fuel'
          else None
     end) f (f s) h fuel'
 else None) = Some y -> x != f x
      move=> EQ.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
y, fuel': nat
IH: forall s : nat,
find_fixpoint_from f s h fuel' = Some y ->
forall x : nat, s <= x < y -> x != f x
s, x: nat
LEQx: s <= x
LT: x < y
EQ: f s != s
(if f s <= h
 then
  (fix find_fixpoint_from
     (f : nat -> nat) (x h fuel : nat) {struct fuel} :
       option nat :=
     match fuel with
     | 0 => None
     | fuel'.+1 =>
         if f x == x
         then Some x
         else
          if f x <= h
          then find_fixpoint_from f (f x) h fuel'
          else None
     end) f (f s) h fuel'
 else None) = Some y -> x != f x
      case: (leqP (f s) h) => // LEQh.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
y, fuel': nat
IH: forall s : nat,
find_fixpoint_from f s h fuel' = Some y ->
forall x : nat, s <= x < y -> x != f x
s, x: nat
LEQx: s <= x
LT: x < y
EQ: f s != s
LEQh: f s <= h
(fix find_fixpoint_from
   (f : nat -> nat) (x h fuel : nat) {struct fuel} :
     option nat :=
   match fuel with
   | 0 => None
   | fuel'.+1 =>
       if f x == x
       then Some x
       else
        if f x <= h
        then find_fixpoint_from f (f x) h fuel'
        else None
   end) f (f s) h fuel' = Some y -> x != f x
      rewrite -/find_fixpoint_from => FFP.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
y, fuel': nat
IH: forall s : nat,
find_fixpoint_from f s h fuel' = Some y ->
forall x : nat, s <= x < y -> x != f x
s, x: nat
LEQx: s <= x
LT: x < y
EQ: f s != s
LEQh: f s <= h
FFP: find_fixpoint_from f (f s) h fuel' = Some y
x != f x
      case: (leqP (f s) x) => [fsLEQs|sLTfs].
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
y, fuel': nat
IH: forall s : nat,
find_fixpoint_from f s h fuel' = Some y ->
forall x : nat, s <= x < y -> x != f x
s, x: nat
LEQx: s <= x
LT: x < y
EQ: f s != s
LEQh: f s <= h
FFP: find_fixpoint_from f (f s) h fuel' = Some y
fsLEQs: f s <= x
x != f x
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
y, fuel': nat
IH: forall s : nat,
find_fixpoint_from f s h fuel' = Some y ->
forall x : nat, s <= x < y -> x != f x
s, x: nat
LEQx: s <= x
LT: x < y
EQ: f s != s
LEQh: f s <= h
FFP: find_fixpoint_from f (f s) h fuel' = Some y
sLTfs: x < f s
x != f x
      {
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
y, fuel': nat
IH: forall s : nat,
find_fixpoint_from f s h fuel' = Some y ->
forall x : nat, s <= x < y -> x != f x
s, x: nat
LEQx: s <= x
LT: x < y
EQ: f s != s
LEQh: f s <= h
FFP: find_fixpoint_from f (f s) h fuel' = Some y
fsLEQs: f s <= x
x != f x apply: (IH (f s)) => //.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
y, fuel': nat
IH: forall s : nat,
find_fixpoint_from f s h fuel' = Some y ->
forall x : nat, s <= x < y -> x != f x
s, x: nat
LEQx: s <= x
LT: x < y
EQ: f s != s
LEQh: f s <= h
FFP: find_fixpoint_from f (f s) h fuel' = Some y
fsLEQs: f s <= x
f s <= x < y
        by apply /andP; split. }
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
y, fuel': nat
IH: forall s : nat,
find_fixpoint_from f s h fuel' = Some y ->
forall x : nat, s <= x < y -> x != f x
s, x: nat
LEQx: s <= x
LT: x < y
EQ: f s != s
LEQh: f s <= h
FFP: find_fixpoint_from f (f s) h fuel' = Some y
sLTfs: x < f s
x != f x
      {
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
y, fuel': nat
IH: forall s : nat,
find_fixpoint_from f s h fuel' = Some y ->
forall x : nat, s <= x < y -> x != f x
s, x: nat
LEQx: s <= x
LT: x < y
EQ: f s != s
LEQh: f s <= h
FFP: find_fixpoint_from f (f s) h fuel' = Some y
sLTfs: x < f s
x != f x apply: (no_fixpoint_skipped s (f s)) => //.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
y, fuel': nat
IH: forall s : nat,
find_fixpoint_from f s h fuel' = Some y ->
forall x : nat, s <= x < y -> x != f x
s, x: nat
LEQx: s <= x
LT: x < y
EQ: f s != s
LEQh: f s <= h
FFP: find_fixpoint_from f (f s) h fuel' = Some y
sLTfs: x < f s
s <= x < f s
        by apply /andP; split. }
    Qed.

    (** Hence [find_fixpoint] finds the least positive fixpoint of [f]. *)
    Corollary ffp_finds_least_fixpoint :
      forall x y,
        0 < x < y ->
        find_fixpoint f h = Some y ->
        x != f x.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
forall x y : nat,
0 < x < y -> find_fixpoint f h = Some y -> x != f x
    Proof.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
forall x y : nat,
0 < x < y -> find_fixpoint f h = Some y -> x != f x by move=> x y LT FFP; apply: ffpf_finds_least_fixpoint; eauto. Qed.

  (** Furthermore, we observe that [find_fixpoint_from] finds positive fixpoints
      when provided with a positive starting point [s]. *)
  Lemma ffpf_finds_positive_fixpoint :
    forall s fuel x,
      Some x = find_fixpoint_from f s h fuel ->
      0 < s ->
      0 < x.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
forall s fuel x : nat,
Some x = find_fixpoint_from f s h fuel ->
0 < s -> 0 < x
  Proof.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
forall s fuel x : nat,
Some x = find_fixpoint_from f s h fuel ->
0 < s -> 0 < x
    move=> s fuel x.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
s, fuel, x: nat
Some x = find_fixpoint_from f s h fuel ->
0 < s -> 0 < x
    rewrite /find_fixpoint_from.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
s, fuel, x: nat
Some x =
(fix find_fixpoint_from
   (f : nat -> nat) (x h fuel : nat) {struct fuel} :
     option nat :=
   match fuel with
   | 0 => None
   | fuel'.+1 =>
       if f x == x
       then Some x
       else
        if f x <= h
        then find_fixpoint_from f (f x) h fuel'
        else None
   end) f s h fuel -> 0 < s -> 0 < x
    elim: fuel s => // fuel' IH s.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
x, fuel': nat
IH: forall s : nat,
Some x =
(fix find_fixpoint_from
   (f : nat -> nat) (x h fuel : nat) {struct
    fuel} : option nat :=
   match fuel with
   | 0 => None
   | fuel'.+1 =>
       if f x == x
       then Some x
       else
        if f x <= h
        then find_fixpoint_from f (f x) h fuel'
        else None
   end) f s h fuel' -> 
0 < s -> 0 < x
s: nat
Some x =
(if f s == s
 then Some s
 else
  if f s <= h
  then
   (fix find_fixpoint_from
      (f : nat -> nat) (x h fuel : nat) {struct fuel} :
        option nat :=
      match fuel with
      | 0 => None
      | fuel'.+1 =>
          if f x == x
          then Some x
          else
           if f x <= h
           then find_fixpoint_from f (f x) h fuel'
           else None
      end) f (f s) h fuel'
  else None) -> 0 < s -> 0 < x
    case: (eqVneq (f s) s) => [_ SOME | NEQ].
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
x, fuel': nat
IH: forall s : nat,
Some x =
(fix find_fixpoint_from
   (f : nat -> nat) (x h fuel : nat) {struct
    fuel} : option nat :=
   match fuel with
   | 0 => None
   | fuel'.+1 =>
       if f x == x
       then Some x
       else
        if f x <= h
        then find_fixpoint_from f (f x) h fuel'
        else None
   end) f s h fuel' -> 
0 < s -> 0 < x
s: nat
SOME: Some x = Some s
0 < s -> 0 < x
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
x, fuel': nat
IH: forall s : nat,
Some x =
(fix find_fixpoint_from
   (f : nat -> nat) (x h fuel : nat) {struct
    fuel} : option nat :=
   match fuel with
   | 0 => None
   | fuel'.+1 =>
       if f x == x
       then Some x
       else
        if f x <= h
        then find_fixpoint_from f (f x) h fuel'
        else None
   end) f s h fuel' -> 
0 < s -> 0 < x
s: nat
NEQ: f s != s
Some x =
(if f s <= h
 then
  (fix find_fixpoint_from
     (f : nat -> nat) (x h fuel : nat) {struct fuel} :
       option nat :=
     match fuel with
     | 0 => None
     | fuel'.+1 =>
         if f x == x
         then Some x
         else
          if f x <= h
          then find_fixpoint_from f (f x) h fuel'
          else None
     end) f (f s) h fuel'
 else None) -> 0 < s -> 0 < x
    -
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
x, fuel': nat
IH: forall s : nat,
Some x =
(fix find_fixpoint_from
   (f : nat -> nat) (x h fuel : nat) {struct
    fuel} : option nat :=
   match fuel with
   | 0 => None
   | fuel'.+1 =>
       if f x == x
       then Some x
       else
        if f x <= h
        then find_fixpoint_from f (f x) h fuel'
        else None
   end) f s h fuel' -> 
0 < s -> 0 < x
s: nat
SOME: Some x = Some s
0 < s -> 0 < x by move: SOME => []; lia.
    -
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
x, fuel': nat
IH: forall s : nat,
Some x =
(fix find_fixpoint_from
   (f : nat -> nat) (x h fuel : nat) {struct
    fuel} : option nat :=
   match fuel with
   | 0 => None
   | fuel'.+1 =>
       if f x == x
       then Some x
       else
        if f x <= h
        then find_fixpoint_from f (f x) h fuel'
        else None
   end) f s h fuel' -> 
0 < s -> 0 < x
s: nat
NEQ: f s != s
Some x =
(if f s <= h
 then
  (fix find_fixpoint_from
     (f : nat -> nat) (x h fuel : nat) {struct fuel} :
       option nat :=
     match fuel with
     | 0 => None
     | fuel'.+1 =>
         if f x == x
         then Some x
         else
          if f x <= h
          then find_fixpoint_from f (f x) h fuel'
          else None
     end) f (f s) h fuel'
 else None) -> 0 < s -> 0 < x case (f s <= h) => // SOME GT.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
x, fuel': nat
IH: forall s : nat,
Some x =
(fix find_fixpoint_from
   (f : nat -> nat) (x h fuel : nat) {struct
    fuel} : option nat :=
   match fuel with
   | 0 => None
   | fuel'.+1 =>
       if f x == x
       then Some x
       else
        if f x <= h
        then find_fixpoint_from f (f x) h fuel'
        else None
   end) f s h fuel' -> 
0 < s -> 0 < x
s: nat
NEQ: f s != s
SOME: Some x =
(fix find_fixpoint_from
   (f : nat -> nat) (x h fuel : nat) {struct
    fuel} : option nat :=
   match fuel with
   | 0 => None
   | fuel'.+1 =>
       if f x == x
       then Some x
       else
        if f x <= h
        then find_fixpoint_from f (f x) h fuel'
        else None
   end) f (f s) h fuel'
GT: 0 < s
0 < x
      have: 0 < f s.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
x, fuel': nat
IH: forall s : nat,
Some x =
(fix find_fixpoint_from
   (f : nat -> nat) (x h fuel : nat) {struct
    fuel} : option nat :=
   match fuel with
   | 0 => None
   | fuel'.+1 =>
       if f x == x
       then Some x
       else
        if f x <= h
        then find_fixpoint_from f (f x) h fuel'
        else None
   end) f s h fuel' -> 
0 < s -> 0 < x
s: nat
NEQ: f s != s
SOME: Some x =
(fix find_fixpoint_from
   (f : nat -> nat) (x h fuel : nat) {struct
    fuel} : option nat :=
   match fuel with
   | 0 => None
   | fuel'.+1 =>
       if f x == x
       then Some x
       else
        if f x <= h
        then find_fixpoint_from f (f x) h fuel'
        else None
   end) f (f s) h fuel'
GT: 0 < s
0 < f s
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
x, fuel': nat
IH: forall s : nat,
Some x =
(fix find_fixpoint_from
   (f : nat -> nat) (x h fuel : nat) {struct
    fuel} : option nat :=
   match fuel with
   | 0 => None
   | fuel'.+1 =>
       if f x == x
       then Some x
       else
        if f x <= h
        then find_fixpoint_from f (f x) h fuel'
        else None
   end) f s h fuel' -> 
0 < s -> 0 < x
s: nat
NEQ: f s != s
SOME: Some x =
(fix find_fixpoint_from
   (f : nat -> nat) (x h fuel : nat) {struct
    fuel} : option nat :=
   match fuel with
   | 0 => None
   | fuel'.+1 =>
       if f x == x
       then Some x
       else
        if f x <= h
        then find_fixpoint_from f (f x) h fuel'
        else None
   end) f (f s) h fuel'
GT: 0 < s
0 < f s -> 0 < x {
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
x, fuel': nat
IH: forall s : nat,
Some x =
(fix find_fixpoint_from
   (f : nat -> nat) (x h fuel : nat) {struct
    fuel} : option nat :=
   match fuel with
   | 0 => None
   | fuel'.+1 =>
       if f x == x
       then Some x
       else
        if f x <= h
        then find_fixpoint_from f (f x) h fuel'
        else None
   end) f s h fuel' -> 
0 < s -> 0 < x
s: nat
NEQ: f s != s
SOME: Some x =
(fix find_fixpoint_from
   (f : nat -> nat) (x h fuel : nat) {struct
    fuel} : option nat :=
   match fuel with
   | 0 => None
   | fuel'.+1 =>
       if f x == x
       then Some x
       else
        if f x <= h
        then find_fixpoint_from f (f x) h fuel'
        else None
   end) f (f s) h fuel'
GT: 0 < s
0 < f s by move: (H_f_mono 1 s GT) => MONO; lia. }
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
x, fuel': nat
IH: forall s : nat,
Some x =
(fix find_fixpoint_from
   (f : nat -> nat) (x h fuel : nat) {struct
    fuel} : option nat :=
   match fuel with
   | 0 => None
   | fuel'.+1 =>
       if f x == x
       then Some x
       else
        if f x <= h
        then find_fixpoint_from f (f x) h fuel'
        else None
   end) f s h fuel' -> 
0 < s -> 0 < x
s: nat
NEQ: f s != s
SOME: Some x =
(fix find_fixpoint_from
   (f : nat -> nat) (x h fuel : nat) {struct
    fuel} : option nat :=
   match fuel with
   | 0 => None
   | fuel'.+1 =>
       if f x == x
       then Some x
       else
        if f x <= h
        then find_fixpoint_from f (f x) h fuel'
        else None
   end) f (f s) h fuel'
GT: 0 < s
0 < f s -> 0 < x
      by apply (IH (f s)).
    Qed.

    (** Hence [finds_fixpoint] finds only positive fixpoints. *)
    Lemma ffp_finds_positive_fixpoint :
      forall x,
        Some x = find_fixpoint f h ->
        0 < x.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
forall x : nat, Some x = find_fixpoint f h -> 0 < x
    Proof.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
forall x : nat, Some x = find_fixpoint f h -> 0 < x
      move=> x.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
x: nat
Some x = find_fixpoint f h -> 0 < x
      rewrite /find_fixpoint => FIX.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
x: nat
FIX: Some x = find_fixpoint_from f 1 h h
0 < x
      by apply: ffpf_finds_positive_fixpoint; first apply FIX.
    Qed.

    (** If [find_fixpoint_from] finds no fixpoint between s and h,
        there is none. *)
    Lemma ffpf_finds_none :
      forall s fuel,
        s <= f s ->
        fuel >= h - s ->
        find_fixpoint_from f s h fuel = None ->
        forall x,
          s <= x < h ->
          x != f x.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
forall s fuel : nat,
s <= f s ->
h - s <= fuel ->
find_fixpoint_from f s h fuel = None ->
forall x : nat, s <= x < h -> x != f x
    Proof.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
forall s fuel : nat,
s <= f s ->
h - s <= fuel ->
find_fixpoint_from f s h fuel = None ->
forall x : nat, s <= x < h -> x != f x
      move=> s fuel.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
s, fuel: nat
s <= f s ->
h - s <= fuel ->
find_fixpoint_from f s h fuel = None ->
forall x : nat, s <= x < h -> x != f x
      elim: fuel s => [|fuel' IH s GEQ FUEL]; first by lia.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
fuel': nat
IH: forall s : nat,
s <= f s ->
h - s <= fuel' ->
find_fixpoint_from f s h fuel' = None ->
forall x : nat, s <= x < h -> x != f x
s: nat
GEQ: s <= f s
FUEL: h - s <= fuel'.+1
find_fixpoint_from f s h fuel'.+1 = None ->
forall x : nat, s <= x < h -> x != f x
      rewrite /find_fixpoint_from.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
fuel': nat
IH: forall s : nat,
s <= f s ->
h - s <= fuel' ->
find_fixpoint_from f s h fuel' = None ->
forall x : nat, s <= x < h -> x != f x
s: nat
GEQ: s <= f s
FUEL: h - s <= fuel'.+1
(if f s == s
 then Some s
 else
  if f s <= h
  then
   (fix find_fixpoint_from
      (f : nat -> nat) (x h fuel : nat) {struct fuel} :
        option nat :=
      match fuel with
      | 0 => None
      | fuel'.+1 =>
          if f x == x
          then Some x
          else
           if f x <= h
           then find_fixpoint_from f (f x) h fuel'
           else None
      end) f (f s) h fuel'
  else None) = None ->
forall x : nat, s <= x < h -> x != f x
      case: (eqVneq (f s) s) => // F.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
fuel': nat
IH: forall s : nat,
s <= f s ->
h - s <= fuel' ->
find_fixpoint_from f s h fuel' = None ->
forall x : nat, s <= x < h -> x != f x
s: nat
GEQ: s <= f s
FUEL: h - s <= fuel'.+1
F: f s != s
(if f s <= h
 then
  (fix find_fixpoint_from
     (f : nat -> nat) (x h fuel : nat) {struct fuel} :
       option nat :=
     match fuel with
     | 0 => None
     | fuel'.+1 =>
         if f x == x
         then Some x
         else
          if f x <= h
          then find_fixpoint_from f (f x) h fuel'
          else None
     end) f (f s) h fuel'
 else None) = None ->
forall x : nat, s <= x < h -> x != f x
      case: (leqP (f s) h) => [_ | GTNh _]; last first.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
fuel': nat
IH: forall s : nat,
s <= f s ->
h - s <= fuel' ->
find_fixpoint_from f s h fuel' = None ->
forall x : nat, s <= x < h -> x != f x
s: nat
GEQ: s <= f s
FUEL: h - s <= fuel'.+1
F: f s != s
GTNh: h < f s
forall x : nat, s <= x < h -> x != f x
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
fuel': nat
IH: forall s : nat,
s <= f s ->
h - s <= fuel' ->
find_fixpoint_from f s h fuel' = None ->
forall x : nat, s <= x < h -> x != f x
s: nat
GEQ: s <= f s
FUEL: h - s <= fuel'.+1
F: f s != s
(fix find_fixpoint_from
   (f : nat -> nat) (x h fuel : nat) {struct fuel} :
     option nat :=
   match fuel with
   | 0 => None
   | fuel'.+1 =>
       if f x == x
       then Some x
       else
        if f x <= h
        then find_fixpoint_from f (f x) h fuel'
        else None
   end) f (f s) h fuel' = None ->
forall x : nat, s <= x < h -> x != f x
      {
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
fuel': nat
IH: forall s : nat,
s <= f s ->
h - s <= fuel' ->
find_fixpoint_from f s h fuel' = None ->
forall x : nat, s <= x < h -> x != f x
s: nat
GEQ: s <= f s
FUEL: h - s <= fuel'.+1
F: f s != s
GTNh: h < f s
forall x : nat, s <= x < h -> x != f x rewrite -/find_fixpoint_from => x /andP[SX LT].
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
fuel': nat
IH: forall s : nat,
s <= f s ->
h - s <= fuel' ->
find_fixpoint_from f s h fuel' = None ->
forall x : nat, s <= x < h -> x != f x
s: nat
GEQ: s <= f s
FUEL: h - s <= fuel'.+1
F: f s != s
GTNh: h < f s
x: nat
SX: s <= x
LT: x < h
x != f x
        apply: (no_fixpoint_skipped s) => //.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
fuel': nat
IH: forall s : nat,
s <= f s ->
h - s <= fuel' ->
find_fixpoint_from f s h fuel' = None ->
forall x : nat, s <= x < h -> x != f x
s: nat
GEQ: s <= f s
FUEL: h - s <= fuel'.+1
F: f s != s
GTNh: h < f s
x: nat
SX: s <= x
LT: x < h
s <= x < f s
        apply /andP; split => //.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
fuel': nat
IH: forall s : nat,
s <= f s ->
h - s <= fuel' ->
find_fixpoint_from f s h fuel' = None ->
forall x : nat, s <= x < h -> x != f x
s: nat
GEQ: s <= f s
FUEL: h - s <= fuel'.+1
F: f s != s
GTNh: h < f s
x: nat
SX: s <= x
LT: x < h
x < f s
        by apply: ltn_trans LT GTNh. }
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
fuel': nat
IH: forall s : nat,
s <= f s ->
h - s <= fuel' ->
find_fixpoint_from f s h fuel' = None ->
forall x : nat, s <= x < h -> x != f x
s: nat
GEQ: s <= f s
FUEL: h - s <= fuel'.+1
F: f s != s
(fix find_fixpoint_from
   (f : nat -> nat) (x h fuel : nat) {struct fuel} :
     option nat :=
   match fuel with
   | 0 => None
   | fuel'.+1 =>
       if f x == x
       then Some x
       else
        if f x <= h
        then find_fixpoint_from f (f x) h fuel'
        else None
   end) f (f s) h fuel' = None ->
forall x : nat, s <= x < h -> x != f x
      {
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
fuel': nat
IH: forall s : nat,
s <= f s ->
h - s <= fuel' ->
find_fixpoint_from f s h fuel' = None ->
forall x : nat, s <= x < h -> x != f x
s: nat
GEQ: s <= f s
FUEL: h - s <= fuel'.+1
F: f s != s
(fix find_fixpoint_from
   (f : nat -> nat) (x h fuel : nat) {struct fuel} :
     option nat :=
   match fuel with
   | 0 => None
   | fuel'.+1 =>
       if f x == x
       then Some x
       else
        if f x <= h
        then find_fixpoint_from f (f x) h fuel'
        else None
   end) f (f s) h fuel' = None ->
forall x : nat, s <= x < h -> x != f x rewrite -/find_fixpoint_from => FFP x /andP[SX XH].
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
fuel': nat
IH: forall s : nat,
s <= f s ->
h - s <= fuel' ->
find_fixpoint_from f s h fuel' = None ->
forall x : nat, s <= x < h -> x != f x
s: nat
GEQ: s <= f s
FUEL: h - s <= fuel'.+1
F: f s != s
FFP: find_fixpoint_from f (f s) h fuel' = None
x: nat
SX: s <= x
XH: x < h
x != f x
        case: (leqP (f s) x) => FSX.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
fuel': nat
IH: forall s : nat,
s <= f s ->
h - s <= fuel' ->
find_fixpoint_from f s h fuel' = None ->
forall x : nat, s <= x < h -> x != f x
s: nat
GEQ: s <= f s
FUEL: h - s <= fuel'.+1
F: f s != s
FFP: find_fixpoint_from f (f s) h fuel' = None
x: nat
SX: s <= x
XH: x < h
FSX: f s <= x
x != f x
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
fuel': nat
IH: forall s : nat,
s <= f s ->
h - s <= fuel' ->
find_fixpoint_from f s h fuel' = None ->
forall x : nat, s <= x < h -> x != f x
s: nat
GEQ: s <= f s
FUEL: h - s <= fuel'.+1
F: f s != s
FFP: find_fixpoint_from f (f s) h fuel' = None
x: nat
SX: s <= x
XH: x < h
FSX: x < f s
x != f x
        {
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
fuel': nat
IH: forall s : nat,
s <= f s ->
h - s <= fuel' ->
find_fixpoint_from f s h fuel' = None ->
forall x : nat, s <= x < h -> x != f x
s: nat
GEQ: s <= f s
FUEL: h - s <= fuel'.+1
F: f s != s
FFP: find_fixpoint_from f (f s) h fuel' = None
x: nat
SX: s <= x
XH: x < h
FSX: f s <= x
x != f x apply: (IH (f s)) => //.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
fuel': nat
IH: forall s : nat,
s <= f s ->
h - s <= fuel' ->
find_fixpoint_from f s h fuel' = None ->
forall x : nat, s <= x < h -> x != f x
s: nat
GEQ: s <= f s
FUEL: h - s <= fuel'.+1
F: f s != s
FFP: find_fixpoint_from f (f s) h fuel' = None
x: nat
SX: s <= x
XH: x < h
FSX: f s <= x
h - f s <= fuel'
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
fuel': nat
IH: forall s : nat,
s <= f s ->
h - s <= fuel' ->
find_fixpoint_from f s h fuel' = None ->
forall x : nat, s <= x < h -> x != f x
s: nat
GEQ: s <= f s
FUEL: h - s <= fuel'.+1
F: f s != s
FFP: find_fixpoint_from f (f s) h fuel' = None
x: nat
SX: s <= x
XH: x < h
FSX: f s <= x
f s <= x < h
          -
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
fuel': nat
IH: forall s : nat,
s <= f s ->
h - s <= fuel' ->
find_fixpoint_from f s h fuel' = None ->
forall x : nat, s <= x < h -> x != f x
s: nat
GEQ: s <= f s
FUEL: h - s <= fuel'.+1
F: f s != s
FFP: find_fixpoint_from f (f s) h fuel' = None
x: nat
SX: s <= x
XH: x < h
FSX: f s <= x
h - f s <= fuel' by lia.
          -
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
fuel': nat
IH: forall s : nat,
s <= f s ->
h - s <= fuel' ->
find_fixpoint_from f s h fuel' = None ->
forall x : nat, s <= x < h -> x != f x
s: nat
GEQ: s <= f s
FUEL: h - s <= fuel'.+1
F: f s != s
FFP: find_fixpoint_from f (f s) h fuel' = None
x: nat
SX: s <= x
XH: x < h
FSX: f s <= x
f s <= x < h by apply /andP; split. }
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
fuel': nat
IH: forall s : nat,
s <= f s ->
h - s <= fuel' ->
find_fixpoint_from f s h fuel' = None ->
forall x : nat, s <= x < h -> x != f x
s: nat
GEQ: s <= f s
FUEL: h - s <= fuel'.+1
F: f s != s
FFP: find_fixpoint_from f (f s) h fuel' = None
x: nat
SX: s <= x
XH: x < h
FSX: x < f s
x != f x
        {
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
fuel': nat
IH: forall s : nat,
s <= f s ->
h - s <= fuel' ->
find_fixpoint_from f s h fuel' = None ->
forall x : nat, s <= x < h -> x != f x
s: nat
GEQ: s <= f s
FUEL: h - s <= fuel'.+1
F: f s != s
FFP: find_fixpoint_from f (f s) h fuel' = None
x: nat
SX: s <= x
XH: x < h
FSX: x < f s
x != f x apply: (no_fixpoint_skipped s) => //.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
fuel': nat
IH: forall s : nat,
s <= f s ->
h - s <= fuel' ->
find_fixpoint_from f s h fuel' = None ->
forall x : nat, s <= x < h -> x != f x
s: nat
GEQ: s <= f s
FUEL: h - s <= fuel'.+1
F: f s != s
FFP: find_fixpoint_from f (f s) h fuel' = None
x: nat
SX: s <= x
XH: x < h
FSX: x < f s
s <= x < f s
          by apply /andP; split. }}
    Qed.

    (** Hence, if [find_fixpoint] finds no positive fixpoint less than h, there
        is none. *)
    Lemma ffp_finds_none :
      find_fixpoint f h = None ->
        forall x,
        0 < x < h ->
        x != f x.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
find_fixpoint f h = None ->
forall x : nat, 0 < x < h -> x != f x
    Proof.
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
find_fixpoint f h = None ->
forall x : nat, 0 < x < h -> x != f x
      move=> FFP x /andP [POS LT].
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
FFP: find_fixpoint f h = None
x: nat
POS: 0 < x
LT: x < h
x != f x
      apply: (ffpf_finds_none 1 h).
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
FFP: find_fixpoint f h = None
x: nat
POS: 0 < x
LT: x < h
0 < f 1
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
FFP: find_fixpoint f h = None
x: nat
POS: 0 < x
LT: x < h
h - 1 <= h
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
FFP: find_fixpoint f h = None
x: nat
POS: 0 < x
LT: x < h
find_fixpoint_from f 1 h h = None
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
FFP: find_fixpoint f h = None
x: nat
POS: 0 < x
LT: x < h
0 < x < h
      -
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
FFP: find_fixpoint f h = None
x: nat
POS: 0 < x
LT: x < h
0 < f 1 by move: F1; case (f 1) => //.
      -
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
FFP: find_fixpoint f h = None
x: nat
POS: 0 < x
LT: x < h
h - 1 <= h by rewrite subn1; exact /leq_pred.
      -
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
FFP: find_fixpoint f h = None
x: nat
POS: 0 < x
LT: x < h
find_fixpoint_from f 1 h h = None by exact: FFP.
      -
f: nat -> nat
h: nat
H_f_mono: monotone leq f
F1: 0 < f 1
FFP: find_fixpoint f h = None
x: nat
POS: 0 < x
LT: x < h
0 < x < h by apply /andP; split.
    Qed.

  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) (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. *)
Lemma fmfs_finds_fixpoint :
  forall (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.
forall (f : nat -> nat -> nat) (sp : seq nat)
  (h x : nat),
~~ nilp sp ->
find_max_fixpoint_of_seq f sp h = Some x ->
exists2 a : Datatypes_nat__canonical__eqtype_Equality,
  a \in sp & x = f a x
Proof.
forall (f : nat -> nat -> nat) (sp : seq nat)
  (h x : nat),
~~ nilp sp ->
find_max_fixpoint_of_seq f sp h = Some x ->
exists2 a : Datatypes_nat__canonical__eqtype_Equality,
  a \in sp & x = f a x
  move=> f sp h x NN.
f: nat -> nat -> nat
sp: seq nat
h, x: nat
NN: ~~ nilp sp
find_max_fixpoint_of_seq f sp h = Some x ->
exists2 a : Datatypes_nat__canonical__eqtype_Equality,
  a \in sp & x = f a x
  rewrite /find_max_fixpoint_of_seq //=.
f: nat -> nat -> nat
sp: seq nat
h, x: nat
NN: ~~ nilp sp
(if
  all (fun opt : option nat => opt != None)
    [seq find_fixpoint (f s) h | s <- sp]
 then
  Some
    (\max_(fp <- [seq find_fixpoint (f s) h | s <- sp] | 
     fp != None) odflt 0 fp)
 else None) = Some x ->
exists2 a : nat, a \in sp & x = f a x
  set fps := [seq find_fixpoint (f s) h | s <- sp] => H.
f: nat -> nat -> nat
sp: seq nat
h, x: nat
NN: ~~ nilp sp
fps:= [seq find_fixpoint (f s) h | s <- sp]: seq (option nat)
H: (if all (fun opt : option nat => opt != None) fps
 then
  Some (\max_(fp <- fps | fp != None) odflt 0 fp)
 else None) = Some x
exists2 a : nat, a \in sp & x = f a x
  have ALL: all (fun opt => opt != None) fps
              by case: (all _ _) H => //.
f: nat -> nat -> nat
sp: seq nat
h, x: nat
NN: ~~ nilp sp
fps:= [seq find_fixpoint (f s) h | s <- sp]: seq (option nat)
H: (if all (fun opt : option nat => opt != None) fps
 then
  Some (\max_(fp <- fps | fp != None) odflt 0 fp)
 else None) = Some x
ALL: all
(fun
opt : Datatypes_option__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality => opt != None) fps
exists2 a : nat, a \in sp & x = f a x
  move: H.
f: nat -> nat -> nat
sp: seq nat
h, x: nat
NN: ~~ nilp sp
fps:= [seq find_fixpoint (f s) h | s <- sp]: seq (option nat)
ALL: all
(fun
opt : Datatypes_option__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality => opt != None) fps
(if all (fun opt : option nat => opt != None) fps
 then Some (\max_(fp <- fps | fp != None) odflt 0 fp)
 else None) = Some x ->
exists2 a : nat, a \in sp & x = f a x rewrite ifT //; move => [] H.
f: nat -> nat -> nat
sp: seq nat
h, x: nat
NN: ~~ nilp sp
fps:= [seq find_fixpoint (f s) h | s <- sp]: seq (option nat)
ALL: all
(fun
opt : Datatypes_option__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality => opt != None) fps
H: \max_(fp <- fps | fp != None) odflt 0 fp = x
exists2 a : nat, a \in sp & x = f a x
  have NN': ~~ nilp fps
    by rewrite /fps /nilp size_map -/(nilp sp).
f: nat -> nat -> nat
sp: seq nat
h, x: nat
NN: ~~ nilp sp
fps:= [seq find_fixpoint (f s) h | s <- sp]: seq (option nat)
ALL: all
(fun
opt : Datatypes_option__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality => opt != None) fps
H: \max_(fp <- fps | fp != None) odflt 0 fp = x
NN': ~~ nilp fps
exists2 a : nat, a \in sp & x = f a x
  move: (bigmax_witness
           (fun fp => match fp with | Some x' => x' | None => 0 end)
           (has_all_nilp _ _ ALL NN'))
      => //= [w [IN [SOME MAX]]].
f: nat -> nat -> nat
sp: seq nat
h, x: nat
NN: ~~ nilp sp
fps:= [seq find_fixpoint (f s) h | s <- sp]: seq (option nat)
ALL: all
(fun
opt : Datatypes_option__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality => opt != None) fps
H: \max_(fp <- fps | fp != None) odflt 0 fp = x
NN': ~~ nilp fps
w: option nat
IN: w \in fps
SOME: w != None
MAX: match w with
| Some x' => x'
| None => 0
end =
\max_(x <- fps | x != None)
   match x with
   | Some x' => x'
   | None => 0
   end
exists2 a : nat, a \in sp & x = f a x
  case: w IN SOME MAX => // w IN _.
f: nat -> nat -> nat
sp: seq nat
h, x: nat
NN: ~~ nilp sp
fps:= [seq find_fixpoint (f s) h | s <- sp]: seq (option nat)
ALL: all
(fun
opt : Datatypes_option__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality => opt != None) fps
H: \max_(fp <- fps | fp != None) odflt 0 fp = x
NN': ~~ nilp fps
w: nat
IN: Some w \in fps
w =
\max_(x <- fps | x != None)
   match x with
   | Some x' => x'
   | None => 0
   end -> exists2 a : nat, a \in sp & x = f a x
  rewrite {}H => WX.
f: nat -> nat -> nat
sp: seq nat
h, x: nat
NN: ~~ nilp sp
fps:= [seq find_fixpoint (f s) h | s <- sp]: seq (option nat)
ALL: all
(fun
opt : Datatypes_option__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality => opt != None) fps
NN': ~~ nilp fps
w: nat
IN: Some w \in fps
WX: w = x
exists2 a : nat, a \in sp & x = f a x
  move: IN; rewrite WX /fps => /mapP [a IN FIX].
f: nat -> nat -> nat
sp: seq nat
h, x: nat
NN: ~~ nilp sp
fps:= [seq find_fixpoint (f s) h | s <- sp]: seq (option nat)
ALL: all
(fun
opt : Datatypes_option__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality => opt != None) fps
NN': ~~ nilp fps
w: nat
WX: w = x
a: Datatypes_nat__canonical__eqtype_Equality
IN: a \in sp
FIX: Some x = find_fixpoint (f a) h
exists2 a : nat, a \in sp & x = f a x
  exists a => //.
f: nat -> nat -> nat
sp: seq nat
h, x: nat
NN: ~~ nilp sp
fps:= [seq find_fixpoint (f s) h | s <- sp]: seq (option nat)
ALL: all
(fun
opt : Datatypes_option__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality => opt != None) fps
NN': ~~ nilp fps
w: nat
WX: w = x
a: Datatypes_nat__canonical__eqtype_Equality
IN: a \in sp
FIX: Some x = find_fixpoint (f a) h
x = f a x
  by eapply ffp_finds_fixpoint, ssrfun.esym, FIX.
Qed.

(** Furthermore, we show that the result is the maximum of all fixpoints, with
    regard to the search space.*)
Lemma fmfs_is_maximum :
  forall (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.
forall (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 : nat,
  Some v = find_fixpoint (f s) h & v <= r
Proof.
forall (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 : nat,
  Some v = find_fixpoint (f s) h & v <= r
  move=> f sp h s r.
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 : nat,
  Some v = find_fixpoint (f s) h & v <= r
  rewrite /find_max_fixpoint_of_seq //=.
f: nat -> nat -> nat
sp: seq nat
h, s, r: nat
Some r =
(if
  all (fun opt : option nat => opt != None)
    [seq find_fixpoint (f s) h | s <- sp]
 then
  Some
    (\max_(fp <- [seq find_fixpoint (f s) h | s <- sp] | 
     fp != None) odflt 0 fp)
 else None) ->
s \in sp ->
exists2 v : nat,
  Some v = find_fixpoint (f s) h & v <= r
  set fps := [seq find_fixpoint (f s) h | s <- sp] => H.
f: nat -> nat -> nat
sp: seq nat
h, s, r: nat
fps:= [seq find_fixpoint (f s) h | s <- sp]: seq (option nat)
H: Some r =
(if all (fun opt : option nat => opt != None) fps
 then
  Some (\max_(fp <- fps | fp != None) odflt 0 fp)
 else None)
s \in sp ->
exists2 v : nat,
  Some v = find_fixpoint (f s) h & v <= r
  have ALL : all (fun opt => opt != None) fps
    by case: (all _ _) H => //.
f: nat -> nat -> nat
sp: seq nat
h, s, r: nat
fps:= [seq find_fixpoint (f s) h | s <- sp]: seq (option nat)
H: Some r =
(if all (fun opt : option nat => opt != None) fps
 then
  Some (\max_(fp <- fps | fp != None) odflt 0 fp)
 else None)
ALL: all
(fun
opt : Datatypes_option__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality => opt != None) fps
s \in sp ->
exists2 v : nat,
  Some v = find_fixpoint (f s) h & v <= r
  move: H.
f: nat -> nat -> nat
sp: seq nat
h, s, r: nat
fps:= [seq find_fixpoint (f s) h | s <- sp]: seq (option nat)
ALL: all
(fun
opt : Datatypes_option__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality => opt != None) fps
Some r =
(if all (fun opt : option nat => opt != None) fps
 then Some (\max_(fp <- fps | fp != None) odflt 0 fp)
 else None) ->
s \in sp ->
exists2 v : nat,
  Some v = find_fixpoint (f s) h & v <= r rewrite ifT //; move => [] H IN.
f: nat -> nat -> nat
sp: seq nat
h, s, r: nat
fps:= [seq find_fixpoint (f s) h | s <- sp]: seq (option nat)
ALL: all
(fun
opt : Datatypes_option__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality => opt != None) fps
H: r = \max_(fp <- fps | fp != None) odflt 0 fp
IN: s \in sp
exists2 v : nat,
  Some v = find_fixpoint (f s) h & v <= r
  exists ((odflt 0) (find_fixpoint (f s) h)).
f: nat -> nat -> nat
sp: seq nat
h, s, r: nat
fps:= [seq find_fixpoint (f s) h | s <- sp]: seq (option nat)
ALL: all
(fun
opt : Datatypes_option__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality => opt != None) fps
H: r = \max_(fp <- fps | fp != None) odflt 0 fp
IN: s \in sp
Some (odflt 0 (find_fixpoint (f s) h)) =
find_fixpoint (f s) h
f: nat -> nat -> nat
sp: seq nat
h, s, r: nat
fps:= [seq find_fixpoint (f s) h | s <- sp]: seq (option nat)
ALL: all
(fun
opt : Datatypes_option__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality => opt != None) fps
H: r = \max_(fp <- fps | fp != None) odflt 0 fp
IN: s \in sp
odflt 0 (find_fixpoint (f s) h) <= r
  -
f: nat -> nat -> nat
sp: seq nat
h, s, r: nat
fps:= [seq find_fixpoint (f s) h | s <- sp]: seq (option nat)
ALL: all
(fun
opt : Datatypes_option__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality => opt != None) fps
H: r = \max_(fp <- fps | fp != None) odflt 0 fp
IN: s \in sp
Some (odflt 0 (find_fixpoint (f s) h)) =
find_fixpoint (f s) h case FFP: (find_fixpoint _ _) => //=; exfalso.
f: nat -> nat -> nat
sp: seq nat
h, s, r: nat
fps:= [seq find_fixpoint (f s) h | s <- sp]: seq (option nat)
ALL: all
(fun
opt : Datatypes_option__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality => opt != None) fps
H: r = \max_(fp <- fps | fp != None) odflt 0 fp
IN: s \in sp
FFP: find_fixpoint (f s) h = None
False
    suff: find_fixpoint (f s) h != None;
      first by move=> /eqP.
f: nat -> nat -> nat
sp: seq nat
h, s, r: nat
fps:= [seq find_fixpoint (f s) h | s <- sp]: seq (option nat)
ALL: all
(fun
opt : Datatypes_option__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality => opt != None) fps
H: r = \max_(fp <- fps | fp != None) odflt 0 fp
IN: s \in sp
FFP: find_fixpoint (f s) h = None
find_fixpoint (f s) h != None
    move: ALL => /allP //=; apply.
f: nat -> nat -> nat
sp: seq nat
h, s, r: nat
fps:= [seq find_fixpoint (f s) h | s <- sp]: seq (option nat)
H: r = \max_(fp <- fps | fp != None) odflt 0 fp
IN: s \in sp
FFP: find_fixpoint (f s) h = None
find_fixpoint (f s) h \in fps
    by rewrite /fps; exact: map_f.
  -
f: nat -> nat -> nat
sp: seq nat
h, s, r: nat
fps:= [seq find_fixpoint (f s) h | s <- sp]: seq (option nat)
ALL: all
(fun
opt : Datatypes_option__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality => opt != None) fps
H: r = \max_(fp <- fps | fp != None) odflt 0 fp
IN: s \in sp
odflt 0 (find_fixpoint (f s) h) <= r rewrite H.
f: nat -> nat -> nat
sp: seq nat
h, s, r: nat
fps:= [seq find_fixpoint (f s) h | s <- sp]: seq (option nat)
ALL: all
(fun
opt : Datatypes_option__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality => opt != None) fps
H: r = \max_(fp <- fps | fp != None) odflt 0 fp
IN: s \in sp
odflt 0 (find_fixpoint (f s) h) <=
\max_(fp <- fps | fp != None) odflt 0 fp
    apply leq_bigmax_cond_seq; [|move: ALL => /allP //=; apply].
f: nat -> nat -> nat
sp: seq nat
h, s, r: nat
fps:= [seq find_fixpoint (f s) h | s <- sp]: seq (option nat)
ALL: all
(fun
opt : Datatypes_option__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality => opt != None) fps
H: r = \max_(fp <- fps | fp != None) odflt 0 fp
IN: s \in sp
find_fixpoint (f s) h \in fps
f: nat -> nat -> nat
sp: seq nat
h, s, r: nat
fps:= [seq find_fixpoint (f s) h | s <- sp]: seq (option nat)
H: r = \max_(fp <- fps | fp != None) odflt 0 fp
IN: s \in sp
find_fixpoint (f s) h \in fps
    all: by rewrite /fps; exact: map_f.
Qed.

(** ** 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 :
    forall (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.
L: nat
P: pred nat
is_in_search_space:= fun A : nat => (A < L) && P A: nat -> bool
sp:= [seq s <- iota 0 L | P s]: seq nat
forall (f : nat -> nat -> nat) (h x : nat),
find_max_fixpoint f h = Some x ->
exists2 a : nat, is_in_search_space a & x = f a x
  Proof.
L: nat
P: pred nat
is_in_search_space:= fun A : nat => (A < L) && P A: nat -> bool
sp:= [seq s <- iota 0 L | P s]: seq nat
forall (f : nat -> nat -> nat) (h x : nat),
find_max_fixpoint f h = Some x ->
exists2 a : nat, is_in_search_space a & x = f a x
    move=> f h x SOME.
L: nat
P: pred nat
is_in_search_space:= fun A : nat => (A < L) && P A: nat -> bool
sp:= [seq s <- iota 0 L | P s]: seq nat
f: nat -> nat -> nat
h, x: nat
SOME: find_max_fixpoint f h = Some x
exists2 a : nat, is_in_search_space a & x = f a x
    have NILP: ~~ nilp sp.
L: nat
P: pred nat
is_in_search_space:= fun A : nat => (A < L) && P A: nat -> bool
sp:= [seq s <- iota 0 L | P s]: seq nat
f: nat -> nat -> nat
h, x: nat
SOME: find_max_fixpoint f h = Some x
~~ nilp sp
L: nat
P: pred nat
is_in_search_space:= fun A : nat => (A < L) && P A: nat -> bool
sp:= [seq s <- iota 0 L | P s]: seq nat
f: nat -> nat -> nat
h, x: nat
SOME: find_max_fixpoint f h = Some x
NILP: ~~ nilp sp
exists2 a : nat, is_in_search_space a & x = f a x
    {
L: nat
P: pred nat
is_in_search_space:= fun A : nat => (A < L) && P A: nat -> bool
sp:= [seq s <- iota 0 L | P s]: seq nat
f: nat -> nat -> nat
h, x: nat
SOME: find_max_fixpoint f h = Some x
~~ nilp sp move: SOME.
L: nat
P: pred nat
is_in_search_space:= fun A : nat => (A < L) && P A: nat -> bool
sp:= [seq s <- iota 0 L | P s]: seq nat
f: nat -> nat -> nat
h, x: nat
find_max_fixpoint f h = Some x -> ~~ nilp sp
      rewrite /find_max_fixpoint has_count /sp /nilp size_filter.
L: nat
P: pred nat
is_in_search_space:= fun A : nat => (A < L) && P A: nat -> bool
sp:= [seq s <- iota 0 L | P s]: seq nat
f: nat -> nat -> nat
h, x: nat
(if 0 < count P (iota 0 L)
 then
  find_max_fixpoint_of_seq f [seq s <- iota 0 L | P s]
    h
 else None) = Some x -> count [eta P] (iota 0 L) != 0
      change (fun s : nat => P s) with P.
L: nat
P: pred nat
is_in_search_space:= fun A : nat => (A < L) && P A: nat -> bool
sp:= [seq s <- iota 0 L | P s]: seq nat
f: nat -> nat -> nat
h, x: nat
(if 0 < count P (iota 0 L)
 then
  find_max_fixpoint_of_seq f [seq x <- iota 0 L | P x]
    h
 else None) = Some x -> count P (iota 0 L) != 0
      by case (count P (iota 0 L)) => //. }
L: nat
P: pred nat
is_in_search_space:= fun A : nat => (A < L) && P A: nat -> bool
sp:= [seq s <- iota 0 L | P s]: seq nat
f: nat -> nat -> nat
h, x: nat
SOME: find_max_fixpoint f h = Some x
NILP: ~~ nilp sp
exists2 a : nat, is_in_search_space a & x = f a x
    have FP: exists2 a, a \in sp & x = f a x.
L: nat
P: pred nat
is_in_search_space:= fun A : nat => (A < L) && P A: nat -> bool
sp:= [seq s <- iota 0 L | P s]: seq nat
f: nat -> nat -> nat
h, x: nat
SOME: find_max_fixpoint f h = Some x
NILP: ~~ nilp sp
exists2 a : Datatypes_nat__canonical__eqtype_Equality,
  a \in sp & x = f a x
L: nat
P: pred nat
is_in_search_space:= fun A : nat => (A < L) && P A: nat -> bool
sp:= [seq s <- iota 0 L | P s]: seq nat
f: nat -> nat -> nat
h, x: nat
SOME: find_max_fixpoint f h = Some x
NILP: ~~ nilp sp
FP: exists2
  a : Datatypes_nat__canonical__eqtype_Equality,
  a \in sp & x = f a x
exists2 a : nat, is_in_search_space a & x = f a x
    {
L: nat
P: pred nat
is_in_search_space:= fun A : nat => (A < L) && P A: nat -> bool
sp:= [seq s <- iota 0 L | P s]: seq nat
f: nat -> nat -> nat
h, x: nat
SOME: find_max_fixpoint f h = Some x
NILP: ~~ nilp sp
exists2 a : Datatypes_nat__canonical__eqtype_Equality,
  a \in sp & x = f a x apply: fmfs_finds_fixpoint.
L: nat
P: pred nat
is_in_search_space:= fun A : nat => (A < L) && P A: nat -> bool
sp:= [seq s <- iota 0 L | P s]: seq nat
f: nat -> nat -> nat
h, x: nat
SOME: find_max_fixpoint f h = Some x
NILP: ~~ nilp sp
~~ nilp sp
L: nat
P: pred nat
is_in_search_space:= fun A : nat => (A < L) && P A: nat -> bool
sp:= [seq s <- iota 0 L | P s]: seq nat
f: nat -> nat -> nat
h, x: nat
SOME: find_max_fixpoint f h = Some x
NILP: ~~ nilp sp
find_max_fixpoint_of_seq f sp ?Goal0 = Some x
      -
L: nat
P: pred nat
is_in_search_space:= fun A : nat => (A < L) && P A: nat -> bool
sp:= [seq s <- iota 0 L | P s]: seq nat
f: nat -> nat -> nat
h, x: nat
SOME: find_max_fixpoint f h = Some x
NILP: ~~ nilp sp
~~ nilp sp exact: NILP.
      -
L: nat
P: pred nat
is_in_search_space:= fun A : nat => (A < L) && P A: nat -> bool
sp:= [seq s <- iota 0 L | P s]: seq nat
f: nat -> nat -> nat
h, x: nat
SOME: find_max_fixpoint f h = Some x
NILP: ~~ nilp sp
find_max_fixpoint_of_seq f sp ?Goal0 = Some x move: SOME.
L: nat
P: pred nat
is_in_search_space:= fun A : nat => (A < L) && P A: nat -> bool
sp:= [seq s <- iota 0 L | P s]: seq nat
f: nat -> nat -> nat
h, x: nat
NILP: ~~ nilp sp
find_max_fixpoint f h = Some x ->
find_max_fixpoint_of_seq f sp ?Goal0 = Some x
        rewrite /find_max_fixpoint.
L: nat
P: pred nat
is_in_search_space:= fun A : nat => (A < L) && P A: nat -> bool
sp:= [seq s <- iota 0 L | P s]: seq nat
f: nat -> nat -> nat
h, x: nat
NILP: ~~ nilp sp
(if has P (iota 0 L)
 then find_max_fixpoint_of_seq f sp h
 else None) = Some x ->
find_max_fixpoint_of_seq f sp ?Goal0 = Some x
        case: (has P (iota 0 L)) => //; exact. }
L: nat
P: pred nat
is_in_search_space:= fun A : nat => (A < L) && P A: nat -> bool
sp:= [seq s <- iota 0 L | P s]: seq nat
f: nat -> nat -> nat
h, x: nat
SOME: find_max_fixpoint f h = Some x
NILP: ~~ nilp sp
FP: exists2
  a : Datatypes_nat__canonical__eqtype_Equality,
  a \in sp & x = f a x
exists2 a : nat, is_in_search_space a & x = f a x
    move: FP => [a IN FP].
L: nat
P: pred nat
is_in_search_space:= fun A : nat => (A < L) && P A: nat -> bool
sp:= [seq s <- iota 0 L | P s]: seq nat
f: nat -> nat -> nat
h, x: nat
SOME: find_max_fixpoint f h = Some x
NILP: ~~ nilp sp
a: Datatypes_nat__canonical__eqtype_Equality
IN: a \in sp
FP: x = f a x
exists2 a : nat, is_in_search_space a & x = f a x
    exists a => //.
L: nat
P: pred nat
is_in_search_space:= fun A : nat => (A < L) && P A: nat -> bool
sp:= [seq s <- iota 0 L | P s]: seq nat
f: nat -> nat -> nat
h, x: nat
SOME: find_max_fixpoint f h = Some x
NILP: ~~ nilp sp
a: Datatypes_nat__canonical__eqtype_Equality
IN: a \in sp
FP: x = f a x
is_in_search_space a
    by move: IN; rewrite /sp /is_in_search_space mem_filter mem_iota andbC.
  Qed.

  (** Finally, we observe that there is no fixpoint in the search space larger
      than the result of [find_maximum_fixpoint]. *)
  Corollary fmf_is_maximum :
    forall {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.
L: nat
P: pred nat
is_in_search_space:= fun A : nat => (A < L) && P A: nat -> bool
sp:= [seq s <- iota 0 L | P s]: seq nat
forall (f : nat -> nat -> nat) (h s r : nat),
Some r = find_max_fixpoint f h ->
is_in_search_space s ->
exists2 v : nat,
  Some v = find_fixpoint (f s) h & v <= r
  Proof.
L: nat
P: pred nat
is_in_search_space:= fun A : nat => (A < L) && P A: nat -> bool
sp:= [seq s <- iota 0 L | P s]: seq nat
forall (f : nat -> nat -> nat) (h s r : nat),
Some r = find_max_fixpoint f h ->
is_in_search_space s ->
exists2 v : nat,
  Some v = find_fixpoint (f s) h & v <= r
    move=> f h s r.
L: nat
P: pred nat
is_in_search_space:= fun A : nat => (A < L) && P A: nat -> bool
sp:= [seq s <- iota 0 L | P s]: seq nat
f: nat -> nat -> nat
h, s, r: nat
Some r = find_max_fixpoint f h ->
is_in_search_space s ->
exists2 v : nat,
  Some v = find_fixpoint (f s) h & v <= r
    rewrite /find_max_fixpoint.
L: nat
P: pred nat
is_in_search_space:= fun A : nat => (A < L) && P A: nat -> bool
sp:= [seq s <- iota 0 L | P s]: seq nat
f: nat -> nat -> nat
h, s, r: nat
Some r =
(if has P (iota 0 L)
 then find_max_fixpoint_of_seq f sp h
 else None) ->
is_in_search_space s ->
exists2 v : nat,
  Some v = find_fixpoint (f s) h & v <= r
    case: (has P (iota 0 L)) => // SOME PRED.
L: nat
P: pred nat
is_in_search_space:= fun A : nat => (A < L) && P A: nat -> bool
sp:= [seq s <- iota 0 L | P s]: seq nat
f: nat -> nat -> nat
h, s, r: nat
SOME: Some r = find_max_fixpoint_of_seq f sp h
PRED: is_in_search_space s
exists2 v : nat,
  Some v = find_fixpoint (f s) h & v <= r
    apply: fmfs_is_maximum; first exact SOME.
L: nat
P: pred nat
is_in_search_space:= fun A : nat => (A < L) && P A: nat -> bool
sp:= [seq s <- iota 0 L | P s]: seq nat
f: nat -> nat -> nat
h, s, r: nat
SOME: Some r = find_max_fixpoint_of_seq f sp h
PRED: is_in_search_space s
s \in sp
    by move: PRED; rewrite /is_in_search_space /sp mem_filter mem_iota //= add0n andbC.
  Qed.

End PredicateSearchSpace.