ATBR.Utils_WF
(**************************************************************************)
(* This is part of ATBR, it is distributed under the terms of the *)
(* GNU Lesser General Public License version 3 *)
(* (see file LICENSE for more details) *)
(* *)
(* Copyright 2009-2011: Thomas Braibant, Damien Pous. *)
(**************************************************************************)
(* This is part of ATBR, it is distributed under the terms of the *)
(* GNU Lesser General Public License version 3 *)
(* (see file LICENSE for more details) *)
(* *)
(* Copyright 2009-2011: Thomas Braibant, Damien Pous. *)
(**************************************************************************)
Several results to ease the definition and the analysis of
(well-founded) recursive functions
Trick to compute with well-founded recursions: lazily add 2^n
Acc_intro constructors in front of a well_foundedness proof, so
that the actual proof is never reached in practise
Fixpoint guard A (R: A -> A -> Prop) n (wfR: well_founded R): well_founded R :=
match n with
| 0 => wfR
| S n => fun x => Acc_intro x (fun y _ => guard n (guard n wfR) y)
end.
match n with
| 0 => wfR
| S n => fun x => Acc_intro x (fun y _ => guard n (guard n wfR) y)
end.
Lexicographic product of two well-founded relations
Section lexico.
Variables A B: Type.
Variable R: relation A.
Variable S: relation B.
Inductive lexico: relation (A*B) :=
| lexico_left: forall a a' b b', R a' a -> lexico (a',b') (a,b)
| lexico_right: forall a b b', S b' b -> lexico (a,b') (a,b)
.
Hypothesis HR: well_founded R.
Hypothesis HS: well_founded S.
Theorem lexico_wf: well_founded lexico.
Proof.
intros [a b]. revert b.
induction a as [a IHa] using (well_founded_induction HR).
induction b as [b IHb] using (well_founded_induction HS).
constructor. intros [a' b'] H. inversion_clear H; auto.
Qed.
End lexico.
Variables A B: Type.
Variable R: relation A.
Variable S: relation B.
Inductive lexico: relation (A*B) :=
| lexico_left: forall a a' b b', R a' a -> lexico (a',b') (a,b)
| lexico_right: forall a b b', S b' b -> lexico (a,b') (a,b)
.
Hypothesis HR: well_founded R.
Hypothesis HS: well_founded S.
Theorem lexico_wf: well_founded lexico.
Proof.
intros [a b]. revert b.
induction a as [a IHa] using (well_founded_induction HR).
induction b as [b IHb] using (well_founded_induction HS).
constructor. intros [a' b'] H. inversion_clear H; auto.
Qed.
End lexico.
A relation contained in a well-founded relation is well-founded
Section wf_incl.
Variable A: Type.
Variable S: relation A.
Hypothesis HS: well_founded S.
Variable R: relation A.
Hypothesis H: forall a' a, R a' a -> S a' a.
Theorem incl_wf: well_founded R.
Proof.
intros a. induction a as [a IHa] using (well_founded_induction HS).
constructor. eauto.
Qed.
End wf_incl.
Variable A: Type.
Variable S: relation A.
Hypothesis HS: well_founded S.
Variable R: relation A.
Hypothesis H: forall a' a, R a' a -> S a' a.
Theorem incl_wf: well_founded R.
Proof.
intros a. induction a as [a IHa] using (well_founded_induction HS).
constructor. eauto.
Qed.
End wf_incl.
Equivalent of well_founded_ltof, using an underlying well-founded relation
Section wf_of.
Variables U V: Type.
Variable f: U -> V.
Variable R: relation V.
Hypothesis HR: well_founded R.
Definition rel_of: relation U := fun a' a => R (f a') (f a).
Theorem rel_of_wf: well_founded rel_of.
Proof.
unfold rel_of.
intro a. remember (f a) as fa. revert a Heqfa.
induction fa as [fa IHa] using (well_founded_induction HR).
constructor. intros a' H. subst. eauto.
Qed.
End wf_of.
Variables U V: Type.
Variable f: U -> V.
Variable R: relation V.
Hypothesis HR: well_founded R.
Definition rel_of: relation U := fun a' a => R (f a') (f a).
Theorem rel_of_wf: well_founded rel_of.
Proof.
unfold rel_of.
intro a. remember (f a) as fa. revert a Heqfa.
induction fa as [fa IHa] using (well_founded_induction HR).
constructor. intros a' H. subst. eauto.
Qed.
End wf_of.
Similarly, in the other direction
Section wf_to.
Variables U V: Type.
Variable f: U -> V.
Variable R: relation U.
Inductive rel_to: relation V :=
rel_to_intro: forall a' a, R a' a -> rel_to (f a') (f a).
Hypothesis HR: well_founded rel_to.
Theorem rel_to_wf: well_founded R.
intro a. remember (f a) as fa. revert a Heqfa.
induction fa as [fa IHa] using (well_founded_induction HR).
constructor. intros a' H. subst. eapply IHa; trivial. constructor. trivial.
Qed.
End wf_to.
Variables U V: Type.
Variable f: U -> V.
Variable R: relation U.
Inductive rel_to: relation V :=
rel_to_intro: forall a' a, R a' a -> rel_to (f a') (f a).
Hypothesis HR: well_founded rel_to.
Theorem rel_to_wf: well_founded R.
intro a. remember (f a) as fa. revert a Heqfa.
induction fa as [fa IHa] using (well_founded_induction HR).
constructor. intros a' H. subst. eapply IHa; trivial. constructor. trivial.
Qed.
End wf_to.
Combination of the above reductions : reduction to a lexicographic product of two well-founded relations
Section wf_lexico_incl.
Variables U A B: Type.
Variable f: U -> A*B.
Variable RA: relation A.
Variable RB: relation B.
Hypothesis HRA: well_founded RA.
Hypothesis HRB: well_founded RB.
Variable R: relation U.
Hypothesis H: forall u' u, R u' u -> lexico RA RB (f u') (f u).
Theorem lexico_incl_wf: well_founded R.
Proof.
apply (rel_to_wf (f:=f)). eapply incl_wf. apply lexico_wf; eassumption.
intros [a' b'] [a b] [u' u Hab]. auto.
Qed.
End wf_lexico_incl.
Variables U A B: Type.
Variable f: U -> A*B.
Variable RA: relation A.
Variable RB: relation B.
Hypothesis HRA: well_founded RA.
Hypothesis HRB: well_founded RB.
Variable R: relation U.
Hypothesis H: forall u' u, R u' u -> lexico RA RB (f u') (f u).
Theorem lexico_incl_wf: well_founded R.
Proof.
apply (rel_to_wf (f:=f)). eapply incl_wf. apply lexico_wf; eassumption.
intros [a' b'] [a b] [u' u Hab]. auto.
Qed.
End wf_lexico_incl.
Lazy partial fixpoint operators (lazy iterator):
we use these functions to avoid the computation of a (2^n) worst-case
bound which is never reached in practise
the three following functions "iterate" their f argument lazily: iteration stops whenever f
no longer makes recursive calls.
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.
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.
Fixpoint power n := match n with O => 1 | S n => 2*power n end.
Lemma power_positive: forall n, 0 < power n.
Proof. induction n; simpl; omega. Qed.
Lemma power_positive: forall n, 0 < power n.
Proof. induction n; simpl; omega. Qed.
the functional f as to use its first argument "in extension"
Hypothesis Hf: Proper (pointwise_relation A R ==> @eq A ==> R) f.
Instance linearfix_compat n:
Proper (pointwise_relation A R ==> pointwise_relation A R) (linearfix n f).
Proof.
induction n; intros k k' H a; simpl.
apply H.
apply Hf; auto.
Qed.
Lemma linearfix_plus: forall n m k, pointwise_relation A R
(linearfix n f (linearfix m f k)) (linearfix (n + m) f k).
Proof.
induction n; intros m k a; simpl.
reflexivity.
rewrite IHn. reflexivity.
Qed.
Instance powerfix'_compat n:
Proper (pointwise_relation A R ==> pointwise_relation A R) (powerfix' n f).
Proof.
induction n; intros k k' H a; simpl.
apply H.
apply Hf; auto.
Qed.
Instance powerfix_compat n:
Proper (pointwise_relation A R ==> pointwise_relation A R) (powerfix n f).
Proof.
intros k k' H. unfold powerfix. setoid_rewrite H. reflexivity.
Qed.
Lemma powerfix'_linearfix: forall n k,
pointwise_relation A R (powerfix' n f k) (linearfix (pred (power n)) f k).
Proof.
induction n; intros; simpl; intro a.
reflexivity.
rewrite IHn. rewrite IHn.
pose proof (power_positive n).
replace (pred (power n + (power n + 0))) with (S (pred (power n) + pred (power n))) by omega.
rewrite linearfix_plus.
reflexivity.
Qed.
Instance linearfix_compat n:
Proper (pointwise_relation A R ==> pointwise_relation A R) (linearfix n f).
Proof.
induction n; intros k k' H a; simpl.
apply H.
apply Hf; auto.
Qed.
Lemma linearfix_plus: forall n m k, pointwise_relation A R
(linearfix n f (linearfix m f k)) (linearfix (n + m) f k).
Proof.
induction n; intros m k a; simpl.
reflexivity.
rewrite IHn. reflexivity.
Qed.
Instance powerfix'_compat n:
Proper (pointwise_relation A R ==> pointwise_relation A R) (powerfix' n f).
Proof.
induction n; intros k k' H a; simpl.
apply H.
apply Hf; auto.
Qed.
Instance powerfix_compat n:
Proper (pointwise_relation A R ==> pointwise_relation A R) (powerfix n f).
Proof.
intros k k' H. unfold powerfix. setoid_rewrite H. reflexivity.
Qed.
Lemma powerfix'_linearfix: forall n k,
pointwise_relation A R (powerfix' n f k) (linearfix (pred (power n)) f k).
Proof.
induction n; intros; simpl; intro a.
reflexivity.
rewrite IHn. rewrite IHn.
pose proof (power_positive n).
replace (pred (power n + (power n + 0))) with (S (pred (power n) + pred (power n))) by omega.
rewrite linearfix_plus.
reflexivity.
Qed.
The expected characterisation
Theorem powerfix_linearfix: forall n k,
pointwise_relation A R (powerfix n f k) (linearfix (power n) f k).
Proof.
intros. unfold powerfix. setoid_rewrite powerfix'_linearfix.
generalize (power_positive n). destruct (power n).
intro. omega_false.
intro. reflexivity.
Qed.
End linear_carac.
pointwise_relation A R (powerfix n f k) (linearfix (power n) f k).
Proof.
intros. unfold powerfix. setoid_rewrite powerfix'_linearfix.
generalize (power_positive n). destruct (power n).
intro. omega_false.
intro. reflexivity.
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.
Hypothesis HP: forall k, P k -> P (fun a => k a).
(* Alternative hypothesis: *)
(* Hypothesis HP: Proper (pointwise_relation A (@eq B) ==> iff) P. *)
Lemma powerfix'_invariant': forall n f g, (forall k, P k -> P (f k)) -> P g -> P (powerfix' n f g).
Proof.
induction n; intros f g Hf Hg; simpl; apply HP; auto.
Qed.
Lemma powerfix_invariant': forall n f g, (forall k, P k -> P (f k)) -> P g -> P (powerfix n f g).
Proof.
intros n f g Hf Hg. apply HP, Hf, powerfix'_invariant'; assumption.
Qed.
End invariant.
End powerfix.
Variable P: Fun -> Prop.
Hypothesis HP: forall k, P k -> P (fun a => k a).
(* Alternative hypothesis: *)
(* Hypothesis HP: Proper (pointwise_relation A (@eq B) ==> iff) P. *)
Lemma powerfix'_invariant': forall n f g, (forall k, P k -> P (f k)) -> P g -> P (powerfix' n f g).
Proof.
induction n; intros f g Hf Hg; simpl; apply HP; auto.
Qed.
Lemma powerfix_invariant': forall n f g, (forall k, P k -> P (f k)) -> P g -> P (powerfix n f g).
Proof.
intros n f g Hf Hg. apply HP, Hf, powerfix'_invariant'; assumption.
Qed.
End invariant.
End powerfix.
Another way to construct well-founded relations: start with a well-founded one (e.g., the empty one),
and progressively add pairs satisfying some acyclicity property w.r.t. the current relation
Require Relations.
Section add_pair.
Import Relations.
Variable T: Set.
Definition add_pair i j R: relation T := fun s t => s=i /\ t=j \/ R s t.
Lemma wf_add_pair: forall R, well_founded R ->
forall i j, ~ clos_refl_trans T R j i -> well_founded (add_pair i j R).
Proof.
intros R Hwf i j Hij.
assert (Hi: forall v, clos_refl_trans _ R v i -> Acc (add_pair i j R) v).
induction v as [v IH] using (well_founded_induction Hwf); intros Hui.
constructor. intros u [[-> ->]|Huv].
elim Hij. assumption.
apply IH. assumption.
eauto using rt_trans, rt_step.
intro v. induction v as [v IH] using (well_founded_induction Hwf).
constructor. intros u [[-> ->] | Huv].
apply Hi. constructor 2.
apply IH. assumption.
Qed.
End add_pair.
Section add_pair.
Import Relations.
Variable T: Set.
Definition add_pair i j R: relation T := fun s t => s=i /\ t=j \/ R s t.
Lemma wf_add_pair: forall R, well_founded R ->
forall i j, ~ clos_refl_trans T R j i -> well_founded (add_pair i j R).
Proof.
intros R Hwf i j Hij.
assert (Hi: forall v, clos_refl_trans _ R v i -> Acc (add_pair i j R) v).
induction v as [v IH] using (well_founded_induction Hwf); intros Hui.
constructor. intros u [[-> ->]|Huv].
elim Hij. assumption.
apply IH. assumption.
eauto using rt_trans, rt_step.
intro v. induction v as [v IH] using (well_founded_induction Hwf).
constructor. intros u [[-> ->] | Huv].
apply Hi. constructor 2.
apply IH. assumption.
Qed.
End add_pair.
An induction principle for Fix, which is less demanding than the corresponding results
of the standard library (no additional hypothesis about P or F)
Section Fix_induction.
Variable A: Type.
Variable R: relation A.
Hypothesis Hwf: well_founded R.
Variable T: A -> Type.
Variable F: forall x, (forall y, R y x -> T y) -> T x.
Variable P: forall x, T x -> Prop.
Hypothesis IH: forall x (G: forall y, R y x -> T y), (forall y (H: R y x), P (G y H)) -> P (F G).
Theorem Fix_induction: forall x, P (Fix Hwf _ F x).
Proof.
unfold Fix. intro x. generalize (Hwf x) as Hx.
induction x as [x IHwf] using (well_founded_induction Hwf); intros.
rewrite <- Fix_F_eq. auto.
Qed.
End Fix_induction.
Arguments Fix_induction [A R] Hwf [T F P].
Variable A: Type.
Variable R: relation A.
Hypothesis Hwf: well_founded R.
Variable T: A -> Type.
Variable F: forall x, (forall y, R y x -> T y) -> T x.
Variable P: forall x, T x -> Prop.
Hypothesis IH: forall x (G: forall y, R y x -> T y), (forall y (H: R y x), P (G y H)) -> P (F G).
Theorem Fix_induction: forall x, P (Fix Hwf _ F x).
Proof.
unfold Fix. intro x. generalize (Hwf x) as Hx.
induction x as [x IHwf] using (well_founded_induction Hwf); intros.
rewrite <- Fix_F_eq. auto.
Qed.
End Fix_induction.
Arguments Fix_induction [A R] Hwf [T F P].