fixedpoint.v 4.33 KB
Newer Older
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1
Require Import rt.util.tactics rt.util.induction.
2
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72

Section FixedPoint.
  
  Lemma iter_fix T (F : T -> T) x k n :
    iter k F x = iter k.+1 F x ->
    k <= n ->
    iter n F x = iter n.+1 F x.
  Proof.
    move => e. elim: n. rewrite leqn0. by move/eqP<-.
    move => n IH. rewrite leq_eqVlt; case/orP; first by move/eqP<-.
    move/IH => /= IHe. by rewrite -!IHe.
  Qed.

  Lemma fun_mon_iter_mon :
    forall (f: nat -> nat) x0 x1 x2,
      x1 <= x2 ->
      f x0 >= x0 ->
      (forall x1 x2, x1 <= x2 -> f x1 <= f x2) ->
      iter x1 f x0 <= iter x2 f x0.
  Proof.
    intros f x0 x1 x2 LE MIN MON.
    revert LE; revert x2; rewrite leq_as_delta; intros delta.
    induction x1; try rewrite add0n.
    {
      induction delta; first by apply leqnn.
      apply leq_trans with (n := iter delta f x0); first by done.
      clear IHdelta.
      induction delta; first by done.
      {
        rewrite 2!iterS; apply MON.
        apply IHdelta.
      }
    }
    {
      rewrite iterS -addn1 -addnA [1 + delta]addnC addnA addn1 iterS.
      by apply MON, IHx1.
    }
  Qed.

  Lemma fun_mon_iter_mon_helper :
    forall T (f: T -> T) (le: rel T) x0 x1,
      reflexive le ->
      transitive le ->
      (forall x2, le x0 (iter x2 f x0)) ->
      (forall x1 x2, le x0 x1 -> le x1 x2 -> le (f x1) (f x2)) ->
      le (iter x1 f x0) (iter x1.+1 f x0).
  Proof.
    intros T f le x0 x1 REFL TRANS MIN MON.
    generalize dependent x0.
    induction x1; first by ins; apply (MIN 1).
    by ins; apply MON; [by apply MIN | by apply IHx1].
  Qed.

  Lemma fun_mon_iter_mon_generic :
    forall T (f: T -> T) (le: rel T) x0 x1 x2,
      reflexive le ->
      transitive le ->
      x1 <= x2 ->
      (forall x1 x2, le x0 x1 -> le x1 x2 -> le (f x1) (f x2)) ->
      (forall x2 : nat, le x0 (iter x2 f x0)) ->
      le (iter x1 f x0) (iter x2 f x0).
  Proof.
    intros T f le x0 x1 x2 REFL TRANS LE MON MIN.
    revert LE; revert x2; rewrite leq_as_delta; intros delta.
    induction delta; first by rewrite addn0; apply REFL.
    apply (TRANS) with (y := iter (x1 + delta) f x0);
      first by apply IHdelta.
    by rewrite addnS; apply fun_mon_iter_mon_helper.
  Qed.

73 74
End FixedPoint.

75 76 77 78 79 80 81 82 83 84 85 86 87
(* 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.

88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103
(* 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.

104
  Section BasicLemmas.
105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126

    (* 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. 

127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156
  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.
157 158
  
End Iteration.