--- /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/primes.ma".
+include "arithmetics/bigops.ma".
+
+theorem sigma_const: ∀n:nat. ∑_{i<n} 1 = n.
+#n elim n // #n1 >bigop_Strue //
+qed.
+
+(* monotonicity; these roperty should be expressed at a more
+genral level *)
+
+theorem le_pi:
+∀n.∀p:nat → bool.∀g1,g2:nat → nat.
+ (∀i.i<n → p i = true → g1 i ≤ g2 i ) →
+ ∏_{i < n | p i} (g1 i) ≤ ∏_{i < n | p i} (g2 i).
+#n #p #g1 #g2 elim n
+ [#_ @le_n
+ |#n1 #Hind #Hle cases (true_or_false (p n1)) #Hcase
+ [ >bigop_Strue // >bigop_Strue // @le_times
+ [@Hle // |@Hind #i #lti #Hpi @Hle [@lt_to_le @le_S_S @lti|@Hpi]]
+ |>bigop_Sfalse // >bigop_Sfalse // @Hind
+ #i #lti #Hpi @Hle [@lt_to_le @le_S_S @lti|@Hpi]
+ ]
+ ]
+qed.
+
+theorem exp_sigma: ∀n,a,p.
+ ∏_{i < n | p i} a = exp a (∑_{i < n | p i} 1).
+#n #a #p elim n // #n1 cases (true_or_false (p n1)) #Hcase
+ [>bigop_Strue // >bigop_Strue // |>bigop_Sfalse // >bigop_Sfalse //]
+qed.
+
+theorem times_pi: ∀n,p,f,g.
+ ∏_{i<n|p i}(f i*g i) = ∏_{i<n|p i}(f i) * ∏_{i<n|p i}(g i).
+#n #p #f #g elim n // #n1 cases (true_or_false (p n1)) #Hcase #Hind
+ [>bigop_Strue // >bigop_Strue // >bigop_Strue //
+ |>bigop_Sfalse // >bigop_Sfalse // >bigop_Sfalse //
+ ]
+qed.
+
+(*
+theorem true_to_pi_p_Sn: ∀n,p,g.
+ p n = true \to pi_p (S n) p g = (g n)*(pi_p n p g).
+intros.
+unfold pi_p.
+apply true_to_iter_p_gen_Sn.
+assumption.
+qed.
+
+theorem false_to_pi_p_Sn:
+\forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
+p n = false \to pi_p (S n) p g = pi_p n p g.
+intros.
+unfold pi_p.
+apply false_to_iter_p_gen_Sn.
+assumption.
+qed.
+
+theorem eq_pi_p: \forall p1,p2:nat \to bool.
+\forall g1,g2: nat \to nat.\forall n.
+(\forall x. x < n \to p1 x = p2 x) \to
+(\forall x. x < n \to g1 x = g2 x) \to
+pi_p n p1 g1 = pi_p n p2 g2.
+intros.
+unfold pi_p.
+apply eq_iter_p_gen;
+assumption.
+qed.
+
+theorem eq_pi_p1: \forall p1,p2:nat \to bool.
+\forall g1,g2: nat \to nat.\forall n.
+(\forall x. x < n \to p1 x = p2 x) \to
+(\forall x. x < n \to p1 x = true \to g1 x = g2 x) \to
+pi_p n p1 g1 = pi_p n p2 g2.
+intros.
+unfold pi_p.
+apply eq_iter_p_gen1;
+assumption.
+qed.
+
+theorem pi_p_false:
+\forall g: nat \to nat.\forall n.pi_p n (\lambda x.false) g = S O.
+intros.
+unfold pi_p.
+apply iter_p_gen_false.
+qed.
+
+theorem pi_p_times: \forall n,k:nat.\forall p:nat \to bool.
+\forall g: nat \to nat.
+pi_p (k+n) p g
+= pi_p k (\lambda x.p (x+n)) (\lambda x.g (x+n)) * pi_p n p g.
+intros.
+unfold pi_p.
+apply (iter_p_gen_plusA nat n k p g (S O) times)
+[ apply sym_times.
+| intros.
+ apply sym_eq.
+ apply times_n_SO
+| apply associative_times
+]
+qed.
+
+theorem false_to_eq_pi_p: \forall n,m:nat.n \le m \to
+\forall p:nat \to bool.
+\forall g: nat \to nat. (\forall i:nat. n \le i \to i < m \to
+p i = false) \to pi_p m p g = pi_p n p g.
+intros.
+unfold pi_p.
+apply (false_to_eq_iter_p_gen);
+assumption.
+qed.
+
+theorem or_false_eq_SO_to_eq_pi_p:
+\forall n,m:nat.\forall p:nat \to bool.
+\forall g: nat \to nat.
+n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false \lor g i = S O)
+\to pi_p m p g = pi_p n p g.
+intros.
+unfold pi_p.
+apply or_false_eq_baseA_to_eq_iter_p_gen
+ [intros.simplify.rewrite < plus_n_O.reflexivity
+ |assumption
+ |assumption
+ ]
+qed.
+
+theorem pi_p2 :
+\forall n,m:nat.
+\forall p1,p2:nat \to bool.
+\forall g: nat \to nat \to nat.
+pi_p (n*m)
+ (\lambda x.andb (p1 (div x m)) (p2 (mod x m)))
+ (\lambda x.g (div x m) (mod x m)) =
+pi_p n p1
+ (\lambda x.pi_p m p2 (g x)).
+intros.
+unfold pi_p.
+apply (iter_p_gen2 n m p1 p2 nat g (S O) times)
+[ apply sym_times
+| apply associative_times
+| intros.
+ apply sym_eq.
+ apply times_n_SO
+]
+qed.
+
+theorem pi_p2' :
+\forall n,m:nat.
+\forall p1:nat \to bool.
+\forall p2:nat \to nat \to bool.
+\forall g: nat \to nat \to nat.
+pi_p (n*m)
+ (\lambda x.andb (p1 (div x m)) (p2 (div x m) (mod x m)))
+ (\lambda x.g (div x m) (mod x m)) =
+pi_p n p1
+ (\lambda x.pi_p m (p2 x) (g x)).
+intros.
+unfold pi_p.
+apply (iter_p_gen2' n m p1 p2 nat g (S O) times)
+[ apply sym_times
+| apply associative_times
+| intros.
+ apply sym_eq.
+ apply times_n_SO
+]
+qed.
+
+lemma pi_p_gi: \forall g: nat \to nat.
+\forall n,i.\forall p:nat \to bool.i < n \to p i = true \to
+pi_p n p g = g i * pi_p n (\lambda x. andb (p x) (notb (eqb x i))) g.
+intros.
+unfold pi_p.
+apply (iter_p_gen_gi)
+[ apply sym_times
+| apply associative_times
+| intros.
+ apply sym_eq.
+ apply times_n_SO
+| assumption
+| assumption
+]
+qed.
+
+theorem eq_pi_p_gh:
+\forall g,h,h1: nat \to nat.\forall n,n1.
+\forall p1,p2:nat \to bool.
+(\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
+(\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to
+(\forall i. i < n \to p1 i = true \to h i < n1) \to
+(\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
+(\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to
+(\forall j. j < n1 \to p2 j = true \to h1 j < n) \to
+pi_p n p1 (\lambda x.g(h x)) = pi_p n1 p2 g.
+intros.
+unfold pi_p.
+apply (eq_iter_p_gen_gh nat (S O) times ? ? ? g h h1 n n1 p1 p2)
+[ apply sym_times
+| apply associative_times
+| intros.
+ apply sym_eq.
+ apply times_n_SO
+| assumption
+| assumption
+| assumption
+| assumption
+| assumption
+| assumption
+]
+qed.
+
+theorem exp_sigma_p: \forall n,a,p.
+pi_p n p (\lambda x.a) = (exp a (sigma_p n p (\lambda x.S O))).
+intros.
+elim n
+ [reflexivity
+ |apply (bool_elim ? (p n1))
+ [intro.
+ rewrite > true_to_pi_p_Sn
+ [rewrite > true_to_sigma_p_Sn
+ [simplify.
+ rewrite > H.
+ reflexivity.
+ |assumption
+ ]
+ |assumption
+ ]
+ |intro.
+ rewrite > false_to_pi_p_Sn
+ [rewrite > false_to_sigma_p_Sn
+ [simplify.assumption
+ |assumption
+ ]
+ |assumption
+ ]
+ ]
+ ]
+qed.
+
+theorem exp_sigma_p1: \forall n,a,p,f.
+pi_p n p (\lambda x.(exp a (f x))) = (exp a (sigma_p n p f)).
+intros.
+elim n
+ [reflexivity
+ |apply (bool_elim ? (p n1))
+ [intro.
+ rewrite > true_to_pi_p_Sn
+ [rewrite > true_to_sigma_p_Sn
+ [simplify.
+ rewrite > H.
+ rewrite > exp_plus_times.
+ reflexivity.
+ |assumption
+ ]
+ |assumption
+ ]
+ |intro.
+ rewrite > false_to_pi_p_Sn
+ [rewrite > false_to_sigma_p_Sn
+ [simplify.assumption
+ |assumption
+ ]
+ |assumption
+ ]
+ ]
+ ]
+qed.
+
+theorem times_pi_p: \forall n,p,f,g.
+pi_p n p (\lambda x.f x*g x) = pi_p n p f * pi_p n p g.
+intros.
+elim n
+ [simplify.reflexivity
+ |apply (bool_elim ? (p n1))
+ [intro.
+ rewrite > true_to_pi_p_Sn
+ [rewrite > true_to_pi_p_Sn
+ [rewrite > true_to_pi_p_Sn
+ [rewrite > H.autobatch
+ |assumption
+ ]
+ |assumption
+ ]
+ |assumption
+ ]
+ |intro.
+ rewrite > false_to_pi_p_Sn
+ [rewrite > false_to_pi_p_Sn
+ [rewrite > false_to_pi_p_Sn;assumption
+ |assumption
+ ]
+ |assumption
+ ]
+ ]
+ ]
+qed.
+
+theorem pi_p_SO: \forall n,p.
+pi_p n p (\lambda i.S O) = S O.
+intros.elim n
+ [reflexivity
+ |simplify.elim (p n1)
+ [simplify.rewrite < plus_n_O.assumption
+ |simplify.assumption
+ ]
+ ]
+qed.
+
+theorem exp_pi_p: \forall n,m,p,f.
+pi_p n p (\lambda x.exp (f x) m) = exp (pi_p n p f) m.
+intros.
+elim m
+ [simplify.apply pi_p_SO
+ |simplify.
+ rewrite > times_pi_p.
+ rewrite < H.
+ reflexivity
+ ]
+qed.
+
+theorem exp_times_pi_p: \forall n,m,k,p,f.
+pi_p n p (\lambda x.exp k (m*(f x))) =
+exp (pi_p n p (\lambda x.exp k (f x))) m.
+intros.
+apply (trans_eq ? ? (pi_p n p (\lambda x.(exp (exp k (f x)) m))))
+ [apply eq_pi_p;intros
+ [reflexivity
+ |apply sym_eq.rewrite > sym_times.
+ apply exp_exp_times
+ ]
+ |apply exp_pi_p
+ ]
+qed.
+
+
+theorem pi_p_knm:
+\forall g: nat \to nat.
+\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 ∧ 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) →
+(*
+Pi z < k | p1 z. g z =
+Pi x < n | p21 x. Pi y < m | p22 x y.g (h2 x y).
+*)
+pi_p k p1 g =
+pi_p n p21 (\lambda x:nat.pi_p m (p22 x) (\lambda y. g (h2 x y))).
+intros.
+unfold pi_p.unfold pi_p.
+apply (iter_p_gen_knm nat (S O) times sym_times assoc_times ? ? ? h11 h12)
+ [intros.apply sym_eq.apply times_n_SO.
+ |assumption
+ |assumption
+ ]
+qed.
+
+theorem pi_p_pi_p:
+\forall g: nat \to nat \to nat.
+\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
+pi_p n1 p11
+ (\lambda x:nat .pi_p m1 (p12 x) (\lambda y. g x y)) =
+pi_p n2 p21
+ (\lambda x:nat .pi_p m2 (p22 x) (\lambda y. g (h11 x y) (h12 x y))).
+intros.
+unfold pi_p.unfold pi_p.
+apply (iter_p_gen_2_eq ? ? ? sym_times assoc_times ? ? ? ? h21 h22)
+ [intros.apply sym_eq.apply times_n_SO.
+ |assumption
+ |assumption
+ ]
+qed.
+
+theorem pi_p_pi_p1:
+\forall g: nat \to nat \to nat.
+\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
+pi_p n p11 (\lambda x:nat.pi_p m (p12 x) (\lambda y. g x y)) =
+pi_p m p21 (\lambda y:nat.pi_p n (p22 y) (\lambda x. g x y)).
+intros.
+unfold pi_p.unfold pi_p.
+apply (iter_p_gen_iter_p_gen ? ? ? sym_times assoc_times)
+ [intros.apply sym_eq.apply times_n_SO.
+ |assumption
+ ]
+qed. *)
\ No newline at end of file
--- /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 "basics/types.ma".
+include "arithmetics/primes.ma".
+include "arithmetics/gcd.ma".
+(*
+include "arithmetics/nth_prime.ma".
+(* for some properties of divides *)
+*)
+
+let rec p_ord_aux p n m ≝
+ match n \mod m with
+ [ O ⇒
+ match p with
+ [ O ⇒ 〈O,n〉
+ | S p ⇒ let 〈q,r〉 ≝ p_ord_aux p (n / m) m in 〈S q,r〉]
+ | S a ⇒ 〈O,n〉].
+
+(* p_ord n m = <q,r> if m divides n q times, with remainder r *)
+definition p_ord ≝ λn,m:nat.p_ord_aux n n m.
+
+lemma p_ord_aux_0: ∀n,m.p_ord_aux 0 n m = 〈0,n〉.
+#n #m whd in match (p_ord_aux 0??); cases (n\mod m) normalize //
+qed.
+
+lemma p_ord_aux_Strue: ∀n,m,p,q,r.
+ n\mod m = 0 → p_ord_aux p (n / m) m = 〈q,r〉 →
+ p_ord_aux (S p) n m = 〈S q,r〉.
+#n #m #p #q #r whd in match (p_ord_aux (S p)??); #H >H
+#Hord whd in ⊢(??%?); >Hord //
+qed.
+
+lemma p_ord_aux_false: ∀p,n,m,a.
+ n\mod m = (S a) → p_ord_aux p n m = 〈0,n〉.
+#p #n #m #a cases p whd in match (p_ord_aux ???);
+ [#H whd in match (p_ord_aux ???); >H //
+ |#p1 #H whd in match (p_ord_aux ???); >H //
+ ]
+qed.
+
+(* the definition of p_ord_aux only makes sense for m>1.
+ In case m=1 we always end up with the pair 〈p,n〉 *)
+
+lemma p_ord_degenerate: ∀p,n. p_ord_aux p n 1 = 〈p,n〉.
+#p elim p // #p1 #Hind #n
+cut (mod n 1 = 0) [@divides_to_mod_O //] #Hmod
+>(p_ord_aux_Strue … (Hind … ) ) // >(div_mod n 1) in ⊢ (???%);
+>Hmod <plus_n_O <times_n_1 //
+qed.
+
+theorem p_ord_aux_to_exp: ∀p,n,m,q,r. O < m →
+ p_ord_aux p n m = 〈q,r〉 → n = m \sup q *r .
+#p elim p
+ [#n #m @(nat_case (n \mod m))
+ [#Hmod #q #r #posm >p_ord_aux_0 #Hqr destruct (Hqr) //
+ |#a #H #q #r #posm >(p_ord_aux_false … H) #Hqr destruct (Hqr) //
+ ]
+ |#p1 #Hind #n #m @(nat_case (n \mod m))
+ [#Hmod #q #r #posm lapply (refl …(p_ord_aux p1 (n/m) m));
+ cases (p_ord_aux p1 (n/m) m) in ⊢ (???%→?); #q1 #r1 #H1
+ >(p_ord_aux_Strue … Hmod H1) #H destruct (H) whd in match (exp ??);
+ >(div_mod n m) >Hmod <plus_n_O >(Hind … H1) //
+ |#a #H #q #r #posm >(p_ord_aux_false … H) #Hqr destruct (Hqr) //
+ ]
+ ]
+qed.
+
+(* questo va spostato in primes1.ma *)
+theorem p_ord_exp: ∀n,m,i. O < m → n \mod m ≠ O →
+ ∀p. i ≤ p → p_ord_aux p (m \sup i * n) m = 〈i,n〉.
+#n #m #i #posm #Hmod
+cut (∃a.n\mod m = S a)
+ [@(nat_case (n\mod m)) [#H @False_ind /2/|#a #Hmod1 %{a} //]] * #mod1 #Hmod1
+elim i
+ [#p normalize #posp <plus_n_O @(p_ord_aux_false … Hmod1)
+ |-i #i #Hind #p
+ @(nat_case p) [#Hp >Hp #Habs @False_ind @(absurd … Habs) //]
+ #p1 #Hp1 #lep1
+ cut (((m \sup (S i)*n) \mod m) = O)
+ [whd in match (exp ??); @divides_to_mod_O // %{(m^i*n)} //] #Hmod2
+ @(p_ord_aux_Strue … Hmod2) <(Hind p1) [2: @le_S_S_to_le //]
+ @eq_f2 // whd in match (exp ??); >associative_times >(commutative_times m)
+ <associative_times >div_times //
+ ]
+qed.
+
+theorem p_ord_aux_to_not_mod_O: ∀p,n,m,q,r. 1<m → O<n → n≤p →
+ p_ord_aux p n m = 〈q,r〉 → r \mod m ≠ O.
+#p elim p
+ [#n #m #q #r #_ #posn #nposn @False_ind @(absurd … posn) /2/
+ |#p1 #Hind #n #m @(nat_case (n \mod m))
+ [#Hmod #q #r #lt1m #posn #len lapply (refl …(p_ord_aux p1 (n/m) m));
+ cases (p_ord_aux p1 (n/m) m) in ⊢ (???%→?); #q1 #r1 #H1
+ >(p_ord_aux_Strue … Hmod H1) #H destruct (H) whd in match (exp ??);
+ @(Hind … lt1m … H1)
+ [@(pos_div … posn Hmod) @lt_to_le //
+ |@le_S_S_to_le @(transitive_le … len) @lt_times_to_lt_div
+ >(times_n_1 n) in ⊢ (?%?); @monotonic_lt_times_r //
+ ]
+ |#a #H #q #r #lt1m #posn #posm >(p_ord_aux_false … H) #Hqr destruct (Hqr)
+ >H @sym_not_eq //
+ ]
+ ]
+qed.
+
+theorem p_ord_exp1: ∀p,n,q,r. O < p → p ∤ r →
+ n = p \sup q * r → p_ord n p = 〈q,r〉.
+#p #n #q #r #posp #ndivpr #Hn >Hn -Hn -n @(p_ord_exp … posp)
+ [@(not_to_not … ndivpr) /2/
+ |@(transitive_le ? (p \sup q))
+ [cut (1<p)
+ [cases (le_to_or_lt_eq … posp) // #eqp1 @False_ind @(absurd ?? ndivpr)
+ <eqp1 % //]
+ #lt1p elim q // -q #q whd in match (exp ??);
+ cases q [#_ normalize <plus_n_O @lt_to_le //]
+ #q1 #Hind @(lt_to_le_to_lt ? ((S q1)*2))
+ [>(times_n_1 (S q1)) in ⊢ (?%?); @monotonic_lt_times_r //
+ |@le_times //
+ ]
+ |>(times_n_1 (p^q)) in ⊢ (?%?); @le_times //
+ lapply ndivpr -ndivpr cases r // #Habs @False_ind @(absurd ?? Habs) % //
+ ]
+ ]
+qed.
+
+theorem p_ord_to_exp1: ∀p,n,q,r. 1<p → O<n → p_ord n p = 〈q,r〉 →
+ p ∤ r ∧ n = p \sup q * r.
+#p #n #q #r #lt1p #posn #Hord %
+ [@(not_to_not … (p_ord_aux_to_not_mod_O … lt1p posn (le_n n)… Hord))
+ @divides_to_mod_O @lt_to_le //
+ |@(p_ord_aux_to_exp n …Hord) @lt_to_le //
+ ]
+qed.
+
+theorem eq_p_ord_q_O: ∀p,n,q. p_ord n p = 〈q,O〉 → n=O ∧ q=O.
+#p #n whd in match (p_ord ??); cases n
+ [#q cases p normalize [|#q1] #H destruct (H) % //
+ |#n1 #q cases p
+ [normalize #H destruct (H)
+ |#p1 cases p1
+ [>p_ord_degenerate #H destruct (H)
+ |#p2 lapply (refl …(p_ord_aux (S n1) (S n1) (S (S p2))));
+ cases (p_ord_aux (S n1) (S n1) (S (S p2))) in ⊢ (???%→?); #qa #ra #H
+ lapply (p_ord_to_exp1 (S (S p2)) (S n1) … H) //
+ * #_ #H1 >H #H2 @False_ind destruct (H2) <times_n_O in H1;
+ #Habs destruct (Habs)
+ ]
+ ]
+ ]
+qed.
+
+theorem p_ord_times: ∀p,a,b,qa,ra,qb,rb. prime p → O < a → O < b
+ → p_ord a p = 〈qa,ra〉 → p_ord b p = 〈qb,rb〉
+ → p_ord (a*b) p = 〈qa + qb, ra*rb〉.
+#p #a #b #qa #ra #qb #rb #Hprime #posa #posb #porda #pordb
+cut (1<p) [@prime_to_lt_SO //] #Hp1
+cases (p_ord_to_exp1 ???? Hp1 posa porda) -posa -porda #Hdiva #Ha
+elim (p_ord_to_exp1 ???? Hp1 posb pordb) -posb -pordb #Hdivb #Hb
+@p_ord_exp1
+ [@lt_to_le //
+ |% #Hdiv cases (divides_times_to_divides ? ? ? Hprime Hdiv)
+ #Habs @absurd /2/
+ |>Ha >Hb -Ha -Hb <associative_times <associative_times //
+ ]
+qed.
+
+theorem fst_p_ord_times: ∀p,a,b. prime p → O < a → O < b →
+ fst ?? (p_ord (a*b) p) = (fst ?? (p_ord a p)) + (fst ?? (p_ord b p)).
+#p #a #b #primep #posa #posb
+>(p_ord_times p a b (fst ?? (p_ord a p)) (snd ?? (p_ord a p))
+ (fst ?? (p_ord b p)) (snd ? ? (p_ord b p)) primep posa posb) //
+qed.
+
+theorem p_ord_p: ∀p:nat. 1 < p → p_ord p p = 〈1,1〉.
+#p #ltp1 @p_ord_exp1
+ [@lt_to_le //
+ |% #divp1 @(absurd … ltp1) @le_to_not_lt @divides_to_le //
+ |//
+ ]
+qed.
+
+(* p_ord and divides *)
+theorem divides_to_p_ord: ∀p,a,b,c,d,n,m:nat. O < n → O < m → prime p
+→ divides n m → p_ord n p = 〈a,b〉 →
+ p_ord m p = 〈c,d〉 → divides b d ∧ a ≤ c.
+#p #a #b #c #d #n #m #posn #posm #primep #divnm #ordn #ordm
+cut (1<p) [@prime_to_lt_SO //] #Hposp
+cases (p_ord_to_exp1 ? ? ? ? Hposp posn ordn) #divn #eqn
+cases (p_ord_to_exp1 ? ? ? ? Hposp posm ordm) #divm #eqm %
+ [@(gcd_1_to_divides_times_to_divides b (exp p c))
+ [cases (le_to_or_lt_eq ?? (le_O_n b)) //
+ |elim c
+ [>commutative_gcd //
+ |#c0 #Hind @eq_gcd_times_1
+ [@lt_O_exp @lt_to_le //
+ |@lt_to_le //
+ |@Hind
+ |>commutative_gcd @prime_to_gcd_1 //
+ ]
+ ]
+ |@(transitive_divides ? n) [%{(exp p a)} // |<eqm //]
+ ]
+ |@(le_exp_to_le p) //
+ @divides_to_le
+ [@lt_O_exp @lt_to_le //
+ |@(gcd_1_to_divides_times_to_divides ? d)
+ [@lt_O_exp @lt_to_le //
+ |elim a
+ [@gcd_SO_n
+ |#a0 #Hind whd in match (exp ??);
+ >commutative_gcd @eq_gcd_times_1
+ [@lt_O_exp @lt_to_le //
+ |@lt_to_le //
+ |>commutative_gcd //
+ |>commutative_gcd @prime_to_gcd_1 //
+ ]
+ ]
+ |@(transitive_divides ? n) // %{b} //
+ ]
+ ]
+ ]
+qed.
+
+(* p_ord and primes *)
+theorem not_divides_to_p_ord_O: ∀n,i.
+ (nth_prime i) ∤ n → p_ord n (nth_prime i) = 〈O,n〉.
+#n #i #H @p_ord_exp1 //
+qed.
+
+theorem p_ord_O_to_not_divides: ∀n,i,r. O < n →
+ p_ord n (nth_prime i) = 〈O,r〉
+ → (nth_prime i) ∤ n.
+#n #i #r #posn #Hord
+lapply (p_ord_to_exp1 … Hord) // * #H
+normalize <plus_n_O //
+qed.
+
+theorem p_ord_to_not_eq_O : ∀n,p,q,r. 1<n →
+ p_ord n (nth_prime p) = 〈q,r〉 → r≠O.
+#n #p #q #r #lt1n #Hord
+cut (O<n) [@lt_to_le //] #posn
+lapply (p_ord_to_exp1 …posn … Hord)
+ [@lt_SO_nth_prime_n
+ |* #H1 #H2 @(not_to_not …(lt_to_not_eq … posn))
+ #eqr >eqr in H2; //
+ ]
+qed.
+
+definition ord :nat → nat → nat ≝
+ λn,p. fst ?? (p_ord n p).
+
+definition ord_rem :nat → nat → nat ≝
+ λn,p. snd ?? (p_ord n p).
+
+lemma ord_eq: ∀n,p. ord n p = fst ?? (p_ord n p). //
+qed.
+
+lemma ord_rem_eq: ∀n,p. ord_rem n p = snd ?? (p_ord n p). //
+qed.
+
+theorem divides_to_ord: ∀p,n,m:nat.
+ O < n → O < m → prime p → divides n m
+ → divides (ord_rem n p) (ord_rem m p) ∧ (ord n p) ≤ (ord m p).
+#p #n #m #H #H1 #H2 #H3
+@(divides_to_p_ord p ? ? ? ? n m H H1 H2 H3)
+ [@eq_pair_fst_snd|@eq_pair_fst_snd]
+qed.
+
+theorem divides_to_divides_ord_rem: ∀p,n,m:nat.
+O < n → O < m → prime p → divides n m →
+ divides (ord_rem n p) (ord_rem m p).
+#p #n #m #H #H1 #H2 #H3 cases (divides_to_ord p n m H H1 H2 H3) //
+qed.
+
+theorem divides_to_le_ord: ∀p,n,m:nat.
+O < n → O < m → prime p → divides n m →
+ ord n p ≤ ord m p.
+#p #n #m #H #H1 #H2 #H3 cases (divides_to_ord p n m H H1 H2 H3) //
+qed.
+
+theorem exp_ord: \forall p,n. 1 < p → O < n →
+ n = p \sup (ord n p) * (ord_rem n p).
+#p #n #H #H1
+cases (p_ord_to_exp1 p n (ord n p) (ord_rem n p) H H1 ?)
+ [// |@eq_pair_fst_snd]
+qed.
+
+theorem divides_ord_rem: ∀p,n. 1 < p → O < n
+ → divides (ord_rem n p) n.
+#p #n #H #H1 %{(p \sup (ord n p))} >commutative_times @exp_ord //
+qed.
+
+theorem lt_O_ord_rem: ∀p,n. 1 < p → O < n → O < ord_rem n p.
+#p #n #H #H1
+cases (le_to_or_lt_eq … (le_O_n (ord_rem n p))) //
+#remO lapply(divides_ord_rem ?? H H1) <remO -remO #Hdiv0
+@False_ind @(absurd (0=n)) [cases Hdiv0 // | @lt_to_not_eq //]
+qed.
+
+(* properties of ord e ord_rem *)
+
+theorem ord_times: ∀p,m,n.O<m → O<n → prime p →
+ ord (m*n) p = ord m p+ord n p.
+#p #m #n #H #H1 #H2
+lapply (p_ord_times ??? (ord m p) (ord_rem m p) (ord n p) (ord_rem n p) H2 H H1
+ (eq_pair_fst_snd …) (eq_pair_fst_snd …)) #H3
+ @(eq_f … (fst …) … H3)
+qed.
+
+theorem ord_exp: ∀p,m. 1 < p → ord (exp p m) p = m.
+#p #m #H >ord_eq >(p_ord_exp1 p (exp p m) m (S O)) //
+ [@(not_to_not … (lt_to_not_le … H)) @divides_to_le //
+ |@lt_to_le //
+ ]
+qed.
+
+theorem not_divides_to_ord_O:
+∀p,m. prime p → p ∤ m → ord m p = O.
+#p #m #H #H1 >ord_eq >(p_ord_exp1 p m O m) // @prime_to_lt_O //
+qed.
+
+theorem ord_O_to_not_divides: ∀p,m. O < m → prime p →
+ ord m p = O → p ∤ m.
+#p #m #H #H1 #H2
+lapply (p_ord_to_exp1 p m (ord m p) (ord_rem m p) … H … (eq_pair_fst_snd …))
+ [@prime_to_lt_SO //
+ |* #H3 >H2 >commutative_times <times_n_1 //
+ ]
+qed.
+
+theorem divides_to_not_ord_O:
+∀p,m. O < m → prime p → divides p m →
+ ord m p ≠ O.
+#p #m #H #H1 #H2 % #H3 @(absurd … H2) @(ord_O_to_not_divides ? ? H H1 H3)
+qed.
+
+theorem not_ord_O_to_divides:
+∀p,m. O < m → prime p → (ord m p ≠ O) → divides p m.
+#p #m #H #H1 #H2 >(exp_ord p m) in ⊢ (??%);
+ [@(transitive_divides ? (exp p (ord m p)))
+ [lapply H2 cases (ord m p)
+ [* #H3 @False_ind @H3 //
+ |#a #_ normalize % //
+ ]
+ |%{(ord_rem m p)} //
+ ]
+ |//
+ |@prime_to_lt_SO //
+ ]
+qed.
+
+theorem not_divides_ord_rem: ∀m,p.O< m → 1 < p →
+ p ∤ (ord_rem m p).
+#m #p #H #H1
+lapply (p_ord_to_exp1 p m (ord m p) (ord_rem m p) ?? (eq_pair_fst_snd …)) // *
+#H2 #H3 @H2
+qed.
+
+theorem ord_ord_rem: ∀p,q,m. O < m → prime p → prime q →q < p →
+ ord (ord_rem m p) q = ord m q.
+#p #q #m #H #H1 #H2 #H3 >(exp_ord p m) in ⊢ (???(?%?));
+ [>(ord_times … H2)
+ [>not_divides_to_ord_O in ⊢ (???(?%?)); //
+ @(not_to_not … (lt_to_not_eq ? ? H3))
+ @(divides_exp_to_eq ? ? ? H2 H1)
+ |@lt_O_ord_rem // @prime_to_lt_SO //
+ |@lt_O_exp @prime_to_lt_O //
+ ]
+ |//
+ |@prime_to_lt_SO //
+ ]
+qed.
+
+theorem lt_ord_rem: ∀n,m. prime n → O < m →
+ divides n m → ord_rem m n < m.
+#n #m #H #H1 #H2
+cases (le_to_or_lt_eq (ord_rem m n) m ?)
+ [//
+ |#Hm @False_ind <Hm in H2; #Habs @(absurd ? Habs)
+ @not_divides_ord_rem // @prime_to_lt_SO //
+ |@divides_to_le //
+ @divides_ord_rem // @prime_to_lt_SO //
+ ]
+qed.
+
+(* p_ord_inv may be used to encode the pair ord and rem into
+ a single natural number. *)
+
+definition p_ord_inv ≝ λp,m,x.
+ let 〈q,r〉 ≝ p_ord x p in r*m+q.
+
+theorem eq_p_ord_inv: ∀p,m,x.
+ p_ord_inv p m x = (ord_rem x p)*m+(ord x p).
+#p #m #x normalize cases(p_ord_aux x x p) //
+qed.
+
+theorem div_p_ord_inv:
+∀p,m,x. ord x p < m → p_ord_inv p m x / m = ord_rem x p.
+#p #m #x >eq_p_ord_inv @div_plus_times
+qed.
+
+theorem mod_p_ord_inv:
+∀p,m,x. ord x p < m → p_ord_inv p m x \mod m = ord x p.
+#p #m #x >eq_p_ord_inv @mod_plus_times
+qed.
projects / helm.git / commitdiff