X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fpi_p.ma;h=b526e8d51be947dd7cc114340b6ccf75da4ee765;hb=4dc47c9675ffd5fa50296ffaa9b5997501518c98;hp=e649f5f193ecdda0b0d9e7fc0c54b0d7355a233c;hpb=6db38e3d8e4083765f2fce40c7845c9827b9afd0;p=helm.git

diff --git a/helm/software/matita/library/nat/pi_p.ma b/helm/software/matita/library/nat/pi_p.ma
index e649f5f19..b526e8d51 100644
--- a/helm/software/matita/library/nat/pi_p.ma
+++ b/helm/software/matita/library/nat/pi_p.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/pi_p".
-
 include "nat/primes.ma".
 (* include "nat/ord.ma". *)
 include "nat/generic_iter_p.ma".
@@ -24,9 +22,40 @@ include "nat/iteration2.ma".
 definition pi_p: nat \to (nat \to bool) \to (nat \to nat) \to nat \def
 \lambda n, p, g. (iter_p_gen n p nat g (S O) times).
 
-theorem true_to_pi_p_Sn: 
-\forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
-p n = true \to pi_p (S n) p g = (g n)*(pi_p n p g).
+(*
+notation < "(mstyle scriptlevel 1 scriptsizemultiplier 1.7(Π) ­
+             ) 
+            \below 
+            (p
+            \atop 
+            (ident i < n)) f" 
+non associative with precedence 60 for 
+@{ 'product $n (λ${ident i}:$xx1.$p) (λ${ident i}:$xx2.$f) }.
+
+notation < "(mstyle scriptlevel 1 scriptsizemultiplier 1.7(Π) ­
+             ) 
+            \below 
+            ((ident i < n)) f" 
+non associative with precedence 60 for 
+@{ 'product $n (λ_:$xx1.$xx3) (λ${ident i}:$xx2.$f) }.
+
+interpretation "big product" 'product n p f = (pi_p n p f).
+
+notation > "'Pi' (ident x) < n | p . term 46 f"
+non associative with precedence 60
+for @{ 'product $n (λ${ident x}.$p) (λ${ident x}.$f) }. 
+
+notation > "'Pi' (ident x) ≤ n | p . term 46 f"
+non associative with precedence 60
+for @{ 'product (S $n) (λ${ident x}.$p) (λ${ident x}.$f) }. 
+
+notation > "'Pi' (ident x) < n . term 46 f"
+non associative with precedence 60
+for @{ 'product $n (λ_.true) (λ${ident x}.$f) }. 
+*)
+
+theorem true_to_pi_p_Sn: ∀n,p,g.
+  p n = true \to pi_p (S n) p g = (g n)*(pi_p n p g).
 intros.
 unfold pi_p.
 apply true_to_iter_p_gen_Sn.
@@ -200,17 +229,16 @@ theorem le_pi_p:
 (\forall i. i < n \to p i = true \to g1 i \le g2 i ) \to 
 pi_p n p g1 \le pi_p n p g2.
 intros.
-generalize in match H.
-elim n
+elim n in H ⊢ %
   [apply le_n.
   |apply (bool_elim ? (p n1));intros
     [rewrite > true_to_pi_p_Sn
       [rewrite > true_to_pi_p_Sn in ⊢ (? ? %)
         [apply le_times
-          [apply H2[apply le_n|assumption]
-          |apply H1.
+          [apply H1[apply le_n|assumption]
+          |apply H.
            intros.
-           apply H2[apply le_S.assumption|assumption]
+           apply H1[apply le_S.assumption|assumption]
           ]
         |assumption
         ]
@@ -218,9 +246,9 @@ elim n
       ]
     |rewrite > false_to_pi_p_Sn
       [rewrite > false_to_pi_p_Sn in ⊢ (? ? %)
-        [apply H1.
+        [apply H.
          intros.
-         apply H2[apply le_S.assumption|assumption]
+         apply H1[apply le_S.assumption|assumption]
         |assumption
         ]
       |assumption
@@ -257,6 +285,35 @@ elim n
   ]
 qed.
 
+theorem exp_sigma_p1: \forall n,a,p,f. 
+pi_p n p (\lambda x.(exp a (f x))) = (exp a (sigma_p n p f)).
+intros.
+elim n
+  [reflexivity
+  |apply (bool_elim ? (p n1))
+    [intro.
+     rewrite > true_to_pi_p_Sn
+      [rewrite > true_to_sigma_p_Sn
+        [simplify.
+         rewrite > H.
+         rewrite > exp_plus_times.
+         reflexivity.
+        |assumption
+        ]
+      |assumption
+      ]
+    |intro.
+     rewrite > false_to_pi_p_Sn
+      [rewrite > false_to_sigma_p_Sn
+        [simplify.assumption
+        |assumption
+        ]
+      |assumption
+      ]
+    ]
+  ]
+qed.
+
 theorem times_pi_p: \forall n,p,f,g. 
 pi_p n p (\lambda x.f x*g x) = pi_p n p f * pi_p n p  g. 
 intros.
@@ -332,13 +389,17 @@ theorem pi_p_knm:
 \forall p1,p21:nat \to bool.
 \forall p22:nat \to nat \to bool.
 (\forall x. x < k \to p1 x = true \to 
-p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true
+p21 (h11 x) = true ∧ p22 (h11 x) (h12 x) = true
 \land h2 (h11 x) (h12 x) = x 
 \land (h11 x) < n \land (h12 x) < m) \to
 (\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to 
 p1 (h2 i j) = true \land 
 h11 (h2 i j) = i \land h12 (h2 i j) = j
-\land h2 i j < k) \to
+\land h2 i j < k) →
+(*
+Pi z < k | p1 z. g z = 
+Pi x < n | p21 x. Pi y < m | p22 x y.g (h2 x y).
+*)
 pi_p k p1 g =
 pi_p n p21 (\lambda x:nat.pi_p m (p22 x) (\lambda y. g (h2 x y))).
 intros.