From 5d02df7f5c5d49ed2ac5c253cb47aebe4f0987f8 Mon Sep 17 00:00:00 2001
From: Felipe Cerqueira <felipec@mpi-sws.org>
Date: Mon, 22 Aug 2016 15:38:54 +0200
Subject: [PATCH] Add lemmas about iter_fixpoint

---
 util/fixedpoint.v | 46 ++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 44 insertions(+), 2 deletions(-)

diff --git a/util/fixedpoint.v b/util/fixedpoint.v
index 93742e1..5ea14a0 100644
--- a/util/fixedpoint.v
+++ b/util/fixedpoint.v
@@ -72,6 +72,19 @@ Section FixedPoint.
 
 End FixedPoint.
 
+(* In this section, we define some properties of relations
+   that are important for fixed-point iterations. *)
+Section Relations.
+
+  Context {T: Type}.
+  Variable R: rel T.
+  Variable f: T -> T.
+  
+  Definition monotone (R: rel T) :=
+    forall x y, R x y -> R (f x) (f y).
+
+End Relations.
+
 (* 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. *)
@@ -88,7 +101,7 @@ Section Iteration.
         else iter_fixpoint step x'
     else None.
 
-  Section Lemmas.
+  Section BasicLemmas.
 
     (* We prove that iter_fixpoint either returns either None
        or Some y, where y is a fixed point. *)
@@ -111,6 +124,35 @@ Section Iteration.
       }
     Qed. 
 
-  End Lemmas.
+  End BasicLemmas.
+
+  Section RelationLemmas.
+
+    Variable R: rel T.
+    Hypothesis H_reflexive: reflexive R.
+    Hypothesis H_transitive: transitive R.
+    Hypothesis H_monotone: monotone f R.
+                                  
+    Lemma iter_fixpoint_ge_min:
+      forall max_steps x0 x,
+        iter_fixpoint max_steps x0 = Some x ->
+        R x0 (f x0) ->
+        R x0 x.
+    Proof.
+      induction max_steps.
+      {
+        intros x0 x SOME MIN; first by done.
+      }
+      {
+        intros x0 x SOME MIN; simpl in SOME.
+        destruct (x0 == f x0) eqn:EQ1;
+          first by inversion SOME; apply H_reflexive.
+        apply IHmax_steps in SOME;
+          first by apply H_transitive with (y := f x0).
+        by apply H_monotone.
+      }
+    Qed.
+    
+  End RelationLemmas.
   
 End Iteration.
\ No newline at end of file
-- 
2.26.2