Library GraphTheory.bounded

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

A fixpoint operator for bounded recursion

Section Bounded.
  Variables (aT rT : Type) (P : aT Prop) (x0 : rT).
  Variables (measure : aT nat) (F : (aT rT) (aT rT)).

  Hypothesis F_wf :
     f g x, P x ( y, P y measure y < measure x f y = g y) F f x = F g x.

Note: The use of equality here effectively limits this to functions in one argument
  Fixpoint F_rec (n : nat) (x : aT) :=
    if n is n'.+1 then F (F_rec n') x else x0.

  Lemma F_rec_narrow m n x :
    P x measure x < n n m F_rec m x = F_rec n x.
    elim: n m x ⇒ // ⇒ n IHn [//|m] x Px A B /=.
    apply: F_wf ⇒ // y Py Hy. apply: IHn ⇒ //. exact: leq_trans Hy _.

  Definition Fix x := F_rec (measure x).+1 x.

  Lemma Fix_eq x : P x Fix x = F Fix x.
    rewrite /Fix /= ⇒ Px. apply: F_wf ⇒ // y Py Hy.
    by rewrite (@F_rec_narrow (measure x) (measure y).+1).

End Bounded.
Arguments Fix_eq [aT rT] P.

Example Instances

Definition const0_rec (F : nat nat) n := if n == 0 then 0 else F (n.-1).

Definition const0 := Fix 1 id const0_rec.

Lemma const0_eq n : const0 n = if n == 0 then 0 else const0 (n.-1).
  apply: (Fix_eq xpredT) ⇒ // {n} f g n _.
  rewrite /const0_rec. case: ifP ⇒ // /negbT.
  case: n ⇒ //= n _ Hfg. exact: Hfg.

The following example shows that one can freely combine bounded recursion with subroutines and big operators

Section Max.
Variable split : nat seq nat.
Hypothesis split_lt : n m, m \in split n m < n.

Definition foo_rec F n :=
  if n < 4 then n else \max_(m <- split n) F m.

Definition foo := Fix 0 id foo_rec.

Lemma foo_eq n : foo n = if n < 4 then n else \max_(m <- split n) foo m.
  apply: (Fix_eq xpredT) ⇒ // {n} g f n _ H.
  rewrite /foo_rec. case: ifP ⇒ // _.
  apply: eq_big_seqm /split_lt. exact: H.
End Max.