notation "\big [ op , nil ]_{ ident j ∈ [a,b[ } f"
with precedence 80
-for @{'bigop ($b-$a) $op $nil (λ${ident j}.((λ${ident j}.$true) (${ident j}+$a)))
+for @{'bigop ($b-$a) $op $nil (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
(λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
(* notation "\big [ op , nil ]_{( term 50) a ≤ ident j < b | p } f"
\big[op,nil]_{i ∈ [a,b[ |p i}(f i).
#a #b # c #p #B #nil #op #f #leab #lebc
>(plus_minus_m_m (c-a) (b-a)) in ⊢ (??%?) /2/
->minus_
minus >(commutative_plus a) <plus_minus_m_m //
+>minus_
plus >(commutative_plus a) <plus_minus_m_m //
>bigop_sum (cut (∀i. b -a ≤ i → i+a = i-(b-a)+b))
[#i #lei >plus_minus // <plus_minus1
[@eq_f @sym_eq @plus_to_minus /2/ | /2/]]
#H @same_bigop #i #ltic @leb_elim normalize // #lei <H //
qed.
+theorem bigop_a: ∀a,b,B.∀nil.∀op:Aop B nil.∀f:nat→B. a ≤ b →
+\big[op,nil]_{i∈[a,S b[ }(f i) =
+ op (\big[op,nil]_{i ∈ [a,b[ }(f (S i))) (f a).
+#a #b #B #nil #op #f #leab
+>(bigop_sumI a (S a) (S b)) [|@le_S_S //|//] @eq_f2
+ [@same_bigop // |<minus_Sn_n normalize @nilr]
+qed.
+
+theorem bigop_0: ∀n,B.∀nil.∀op:Aop B nil.∀f:nat→B.
+\big[op,nil]_{i < S n}(f i) =
+ op (\big[op,nil]_{i < n}(f (S i))) (f 0).
+#n #B #nil #op #f
+<bigop_I >bigop_a [|//] @eq_f2 [|//] <minus_n_O
+@same_bigop //
+qed.
+
theorem bigop_prod: ∀k1,k2,p1,p2,B.∀nil.∀op:Aop B nil.∀f: nat →nat → B.
\big[op,nil]_{x<k1|p1 x}(\big[op,nil]_{i<k2|p2 x i}(f x i)) =
\big[op,nil]_{i<k1*k2|andb (p1 (div i k2)) (p2 (div i k2) (i \mod k2))}
[>bigop_Strue // >Hind >bigop_sum @same_bigop
#i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2/
#eqi [|#H] (>eqi in ⊢ (???%))
- >div_plus_times /2/ >Hp1 >(mod_plus_times …) /2/
+ >div_plus_times /2/ >Hp1 >(mod_plus_times …) /2/ normalize //
|>bigop_Sfalse // >Hind >(pad_bigop (S n*k2)) // @same_bigop
#i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2/
#eqi >eqi in ⊢ (???%) >div_plus_times /2/
{aop :> Aop A nil;
comm: ∀a,b.aop a b = aop b a
}.
-
+
+lemma bigop_op: ∀k,p,B.∀nil.∀op:ACop B nil.∀f,g: nat → B.
+op (\big[op,nil]_{i<k|p i}(f i)) (\big[op,nil]_{i<k|p i}(g i)) =
+ \big[op,nil]_{i<k|p i}(op (f i) (g i)).
+#k #p #B #nil #op #f #g (elim k) [normalize @nill]
+-k #k #Hind (cases (true_or_false (p k))) #H
+ [>bigop_Strue // >bigop_Strue // >bigop_Strue //
+ normalize <assoc <assoc in ⊢ (???%) @eq_f >assoc >comm in ⊢ (??(????%?)?)
+ <assoc @eq_f @Hind
+ |>bigop_Sfalse // >bigop_Sfalse // >bigop_Sfalse //
+ ]
+qed.
+
lemma bigop_diff: ∀p,B.∀nil.∀op:ACop B nil.∀f:nat → B.∀i,n.
i < n → p i = true →
\big[op,nil]_{x<n|p x}(f x)=
[>(not_eq_to_eqb_false … (lt_to_not_eq … Hi)) //] #Hcut
cases (true_or_false (p n)) #pn
[>bigop_Strue // >bigop_Strue //
- >assoc >(comm ?? op (f i) (f n)) <assoc >Hind //
+
normalize >assoc >(comm ?? op (f i) (f n)) <assoc >Hind //
|>bigop_Sfalse // >bigop_Sfalse // >Hind //
]
|<Hi >bigop_Strue // @eq_f >bigop_Sfalse
]
qed.
-(* Sigma e Pi *)
+(* distributivity *)
+
+record Dop (A:Type[0]) (nil:A): Type[0] ≝
+ {sum : ACop A nil;
+ prod: A → A →A;
+ null: \forall a. prod a nil = nil;
+ distr: ∀a,b,c:A. prod a (sum b c) = sum (prod a b) (prod a c)
+ }.
+
+theorem bigop_distr: ∀n,p,B,nil.∀R:Dop B nil.\forall f,a.
+ let aop \def sum B nil R in
+ let mop \def prod B nil R in
+ mop a \big[aop,nil]_{i<n|p i}(f i) =
+ \big[aop,nil]_{i<n|p i}(mop a (f i)).
+#n #p #B #nil #R #f #a normalize (elim n) [@null]
+#n #Hind (cases (true_or_false (p n))) #H
+ [>bigop_Strue // >bigop_Strue // >(distr B nil R) >Hind //
+ |>bigop_Sfalse // >bigop_Sfalse //
+ ]
+qed.
+
+(* Sigma e Pi
+
+
notation "Σ_{ ident i < n | p } f"
with precedence 80
for @{'bigop $n plus 0 (λ${ident i}.p) (λ${ident i}. $f)}.
with precedence 80
for @{'bigop ($b-$a) times 1 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
(λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
-
+
+*)
(*
definition p_ord_times \def
]
qed.
-(*distributive property for iter_p_gen*)
-theorem distributive_times_plus_iter_p_gen: \forall A:Type.
-\forall plusA: A \to A \to A. \forall basePlusA: A.
-\forall timesA: A \to A \to A.
-\forall n:nat. \forall k:A. \forall p:nat \to bool. \forall g:nat \to A.
-(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a basePlusA) = a) \to
-(symmetric A timesA) \to (distributive A timesA plusA) \to
-(\forall a:A. (timesA a basePlusA) = basePlusA)
-
- \to
-((timesA k (iter_p_gen n p A g basePlusA plusA)) =
- (iter_p_gen n p A (\lambda i:nat.(timesA k (g i))) basePlusA plusA)).
-intros.
-elim n
-[ simplify.
- apply H5
-| cut( (p n1) = true \lor (p n1) = false)
- [ elim Hcut
- [ rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H7).
- rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H7) in \vdash (? ? ? %).
- rewrite > (H4).
- rewrite > (H3 k (g n1)).
- apply eq_f.
- assumption
- | rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H7).
- rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H7) in \vdash (? ? ? %).
- assumption
- ]
- | elim ((p n1))
- [ left.
- reflexivity
- | right.
- reflexivity
- ]
- ]
-]
-qed.
theorem iter_p_gen_2_eq:
\forall A:Type.
projects / helm.git / blobdiff