From 9cc1d6419128c1ee08cb00d1d4e7a6b7b05ae9d0 Mon Sep 17 00:00:00 2001 From: Felipe Cerqueira Date: Thu, 4 Aug 2016 17:00:44 +0200 Subject: [PATCH] Add new function for fixed-point iteration --- util/fixedpoint.v | 45 ++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 44 insertions(+), 1 deletion(-) diff --git a/util/fixedpoint.v b/util/fixedpoint.v index b1d31d9..93742e1 100644 --- a/util/fixedpoint.v +++ b/util/fixedpoint.v @@ -70,4 +70,47 @@ Section FixedPoint. by rewrite addnS; apply fun_mon_iter_mon_helper. Qed. -End FixedPoint. \ No newline at end of file +End FixedPoint. + +(* In this section we define a fixed-point iteration function + that stops as soon as it finds the solution. If no solution + is found, the function returns None. *) +Section Iteration. + + Variable T : eqType. + Variable f: T -> T. + + Fixpoint iter_fixpoint max_steps (x: T) := + if max_steps is step.+1 then + let x' := f x in + if x == x' then + Some x + else iter_fixpoint step x' + else None. + + Section Lemmas. + + (* We prove that iter_fixpoint either returns either None + or Some y, where y is a fixed point. *) + Lemma iter_fixpoint_cases : + forall max_steps x0, + iter_fixpoint max_steps x0 = None \/ + exists y, + iter_fixpoint max_steps x0 = Some y /\ + y = f y. + Proof. + induction max_steps. + { + by ins; simpl; destruct (x0 == f x0); left. + } + { + intros x0; simpl. + destruct (x0 == f x0) eqn:EQ1; + first by right; exists x0; split; last by apply/eqP. + by destruct (IHmax_steps (f x0)) as [NONE | FOUND]. + } + Qed. + + End Lemmas. + +End Iteration. \ No newline at end of file -- 2.26.2