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.
  Proof.
    elim: n m x ⇒ // ⇒ n IHn [//|m] x Px A B /=.
    apply: F_wf ⇒ // y Py Hy. apply: IHn ⇒ //. exact: leq_trans Hy _.
  Qed.

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

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

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).
Proof.
  apply: (Fix_eq xpredT) ⇒ // {n} f g n _.
  rewrite /const0_rec. case: ifP ⇒ // /negbT.
  case: n ⇒ //= n _ Hfg. exact: Hfg.
Qed.

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.
Proof.
  apply: (Fix_eq xpredT) ⇒ // {n} g f n _ H.
  rewrite /foo_rec. case: ifP ⇒ // _.
  apply: eq_big_seq ⇒ m /split_lt. exact: H.
Qed.
End Max.