From 874cacec64d0aab52ab1a21aad23208f52f50caf Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 31 May 2013 09:47:33 +0000 Subject: [PATCH] iteration.ma --- matita/matita/lib/arithmetics/iteration.ma | 46 ++++++++++++++++++++++ 1 file changed, 46 insertions(+) create mode 100644 matita/matita/lib/arithmetics/iteration.ma diff --git a/matita/matita/lib/arithmetics/iteration.ma b/matita/matita/lib/arithmetics/iteration.ma new file mode 100644 index 000000000..78d4eb4d0 --- /dev/null +++ b/matita/matita/lib/arithmetics/iteration.ma @@ -0,0 +1,46 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +include "arithmetics/nat.ma". + +(* iteration *) + +let rec iter (A:Type[0]) (g:A→A) n a on n ≝ +match n with + [O ⇒ a + |S m ⇒ g (iter A g m a)]. + +interpretation "iteration" 'exp g i = (iter ? g i). + +lemma le_iter: ∀g,a. (∀x. x ≤ g x) → ∀i. a ≤ g^i a. +#g #a #leg #i elim i // +#n #Hind @(transitive_le … Hind) @leg +qed. + +lemma iter_iter: ∀A.∀g:A→A.∀a,b,c. + g^c (g^b a) = g^(b+c) a. +#A #g #a #b #c elim c + [