(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/log".
+set "baseuri" "cic:/matita/nat/ord".
include "datatypes/constructors.ma".
include "nat/exp.ma".
-include "nat/lt_arith.ma".
-include "nat/primes.ma".
-
-(* this definition of log is based on pairs, with a remainder *)
+include "nat/nth_prime.ma".
+include "nat/relevant_equations.ma". (* required by autobatch paramod *)
let rec p_ord_aux p n m \def
match n \mod m with
apply p_ord_aux_to_Prop.
assumption.
qed.
+
(* questo va spostato in primes1.ma *)
theorem p_ord_exp: \forall n,m,i. O < m \to n \mod m \neq O \to
\forall p. i \le p \to p_ord_aux p (m \sup i * n) m = pair nat nat i n.
apply p_ord_aux_to_Prop1.
assumption.assumption.assumption.
qed.
+
+theorem p_ord_exp1: \forall p,n,q,r. O < p \to \lnot p \divides r \to
+n = p \sup q * r \to p_ord n p = pair nat nat q r.
+intros.unfold p_ord.
+rewrite > H2.
+apply p_ord_exp
+ [assumption
+ |unfold.intro.apply H1.
+ apply mod_O_to_divides[assumption|assumption]
+ |apply (trans_le ? (p \sup q)).
+ cut ((S O) \lt p).
+ elim q.simplify.apply le_n_Sn.
+ simplify.
+ generalize in match H3.
+ apply (nat_case n1).simplify.
+ rewrite < times_n_SO.intro.assumption.
+ intros.
+ apply (trans_le ? (p*(S m))).
+ apply (trans_le ? ((S (S O))*(S m))).
+ simplify.rewrite > plus_n_Sm.
+ rewrite < plus_n_O.
+ apply le_plus_n.
+ apply le_times_l.
+ assumption.
+ apply le_times_r.assumption.
+ apply not_eq_to_le_to_lt.
+ unfold.intro.apply H1.
+ rewrite < H3.
+ apply (witness ? r r ?).simplify.apply plus_n_O.
+ assumption.
+ rewrite > times_n_SO in \vdash (? % ?).
+ apply le_times_r.
+ change with (O \lt r).
+ apply not_eq_to_le_to_lt.
+ unfold.intro.
+ apply H1.rewrite < H3.
+ apply (witness ? ? O ?).rewrite < times_n_O.reflexivity.
+ apply le_O_n.
+ ]
+qed.
+
+theorem p_ord_to_exp1: \forall p,n,q,r. (S O) \lt p \to O \lt n \to p_ord n p = pair nat nat q r\to
+\lnot p \divides r \land n = p \sup q * r.
+intros.
+unfold p_ord in H2.
+split.unfold.intro.
+apply (p_ord_aux_to_not_mod_O n n p q r).assumption.assumption.
+apply le_n.symmetry.assumption.
+apply divides_to_mod_O.apply (trans_lt ? (S O)).
+unfold.apply le_n.assumption.assumption.
+apply (p_ord_aux_to_exp n).apply (trans_lt ? (S O)).
+unfold.apply le_n.assumption.symmetry.assumption.
+qed.
+
+theorem p_ord_times: \forall p,a,b,qa,ra,qb,rb. prime p
+\to O \lt a \to O \lt b
+\to p_ord a p = pair nat nat qa ra
+\to p_ord b p = pair nat nat qb rb
+\to p_ord (a*b) p = pair nat nat (qa + qb) (ra*rb).
+intros.
+cut ((S O) \lt p).
+elim (p_ord_to_exp1 ? ? ? ? Hcut H1 H3).
+elim (p_ord_to_exp1 ? ? ? ? Hcut H2 H4).
+apply p_ord_exp1.
+apply (trans_lt ? (S O)).unfold.apply le_n.assumption.
+unfold.intro.
+elim (divides_times_to_divides ? ? ? H H9).
+apply (absurd ? ? H10 H5).
+apply (absurd ? ? H10 H7).
+(* rewrite > H6.
+rewrite > H8. *)
+autobatch paramodulation.
+unfold prime in H. elim H. assumption.
+qed.
+
+theorem fst_p_ord_times: \forall p,a,b. prime p
+\to O \lt a \to O \lt b
+\to fst ? ? (p_ord (a*b) p) = (fst ? ? (p_ord a p)) + (fst ? ? (p_ord b p)).
+intros.
+rewrite > (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)) H H1 H2).
+simplify.reflexivity.
+apply eq_pair_fst_snd.
+apply eq_pair_fst_snd.
+qed.
+
+theorem p_ord_p : \forall p:nat. (S O) \lt p \to p_ord p p = pair ? ? (S O) (S O).
+intros.
+apply p_ord_exp1.
+apply (trans_lt ? (S O)). unfold.apply le_n.assumption.
+unfold.intro.
+apply (absurd ? ? H).
+apply le_to_not_lt.
+apply divides_to_le.unfold.apply le_n.assumption.
+rewrite < times_n_SO.
+apply exp_n_SO.
+qed.
+
+(* p_ord and divides *)
+theorem divides_to_p_ord: \forall p,a,b,c,d,n,m:nat.
+O < n \to O < m \to prime p
+\to divides n m \to p_ord n p = pair ? ? a b \to
+p_ord m p = pair ? ? c d \to divides b d \land a \le c.
+intros.
+cut (S O < p)
+ [lapply (p_ord_to_exp1 ? ? ? ? Hcut H H4).
+ lapply (p_ord_to_exp1 ? ? ? ? Hcut H1 H5).
+ elim Hletin. clear Hletin.
+ elim Hletin1. clear Hletin1.
+ rewrite > H9 in H3.
+ split
+ [apply (gcd_SO_to_divides_times_to_divides (exp p c))
+ [elim (le_to_or_lt_eq ? ? (le_O_n b))
+ [assumption
+ |apply False_ind.
+ apply (lt_to_not_eq O ? H).
+ rewrite > H7.
+ rewrite < H10.
+ autobatch
+ ]
+ |elim c
+ [rewrite > sym_gcd.
+ apply gcd_SO_n
+ |simplify.
+ apply eq_gcd_times_SO
+ [apply lt_to_le.assumption
+ |apply lt_O_exp.apply lt_to_le.assumption
+ |rewrite > sym_gcd.
+ (* hint non trova prime_to_gcd_SO e
+ autobatch non chiude il goal *)
+ apply prime_to_gcd_SO
+ [assumption|assumption]
+ |assumption
+ ]
+ ]
+ |apply (trans_divides ? n)
+ [apply (witness ? ? (exp p a)).
+ rewrite > sym_times.
+ assumption
+ |assumption
+ ]
+ ]
+ |apply (le_exp_to_le p)
+ [assumption
+ |apply divides_to_le
+ [apply lt_O_exp.apply lt_to_le.assumption
+ |apply (gcd_SO_to_divides_times_to_divides d)
+ [apply lt_O_exp.apply lt_to_le.assumption
+ |elim a
+ [apply gcd_SO_n
+ |simplify.rewrite < sym_gcd.
+ apply eq_gcd_times_SO
+ [apply lt_to_le.assumption
+ |apply lt_O_exp.apply lt_to_le.assumption
+ |rewrite > sym_gcd.
+ (* hint non trova prime_to_gcd_SO e
+ autobatch non chiude il goal *)
+ apply prime_to_gcd_SO
+ [assumption|assumption]
+ |rewrite > sym_gcd. assumption
+ ]
+ ]
+ |apply (trans_divides ? n)
+ [apply (witness ? ? b).assumption
+ |rewrite > sym_times.assumption
+ ]
+ ]
+ ]
+ ]
+ ]
+ |elim H2.assumption
+ ]
+qed.
+
+(* p_ord and primes *)
+theorem not_divides_to_p_ord_O: \forall n,i.
+Not (divides (nth_prime i) n) \to p_ord n (nth_prime i) =
+pair nat nat O n.
+intros.
+apply p_ord_exp1
+ [apply lt_O_nth_prime_n
+ |assumption
+ |autobatch
+ ]
+qed.
+
+theorem p_ord_O_to_not_divides: \forall n,i,r.
+O < n \to
+p_ord n (nth_prime i) = pair nat nat O r
+\to Not (divides (nth_prime i) n).
+intros.
+lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
+ [apply lt_SO_nth_prime_n
+ |assumption
+ |elim Hletin.
+ simplify in H3.
+ rewrite > H3.
+ rewrite < plus_n_O.
+ assumption
+ ]
+qed.
+
+theorem p_ord_to_not_eq_O : \forall n,p,q,r.
+ (S O) < n \to
+ p_ord n (nth_prime p) = pair nat nat q r \to
+ Not (r=O).
+intros.
+unfold.intro.
+cut (O < n)
+ [lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
+ [apply lt_SO_nth_prime_n.
+ |assumption
+ |elim Hletin.
+ apply (lt_to_not_eq ? ? Hcut).
+ rewrite > H4.
+ rewrite > H2.
+ apply times_n_O
+ ]
+ |apply (trans_lt ? (S O))[apply lt_O_S|assumption]
+ ]
+qed.
+
+definition ord :nat \to nat \to nat \def
+\lambda n,p. fst ? ? (p_ord n p).
+
+definition ord_rem :nat \to nat \to nat \def
+\lambda n,p. snd ? ? (p_ord n p).
+
+theorem divides_to_ord: \forall p,n,m:nat.
+O < n \to O < m \to prime p
+\to divides n m
+\to divides (ord_rem n p) (ord_rem m p) \land (ord n p) \le (ord m p).
+intros.
+apply (divides_to_p_ord p ? ? ? ? n m H H1 H2 H3)
+ [unfold ord.unfold ord_rem.apply eq_pair_fst_snd
+ |unfold ord.unfold ord_rem.apply eq_pair_fst_snd
+ ]
+qed.
+
+theorem divides_to_divides_ord_rem: \forall p,n,m:nat.
+O < n \to O < m \to prime p \to divides n m \to
+divides (ord_rem n p) (ord_rem m p).
+intros.
+elim (divides_to_ord p n m H H1 H2 H3).assumption.
+qed.
+
+theorem divides_to_le_ord: \forall p,n,m:nat.
+O < n \to O < m \to prime p \to divides n m \to
+(ord n p) \le (ord m p).
+intros.
+elim (divides_to_ord p n m H H1 H2 H3).assumption.
+qed.
+
+theorem exp_ord: \forall p,n. (S O) \lt p
+\to O \lt n \to n = p \sup (ord n p) * (ord_rem n p).
+intros.
+elim (p_ord_to_exp1 p n (ord n p) (ord_rem n p))
+ [assumption
+ |assumption
+ |assumption
+ |unfold ord.unfold ord_rem.
+ apply eq_pair_fst_snd
+ ]
+qed.
+
+theorem divides_ord_rem: \forall p,n. (S O) < p \to O < n
+\to divides (ord_rem n p) n.
+intros.
+apply (witness ? ? (p \sup (ord n p))).
+rewrite > sym_times.
+apply exp_ord[assumption|assumption]
+qed.
+
+theorem lt_O_ord_rem: \forall p,n. (S O) < p \to O < n \to O < ord_rem n p.
+intros.
+elim (le_to_or_lt_eq O (ord_rem n p))
+ [assumption
+ |apply False_ind.
+ apply (lt_to_not_eq ? ? H1).
+ lapply (divides_ord_rem ? ? H H1).
+ rewrite < H2 in Hletin.
+ elim Hletin.
+ rewrite > H3.
+ reflexivity
+ |apply le_O_n
+ ]
+qed.
+
+(* p_ord_inv is the inverse of ord *)
+definition p_ord_inv \def
+\lambda p,m,x.
+ match p_ord x p with
+ [pair q r \Rightarrow r*m+q].
+theorem eq_p_ord_inv: \forall p,m,x.
+p_ord_inv p m x = (ord_rem x p)*m+(ord x p).
+intros.unfold p_ord_inv. unfold ord_rem.
+unfold ord.
+elim (p_ord x p).
+reflexivity.
+qed.
+
+theorem div_p_ord_inv:
+\forall p,m,x. ord x p < m \to p_ord_inv p m x / m = ord_rem x p.
+intros.rewrite > eq_p_ord_inv.
+apply div_plus_times.
+assumption.
+qed.
+
+theorem mod_p_ord_inv:
+\forall p,m,x. ord x p < m \to p_ord_inv p m x \mod m = ord x p.
+intros.rewrite > eq_p_ord_inv.
+apply mod_plus_times.
+assumption.
+qed.