include "basics/types.ma".
include "arithmetics/div_and_mod.ma".
-definition sameF_upto: nat → ∀A.relation(nat→A) ≝
-λk.λA.λf,g.∀i. i < k → f i = g i.
+\ 5img class="anchor" src="icons/tick.png" id="sameF_upto"\ 6definition sameF_upto: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → ∀A.\ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→A) ≝
+λk.λA.λf,g.∀i. i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 k → f i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g i.
-definition sameF_p: nat → (nat → bool) →∀A.relation(nat→A) ≝
-λk,p,A,f,g.∀i. i < k → p i = true → f i = g i.
+\ 5img class="anchor" src="icons/tick.png" id="sameF_p"\ 6definition sameF_p: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → (\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) →∀A.\ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→A) ≝
+λk,p,A,f,g.∀i. i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 k → p i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → f i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g i.
-lemma sameF_upto_le: ∀A,f,g,n,m.
- n ≤m → sameF_upto m A f g → sameF_upto n A f g.
-#A #f #g #n #m #lenm #samef #i #ltin @samef /2/
+\ 5img class="anchor" src="icons/tick.png" id="sameF_upto_le"\ 6lemma sameF_upto_le: ∀A,f,g,n,m.
+ n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6m → \ 5a href="cic:/matita/arithmetics/bigops/sameF_upto.def(2)"\ 6sameF_upto\ 5/a\ 6 m A f g → \ 5a href="cic:/matita/arithmetics/bigops/sameF_upto.def(2)"\ 6sameF_upto\ 5/a\ 6 n A f g.
+#A #f #g #n #m #lenm #samef #i #ltin @samef /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"\ 6lt_to_le_to_lt\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.
-lemma sameF_p_le: ∀A,p,f,g,n,m.
- n ≤m → sameF_p m p A f g → sameF_p n p A f g.
-#A #p #f #g #n #m #lenm #samef #i #ltin #pi @samef /2/
+\ 5img class="anchor" src="icons/tick.png" id="sameF_p_le"\ 6lemma sameF_p_le: ∀A,p,f,g,n,m.
+ n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6m → \ 5a href="cic:/matita/arithmetics/bigops/sameF_p.def(2)"\ 6sameF_p\ 5/a\ 6 m p A f g → \ 5a href="cic:/matita/arithmetics/bigops/sameF_p.def(2)"\ 6sameF_p\ 5/a\ 6 n p A f g.
+#A #p #f #g #n #m #lenm #samef #i #ltin #pi @samef /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"\ 6lt_to_le_to_lt\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.
-(*
-definition sumF ≝ λA.λf,g:nat → A.λn,i.
-if_then_else ? (leb n i) (g (i-n)) (f i).
-
-lemma sumF_unfold: ∀A,f,g,n,i.
-sumF A f g n i = if_then_else ? (leb n i) (g (i-n)) (f i).
-// qed. *)
-
-definition prodF ≝
- λA,B.λf:nat→A.λg:nat→B.λm,x.〈 f(div x m), g(mod x m) 〉.
+\ 5img class="anchor" src="icons/tick.png" id="prodF"\ 6definition prodF ≝
+ λA,B.λf:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→A.λg:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B.λm,x.〈 f(\ 5a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"\ 6div\ 5/a\ 6 x m), g(\ 5a href="cic:/matita/arithmetics/div_and_mod/mod.def(3)"\ 6mod\ 5/a\ 6 x m) \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6.
(* bigop *)
-let rec bigop (n:nat) (p:nat → bool) (B:Type[0])
- (nil: B) (op: B → B → B) (f: nat → B) ≝
+\ 5img class="anchor" src="icons/tick.png" id="bigop"\ 6let rec bigop (n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (p:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) (B:Type[0])
+ (nil: B) (op: B → B → B) (f: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → B) ≝
match n with
[ O ⇒ nil
| S k ⇒
with precedence 80
for @{'bigop ($b-$a) $op $nil (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
(λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
-
+
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)))
(λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
-
+
(* notation "\big [ op , nil ]_{( term 50) a ≤ ident j < b | p } f"
with precedence 80
for @{\big[$op,$nil]_{${ident j} < ($b-$a) | ((λ${ident j}.$p) (${ident j}+$a))}((λ${ident j}.$f)(${ident j}+$a))}.
interpretation "bigop" 'bigop n op nil p f = (bigop n p ? nil op f).
-lemma bigop_Strue: ∀k,p,B,nil,op.∀f:nat→B. p k = true →
- \big[op,nil]_{i < S k | p i}(f i) =
- op (f k) (\big[op,nil]_{i < k | p i}(f i)).
+\ 5img class="anchor" src="icons/tick.png" id="bigop_Strue"\ 6lemma bigop_Strue: ∀k,p,B,nil,op.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B. p k \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 →
+ \big[op,nil]_{i < \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 k | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
+ op (f k) (\big[op,nil]_{i < k | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i)).
#k #p #B #nil #op #f #H normalize >H // qed.
-lemma bigop_Sfalse: ∀k,p,B,nil,op.∀f:nat→B. p k = false →
- \big[op,nil]_{ i < S k | p i}(f i) =
- \big[op,nil]_{i < k | p i}(f i).
+\ 5img class="anchor" src="icons/tick.png" id="bigop_Sfalse"\ 6lemma bigop_Sfalse: ∀k,p,B,nil,op.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B. p k \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 →
+ \big[op,nil]_{ i < \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 k | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
+ \big[op,nil]_{i < k | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i).
#k #p #B #nil #op #f #H normalize >H // qed.
-lemma same_bigop : ∀k,p1,p2,B,nil,op.∀f,g:nat→B.
- sameF_upto k bool p1 p2 → sameF_p k p1 B f g →
- \big[op,nil]_{i < k | p1 i}(f i) =
- \big[op,nil]_{i < k | p2 i}(g i).
+\ 5img class="anchor" src="icons/tick.png" id="same_bigop"\ 6lemma same_bigop : ∀k,p1,p2,B,nil,op.∀f,g:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B.
+ \ 5a href="cic:/matita/arithmetics/bigops/sameF_upto.def(2)"\ 6sameF_upto\ 5/a\ 6 k \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 p1 p2 → \ 5a href="cic:/matita/arithmetics/bigops/sameF_p.def(2)"\ 6sameF_p\ 5/a\ 6 k p1 B f g →
+ \big[op,nil]_{i < k | p1 i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
+ \big[op,nil]_{i < k | p2 i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(g i).
#k #p1 #p2 #B #nil #op #f #g (elim k) //
-#n #Hind #samep #samef normalize >Hind /2/
-<(samep … (le_n …)) cases(true_or_false (p1 n)) #H1 >H1
-normalize // <(samef … (le_n …) H1) //
+#n #Hind #samep #samef normalize >Hind
+ [|@(\ 5a href="cic:/matita/arithmetics/bigops/sameF_p_le.def(5)"\ 6sameF_p_le\ 5/a\ 6 … samef) // |@(\ 5a href="cic:/matita/arithmetics/bigops/sameF_upto_le.def(5)"\ 6sameF_upto_le\ 5/a\ 6 … samep) //]
+<(samep … (\ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"\ 6le_n\ 5/a\ 6 …)) cases(\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p1 n)) #H1 >H1
+normalize // <(samef … (\ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"\ 6le_n\ 5/a\ 6 …) H1) //
qed.
-theorem pad_bigop: ∀k,n,p,B,nil,op.∀f:nat→B. n ≤ k →
-\big[op,nil]_{i < n | p i}(f i)
- = \big[op,nil]_{i < k | if_then_else ? (leb n i) false (p i)}(f i).
+\ 5img class="anchor" src="icons/tick.png" id="pad_bigop"\ 6theorem pad_bigop: ∀k,n,p,B,nil,op.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 k →
+\big[op,nil]_{i < n | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i)
+ \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \big[op,nil]_{i < k | \ 5font class="Apple-style-span" color="#FF0000"\ 6if\ 5/font\ 6 (\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 n i) then \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 else p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i).
#k #n #p #B #nil #op #f #lenk (elim lenk)
- [@same_bigop #i #lti // >(not_le_to_leb_false …) /2/
- |#j #leup #Hind >bigop_Sfalse >(le_to_leb_true … leup) //
+ [@\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6 #i #lti // >(\ 5a href="cic:/matita/arithmetics/nat/not_le_to_leb_false.def(7)"\ 6not_le_to_leb_false\ 5/a\ 6 …) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"\ 6lt_to_not_le\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ |#j #leup #Hind >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 >(\ 5a href="cic:/matita/arithmetics/nat/le_to_leb_true.def(7)"\ 6le_to_leb_true\ 5/a\ 6 … leup) //
] qed.
-record Aop (A:Type[0]) (nil:A) : Type[0] ≝
+\ 5img class="anchor" src="icons/tick.png" id="pad_bigop1"\ 6theorem pad_bigop1: ∀k,n,p,B,nil,op.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 k →
+ (∀i. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 i → i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 k → p i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6) →
+ \big[op,nil]_{i < n | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i)
+ \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \big[op,nil]_{i < k | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i).
+#k #n #p #B #nil #op #f #lenk (elim lenk)
+ [#_ @\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6 #i #lti //
+ |#j #leup #Hind #Hfalse >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6
+ [@Hind #i #leni #ltij @Hfalse // @\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"\ 6le_S\ 5/a\ 6 //
+ |@Hfalse //
+ ]
+ ]
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="bigop_false"\ 6theorem bigop_false: ∀n,B,nil,op.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B.
+ \big[op,nil]_{i < n | \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 nil.
+#n #B #nil #op #f elim n // #n1 #Hind
+>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 //
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="Aop"\ 6record Aop (A:Type[0]) (nil:A) : Type[0] ≝
{op :2> A → A → A;
- nill:∀a. op nil a = a;
- nilr:∀a. op a nil = a;
- assoc: ∀a,b,c.op a (op b c) = op (op a b) c
+ nill:∀a. op nil a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a;
+ nilr:∀a. op a nil \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a;
+ assoc: ∀a,b,c.op a (op b c) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 op (op a b) c
}.
-theorem bigop_sum: ∀k1,k2,p1,p2,B.∀nil.∀op:Aop B nil.∀f,g:nat→B.
-op (\big[op,nil]_{i<k1|p1 i}(f i)) \big[op,nil]_{i<k2|p2 i}(g i) =
- \big[op,nil]_{i<k1+k2|if_then_else ? (leb k2 i) (p1 (i-k2)) (p2 i)}
- (if_then_else ? (leb k2 i) (f (i-k2)) (g i)).
+\ 5img class="anchor" src="icons/tick.png" id="pad_bigop_nil"\ 6theorem pad_bigop_nil: ∀k,n,p,B,nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 k →
+ (∀i. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 i → i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 k → p i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 f i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 nil) →
+ \big[op,nil]_{i < n | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i)
+ \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \big[op,nil]_{i < k | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i).
+#k #n #p #B #nil #op #f #lenk (elim lenk)
+ [#_ @\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6 #i #lti //
+ |#j #leup #Hind #Hfalse cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p j)) #Hpj
+ [>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 //
+ cut (f j \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 nil)
+ [cases (Hfalse j leup (\ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"\ 6le_n\ 5/a\ 6 … )) // >Hpj #H destruct (H)] #Hfj
+ >Hfj >\ 5a href="cic:/matita/arithmetics/bigops/nill.fix(0,2,2)"\ 6nill\ 5/a\ 6 @Hind #i #leni #ltij
+ cases (Hfalse i leni (\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"\ 6le_S\ 5/a\ 6 … ltij)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ |>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 // @Hind #i #leni #ltij
+ cases (Hfalse i leni (\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"\ 6le_S\ 5/a\ 6 … ltij)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ ]
+ ]
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="bigop_sum"\ 6theorem bigop_sum: ∀k1,k2,p1,p2,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f,g:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B.
+op (\big[op,nil]_{i<k1|p1 i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i)) \big[op,nil]_{i<k2|p2 i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(g i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
+ \big[op,nil]_{i<k1\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6k2|\ 5font class="Apple-style-span" color="#FF0000"\ 6 if \ 5/font\ 6\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 k2 i then p1 (i\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6k2) else p2 i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6
+ (if \ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 k2 i then f (i\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6k2) else g i).
#k1 #k2 #p1 #p2 #B #nil #op #f #g (elim k1)
- [normalize >nill @same_bigop #i #lti
- >(lt_to_leb_false … lti) normalize /2/
- |#i #Hind normalize <minus_plus_m_m (cases (p1 i))
- >(le_to_leb_true … (le_plus_n …)) normalize <Hind //
- <assoc //
+ [normalize >\ 5a href="cic:/matita/arithmetics/bigops/nill.fix(0,2,2)"\ 6nill\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6 #i #lti
+ >(\ 5a href="cic:/matita/arithmetics/nat/lt_to_leb_false.def(8)"\ 6lt_to_leb_false\ 5/a\ 6 … lti) normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
+ |#i #Hind normalize <\ 5a href="cic:/matita/arithmetics/nat/minus_plus_m_m.def(6)"\ 6minus_plus_m_m\ 5/a\ 6 (cases (p1 i))
+ >(\ 5a href="cic:/matita/arithmetics/nat/le_to_leb_true.def(7)"\ 6le_to_leb_true\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/nat/le_plus_n.def(7)"\ 6le_plus_n\ 5/a\ 6 …)) normalize <Hind //
+ <\ 5a href="cic:/matita/arithmetics/bigops/assoc.fix(0,2,2)"\ 6assoc\ 5/a\ 6 //
]
qed.
-lemma plus_minus1: ∀a,b,c. c ≤ b → a + (b -c) = a + b -c.
-#a #b #c #lecb @sym_eq @plus_to_minus >(commutative_plus c)
->associative_plus <plus_minus_m_m //
+\ 5img class="anchor" src="icons/tick.png" id="plus_minus1"\ 6lemma plus_minus1: ∀a,b,c. c \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 b → a \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 (b \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6c) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 b \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6c.
+#a #b #c #lecb @\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"\ 6plus_to_minus\ 5/a\ 6 >(\ 5a href="cic:/matita/arithmetics/nat/commutative_plus.def(5)"\ 6commutative_plus\ 5/a\ 6 c)
+>\ 5a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"\ 6associative_plus\ 5/a\ 6 <\ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"\ 6plus_minus_m_m\ 5/a\ 6 //
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="bigop_I"\ 6theorem bigop_I: ∀n,p,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B.
+\big[op,nil]_{i∈[\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6,n[ |p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \big[op,nil]_{i < n|p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i).
+#n #p #B #nil #op #f <\ 5a href="cic:/matita/arithmetics/nat/minus_n_O.def(3)"\ 6minus_n_O\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6 //
qed.
-theorem bigop_I: ∀n,p,B.∀nil.∀op:Aop B nil.∀f:nat→B.
-\big[op,nil]_{i∈[0,n[ |p i}(f i) = \big[op,nil]_{i < n|p i}(f i).
-#n #p #B #nil #op #f <minus_n_O @same_bigop //
+\ 5img class="anchor" src="icons/tick.png" id="bigop_I_gen"\ 6theorem bigop_I_gen: ∀a,b,p,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B. a \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6b →
+\big[op,nil]_{i∈[a,b[ |p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \big[op,nil]_{i < b|\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 a i \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i).
+#a #b elim b // -b #b #Hind #p #B #nil #op #f #lea
+cut (∀a,b. a \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 b → \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 b \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (b \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6a))
+ [#a #b cases a // #a1 #lta1 normalize >\ 5a href="cic:/matita/arithmetics/nat/eq_minus_S_pred.def(4)"\ 6eq_minus_S_pred\ 5/a\ 6 >\ 5a href="cic:/matita/arithmetics/nat/S_pred.def(3)"\ 6S_pred\ 5/a\ 6
+ /2 by \ 5a href="cic:/matita/arithmetics/nat/lt_plus_to_minus_r.def(11)"\ 6lt_plus_to_minus_r\ 5/a\ 6/] #Hcut
+cases (\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 … lea) #Ha
+ [cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p b)) #Hcase
+ [>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 [2: >Hcase >(\ 5a href="cic:/matita/arithmetics/nat/le_to_leb_true.def(7)"\ 6le_to_leb_true\ 5/a\ 6 a b) // @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 @Ha]
+ >(Hcut … (\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 … Ha))
+ >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6
+ [@\ 5a href="cic:/matita/basics/logic/eq_f2.def(3)"\ 6eq_f2\ 5/a\ 6
+ [@\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 <\ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"\ 6plus_minus_m_m\ 5/a\ 6 [//|@\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 //] @Hind
+ |@Hind @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 //
+ ]
+ |<\ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"\ 6plus_minus_m_m\ 5/a\ 6 // @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 //
+ ]
+ |>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 [2: >Hcase cases (\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 a b)//]
+ >(Hcut … (\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 … Ha)) >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6
+ [@Hind @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 // | <\ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"\ 6plus_minus_m_m\ 5/a\ 6 // @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 //]
+ ]
+ |<Ha <\ 5a href="cic:/matita/arithmetics/nat/minus_n_n.def(4)"\ 6minus_n_n\ 5/a\ 6 whd in ⊢ (??%?); <(\ 5a href="cic:/matita/arithmetics/bigops/bigop_false.def(4)"\ 6bigop_false\ 5/a\ 6 a B nil op f) in ⊢ (??%?);
+ @\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6 // #i #ltia >(\ 5a href="cic:/matita/arithmetics/nat/not_le_to_leb_false.def(7)"\ 6not_le_to_leb_false\ 5/a\ 6 a i) // @\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"\ 6lt_to_not_le\ 5/a\ 6 //
+ ]
qed.
-theorem bigop_sumI: ∀a,b,c,p,B.∀nil.∀op:Aop B nil.∀f:nat→B.
-a ≤ b → b ≤ c →
-\big[op,nil]_{i∈[a,c[ |p i}(f i) =
- op (\big[op,nil]_{i ∈ [b,c[ |p i}(f i))
- \big[op,nil]_{i ∈ [a,b[ |p i}(f i).
+\ 5img class="anchor" src="icons/tick.png" id="bigop_sumI"\ 6theorem bigop_sumI: ∀a,b,c,p,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B.
+a \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 b → b \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 c →
+\big[op,nil]_{i∈[a,c[ |p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
+ op (\big[op,nil]_{i ∈ [b,c[ |p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i))
+ \big[op,nil]_{i ∈ [a,b[ |p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i).
#a #b # c #p #B #nil #op #f #leab #lebc
->(plus_minus_m_m (c-a) (b-a)) in ⊢ (??%?) /2/
->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 //
+>(\ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"\ 6plus_minus_m_m\ 5/a\ 6 (c\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6a) (b\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6a)) in ⊢ (??%?); /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/monotonic_le_minus_l.def(9)"\ 6monotonic_le_minus_l\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+>\ 5a href="cic:/matita/arithmetics/nat/minus_plus.def(13)"\ 6minus_plus\ 5/a\ 6 >(\ 5a href="cic:/matita/arithmetics/nat/commutative_plus.def(5)"\ 6commutative_plus\ 5/a\ 6 a) <\ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"\ 6plus_minus_m_m\ 5/a\ 6 //
+>\ 5a href="cic:/matita/arithmetics/bigops/bigop_sum.def(9)"\ 6bigop_sum\ 5/a\ 6 (cut (∀i. b \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6a \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 i → i\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 i\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6(b\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6a)\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6b))
+ [#i #lei >\ 5a href="cic:/matita/arithmetics/nat/plus_minus.def(5)"\ 6plus_minus\ 5/a\ 6 // <\ 5a href="cic:/matita/arithmetics/bigops/plus_minus1.def(8)"\ 6plus_minus1\ 5/a\ 6
+ [@\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 @\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"\ 6plus_to_minus\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/bigops/plus_minus1.def(8)"\ 6plus_minus1\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/monotonic_le_minus_l.def(9)"\ 6monotonic_le_minus_l\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]]
+#H @\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6 #i #ltic @\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"\ 6leb_elim\ 5/a\ 6 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).
+\ 5img class="anchor" src="icons/tick.png" id="bigop_a"\ 6theorem bigop_a: ∀a,b,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B. a \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 b →
+\big[op,nil]_{i∈[a,\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 b[ \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
+ op (\big[op,nil]_{i ∈ [a,b[ \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 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]
+>(\ 5a href="cic:/matita/arithmetics/bigops/bigop_sumI.def(14)"\ 6bigop_sumI\ 5/a\ 6 a (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 a) (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 b)) [|@\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"\ 6le_S_S\ 5/a\ 6 //|//] @\ 5a href="cic:/matita/basics/logic/eq_f2.def(3)"\ 6eq_f2\ 5/a\ 6
+ [@\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6 // |<\ 5a href="cic:/matita/arithmetics/nat/minus_Sn_n.def(4)"\ 6minus_Sn_n\ 5/a\ 6 normalize @\ 5a href="cic:/matita/arithmetics/bigops/nilr.fix(0,2,2)"\ 6nilr\ 5/a\ 6]
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).
+\ 5img class="anchor" src="icons/tick.png" id="bigop_0"\ 6theorem bigop_0: ∀n,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B.
+\big[op,nil]_{i < \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
+ op (\big[op,nil]_{i < n\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 i))) (f \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6).
#n #B #nil #op #f
-<bigop_I >bigop_a [|//] @eq_f2 [|//] <minus_n_O
-@same_bigop //
+<\ 5a href="cic:/matita/arithmetics/bigops/bigop_I.def(7)"\ 6bigop_I\ 5/a\ 6 >\ 5a href="cic:/matita/arithmetics/bigops/bigop_a.def(15)"\ 6bigop_a\ 5/a\ 6 [|//] @\ 5a href="cic:/matita/basics/logic/eq_f2.def(3)"\ 6eq_f2\ 5/a\ 6 [|//] <\ 5a href="cic:/matita/arithmetics/nat/minus_n_O.def(3)"\ 6minus_n_O\ 5/a\ 6
+@\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6 //
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))}
- (f (div i k2) (i \mod k2)).
+\ 5img class="anchor" src="icons/tick.png" id="bigop_prod"\ 6theorem bigop_prod: ∀k1,k2,p1,p2,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 →\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → B.
+\big[op,nil]_{x<k1|p1 x\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(\big[op,nil]_{i<k2|p2 x i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f x i)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
+ \big[op,nil]_{i<k1\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6k2|\ 5a href="cic:/matita/basics/bool/andb.def(1)"\ 6andb\ 5/a\ 6 (p1 (\ 5a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"\ 6div\ 5/a\ 6 i k2)) (p2 (\ 5a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"\ 6div\ 5/a\ 6 i k2) (i \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 k2))\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6
+ (f (\ 5a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"\ 6div\ 5/a\ 6 i k2) (i \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 k2)).
#k1 #k2 #p1 #p2 #B #nil #op #f (elim k1) //
-#n #Hind cases(true_or_false (p1 n)) #Hp1
- [>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/
- |>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/
+#n #Hind cases(\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p1 n)) #Hp1
+ [>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 // >Hind >\ 5a href="cic:/matita/arithmetics/bigops/bigop_sum.def(9)"\ 6bigop_sum\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6
+ #i #lti @\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"\ 6leb_elim\ 5/a\ 6 // #lei cut (i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6k2\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6(i\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6k2)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/bigops/plus_minus1.def(8)"\ 6plus_minus1\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ #eqi [|#H] >eqi in ⊢ (???%);
+ >\ 5a href="cic:/matita/arithmetics/div_and_mod/div_plus_times.def(14)"\ 6div_plus_times\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/lt_plus_to_lt_l.def(6)"\ 6lt_plus_to_lt_l\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ >Hp1 >(\ 5a href="cic:/matita/arithmetics/div_and_mod/mod_plus_times.def(14)"\ 6mod_plus_times\ 5/a\ 6 …) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6, \ 5a href="cic:/matita/arithmetics/nat/lt_plus_to_lt_l.def(6)"\ 6lt_plus_to_lt_l\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ |>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 // >Hind >(\ 5a href="cic:/matita/arithmetics/bigops/pad_bigop.def(8)"\ 6pad_bigop\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6k2)) // @\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6
+ #i #lti @\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"\ 6leb_elim\ 5/a\ 6 // #lei cut (i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6k2\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6(i\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6k2)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/bigops/plus_minus1.def(8)"\ 6plus_minus1\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ #eqi >eqi in ⊢ (???%); >\ 5a href="cic:/matita/arithmetics/div_and_mod/div_plus_times.def(14)"\ 6div_plus_times\ 5/a\ 6 [ >Hp1 %| /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_minus_l.def(12)"\ 6monotonic_lt_minus_l\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
]
qed.
-record ACop (A:Type[0]) (nil:A) : Type[0] ≝
- {aop :> Aop A nil;
- comm: ∀a,b.aop a b = aop b a
+\ 5img class="anchor" src="icons/tick.png" id="ACop"\ 6record ACop (A:Type[0]) (nil:A) : Type[0] ≝
+ {aop :> \ 5a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 A nil;
+ comm: ∀a,b.aop a b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 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 //
- <assoc <assoc in ⊢ (???%) @eq_f >assoc >comm in ⊢ (??(????%?)?)
- <assoc @eq_f @Hind
- |>bigop_Sfalse // >bigop_Sfalse // >bigop_Sfalse //
+\ 5img class="anchor" src="icons/tick.png" id="bigop_op"\ 6lemma bigop_op: ∀k,p,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/ACop.ind(1,0,2)"\ 6ACop\ 5/a\ 6 B nil.∀f,g: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → B.
+op (\big[op,nil]_{i<k|p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i)) (\big[op,nil]_{i<k|p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(g i)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
+ \big[op,nil]_{i<k|p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(op (f i) (g i)).
+#k #p #B #nil #op #f #g (elim k) [normalize @\ 5a href="cic:/matita/arithmetics/bigops/nill.fix(0,2,2)"\ 6nill\ 5/a\ 6]
+-k #k #Hind (cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p k))) #H
+ [>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 // >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 // >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 //
+ normalize <\ 5a href="cic:/matita/arithmetics/bigops/assoc.fix(0,2,2)"\ 6assoc\ 5/a\ 6 <\ 5a href="cic:/matita/arithmetics/bigops/assoc.fix(0,2,2)"\ 6assoc\ 5/a\ 6 in ⊢ (???%); @\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 >\ 5a href="cic:/matita/arithmetics/bigops/assoc.fix(0,2,2)"\ 6assoc\ 5/a\ 6
+ >\ 5a href="cic:/matita/arithmetics/bigops/comm.fix(0,2,3)"\ 6comm\ 5/a\ 6 in ⊢ (??(????%?)?); <\ 5a href="cic:/matita/arithmetics/bigops/assoc.fix(0,2,2)"\ 6assoc\ 5/a\ 6 @\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 @Hind
+ |>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 // >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 // >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 //
]
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)=
- op (f i) (\big[op,nil]_{x<n|andb(notb(eqb i x))(p x)}(f x)).
+\ 5img class="anchor" src="icons/tick.png" id="bigop_diff"\ 6lemma bigop_diff: ∀p,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/ACop.ind(1,0,2)"\ 6ACop\ 5/a\ 6 B nil.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → B.∀i,n.
+ i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → p i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 →
+ \big[op,nil]_{x<n|p x\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f x)\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
+ op (f i) (\big[op,nil]_{x<n|\ 5a href="cic:/matita/basics/bool/andb.def(1)"\ 6andb\ 5/a\ 6(\ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 i x))(p x)\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f x)).
#p #B #nil #op #f #i #n (elim n)
- [#ltO @False_ind /2/
- |#n #Hind #lein #pi cases (le_to_or_lt_eq … (le_S_S_to_le …lein)) #Hi
- [cut (andb(notb(eqb i n))(p n) = (p n))
- [>(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 //
- |>bigop_Sfalse // >bigop_Sfalse // >Hind //
+ [#ltO @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ |#n #Hind #lein #pi cases (\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 …lein)) #Hi
+ [cut (\ 5a href="cic:/matita/basics/bool/andb.def(1)"\ 6andb\ 5/a\ 6(\ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 i n))(p n) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (p n))
+ [>(\ 5a href="cic:/matita/arithmetics/nat/not_eq_to_eqb_false.def(6)"\ 6not_eq_to_eqb_false\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_eq.def(7)"\ 6lt_to_not_eq\ 5/a\ 6 … Hi)) //] #Hcut
+ cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p n)) #pn
+ [>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 // >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 //
+ normalize >\ 5a href="cic:/matita/arithmetics/bigops/assoc.fix(0,2,2)"\ 6assoc\ 5/a\ 6 >(\ 5a href="cic:/matita/arithmetics/bigops/comm.fix(0,2,3)"\ 6comm\ 5/a\ 6 ?? op (f i) (f n)) <\ 5a href="cic:/matita/arithmetics/bigops/assoc.fix(0,2,2)"\ 6assoc\ 5/a\ 6 >Hind //
+ |>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 // >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 // >Hind //
]
- |<Hi >bigop_Strue // @eq_f >bigop_Sfalse
- [@same_bigop // #k #ltki >not_eq_to_eqb_false /2/
- |>eq_to_eqb_true //
+ |<Hi >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 // @\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6
+ [@\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6 // #k #ltki >\ 5a href="cic:/matita/arithmetics/nat/not_eq_to_eqb_false.def(6)"\ 6not_eq_to_eqb_false\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ |>\ 5a href="cic:/matita/arithmetics/nat/eq_to_eqb_true.def(5)"\ 6eq_to_eqb_true\ 5/a\ 6 //
]
]
]
qed.
(* range *)
-record range (A:Type[0]): Type[0] ≝
- {enum:nat→A; upto:nat; filter:nat→bool}.
+\ 5img class="anchor" src="icons/tick.png" id="range"\ 6record range (A:Type[0]): Type[0] ≝
+ {enum:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→A; upto:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6; filter:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6}.
-definition sub_hk: (nat→nat)→(nat→nat)→∀A:Type[0].relation (range A) ≝
-λh,k,A,I,J.∀i.i<(upto A I) → (filter A I i)=true →
- (h i < upto A J
- ∧ filter A J (h i) = true
- ∧ k (h i) = i).
-
-definition iso: ∀A:Type[0].relation (range A) ≝
- λA,I,J.∃h,k.
- (∀i. i < (upto A I) → (filter A I i) = true →
- enum A I i = enum A J (h i)) ∧
- sub_hk h k A I J ∧ sub_hk k h A J I.
+\ 5img class="anchor" src="icons/tick.png" id="sub_hk"\ 6definition sub_hk: (\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6)→(\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6)→∀A:Type[0].\ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/bigops/range.ind(1,0,1)"\ 6range\ 5/a\ 6 A) ≝
+λh,k,A,I,J.∀i.i\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/bigops/upto.fix(0,1,1)"\ 6upto\ 5/a\ 6 A I) → (\ 5a href="cic:/matita/arithmetics/bigops/filter.fix(0,1,1)"\ 6filter\ 5/a\ 6 A I i)\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 →
+ (h i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/bigops/upto.fix(0,1,1)"\ 6upto\ 5/a\ 6 A J
+ \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/bigops/filter.fix(0,1,1)"\ 6filter\ 5/a\ 6 A J (h i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6
+ \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 k (h i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 i).
+
+\ 5img class="anchor" src="icons/tick.png" id="iso"\ 6definition iso: ∀A:Type[0].\ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/bigops/range.ind(1,0,1)"\ 6range\ 5/a\ 6 A) ≝
+ λA,I,J.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6h,k\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6.\ 5/a\ 6
+ (∀i. i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/bigops/upto.fix(0,1,1)"\ 6upto\ 5/a\ 6 A I) → (\ 5a href="cic:/matita/arithmetics/bigops/filter.fix(0,1,1)"\ 6filter\ 5/a\ 6 A I i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 →
+ \ 5a href="cic:/matita/arithmetics/bigops/enum.fix(0,1,1)"\ 6enum\ 5/a\ 6 A I i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/bigops/enum.fix(0,1,1)"\ 6enum\ 5/a\ 6 A J (h i)) \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6
+ \ 5a href="cic:/matita/arithmetics/bigops/sub_hk.def(2)"\ 6sub_hk\ 5/a\ 6 h k A I J \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/bigops/sub_hk.def(2)"\ 6sub_hk\ 5/a\ 6 k h A J I.
-lemma sub_hkO: ∀h,k,A,I,J. upto A I = 0 → sub_hk h k A I J.
-#h #k #A #I #J #up0 #i #lti >up0 @False_ind /2/
+\ 5img class="anchor" src="icons/tick.png" id="sub_hkO"\ 6lemma sub_hkO: ∀h,k,A,I,J. \ 5a href="cic:/matita/arithmetics/bigops/upto.fix(0,1,1)"\ 6upto\ 5/a\ 6 A I \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/bigops/sub_hk.def(2)"\ 6sub_hk\ 5/a\ 6 h k A I J.
+#h #k #A #I #J #up0 #i #lti >up0 @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.
-lemma sub0_to_false: ∀h,k,A,I,J. upto A I = 0 → sub_hk h k A J I →
- ∀i. i < upto A J → filter A J i = false.
-#h #k #A #I #J #up0 #sub #i #lti cases(true_or_false (filter A J i)) //
-#ptrue (cases (sub i lti ptrue)) * #hi @False_ind /2/
+\ 5img class="anchor" src="icons/tick.png" id="sub0_to_false"\ 6lemma sub0_to_false: ∀h,k,A,I,J. \ 5a href="cic:/matita/arithmetics/bigops/upto.fix(0,1,1)"\ 6upto\ 5/a\ 6 A I \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/bigops/sub_hk.def(2)"\ 6sub_hk\ 5/a\ 6 h k A J I →
+ ∀i. i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/bigops/upto.fix(0,1,1)"\ 6upto\ 5/a\ 6 A J → \ 5a href="cic:/matita/arithmetics/bigops/filter.fix(0,1,1)"\ 6filter\ 5/a\ 6 A J i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6.
+#h #k #A #I #J #up0 #sub #i #lti cases(\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/bigops/filter.fix(0,1,1)"\ 6filter\ 5/a\ 6 A J i)) //
+#ptrue (cases (sub i lti ptrue)) * #hi @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.
-lemma sub_lt: ∀A,e,p,n,m. n ≤ m →
- sub_hk (λx.x) (λx.x) A (mk_range A e n p) (mk_range A e m p).
-#A #e #f #n #m #lenm #i #lti #fi % // % /2/
+\ 5img class="anchor" src="icons/tick.png" id="sub_lt"\ 6lemma sub_lt: ∀A,e,p,n,m. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m →
+ \ 5a href="cic:/matita/arithmetics/bigops/sub_hk.def(2)"\ 6sub_hk\ 5/a\ 6 (λx.x) (λx.x) A (\ 5a href="cic:/matita/arithmetics/bigops/range.con(0,1,1)"\ 6mk_range\ 5/a\ 6 A e n p) (\ 5a href="cic:/matita/arithmetics/bigops/range.con(0,1,1)"\ 6mk_range\ 5/a\ 6 A e m p).
+#A #e #f #n #m #lenm #i #lti #fi % // % /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"\ 6lt_to_le_to_lt\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.
-theorem transitive_sub: ∀h1,k1,h2,k2,A,I,J,K.
- sub_hk h1 k1 A I J → sub_hk h2 k2 A J K →
- sub_hk (λx.h2(h1 x)) (λx.k1(k2 x)) A I K.
+\ 5img class="anchor" src="icons/tick.png" id="transitive_sub"\ 6theorem transitive_sub: ∀h1,k1,h2,k2,A,I,J,K.
+ \ 5a href="cic:/matita/arithmetics/bigops/sub_hk.def(2)"\ 6sub_hk\ 5/a\ 6 h1 k1 A I J → \ 5a href="cic:/matita/arithmetics/bigops/sub_hk.def(2)"\ 6sub_hk\ 5/a\ 6 h2 k2 A J K →
+ \ 5a href="cic:/matita/arithmetics/bigops/sub_hk.def(2)"\ 6sub_hk\ 5/a\ 6 (λx.h2(h1 x)) (λx.k1(k2 x)) A I K.
#h1 #k1 #h2 #k2 #A #I #J #K #sub1 #sub2 #i #lti #fi
cases(sub1 i lti fi) * #lth1i #fh1i #ei
cases(sub2 (h1 i) lth1i fh1i) * #H1 #H2 #H3 % // % //
qed.
-theorem bigop_iso: ∀n1,n2,p1,p2,B.∀nil.∀op:ACop B nil.∀f1,f2.
- iso B (mk_range B f1 n1 p1) (mk_range B f2 n2 p2) →
- \big[op,nil]_{i<n1|p1 i}(f1 i) = \big[op,nil]_{i<n2|p2 i}(f2 i).
+\ 5img class="anchor" src="icons/tick.png" id="bigop_iso"\ 6theorem bigop_iso: ∀n1,n2,p1,p2,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/ACop.ind(1,0,2)"\ 6ACop\ 5/a\ 6 B nil.∀f1,f2.
+ \ 5a href="cic:/matita/arithmetics/bigops/iso.def(3)"\ 6iso\ 5/a\ 6 B (\ 5a href="cic:/matita/arithmetics/bigops/range.con(0,1,1)"\ 6mk_range\ 5/a\ 6 B f1 n1 p1) (\ 5a href="cic:/matita/arithmetics/bigops/range.con(0,1,1)"\ 6mk_range\ 5/a\ 6 B f2 n2 p2) →
+ \big[op,nil]_{i<n1|p1 i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f1 i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \big[op,nil]_{i<n2|p2 i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f2 i).
#n1 #n2 #p1 #p2 #B #nil #op #f1 #f2 * #h * #k * * #same
-@(le_gen ? n1) #i (generalize in match p2) (elim i)
+@(\ 5a href="cic:/matita/arithmetics/nat/le_gen.def(1)"\ 6le_gen\ 5/a\ 6 ? n1) #i generalize in match p2; (elim i)
[(elim n2) // #m #Hind #p2 #_ #sub1 #sub2
- >bigop_Sfalse
- [@(Hind ? (le_O_n ?)) [/2/ | @(transitive_sub … (sub_lt …) sub2) //]
- |@(sub0_to_false … sub2) //
+ >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6
+ [@(Hind ? (\ 5a href="cic:/matita/arithmetics/nat/le_O_n.def(2)"\ 6le_O_n\ 5/a\ 6 ?)) [/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/bigops/sub_hkO.def(4)"\ 6sub_hkO\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | @(\ 5a href="cic:/matita/arithmetics/bigops/transitive_sub.def(4)"\ 6transitive_sub\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/bigops/sub_lt.def(5)"\ 6sub_lt\ 5/a\ 6 …) sub2) //]
+ |@(\ 5a href="cic:/matita/arithmetics/bigops/sub0_to_false.def(4)"\ 6sub0_to_false\ 5/a\ 6 … sub2) //
]
- |#n #Hind #p2 #ltn #sub1 #sub2 (cut (n ≤n1)) [/2/] #len
- cases(true_or_false (p1 n)) #p1n
- [>bigop_Strue // (cases (sub1 n (le_n …) p1n)) * #hn #p2hn #eqn
- >(bigop_diff … (h n) n2) // >same //
- @eq_f @(Hind ? len)
- [#i #ltin #p1i (cases (sub1 i (le_S … ltin) p1i)) *
- #h1i #p2h1i #eqi % // % // >not_eq_to_eqb_false normalize //
- @(not_to_not ??? (lt_to_not_eq ? ? ltin)) //
- |#j #ltj #p2j (cases (sub2 j ltj (andb_true_r …p2j))) *
+ |#n #Hind #p2 #ltn #sub1 #sub2 (cut (n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6n1)) [/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"\ 6le_plus_b\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/] #len
+ cases(\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p1 n)) #p1n
+ [>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 // (cases (sub1 n (\ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"\ 6le_n\ 5/a\ 6 …) p1n)) * #hn #p2hn #eqn
+ >(\ 5a href="cic:/matita/arithmetics/bigops/bigop_diff.def(8)"\ 6bigop_diff\ 5/a\ 6 … (h n) n2) // >same //
+ @\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 @(Hind ? len)
+ [#i #ltin #p1i (cases (sub1 i (\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"\ 6le_S\ 5/a\ 6 … ltin) p1i)) *
+ #h1i #p2h1i #eqi % // % // >\ 5a href="cic:/matita/arithmetics/nat/not_eq_to_eqb_false.def(6)"\ 6not_eq_to_eqb_false\ 5/a\ 6 normalize //
+ @(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 ??? (\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_eq.def(7)"\ 6lt_to_not_eq\ 5/a\ 6 ? ? ltin)) //
+ |#j #ltj #p2j (cases (sub2 j ltj (\ 5a href="cic:/matita/basics/bool/andb_true_r.def(4)"\ 6andb_true_r\ 5/a\ 6 …p2j))) *
#ltkj #p1kj #eqj % // % //
- (cases (le_to_or_lt_eq …(le_S_S_to_le …ltkj))) //
- #eqkj @False_ind generalize in match p2j @eqb_elim
- normalize /2/
+ (cases (\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 …(\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 …ltkj))) //
+ #eqkj @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 generalize in match p2j; @\ 5a href="cic:/matita/arithmetics/nat/eqb_elim.def(5)"\ 6eqb_elim\ 5/a\ 6
+ normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
]
- |>bigop_Sfalse // @(Hind ? len)
- [@(transitive_sub … (sub_lt …) sub1) //
+ |>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 // @(Hind ? len)
+ [@(\ 5a href="cic:/matita/arithmetics/bigops/transitive_sub.def(4)"\ 6transitive_sub\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/bigops/sub_lt.def(5)"\ 6sub_lt\ 5/a\ 6 …) sub1) //
|#i #lti #p2i cases(sub2 i lti p2i) * #ltki #p1ki #eqi
- % // % // cases(le_to_or_lt_eq …(le_S_S_to_le …ltki)) //
- #eqki @False_ind /2/
+ % // % // cases(\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 …(\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 …ltki)) //
+ #eqki @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
]
]
]
qed.
-(* 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)}.
-
-notation "Σ_{ ident i < n } f"
- with precedence 80
-for @{'bigop $n plus 0 (λ${ident i}.true) (λ${ident i}. $f)}.
-
-notation "Σ_{ ident j ∈ [a,b[ } f"
- with precedence 80
-for @{'bigop ($b-$a) plus 0 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
- (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
-
-notation "Σ_{ ident j ∈ [a,b[ | p } f"
- with precedence 80
-for @{'bigop ($b-$a) plus 0 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
- (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
-
-notation "Π_{ ident i < n | p} f"
- with precedence 80
-for @{'bigop $n times 1 (λ${ident i}.$p) (λ${ident i}. $f)}.
-
-notation "Π_{ ident i < n } f"
- with precedence 80
-for @{'bigop $n times 1 (λ${ident i}.true) (λ${ident i}. $f)}.
-
-notation "Π_{ ident j ∈ [a,b[ } f"
- with precedence 80
-for @{'bigop ($b-$a) times 1 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
- (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
-
-notation "Π_{ ident j ∈ [a,b[ | p } 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
-\lambda p,m,x.
- match p_ord x p with
- [pair q r \Rightarrow r*m+q].
-
-theorem eq_p_ord_times: \forall p,m,x.
-p_ord_times p m x = (ord_rem x p)*m+(ord x p).
-intros.unfold p_ord_times. unfold ord_rem.
-unfold ord.
-elim (p_ord x p).
-reflexivity.
-qed.
-
-theorem div_p_ord_times:
-\forall p,m,x. ord x p < m \to p_ord_times p m x / m = ord_rem x p.
-intros.rewrite > eq_p_ord_times.
-apply div_plus_times.
-assumption.
-qed.
-
-theorem mod_p_ord_times:
-\forall p,m,x. ord x p < m \to p_ord_times p m x \mod m = ord x p.
-intros.rewrite > eq_p_ord_times.
-apply mod_plus_times.
-assumption.
-qed.
-
-lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m.
-intros.
-elim (le_to_or_lt_eq O ? (le_O_n m))
- [assumption
- |apply False_ind.
- rewrite < H1 in H.
- rewrite < times_n_O in H.
- apply (not_le_Sn_O ? H)
- ]
-qed.
-
-theorem iter_p_gen_knm:
-\forall A:Type.
-\forall baseA: A.
-\forall plusA: A \to A \to A.
-(symmetric A plusA) \to
-(associative A plusA) \to
-(\forall a:A.(plusA a baseA) = a)\to
-\forall g: nat \to A.
-\forall h2:nat \to nat \to nat.
-\forall h11,h12:nat \to nat.
-\forall k,n,m.
-\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
-\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
-iter_p_gen k p1 A g baseA plusA =
-iter_p_gen n p21 A (\lambda x:nat.iter_p_gen m (p22 x) A (\lambda y. g (h2 x y)) baseA plusA) baseA plusA.
-intros.
-rewrite < (iter_p_gen2' n m p21 p22 ? ? ? ? H H1 H2).
-apply sym_eq.
-apply (eq_iter_p_gen_gh A baseA plusA H H1 H2 g ? (\lambda x.(h11 x)*m+(h12 x)))
- [intros.
- elim (H4 (i/m) (i \mod m));clear H4
- [elim H7.clear H7.
- elim H4.clear H4.
- assumption
- |apply (lt_times_to_lt_div ? ? ? H5)
- |apply lt_mod_m_m.
- apply (lt_times_to_lt_O ? ? ? H5)
- |apply (andb_true_true ? ? H6)
- |apply (andb_true_true_r ? ? H6)
- ]
- |intros.
- elim (H4 (i/m) (i \mod m));clear H4
- [elim H7.clear H7.
- elim H4.clear H4.
- rewrite > H10.
- rewrite > H9.
- apply sym_eq.
- apply div_mod.
- apply (lt_times_to_lt_O ? ? ? H5)
- |apply (lt_times_to_lt_div ? ? ? H5)
- |apply lt_mod_m_m.
- apply (lt_times_to_lt_O ? ? ? H5)
- |apply (andb_true_true ? ? H6)
- |apply (andb_true_true_r ? ? H6)
- ]
- |intros.
- elim (H4 (i/m) (i \mod m));clear H4
- [elim H7.clear H7.
- elim H4.clear H4.
- assumption
- |apply (lt_times_to_lt_div ? ? ? H5)
- |apply lt_mod_m_m.
- apply (lt_times_to_lt_O ? ? ? H5)
- |apply (andb_true_true ? ? H6)
- |apply (andb_true_true_r ? ? H6)
- ]
- |intros.
- elim (H3 j H5 H6).
- elim H7.clear H7.
- elim H9.clear H9.
- elim H7.clear H7.
- rewrite > div_plus_times
- [rewrite > mod_plus_times
- [rewrite > H9.
- rewrite > H12.
- reflexivity.
- |assumption
- ]
- |assumption
- ]
- |intros.
- elim (H3 j H5 H6).
- elim H7.clear H7.
- elim H9.clear H9.
- elim H7.clear H7.
- rewrite > div_plus_times
- [rewrite > mod_plus_times
- [assumption
- |assumption
- ]
- |assumption
- ]
- |intros.
- elim (H3 j H5 H6).
- elim H7.clear H7.
- elim H9.clear H9.
- elim H7.clear H7.
- apply (lt_to_le_to_lt ? ((h11 j)*m+m))
- [apply monotonic_lt_plus_r.
- assumption
- |rewrite > sym_plus.
- change with ((S (h11 j)*m) \le n*m).
- apply monotonic_le_times_l.
- assumption
- ]
- ]
-qed.
-
-theorem iter_p_gen_divides:
-\forall A:Type.
-\forall baseA: A.
-\forall plusA: A \to A \to A.
-\forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to
-\forall g: nat \to A.
-(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a)
-
-\to
-
-iter_p_gen (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) A g baseA plusA =
-iter_p_gen (S n) (\lambda x.divides_b x n) A
- (\lambda x.iter_p_gen (S m) (\lambda y.true) A (\lambda y.g (x*(exp p y))) baseA plusA) baseA plusA.
-intros.
-cut (O < p)
- [rewrite < (iter_p_gen2 ? ? ? ? ? ? ? ? H3 H4 H5).
- apply (trans_eq ? ?
- (iter_p_gen (S n*S m) (\lambda x:nat.divides_b (x/S m) n) A
- (\lambda x:nat.g (x/S m*(p)\sup(x\mod S m))) baseA plusA) )
- [apply sym_eq.
- apply (eq_iter_p_gen_gh ? ? ? ? ? ? g ? (p_ord_times p (S m)))
- [ assumption
- | assumption
- | assumption
- |intros.
- lapply (divides_b_true_to_lt_O ? ? H H7).
- apply divides_to_divides_b_true
- [rewrite > (times_n_O O).
- apply lt_times
- [assumption
- |apply lt_O_exp.assumption
- ]
- |apply divides_times
- [apply divides_b_true_to_divides.assumption
- |apply (witness ? ? (p \sup (m-i \mod (S m)))).
- rewrite < exp_plus_times.
- apply eq_f.
- rewrite > sym_plus.
- apply plus_minus_m_m.
- autobatch by le_S_S_to_le, lt_mod_m_m, lt_O_S;
- ]
- ]
- |intros.
- lapply (divides_b_true_to_lt_O ? ? H H7).
- unfold p_ord_times.
- rewrite > (p_ord_exp1 p ? (i \mod (S m)) (i/S m))
- [change with ((i/S m)*S m+i \mod S m=i).
- apply sym_eq.
- apply div_mod.
- apply lt_O_S
- |assumption
- |unfold Not.intro.
- apply H2.
- apply (trans_divides ? (i/ S m))
- [assumption|
- apply divides_b_true_to_divides;assumption]
- |apply sym_times.
- ]
- |intros.
- apply le_S_S.
- apply le_times
- [apply le_S_S_to_le.
- change with ((i/S m) < S n).
- apply (lt_times_to_lt_l m).
- apply (le_to_lt_to_lt ? i);[2:assumption]
- autobatch by eq_plus_to_le, div_mod, lt_O_S.
- |apply le_exp
- [assumption
- |apply le_S_S_to_le.
- apply lt_mod_m_m.
- apply lt_O_S
- ]
- ]
- |intros.
- cut (ord j p < S m)
- [rewrite > div_p_ord_times
- [apply divides_to_divides_b_true
- [apply lt_O_ord_rem
- [elim H1.assumption
- |apply (divides_b_true_to_lt_O ? ? ? H7).
- rewrite > (times_n_O O).
- apply lt_times
- [assumption|apply lt_O_exp.assumption]
- ]
- |cut (n = ord_rem (n*(exp p m)) p)
- [rewrite > Hcut2.
- apply divides_to_divides_ord_rem
- [apply (divides_b_true_to_lt_O ? ? ? H7).
- rewrite > (times_n_O O).
- apply lt_times
- [assumption|apply lt_O_exp.assumption]
- |rewrite > (times_n_O O).
- apply lt_times
- [assumption|apply lt_O_exp.assumption]
- |assumption
- |apply divides_b_true_to_divides.
- assumption
- ]
- |unfold ord_rem.
- rewrite > (p_ord_exp1 p ? m n)
- [reflexivity
- |assumption
- |assumption
- |apply sym_times
- ]
- ]
- ]
- |assumption
- ]
- |cut (m = ord (n*(exp p m)) p)
- [apply le_S_S.
- rewrite > Hcut1.
- apply divides_to_le_ord
- [apply (divides_b_true_to_lt_O ? ? ? H7).
- rewrite > (times_n_O O).
- apply lt_times
- [assumption|apply lt_O_exp.assumption]
- |rewrite > (times_n_O O).
- apply lt_times
- [assumption|apply lt_O_exp.assumption]
- |assumption
- |apply divides_b_true_to_divides.
- assumption
- ]
- |unfold ord.
- rewrite > (p_ord_exp1 p ? m n)
- [reflexivity
- |assumption
- |assumption
- |apply sym_times
- ]
- ]
- ]
- |intros.
- cut (ord j p < S m)
- [rewrite > div_p_ord_times
- [rewrite > mod_p_ord_times
- [rewrite > sym_times.
- apply sym_eq.
- apply exp_ord
- [elim H1.assumption
- |apply (divides_b_true_to_lt_O ? ? ? H7).
- rewrite > (times_n_O O).
- apply lt_times
- [assumption|apply lt_O_exp.assumption]
- ]
- |cut (m = ord (n*(exp p m)) p)
- [apply le_S_S.
- rewrite > Hcut2.
- apply divides_to_le_ord
- [apply (divides_b_true_to_lt_O ? ? ? H7).
- rewrite > (times_n_O O).
- apply lt_times
- [assumption|apply lt_O_exp.assumption]
- |rewrite > (times_n_O O).
- apply lt_times
- [assumption|apply lt_O_exp.assumption]
- |assumption
- |apply divides_b_true_to_divides.
- assumption
- ]
- |unfold ord.
- rewrite > (p_ord_exp1 p ? m n)
- [reflexivity
- |assumption
- |assumption
- |apply sym_times
- ]
- ]
- ]
- |assumption
- ]
- |cut (m = ord (n*(exp p m)) p)
- [apply le_S_S.
- rewrite > Hcut1.
- apply divides_to_le_ord
- [apply (divides_b_true_to_lt_O ? ? ? H7).
- rewrite > (times_n_O O).
- apply lt_times
- [assumption|apply lt_O_exp.assumption]
- |rewrite > (times_n_O O).
- apply lt_times
- [assumption|apply lt_O_exp.assumption]
- |assumption
- |apply divides_b_true_to_divides.
- assumption
- ]
- |unfold ord.
- rewrite > (p_ord_exp1 p ? m n)
- [reflexivity
- |assumption
- |assumption
- |apply sym_times
- ]
- ]
- ]
- |intros.
- rewrite > eq_p_ord_times.
- rewrite > sym_plus.
- apply (lt_to_le_to_lt ? (S m +ord_rem j p*S m))
- [apply lt_plus_l.
- apply le_S_S.
- cut (m = ord (n*(p \sup m)) p)
- [rewrite > Hcut1.
- apply divides_to_le_ord
- [apply (divides_b_true_to_lt_O ? ? ? H7).
- rewrite > (times_n_O O).
- apply lt_times
- [assumption|apply lt_O_exp.assumption]
- |rewrite > (times_n_O O).
- apply lt_times
- [assumption|apply lt_O_exp.assumption]
- |assumption
- |apply divides_b_true_to_divides.
- assumption
- ]
- |unfold ord.
- rewrite > sym_times.
- rewrite > (p_ord_exp1 p ? m n)
- [reflexivity
- |assumption
- |assumption
- |reflexivity
- ]
- ]
- |change with (S (ord_rem j p)*S m \le S n*S m).
- apply le_times_l.
- apply le_S_S.
- cut (n = ord_rem (n*(p \sup m)) p)
- [rewrite > Hcut1.
- apply divides_to_le
- [apply lt_O_ord_rem
- [elim H1.assumption
- |rewrite > (times_n_O O).
- apply lt_times
- [assumption|apply lt_O_exp.assumption]
- ]
- |apply divides_to_divides_ord_rem
- [apply (divides_b_true_to_lt_O ? ? ? H7).
- rewrite > (times_n_O O).
- apply lt_times
- [assumption|apply lt_O_exp.assumption]
- |rewrite > (times_n_O O).
- apply lt_times
- [assumption|apply lt_O_exp.assumption]
- |assumption
- |apply divides_b_true_to_divides.
- assumption
- ]
- ]
- |unfold ord_rem.
- rewrite > sym_times.
- rewrite > (p_ord_exp1 p ? m n)
- [reflexivity
- |assumption
- |assumption
- |reflexivity
- ]
- ]
+(* commutation *)
+\ 5img class="anchor" src="icons/tick.png" id="bigop_commute"\ 6theorem bigop_commute: ∀n,m,p11,p12,p21,p22,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/ACop.ind(1,0,2)"\ 6ACop\ 5/a\ 6 B nil.∀f.
+\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m →
+(∀i,j. i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → j \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → (p11 i \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 p12 i j) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (p21 j \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 p22 i j)) →
+\big[op,nil]_{i<n|p11 i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(\big[op,nil]_{j<m|p12 i j\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i j)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
+ \big[op,nil]_{j<m|p21 j\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(\big[op,nil]_{i<n|p22 i j\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i j)).
+#n #m #p11 #p12 #p21 #p22 #B #nil #op #f #posn #posm #Heq
+>\ 5a href="cic:/matita/arithmetics/bigops/bigop_prod.def(15)"\ 6bigop_prod\ 5/a\ 6 >\ 5a href="cic:/matita/arithmetics/bigops/bigop_prod.def(15)"\ 6bigop_prod\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/bigops/bigop_iso.def(9)"\ 6bigop_iso\ 5/a\ 6
+%{(λi.(i\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 i\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m)} %{(λi.(i\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 n)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 i\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6n)} %
+ [%
+ [#i #lti #Heq (* whd in ⊢ (???(?(?%?)?)); *) @\ 5a href="cic:/matita/basics/logic/eq_f2.def(3)"\ 6eq_f2\ 5/a\ 6
+ [@\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/div_and_mod/mod_plus_times.def(14)"\ 6mod_plus_times\ 5/a\ 6 /2 by \ 5a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"\ 6lt_times_to_lt_div\ 5/a\ 6/
+ |@\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/div_and_mod/div_plus_times.def(14)"\ 6div_plus_times\ 5/a\ 6 /2 by \ 5a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"\ 6lt_times_to_lt_div\ 5/a\ 6/
]
- ]
- |apply eq_iter_p_gen
-
- [intros.
- elim (divides_b (x/S m) n);reflexivity
- |intros.reflexivity
- ]
- ]
-|elim H1.apply lt_to_le.assumption
-]
-qed.
-
-
-
-theorem iter_p_gen_2_eq:
-\forall A:Type.
-\forall baseA: A.
-\forall plusA: A \to A \to A.
-(symmetric A plusA) \to
-(associative A plusA) \to
-(\forall a:A.(plusA a baseA) = a)\to
-\forall g: nat \to nat \to A.
-\forall h11,h12,h21,h22: nat \to nat \to nat.
-\forall n1,m1,n2,m2.
-\forall p11,p21:nat \to bool.
-\forall p12,p22:nat \to nat \to bool.
-(\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to
-p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
-\land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
-\land h11 i j < n1 \land h12 i j < m1) \to
-(\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to
-p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
-\land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
-\land (h21 i j) < n2 \land (h22 i j) < m2) \to
-iter_p_gen n1 p11 A
- (\lambda x:nat .iter_p_gen m1 (p12 x) A (\lambda y. g x y) baseA plusA)
- baseA plusA =
-iter_p_gen n2 p21 A
- (\lambda x:nat .iter_p_gen m2 (p22 x) A (\lambda y. g (h11 x y) (h12 x y)) baseA plusA )
- baseA plusA.
-
-intros.
-rewrite < (iter_p_gen2' ? ? ? ? ? ? ? ? H H1 H2).
-letin ha:= (\lambda x,y.(((h11 x y)*m1) + (h12 x y))).
-letin ha12:= (\lambda x.(h21 (x/m1) (x \mod m1))).
-letin ha22:= (\lambda x.(h22 (x/m1) (x \mod m1))).
-
-apply (trans_eq ? ?
-(iter_p_gen n2 p21 A (\lambda x:nat. iter_p_gen m2 (p22 x) A
- (\lambda y:nat.(g (((h11 x y)*m1+(h12 x y))/m1) (((h11 x y)*m1+(h12 x y))\mod m1))) baseA plusA ) baseA plusA))
-[
- apply (iter_p_gen_knm A baseA plusA H H1 H2 (\lambda e. (g (e/m1) (e \mod m1))) ha ha12 ha22);intros
- [ elim (and_true ? ? H6).
- cut(O \lt m1)
- [ cut(x/m1 < n1)
- [ cut((x \mod m1) < m1)
- [ elim (H4 ? ? Hcut1 Hcut2 H7 H8).
- elim H9.clear H9.
- elim H11.clear H11.
- elim H9.clear H9.
- elim H11.clear H11.
- split
- [ split
- [ split
- [ split
- [ assumption
- | assumption
- ]
- | unfold ha.
- unfold ha12.
- unfold ha22.
- rewrite > H14.
- rewrite > H13.
- apply sym_eq.
- apply div_mod.
- assumption
- ]
- | assumption
- ]
- | assumption
+ |#i #lti #Hi
+ cut ((i\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6i\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m)\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 n\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6i\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m)
+ [@\ 5a href="cic:/matita/arithmetics/div_and_mod/mod_plus_times.def(14)"\ 6mod_plus_times\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"\ 6lt_times_to_lt_div\ 5/a\ 6 //] #H1
+ cut ((i\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6i\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m)\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6n\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6i \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m)
+ [@\ 5a href="cic:/matita/arithmetics/div_and_mod/div_plus_times.def(14)"\ 6div_plus_times\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"\ 6lt_times_to_lt_div\ 5/a\ 6 //] #H2
+ %[%[@(\ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"\ 6lt_to_le_to_lt\ 5/a\ 6 ? (i\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6n))
+ [whd >\ 5a href="cic:/matita/arithmetics/nat/plus_n_Sm.def(4)"\ 6plus_n_Sm\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_plus_r.def(3)"\ 6monotonic_le_plus_r\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"\ 6lt_times_to_lt_div\ 5/a\ 6 //
+ |>\ 5a href="cic:/matita/arithmetics/nat/commutative_plus.def(5)"\ 6commutative_plus\ 5/a\ 6 @(\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(i \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m)) m n n) // @\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6 //
]
- | apply lt_mod_m_m.
- assumption
+ |lapply (Heq (i\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m) (i \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m) ??)
+ [@\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6 // |@\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"\ 6lt_times_to_lt_div\ 5/a\ 6 //|>Hi >H1 >H2 //]
]
- | apply (lt_times_n_to_lt m1)
- [ assumption
- | apply (le_to_lt_to_lt ? x)
- [ apply (eq_plus_to_le ? ? (x \mod m1)).
- apply div_mod.
- assumption
- | assumption
- ]
- ]
- ]
- | apply not_le_to_lt.unfold.intro.
- generalize in match H5.
- apply (le_n_O_elim ? H9).
- rewrite < times_n_O.
- apply le_to_not_lt.
- apply le_O_n.
- ]
- | elim (H3 ? ? H5 H6 H7 H8).
- elim H9.clear H9.
- elim H11.clear H11.
- elim H9.clear H9.
- elim H11.clear H11.
- cut(((h11 i j)*m1 + (h12 i j))/m1 = (h11 i j))
- [ cut(((h11 i j)*m1 + (h12 i j)) \mod m1 = (h12 i j))
- [ split
- [ split
- [ split
- [ apply true_to_true_to_andb_true
- [ rewrite > Hcut.
- assumption
- | rewrite > Hcut1.
- rewrite > Hcut.
- assumption
- ]
- | unfold ha.
- unfold ha12.
- rewrite > Hcut1.
- rewrite > Hcut.
- assumption
- ]
- | unfold ha.
- unfold ha22.
- rewrite > Hcut1.
- rewrite > Hcut.
- assumption
- ]
- | cut(O \lt m1)
- [ cut(O \lt n1)
- [ apply (lt_to_le_to_lt ? ((h11 i j)*m1 + m1) )
- [ unfold ha.
- apply (lt_plus_r).
- assumption
- | rewrite > sym_plus.
- rewrite > (sym_times (h11 i j) m1).
- rewrite > times_n_Sm.
- rewrite > sym_times.
- apply (le_times_l).
- assumption
- ]
- | apply not_le_to_lt.unfold.intro.
- generalize in match H12.
- apply (le_n_O_elim ? H11).
- apply le_to_not_lt.
- apply le_O_n
- ]
- | apply not_le_to_lt.unfold.intro.
- generalize in match H10.
- apply (le_n_O_elim ? H11).
- apply le_to_not_lt.
- apply le_O_n
- ]
- ]
- | rewrite > (mod_plus_times m1 (h11 i j) (h12 i j)).
- reflexivity.
- assumption
- ]
- | rewrite > (div_plus_times m1 (h11 i j) (h12 i j)).
- reflexivity.
- assumption
+ |>H1 >H2 //
+ ]
]
- ]
-| apply (eq_iter_p_gen1)
- [ intros. reflexivity
- | intros.
- apply (eq_iter_p_gen1)
- [ intros. reflexivity
- | intros.
- rewrite > (div_plus_times)
- [ rewrite > (mod_plus_times)
- [ reflexivity
- | elim (H3 x x1 H5 H7 H6 H8).
- assumption
+ |#i #lti #Hi
+ cut ((i\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6i\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6n)\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6i\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6n)
+ [@\ 5a href="cic:/matita/arithmetics/div_and_mod/mod_plus_times.def(14)"\ 6mod_plus_times\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"\ 6lt_times_to_lt_div\ 5/a\ 6 //] #H1
+ cut ((i\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6i\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6n)\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6i \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 n)
+ [@\ 5a href="cic:/matita/arithmetics/div_and_mod/div_plus_times.def(14)"\ 6div_plus_times\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"\ 6lt_times_to_lt_div\ 5/a\ 6 //] #H2
+ %[%[@(\ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"\ 6lt_to_le_to_lt\ 5/a\ 6 ? (i\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6m))
+ [whd >\ 5a href="cic:/matita/arithmetics/nat/plus_n_Sm.def(4)"\ 6plus_n_Sm\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_plus_r.def(3)"\ 6monotonic_le_plus_r\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"\ 6lt_times_to_lt_div\ 5/a\ 6 //
+ |>\ 5a href="cic:/matita/arithmetics/nat/commutative_plus.def(5)"\ 6commutative_plus\ 5/a\ 6 @(\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(i \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 n)) n m m) // @\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6 //
]
- | elim (H3 x x1 H5 H7 H6 H8).
- assumption
+ |lapply (Heq (i \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 n) (i\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6n) ??)
+ [@\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_times_to_lt_div.def(10)"\ 6lt_times_to_lt_div\ 5/a\ 6 // |@\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6 // |>Hi >H1 >H2 //]
]
+ |>H1 >H2 //
]
]
-]
qed.
-theorem iter_p_gen_iter_p_gen:
-\forall A:Type.
-\forall baseA: A.
-\forall plusA: A \to A \to A.
-(symmetric A plusA) \to
-(associative A plusA) \to
-(\forall a:A.(plusA a baseA) = a)\to
-\forall g: nat \to nat \to A.
-\forall n,m.
-\forall p11,p21:nat \to bool.
-\forall p12,p22:nat \to nat \to bool.
-(\forall x,y. x < n \to y < m \to
- (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to
-iter_p_gen n p11 A
- (\lambda x:nat.iter_p_gen m (p12 x) A (\lambda y. g x y) baseA plusA)
- baseA plusA =
-iter_p_gen m p21 A
- (\lambda y:nat.iter_p_gen n (p22 y) A (\lambda x. g x y) baseA plusA )
- baseA plusA.
-intros.
-apply (iter_p_gen_2_eq A baseA plusA H H1 H2 (\lambda x,y. g x y) (\lambda x,y.y) (\lambda x,y.x) (\lambda x,y.y) (\lambda x,y.x)
- n m m n p11 p21 p12 p22)
- [intros.split
- [split
- [split
- [split
- [split
- [apply (andb_true_true ? (p12 j i)).
- rewrite > H3
- [rewrite > H6.rewrite > H7.reflexivity
- |assumption
- |assumption
- ]
- |apply (andb_true_true_r (p11 j)).
- rewrite > H3
- [rewrite > H6.rewrite > H7.reflexivity
- |assumption
- |assumption
- ]
- ]
- |reflexivity
- ]
- |reflexivity
- ]
- |assumption
- ]
- |assumption
- ]
- |intros.split
- [split
- [split
- [split
- [split
- [apply (andb_true_true ? (p22 j i)).
- rewrite < H3
- [rewrite > H6.rewrite > H7.reflexivity
- |assumption
- |assumption
- ]
- |apply (andb_true_true_r (p21 j)).
- rewrite < H3
- [rewrite > H6.rewrite > H7.reflexivity
- |assumption
- |assumption
- ]
- ]
- |reflexivity
- ]
- |reflexivity
- ]
- |assumption
- ]
- |assumption
- ]
+(* distributivity *)
+
+\ 5img class="anchor" src="icons/tick.png" id="Dop"\ 6record Dop (A:Type[0]) (nil:A): Type[0] ≝
+ {sum : \ 5a href="cic:/matita/arithmetics/bigops/ACop.ind(1,0,2)"\ 6ACop\ 5/a\ 6 A nil;
+ prod: A → A →A;
+ null: \forall a. prod a nil \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 nil;
+ distr: ∀a,b,c:A. prod a (sum b c) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 sum (prod a b) (prod a c)
+ }.
+
+\ 5img class="anchor" src="icons/tick.png" id="bigop_distr"\ 6theorem bigop_distr: ∀n,p,B,nil.∀R:\ 5a href="cic:/matita/arithmetics/bigops/Dop.ind(1,0,2)"\ 6Dop\ 5/a\ 6 B nil.\forall f,a.
+ let aop \def \ 5a href="cic:/matita/arithmetics/bigops/sum.fix(0,2,4)"\ 6sum\ 5/a\ 6 B nil R in
+ let mop \def \ 5a href="cic:/matita/arithmetics/bigops/prod.fix(0,2,4)"\ 6prod\ 5/a\ 6 B nil R in
+ mop a \big[aop,nil]_{i<n|p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
+ \big[aop,nil]_{i<n|p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(mop a (f i)).
+#n #p #B #nil #R #f #a normalize (elim n) [@\ 5a href="cic:/matita/arithmetics/bigops/null.fix(0,2,5)"\ 6null\ 5/a\ 6]
+#n #Hind (cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p n))) #H
+ [>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 // >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 // >(\ 5a href="cic:/matita/arithmetics/bigops/distr.fix(0,2,5)"\ 6distr\ 5/a\ 6 B nil R) >Hind //
+ |>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 // >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 //
]
-qed. *)
\ No newline at end of file
+qed.
+
\ No newline at end of file
projects / helm.git / blobdiff