matita/matita/lib/arithmetics/iteration.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "arithmetics/nat.ma".
  13 include "basics/core_notation/exp_2.ma".
  14
  15 (* iteration *)
  16
  17 let rec iter (A:Type[0]) (g:A→A) n a on n ≝
  18 match n with
  19   [O ⇒ a
  20   |S m ⇒ g (iter A g m a)].
  21
  22 interpretation "iteration" 'exp g i = (iter ? g i).
  23
  24 lemma le_iter: ∀g,a. (∀x. x ≤ g x) → ∀i. a ≤ g^i a.
  25 #g #a #leg #i elim i //
  26 #n #Hind @(transitive_le … Hind) @leg
  27 qed.
  28
  29 lemma iter_iter: ∀A.∀g:A→A.∀a,b,c.
  30   g^c (g^b a) = g^(b+c) a.
  31 #A #g #a #b #c elim c
  32   [<plus_n_O normalize //
  33   |#m #Hind <plus_n_Sm normalize @eq_f @Hind
  34   ]
  35 qed.
  36
  37 lemma monotonic_iter: ∀g,a,b,i. (monotonic ? le g) → a ≤ b →
  38   g^i a ≤  g^i b.
  39 #g #a #b #i #Hmono #leab elim i //
  40 #m #Hind normalize @Hmono //
  41 qed.
  42
  43 lemma monotonic_iter2: ∀g,a,i,j. (∀x. x ≤ g x) → i ≤ j →
  44   g^i a ≤  g^j a.
  45 #g #a #i #j #leg #leij elim leij //
  46 #m #leim #Hind normalize @(transitive_le … Hind) @leg
  47 qed.