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))}
{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 //
+ <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)=
]
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.
\ /
V_______________________________________________________________ *)
-include "arithmetics/bigops.ma".
+include "arithmetics/sigma_pi.ma".
include "arithmetics/primes.ma".
(* binomial coefficient *)
qed.
theorem fact_minus: ∀n,k. k < n →
- (n-k)*(n - S k)! = (n - k)!.
+ (n - S k)!*(n-k) = (n - k)!.
#n #k (cases n)
[#ltO @False_ind /2/
- |#l #ltl >minus_Sn_m [>commutative_times //|@le_S_S_to_le //]
+ |#l #ltl >(minus_Sn_m k) [// |@le_S_S_to_le //]
]
qed.
∀k. k ≤n → k!*(n-k)! ∣ n!.
#n (elim n)
[#k #lek0 <(le_n_O_to_eq ? lek0) //
- |#m #Hind #k generalize in match H1;cases k
- [intro;simplify in ⊢ (? (? ? (? %)) ?);simplify in ⊢ (? (? % ?) ?);
- rewrite > sym_times;rewrite < times_n_SO;apply reflexive_divides
- |intro;elim (decidable_eq_nat n2 n1)
- [rewrite > H3;rewrite < minus_n_n;
- rewrite > times_n_SO in ⊢ (? ? %);apply reflexive_divides
- |lapply (H n2)
- [lapply (H (n1 - (S n2)))
- [change in ⊢ (? ? %) with ((S n1)*n1!);
- rewrite > (plus_minus_m_m n1 n2) in ⊢ (? ? (? (? %) ?))
- [rewrite > sym_plus;
- change in ⊢ (? ? (? % ?)) with ((S n2) + (n1 - n2));
- rewrite > sym_times in \vdash (? ? %);
- rewrite > distr_times_plus in ⊢ (? ? %);
- simplify in ⊢ (? (? ? (? %)) ?);
- apply divides_plus
- [rewrite > sym_times;
- change in ⊢ (? (? ? %) ?) with ((S n2)*n2!);
- rewrite > sym_times in ⊢ (? (? ? %) ?);
- rewrite < assoc_times;
- apply divides_times
- [rewrite > sym_times;assumption
- |apply reflexive_divides]
- |rewrite < fact_minus in ⊢ (? (? ? %) ?)
- [rewrite > sym_times in ⊢ (? (? ? %) ?);
- rewrite < assoc_times;
- apply divides_times
- [rewrite < eq_plus_minus_minus_minus in Hletin1;
- [rewrite > sym_times;rewrite < minus_n_n in Hletin1;
- rewrite < plus_n_O in Hletin1;assumption
- |lapply (le_S_S_to_le ? ? H2);
- elim (le_to_or_lt_eq ? ? Hletin2);
- [assumption
- |elim (H3 H4)]
- |constructor 1]
- |apply reflexive_divides]
- |lapply (le_S_S_to_le ? ? H2);
- elim (le_to_or_lt_eq ? ? Hletin2);
- [assumption
- |elim (H3 H4)]]]
- |apply le_S_S_to_le;assumption]
- |apply le_minus_m;apply le_S_S_to_le;assumption]
- |apply le_S_S_to_le;assumption]]]]
-qed.
-
-theorem bc1: \forall n.\forall k. k < n \to bc (S n) (S k) = (bc n k) + (bc n (S k)).
-intros.unfold bc.
-rewrite > (lt_to_lt_to_eq_div_div_times_times ? ? (S k)) in ⊢ (? ? ? (? % ?))
- [rewrite > sym_times in ⊢ (? ? ? (? (? ? %) ?)).
- rewrite < assoc_times in ⊢ (? ? ? (? (? ? %) ?)).
- rewrite > (lt_to_lt_to_eq_div_div_times_times ? ? (n - k)) in ⊢ (? ? ? (? ? %))
- [rewrite > assoc_times in ⊢ (? ? ? (? ? (? ? %))).
- rewrite > sym_times in ⊢ (? ? ? (? ? (? ? (? ? %)))).
- rewrite > fact_minus
- [rewrite < eq_div_plus
- [rewrite < distr_times_plus.
- simplify in ⊢ (? ? ? (? (? ? %) ?)).
- rewrite > sym_plus in ⊢ (? ? ? (? (? ? (? %)) ?)).
- rewrite < plus_minus_m_m
- [rewrite > sym_times in ⊢ (? ? ? (? % ?)).
- reflexivity
- |apply lt_to_le.
- assumption
- ]
- |rewrite > (times_n_O O).
- apply lt_times;apply lt_O_fact
- |change in ⊢ (? (? % ?) ?) with ((S k)*k!);
- rewrite < sym_times in ⊢ (? ? %);
- rewrite > assoc_times;apply divides_times
- [apply reflexive_divides
- |apply bc2;apply le_S_S_to_le;constructor 2;assumption]
- |rewrite < fact_minus
- [rewrite > sym_times in ⊢ (? (? ? %) ?);rewrite < assoc_times;
- apply divides_times
- [apply bc2;assumption
- |apply reflexive_divides]
- |assumption]]
- |assumption]
- |apply lt_to_lt_O_minus;assumption
- |rewrite > (times_n_O O).
- apply lt_times;apply lt_O_fact]
-|apply lt_O_S
-|rewrite > (times_n_O O).
- apply lt_times;apply lt_O_fact]
-qed.
-
-theorem lt_O_bc: \forall n,m. m \le n \to O < bc n m.
-intro.elim n
- [apply (le_n_O_elim ? H).
- simplify.apply le_n
- |elim (le_to_or_lt_eq ? ? H1)
- [generalize in match H2.cases m;intro
- [rewrite > bc_n_O.apply le_n
- |rewrite > bc1
- [apply (trans_le ? (bc n1 n2))
- [apply H.apply le_S_S_to_le.apply lt_to_le.assumption
- |apply le_plus_n_r
- ]
- |apply le_S_S_to_le.assumption
- ]
+ |#m #Hind #k (cases k) normalize //
+ #c #lec cases (le_to_or_lt_eq … (le_S_S_to_le …lec))
+ [#ltcm
+ cut (m-(m-(S c)) = S c) [@plus_to_minus @plus_minus_m_m //] #eqSc
+ lapply (Hind c (le_S_S_to_le … lec)) #Hc
+ lapply (Hind (m - (S c)) ?) [@le_plus_to_minus //] >eqSc #Hmc
+ >(plus_minus_m_m m c) in ⊢ (??(??(?%))) [|@le_S_S_to_le //]
+ >commutative_plus >(distributive_times_plus ? (S c))
+ @divides_plus
+ [>associative_times >(commutative_times (S c))
+ <associative_times @divides_times //
+ |<(fact_minus …ltcm) in ⊢ (?(??%)?)
+ <associative_times @divides_times //
+ >commutative_times @Hmc
]
- |rewrite > H2.
- rewrite > bc_n_n.
- apply le_n
+ |#eqcm >eqcm <minus_n_n <times_n_1 //
]
]
qed.
-
-theorem exp_plus_sigma_p:\forall a,b,n.
-exp (a+b) n = sigma_p (S n) (\lambda k.true)
- (\lambda k.(bc n k)*(exp a (n-k))*(exp b k)).
-intros.elim n
- [simplify.reflexivity
- |simplify in ⊢ (? ? % ?).
- rewrite > true_to_sigma_p_Sn
- [rewrite > H;rewrite > sym_times in ⊢ (? ? % ?);
- rewrite > distr_times_plus in ⊢ (? ? % ?);
- rewrite < minus_n_n in ⊢ (? ? ? (? (? (? ? (? ? %)) ?) ?));
- rewrite > sym_times in ⊢ (? ? (? % ?) ?);
- rewrite > sym_times in ⊢ (? ? (? ? %) ?);
- rewrite > distributive_times_plus_sigma_p in ⊢ (? ? (? % ?) ?);
- rewrite > distributive_times_plus_sigma_p in ⊢ (? ? (? ? %) ?);
- rewrite > true_to_sigma_p_Sn in ⊢ (? ? (? ? %) ?)
- [rewrite < assoc_plus;rewrite < sym_plus in ⊢ (? ? (? % ?) ?);
- rewrite > assoc_plus;
- apply eq_f2
- [rewrite > sym_times;rewrite > assoc_times;autobatch paramodulation
- |rewrite > (sigma_p_gi ? ? O);
- [rewrite < (eq_sigma_p_gh ? S pred n1 (S n1) (λx:nat.true)) in ⊢ (? ? (? (? ? %) ?) ?)
- [rewrite > (sigma_p_gi ? ? O) in ⊢ (? ? ? %);
- [rewrite > assoc_plus;apply eq_f2
- [autobatch paramodulation;
- |rewrite < sigma_p_plus_1;
- rewrite < (eq_sigma_p_gh ? S pred n1 (S n1) (λx:nat.true)) in \vdash (? ? ? %);
- [apply eq_sigma_p
- [intros;reflexivity
- |intros;rewrite > sym_times;rewrite > assoc_times;
- rewrite > sym_times in ⊢ (? ? (? (? ? %) ?) ?);
- rewrite > assoc_times;rewrite < assoc_times in ⊢ (? ? (? (? ? %) ?) ?);
- rewrite > sym_times in ⊢ (? ? (? (? ? (? % ?)) ?) ?);
- change in ⊢ (? ? (? (? ? (? % ?)) ?) ?) with (exp a (S (n1 - S x)));
- rewrite < (minus_Sn_m ? ? H1);rewrite > minus_S_S;
- rewrite > sym_times in \vdash (? ? (? ? %) ?);
- rewrite > assoc_times;
- rewrite > sym_times in ⊢ (? ? (? ? (? ? %)) ?);
- change in \vdash (? ? (? ? (? ? %)) ?) with (exp b (S x));
- rewrite > assoc_times in \vdash (? ? (? ? %) ?);
- rewrite > sym_times in \vdash (? ? (? % ?) ?);
- rewrite > sym_times in \vdash (? ? (? ? %) ?);
- rewrite > assoc_times in \vdash (? ? ? %);
- rewrite > sym_times in \vdash (? ? ? %);
- rewrite < distr_times_plus;
- rewrite > sym_plus;rewrite < bc1;
- [reflexivity|assumption]]
- |intros;simplify;reflexivity
- |intros;simplify;reflexivity
- |intros;apply le_S_S;assumption
- |intros;reflexivity
- |intros 2;elim j
- [simplify in H2;destruct H2
- |simplify;reflexivity]
- |intro;elim j
- [simplify in H2;destruct H2
- |simplify;apply le_S_S_to_le;assumption]]]
- |apply le_S_S;apply le_O_n
- |reflexivity]
- |intros;simplify;reflexivity
- |intros;simplify;reflexivity
- |intros;apply le_S_S;assumption
- |intros;reflexivity
- |intros 2;elim j
- [simplify in H2;destruct H2
- |simplify;reflexivity]
- |intro;elim j
- [simplify in H2;destruct H2
- |simplify;apply le_S_S_to_le;assumption]]
- |apply le_S_S;apply le_O_n
- |reflexivity]]
- |reflexivity]
- |reflexivity]]
+
+theorem bc1: ∀n.∀k. k < n →
+ bc (S n) (S k) = (bc n k) + (bc n (S k)).
+#n #k #ltkn > bceq >(bceq n) >(bceq n (S k))
+>(div_times_times ?? (S k)) in ⊢ (???(?%?))
+ [|>(times_n_O 0) @lt_times // | //]
+>associative_times in ⊢ (???(?(??%)?))
+>commutative_times in ⊢ (???(?(??(??%))?))
+<associative_times in ⊢ (???(?(??%)?))
+>(div_times_times ?? (n - k)) in ⊢ (???(??%))
+ [|>(times_n_O 0) @lt_times //
+ |@(le_plus_to_le_r k ??) <plus_minus_m_m /2/]
+>associative_times in ⊢ (???(??(??%)))
+>fact_minus // <plus_div
+ [<distributive_times_plus
+ >commutative_plus in ⊢ (???%) <plus_n_Sm <plus_minus_m_m [|/2/] @refl
+ |<fact_minus // <associative_times @divides_times // @(bc2 n (S k)) //
+ |>associative_times >(commutative_times (S k))
+ <associative_times @divides_times // @bc2 /2/
+ |>(times_n_O 0) @lt_times [@(le_1_fact (S k)) | //]
+ ]
qed.
-theorem exp_S_sigma_p:\forall a,n.
-exp (S a) n = sigma_p (S n) (\lambda k.true) (\lambda k.(bc n k)*(exp a (n-k))).
-intros.
-rewrite > plus_n_SO.
-rewrite > exp_plus_sigma_p.
-apply eq_sigma_p;intros
- [reflexivity
- |rewrite < exp_SO_n.
- rewrite < times_n_SO.
- reflexivity
+theorem lt_O_bc: ∀n,m. m ≤ n → O < bc n m.
+#n (elim n)
+ [#m #lemO @(le_n_O_elim ? lemO) //
+ |-n #n #Hind #m (cases m) //
+ #m #lemn cases(le_to_or_lt_eq … (le_S_S_to_le …lemn)) //
+ #ltmn >bc1 // >(plus_O_n 0) @lt_plus @Hind /2/
]
+qed.
+
+theorem binomial_law:∀a,b,n.
+ (a+b)^n = Σ_{k < S n}((bc n k)*(a^(n-k))*(b^k)).
+#a #b #n (elim n) //
+-n #n #Hind normalize in ⊢ (? ? % ?).
+>bigop_Strue // >Hind >distributive_times_plus
+<(minus_n_n (S n)) <commutative_times <(commutative_times b)
+(* hint??? *)
+>(bigop_distr ???? natDop ? a) >(bigop_distr ???? natDop ? b)
+>bigop_Strue in ⊢ (??(??%)?) // <associative_plus
+<commutative_plus in ⊢ (??(? % ?) ?) >associative_plus @eq_f2
+ [<minus_n_n >bc_n_n >bc_n_n normalize //
+ |>bigop_0 >associative_plus >commutative_plus in ⊢ (??(??%)?)
+ <associative_plus >bigop_0 // @eq_f2
+ [>(bigop_op n ??? natACop) @same_bigop //
+ #i #ltin #_ <associative_times >(commutative_times b)
+ >(associative_times ?? b) <(distributive_times_plus_r (b^(S i)))
+ @eq_f2 // <associative_times >(commutative_times a)
+ >associative_times cut(∀n.a*a^n = a^(S n)) [#n @commutative_times] #H
+ >H <minus_Sn_m // <(distributive_times_plus_r (a^(n-i)))
+ @eq_f2 // @sym_eq >commutative_plus @bc1 //
+ |>bc_n_O >bc_n_O normalize //
+ ]
+ ]
+qed.
+
+theorem exp_S_sigma_p:∀a,n.
+(S a)^n = Σ_{k < S n}((bc n k)*a^(n-k)).
+#a #n cut (S a = a + 1) // #H >H
+>binomial_law @same_bigop //
qed.
+(*
theorem exp_Sn_SSO: \forall n. exp (S n) 2 = S((exp n 2) + 2*n).
intros.simplify.
rewrite < times_n_SO.
rewrite < assoc_plus.
rewrite < sym_plus.
reflexivity.
-qed.
+qed. *)
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department of the University of Bologna, Italy.
+ ||I||
+ ||T||
+ ||A|| This file is distributed under the terms of the
+ \ / GNU General Public License Version 2
+ \ /
+ V_______________________________________________________________ *)
+
+include "arithmetics/exp.ma".
+include "arithmetics/gcd.ma".
+include "arithmetics/congruence.ma".
+
+theorem congruent_ab: ∀m,n,a,b:nat. O < n → O < m →
+ gcd n m = 1 → ∃x.x ≅_{m} a ∧ x ≅_{n} b.
+#m #n #a #b #posn #posm #pnm
+cut (∃c,d.c*n - d*m = 1 ∨ d*m - c*n = 1) [<pnm @eq_minus_gcd]
+* #c * #d * #H
+ [(* first case *)
+ @(ex_intro nat ? ((a+b*m)*c*n-b*d*m)) %
+ [(* congruent to a *)
+ cut (c*n = d*m + 1)
+ [@minus_to_plus // @(transitive_le … (le_n_Sn …))
+ @(lt_minus_to_plus_r 0) //] -H #H
+ >associative_times >H <(commutative_plus ? (d*m))
+ >distributive_times_plus <times_n_1 >associative_plus
+ <associative_times <distributive_times_plus_r
+ <commutative_plus <plus_minus
+ [@(eq_times_plus_to_congruent … posm) //
+ |applyS monotonic_le_times_r @(transitive_le ? ((a+b*m)*d)) //
+ applyS monotonic_le_times_r apply (transitive_le … (b*m)) /2/
+ ]
+ |(* congruent to b *)
+ -pnm (cut (d*m = c*n-1))
+ [@sym_eq @plus_to_minus >commutative_plus
+ @minus_to_plus // @(transitive_le … (le_n_Sn …))
+ @(lt_minus_to_plus_r 0) //] #H1
+ >(associative_times b d) >H1 >distributive_times_minus
+ <associative_times <minus_minus
+ [@(eq_times_plus_to_congruent … posn) //
+ |applyS monotonic_le_times_r >commutative_times
+ @monotonic_le_times_r @(transitive_le ? (m*b)) /2/
+ |applyS monotonic_le_times_r @le_plus_to_minus //
+ ]
+ ]
+ |(* and now the symmetric case; the price to pay for working
+ in nat instead than Z *)
+ @(ex_intro nat ? ((b+a*n)*d*m-a*c*n)) %
+ [(* congruent to a *)
+ cut (c*n = d*m - 1)
+ [@sym_eq @plus_to_minus >commutative_plus @minus_to_plus // @(transitive_le … (le_n_Sn …))
+ @(lt_minus_to_plus_r 0) //] #H1
+ >(associative_times a c) >H1
+ >distributive_times_minus
+ <minus_minus
+ [@(eq_times_plus_to_congruent … posm) //
+ |<associative_times applyS monotonic_le_times_r
+ >commutative_times @monotonic_le_times_r
+ @(transitive_le ? (n*a)) /2/
+ |@monotonic_le_times_r <H @le_plus_to_minus //
+ ]
+ |(* congruent to b *)
+ cut (d*m = c*n + 1)
+ [@minus_to_plus // @(transitive_le … (le_n_Sn …))
+ @(lt_minus_to_plus_r 0) //] -H #H
+ >associative_times >H
+ >(commutative_plus (c*n))
+ >distributive_times_plus <times_n_1
+ <associative_times >associative_plus
+ <distributive_times_plus_r <commutative_plus <plus_minus
+ [@(eq_times_plus_to_congruent … posn) //
+ |applyS monotonic_le_times_r @(transitive_le ? (c*(b+n*a))) //
+ <commutative_times @monotonic_le_times_r
+ @(transitive_le ? (n*a)) /2/
+ ]
+ ]
+ ]
+qed.
+
+theorem congruent_ab_lt: ∀m,n,a,b. O < n → O < m →
+gcd n m = 1 → ∃x.x ≅_{m} a ∧ x ≅_{n} b ∧ x < m*n.
+#m #n #a #b #posn #posm #pnm
+cases(congruent_ab m n a b posn posm pnm) #x * #cxa #cxb
+@(ex_intro ? ? (x \mod (m*n))) %
+ [%
+ [@(transitive_congruent m ? x) //
+ @sym_eq >commutative_times @congruent_n_mod_times //
+ |@(transitive_congruent n ? x) //
+ @sym_eq @congruent_n_mod_times //
+ ]
+ |@lt_mod_m_m >(times_n_O 0) @lt_times //
+ ]
+qed.
+
+definition cr_pair ≝ λn,m,a,b.
+min (n*m) 0 (λx. andb (eqb (x \mod n) a) (eqb (x \mod m) b)).
+
+example cr_pair1: cr_pair 2 3 O O = O.
+// qed.
+
+example cr_pair2: cr_pair 2 3 1 0 = 3.
+// qed.
+
+example cr_pair3: cr_pair 2 3 1 2 = 5.
+// qed.
+
+example cr_pair4: cr_pair 5 7 3 2 = 23.
+// qed.
+
+example cr_pair5: cr_pair 3 7 0 4 = ?.
+normalize
+// qed.
+
+theorem mod_cr_pair : ∀m,n,a,b. a < m → b < n → gcd n m = 1 →
+(cr_pair m n a b) \mod m = a ∧ (cr_pair m n a b) \mod n = b.
+#m #n #a #b #ltam #ltbn #pnm
+cut (andb (eqb ((cr_pair m n a b) \mod m) a)
+ (eqb ((cr_pair m n a b) \mod n) b) = true)
+ [@f_min_true cases(congruent_ab_lt m n a b ?? pnm)
+ [#x * * #cxa #cxb #ltx @(ex_intro ?? x) % /2/
+ >eq_to_eqb_true
+ [>eq_to_eqb_true // <(lt_to_eq_mod …ltbn) //
+ |<(lt_to_eq_mod …ltam) //
+ ]
+ |@(le_to_lt_to_lt … ltbn) //
+ |@(le_to_lt_to_lt … ltam) //
+ ]
+ |#H >(eqb_true_to_eq … (andb_true_l … H)) >(eqb_true_to_eq … (andb_true_r … H)) /2/
+ ]
+qed.
#n #m #p #posp #congnm @(quotient ? ? ((n / p)-(m / p)))
>commutative_times >(div_mod n p) in ⊢ (??%?)
>(div_mod m p) in ⊢ (??%?) <(commutative_plus (m \mod p))
-<congnm <(minus_minus ? (n \mod p)) <minus_plus_m_m //
+<congnm <(minus_plus ? (n \mod p)) <minus_plus_m_m //
qed.
theorem mod_times: ∀n,m,p:nat. O < p →
]
qed. *)
-theorem le_plus_to_minus_r: ∀a,b,c. a + b ≤ c → a ≤ c -b.
-#a #b #c #H @(le_plus_to_le_r … b) /2/
-qed.
-
-theorem le_minus_to_plus_r: ∀a,b,c. c ≤ b → a ≤ b - c → a + c ≤ b.
-#a #b #c #Hlecb #H >(plus_minus_m_m … Hlecb) /2/
-qed.
-
-theorem lt_minus_to_plus: ∀a,b,c. a - b < c → a < c + b.
-#a #b #c #H @not_le_to_lt
-@(not_to_not … (lt_to_not_le …H)) /2/
-qed.
-
-theorem lt_minus_to_plus_r: ∀a,b,c. c ≤ a →
- a < b + c → a - c < b.
-#a #b #c #lea #H @not_le_to_lt
-@(not_to_not … (lt_to_not_le …H)) /2/
-qed.
-
theorem lt_to_le_times_to_lt_S_to_div: ∀a,c,b:nat.
O < b → (b*c) ≤ a → a < (b*(S c)) → a/b = c.
#a #c #b #posb#lea #lta
@(div_mod_spec_to_eq … (a-b*c) (div_mod_spec_div_mod … posb …))
-@div_mod_spec_intro [@lt_minus_to_plus_r // |/2/]
+@div_mod_spec_intro [@lt_plus_to_minus // |/2/]
qed.
theorem div_times_times: ∀a,b,c:nat. O < c → O < b →
(* a particular case of the previous theorem, with c=1 *)
theorem divides_d_gcd: ∀m,n,d.
- d ∣ m → d ∣ n → d ∣ gcd n m.
-/2/ (* bello *)
+ d ∣ m → d ∣ n → d ∣ gcd n m.
+#m #n #d #divdn #divdn applyS (divides_d_times_gcd m n d 1) //
qed.
theorem eq_minus_gcd_aux: ∀p,m,n.O < n → n ≤ m → n ≤ p →
<commutative_plus >distributive_times_plus_r
>(div_mod m n) in ⊢(? ? (? % ?) ?)
>associative_times <commutative_plus >distributive_times_plus
- <minus_
minus <commutative_plus <plus_minus //
+ <minus_
plus <commutative_plus <plus_minus //
|(* second case *)
<H @(ex_intro ?? (b+a*(m / n))) @(ex_intro ?? a) %1
>distributive_times_plus_r
>(div_mod m n) in ⊢ (? ? (? ? %) ?)
>distributive_times_plus >associative_times
- <minus_
minus <commutative_plus <plus_minus //
+ <minus_
plus <commutative_plus <plus_minus //
]
]
]
[|@le_plus_minus_m_m | @monotonic_le_plus_l // ]
qed.
+theorem le_minus_to_plus_r: ∀a,b,c. c ≤ b → a ≤ b - c → a + c ≤ b.
+#a #b #c #Hlecb #H >(plus_minus_m_m … Hlecb) /2/
+qed.
+
theorem le_plus_to_minus: ∀n,m,p. n ≤ p+m → n-m ≤ p.
#n #m #p #lep /2/ qed.
+theorem le_plus_to_minus_r: ∀a,b,c. a + b ≤ c → a ≤ c -b.
+#a #b #c #H @(le_plus_to_le_r … b) /2/
+qed.
+
+theorem lt_minus_to_plus: ∀a,b,c. a - b < c → a < c + b.
+#a #b #c #H @not_le_to_lt
+@(not_to_not … (lt_to_not_le …H)) /2/
+qed.
+
+theorem lt_minus_to_plus_r: ∀a,b,c. a < b - c → a + c < b.
+#a #b #c #H @not_le_to_lt @(not_to_not … (le_plus_to_minus …))
+@lt_to_not_le //
+qed.
+
+theorem lt_plus_to_minus: ∀n,m,p. m ≤ n → n < p+m → n-m < p.
+#n #m #p #lenm #H normalize <minus_Sn_m // @le_plus_to_minus //
+qed.
+
+theorem lt_plus_to_minus_r: ∀a,b,c. a + b < c → a < c - b.
+#a #b #c #H @le_plus_to_minus_r //
+qed.
+
theorem monotonic_le_minus_r:
∀p,q,n:nat. q ≤ p → n-p ≤ n-q.
#p #q #n #lepq @le_plus_to_minus
@eq_f (applyS plus_minus_m_m) /2/
qed.
-theorem minus_minus: ∀n,m,p. n-m-p = n -(m+p).
+theorem minus_plus: ∀n,m,p. n-m-p = n -(m+p).
#n #m #p
cases (decidable_le (m+p) n) #Hlt
[@plus_to_minus @plus_to_minus <associative_plus
]
qed.
+(*
+theorem plus_minus: ∀n,m,p. p ≤ m → (n+m)-p = n +(m-p).
+#n #m #p #lepm @plus_to_minus >(commutative_plus p)
+>associative_plus <plus_minus_m_m //
+qed. *)
+
+theorem minus_minus: ∀n,m,p:nat. p ≤ m → m ≤ n →
+ p+(n-m) = n-(m-p).
+#n #m #p #lepm #lemn
+@sym_eq @plus_to_minus <associative_plus <plus_minus_m_m //
+<commutative_plus <plus_minus_m_m //
+qed.
+
(*********************** boolean arithmetics ********************)
include "basics/bool.ma".
|@(quotient ?? ((div n q)-(div m q)))
>distributive_times_minus >commutative_times
>(commutative_times q) cut((n/q)*q = n - (n \mod q)) [//] #H
- >H >minus_minus >eqmod >commutative_plus
+ >H >minus_plus >eqmod >commutative_plus
<div_mod //
]
qed.
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department of the University of Bologna, Italy.
+ ||I||
+ ||T||
+ ||A|| This file is distributed under the terms of the
+ \ / GNU General Public License Version 2
+ \ /
+ V_______________________________________________________________ *)
+
+include "arithmetics/bigops.ma".
+
+definition natAop ≝ mk_Aop nat 0 plus (λa.refl ? a) (λn.sym_eq ??? (plus_n_O n))
+ (λa,b,c.sym_eq ??? (associative_plus a b c)).
+
+definition natACop ≝ mk_ACop nat 0 natAop commutative_plus.
+
+definition natDop ≝ mk_Dop nat 0 natACop times (λn.(sym_eq ??? (times_n_O n)))
+ distributive_times_plus.
+
+unification hint 0 ≔ ;
+ S ≟ natAop
+(* ---------------------------------------- *) ⊢
+ plus ≡ op ? ? S.
+
+unification hint 0 ≔ ;
+ S ≟ natACop
+(* ---------------------------------------- *) ⊢
+ plus ≡ op ? ? S.
+
+unification hint 0 ≔ ;
+ S ≟ natDop
+(* ---------------------------------------- *) ⊢
+ plus ≡ sum ? ? S.
+
+unification hint 0 ≔ ;
+ S ≟ natDop
+(* ---------------------------------------- *) ⊢
+ times ≡ prod ? ? S.
+
+(* 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
+ ]
+ ]
+ ]
+ ]
+ |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
+ ]
+ | apply lt_mod_m_m.
+ assumption
+ ]
+ | 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
+ ]
+ ]
+| 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
+ ]
+ | elim (H3 x x1 H5 H7 H6 H8).
+ assumption
+ ]
+ ]
+ ]
+]
+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
+ ]
+ ]
+qed. *)
\ No newline at end of file
projects / helm.git / commitdiff