X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fpnat_iter.ma;h=5361dcef37569b4d306fb6f2492e3327a7f9c00d;hb=503500ff9a6d9cca363a42b5fe7f3f5de69239f9;hp=9e806cfe2cf5d91612027727dfc57cc79d70405c;hpb=5e72e41f4f86814e56d4b00959ccc56c71042a4c;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma
index 9e806cfe2..5361dcef3 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma
@@ -13,10 +13,12 @@
 (**************************************************************************)
 
 include "ground/notation/functions/exp_3.ma".
+include "ground/lib/exteq.ma".
 include "ground/arith/pnat.ma".
 
 (* ITERATED FUNCTION FOR POSITIVE INTEGERS **********************************)
 
+(* Note: see also: lib/arithemetics/bigops.ma *)
 rec definition piter (p:pnat) (A:Type[0]) (f:A→A) (a:A) ≝
 match p with
 [ punit   ⇒ f a
@@ -27,17 +29,35 @@ interpretation
   "iterated function (positive integers)"
   'Exp A f p = (piter p A f).
 
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
 
-lemma piter_unit (A) (f) (a): f a = (f^{A}𝟏) a.
+lemma piter_unit (A) (f): f ≐ f^{A}𝟏.
 // qed.
 
-lemma piter_succ (A) (f) (p) (a): f (f^p a) = f^{A}(↑p) a.
+lemma piter_succ (A) (f) (p): f ∘ f^p ≐ f^{A}(↑p).
 // qed.
 
-(* Advanced rewrites ********************************************************)
+(* Advanced constructions ***************************************************)
 
-lemma piter_appl (A) (f) (p) (a): f (f^p a) = f^{A}p (f a).
+lemma piter_appl (A) (f) (p): f ∘ f^p ≐ f^{A}p ∘ f.
 #A #f #p elim p -p //
-#p #IH #a <piter_succ <piter_succ //
+#p #IH @exteq_repl
+/3 width=5 by compose_repl_fwd_dx, compose_repl_fwd_sn, exteq_canc_dx/
+qed.
+
+lemma piter_compose (A) (B) (f) (g) (h) (p):
+      h ∘ f ≐ g ∘ h → h ∘ (f^{A}p) ≐ (g^{B}p) ∘ h.
+#A #B #f #g #h #p elim p -p
+[ #H @exteq_repl
+  /2 width=5 by compose_repl_fwd_sn, compose_repl_fwd_dx/
+| #p #IH #H @exteq_repl
+  [4: @compose_repl_fwd_dx [| @piter_succ ]
+  |5: @compose_repl_fwd_sn [| @piter_succ ]
+  |1,2: skip
+  ]
+  @exteq_trans [2: @compose_assoc |1: skip ]
+  @exteq_trans [2: @(compose_repl_fwd_sn … H) | 1:skip ]
+  @exteq_canc_sn [2: @compose_assoc |1: skip ]
+  /3 width=1 by compose_repl_fwd_dx/
+]
 qed.