Library Iteration
Require Import Coqlib.
Require Import Classical.
Require Import Max.
Module Type ITER.
Variable iterate
: forall A B : Type, (A -> B + A) -> A -> option B.
Hypothesis iterate_prop
: forall (A B : Type) (step : A -> B + A) (P : A -> Prop) (Q : B -> Prop),
(forall a : A, P a ->
match step a with inl b => Q b | inr a' => P a' end) ->
forall (a : A) (b : B), iterate A B step a = Some b -> P a -> Q b.
End ITER.
Axiom
dependent_description' :
forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop),
(forall x:A,
exists y : B x, R x y /\ (forall y':B x, R x y' -> y = y')) ->
sigT (fun f : forall x:A, B x => (forall x:A, R x (f x))).
Module PrimIter: ITER.
Section ITERATION.
Variables A B: Type.
Variable step: A -> B + A.
The
The naive way to define the iteration is:
However, this is a general recursion, not guaranteed to terminate, and therefore not expressible in Coq. The standard way to work around this difficulty is to use Noetherian recursion (Coq module
Instead, we choose to bound the number of iterations by an arbitrary constant.
Since we know (informally) that our computations terminate, we can take a very large constant as the maximal number of iterations. Failure will therefore never happen in practice, but of course our proofs also cover the failure case and show that nothing bad happens in this hypothetical case either.
step
parameter represents one step of the iteration. From a
current iteration state a: A
, it either returns a value of type B
,
meaning that iteration is over and that this B
value is the final
result of the iteration, or a value a' : A
which is the next state
of the iteration.
The naive way to define the iteration is:
Fixpoint iterate (a: A) : B := match step a with | inl b => b | inr a' => iterate a' end.
However, this is a general recursion, not guaranteed to terminate, and therefore not expressible in Coq. The standard way to work around this difficulty is to use Noetherian recursion (Coq module
Wf
).
This requires that we equip the type A
with a well-founded ordering <
(no infinite ascending chains) and we demand that step
satisfies
step a = inr a' -> a < a'
. For the types A
that are of interest to us
in this development, it is however very painful to define adequate
well-founded orderings, even though we know our iterations always
terminate.
Instead, we choose to bound the number of iterations by an arbitrary constant.
iterate
then becomes a function that can fail,
of type A -> option B
. The None
result denotes failure to reach
a result in the number of iterations prescribed, or, in other terms,
failure to find a solution to the dataflow problem. The compiler
passes that exploit dataflow analysis (the Constprop
, CSE
and
Allocation
passes) will, in this case, either fail (Allocation
)
or turn off the optimization pass (Constprop
and CSE
).
Since we know (informally) that our computations terminate, we can take a very large constant as the maximal number of iterations. Failure will therefore never happen in practice, but of course our proofs also cover the failure case and show that nothing bad happens in this hypothetical case either.
Definition num_iterations := 1000000000000%positive.
The simple definition of bounded iteration is:
This function is structural recursive over the parameter
Fixpoint iterate (niter: nat) (a: A) {struct niter} : option B := match niter with | O => None | S niter' => match step a with | inl b => b | inr a' => iterate niter' a' end end.
This function is structural recursive over the parameter
niter
(number of iterations), represented here as a Peano integer (type nat
).
However, we want to use very large values of niter
. As Peano integers,
these values would be much too large to fit in memory. Therefore,
we must express iteration counts as a binary integer (type positive
).
However, Peano induction over type positive
is not structural recursion,
so we cannot define iterate
as a Coq fixpoint and must use
Noetherian recursion instead.
Definition iter_step (x: positive)
(next: forall y, Plt y x -> A -> option B)
(s: A) : option B :=
match peq x xH with
| left EQ => None
| right NOTEQ =>
match step s with
| inl res => Some res
| inr s' => next (Ppred x) (Ppred_Plt x NOTEQ) s'
end
end.
Definition iter: positive -> A -> option B :=
Fix Plt_wf (fun _ => A -> option B) iter_step.
We then prove the expected unrolling equations for
iter
.
Remark unroll_iter:
forall x, iter x = iter_step x (fun y _ => iter y).
The
iterate
function is defined as iter
up to
num_iterations
through the loop.
Definition iterate := iter num_iterations.
We now prove the invariance property
iterate_prop
.
Variable P: A -> Prop.
Variable Q: B -> Prop.
Hypothesis step_prop:
forall a : A, P a ->
match step a with inl b => Q b | inr a' => P a' end.
Lemma iter_prop:
forall n a b, P a -> iter n a = Some b -> Q b.
Lemma iterate_prop:
forall a b, iterate a = Some b -> P a -> Q b.
End ITERATION.
End PrimIter.
Module GenIter: ITER.
Section ITERATION.
Variables A B: Type.
Variable step: A -> B + A.
Definition B_le (x y: option B) : Prop := x = None \/ y = x.
Definition F_le (x y: A -> option B) : Prop := forall a, B_le (x a) (y a).
Definition F_iter (next: A -> option B) (a: A) : option B :=
match step a with
| inl b => Some b
| inr a' => next a'
end.
Lemma F_iter_monot:
forall f g, F_le f g -> F_le (F_iter f) (F_iter g).
Fixpoint iter (n: nat) : A -> option B :=
match n with
| O => (fun a => None)
| S m => F_iter (iter m)
end.
Lemma iter_monot:
forall p q, (p <= q)%nat -> F_le (iter p) (iter q).
Lemma iter_either:
forall a,
(exists n, exists b, iter n a = Some b) \/
(forall n, iter n a = None).
Definition converges_to (a: A) (b: option B) : Prop :=
exists n, forall m, (n <= m)%nat -> iter m a = b.
Lemma converges_to_Some:
forall a n b, iter n a = Some b -> converges_to a (Some b).
Lemma converges_to_exists:
forall a, exists b, converges_to a b.
Lemma converges_to_unique:
forall a b, converges_to a b -> forall b', converges_to a b' -> b = b'.
Lemma converges_to_exists_uniquely:
forall a, exists b, converges_to a b /\ forall b', converges_to a b' -> b = b'.
Definition exists_iterate :=
dependent_description' A (fun _ => option B)
converges_to converges_to_exists_uniquely.
Definition iterate : A -> option B :=
match exists_iterate with existT f P => f end.
Lemma converges_to_iterate:
forall a b, converges_to a b -> iterate a = b.
Lemma iterate_converges_to:
forall a, converges_to a (iterate a).
Invariance property.
Variable P: A -> Prop.
Variable Q: B -> Prop.
Hypothesis step_prop:
forall a : A, P a ->
match step a with inl b => Q b | inr a' => P a' end.
Lemma iter_prop:
forall n a b, P a -> iter n a = Some b -> Q b.
Lemma iterate_prop:
forall a b, iterate a = Some b -> P a -> Q b.
End ITERATION.
End GenIter.