Library RelationAlgebra.powerfix

powerfix: bounded fixpoint operator

we define a fixpoint operator which recursively unfolds an open-recursive function with recursive depth at most 2^n, for arbitrary n. This allows us to define arbitrary recursive functions, without needing to prove their termination. The operator is defined in a computationally efficient way. (We already used such a trick in ATBR ; it's simplified here thanks to the introduction of eta in Coq v8.4

Require Import common.
Set Implicit Arguments.

Section powerfix.

Variables A B: Type.
Notation Fun := (A → B).

the three following functions "iterate" their f argument lazily: iteration stops whenever f no longer makes recursive calls.
  • powerfix' n f k iterates f at most (2^n-1) times and then yields to k
  • powerfix n f k iterates f at most (2^n) times and then yields to k
  • linearfix n f k iterates f at most n times and then yields to k
Fixpoint powerfix' n (f: Fun → Fun) (k: Fun): Fun :=
  fun a ⇒ match n with O ⇒ k a | S n ⇒ f (powerfix' n f (powerfix' n f k)) a end.
Definition powerfix n f k a := f (powerfix' n f k) a.

Fixpoint linearfix n (f: Fun → Fun) (k: Fun): Fun :=
  fun a ⇒ match n with O ⇒ k a | S n ⇒ f (linearfix n f k) a end.

simple lemmas about 2^n
Lemma pow2_S n: pow2 n = S (pred (pow2 n)).
Proof. induction n. reflexivity. simpl. now rewrite IHn. Qed.

Lemma pred_pow2_Sn n: pred (pow2 (S n)) = S (double (pred (pow2 n))).
Proof. simpl. now rewrite pow2_S. Qed.

characterisation of powerfix with linearfix
Section linear_carac.

 Variable f: Fun → Fun.

 Lemma linearfix_S: ∀ n k,
   f (linearfix n f k) = linearfix n f (f k).
 Proof. induction n; intros k; simpl. reflexivity. now rewrite IHn. Qed.

 Lemma linearfix_double: ∀ n k,
   linearfix n f (linearfix n f k) = linearfix (double n) f k.
 Proof.
   induction n; intros k. reflexivity. simpl linearfix.
   now rewrite <-IHn, <-linearfix_S.
 Qed.

 Lemma powerfix'_linearfix: ∀ n k,
   powerfix' n f k = linearfix (pred (pow2 n)) f k.
 Proof.
   induction n; intros. reflexivity.
   rewrite pred_pow2_Sn. simpl.
   now rewrite <-linearfix_double, 2IHn.
 Qed.

 Theorem powerfix_linearfix: ∀ n k,
   powerfix n f k = linearfix (pow2 n) f k.
 Proof. intros. unfold powerfix. now rewrite powerfix'_linearfix, pow2_S. Qed.

End linear_carac.

powerfix_invariant gives an induction principle for powerfix, that does not care about the number of iterations -- in particular, the trivial "emptyfix" function : (fun f k a ⇒ k a) satisfies the same induction principle, so that this can only be used to reason about partial correctness.
Section invariant.
 Variable P: Fun → Prop.

 Lemma powerfix_invariant: ∀ n f g,
   (∀ k, P k → P (f k)) → P g → P (powerfix n f g).
 Proof.
   intros n f g Hf Hg. apply Hf.
   revert g Hg. induction n; intros g Hg; simpl; auto.
 Qed.

End invariant.

End powerfix.