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
  14 (* iteration *)
  15
  16 let rec iter (A:Type[0]) (g:A→A) n a on n ≝
  17 match n with
  18   [O ⇒ a
  19   |S m ⇒ g (iter A g m a)].
  20
  21 interpretation "iteration" 'exp g i = (iter ? g i).
  22
  23 lemma le_iter: ∀g,a. (∀x. x ≤ g x) → ∀i. a ≤ g^i a.
  24 #g #a #leg #i elim i //
  25 #n #Hind @(transitive_le … Hind) @leg
  26 qed.
  27
  28 lemma iter_iter: ∀A.∀g:A→A.∀a,b,c.
  29   g^c (g^b a) = g^(b+c) a.
  30 #A #g #a #b #c elim c
  31   [<plus_n_O normalize //
  32   |#m #Hind <plus_n_Sm normalize @eq_f @Hind
  33   ]
  34 qed.
  35
  36 lemma monotonic_iter: ∀g,a,b,i. (monotonic ? le g) → a ≤ b →
  37   g^i a ≤  g^i b.
  38 #g #a #b #i #Hmono #leab elim i //
  39 #m #Hind normalize @Hmono //
  40 qed.
  41
  42 lemma monotonic_iter2: ∀g,a,i,j. (∀x. x ≤ g x) → i ≤ j →
  43   g^i a ≤  g^j a.
  44 #g #a #i #j #leg #leij elim leij //
  45 #m #leim #Hind normalize @(transitive_le … Hind) @leg
  46 qed.