some notational experiments

diff --git a/helm/software/matita/library/nat/pi_p.ma b/helm/software/matita/library/nat/pi_p.ma
index 0c5e0d7014bda9cfcc98fb061738499b726d5211..b526e8d51be947dd7cc114340b6ccf75da4ee765 100644 (file)
--- a/helm/software/matita/library/nat/pi_p.ma
+++ b/helm/software/matita/library/nat/pi_p.ma
@@ -22,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.
@@ -358,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.