(* this definition of log is based on pairs, with a remainder *)
let rec p_ord_aux p n m \def
- match (mod n m) with
+ match n \mod m with
[ O \Rightarrow
match p with
[ O \Rightarrow pair nat nat O n
| (S p) \Rightarrow
- match (p_ord_aux p (div n m) m) with
+ match (p_ord_aux p (n / m) m) with
[ (pair q r) \Rightarrow pair nat nat (S q) r]]
| (S a) \Rightarrow pair nat nat O n].
elim p.
change with
match (
-match (mod n m) with
+match n \mod m with
[ O \Rightarrow pair nat nat O n
| (S a) \Rightarrow pair nat nat O n] )
with
[ (pair q r) \Rightarrow n = m \sup q * r ].
-apply nat_case (mod n m).
+apply nat_case (n \mod m).
simplify.apply plus_n_O.
intros.
simplify.apply plus_n_O.
change with
match (
-match (mod n1 m) with
+match n1 \mod m with
[ O \Rightarrow
- match (p_ord_aux n (div n1 m) m) with
+ match (p_ord_aux n (n1 / m) m) with
[ (pair q r) \Rightarrow pair nat nat (S q) r]
| (S a) \Rightarrow pair nat nat O n1] )
with
[ (pair q r) \Rightarrow n1 = m \sup q * r].
-apply nat_case1 (mod n1 m).intro.
+apply nat_case1 (n1 \mod m).intro.
change with
match (
- match (p_ord_aux n (div n1 m) m) with
+ match (p_ord_aux n (n1 / m) m) with
[ (pair q r) \Rightarrow pair nat nat (S q) r])
with
[ (pair q r) \Rightarrow n1 = m \sup q * r].
-generalize in match (H (div n1 m) m).
-elim p_ord_aux n (div n1 m) m.
+generalize in match (H (n1 / m) m).
+elim p_ord_aux n (n1 / m) m.
simplify.
rewrite > assoc_times.
-rewrite < H3.rewrite > plus_n_O (m*(div n1 m)).
+rewrite < H3.rewrite > plus_n_O (m*(n1 / m)).
rewrite < H2.
rewrite > sym_times.
rewrite < div_mod.reflexivity.
assumption.
qed.
(* questo va spostato in primes1.ma *)
-theorem p_ord_exp: \forall n,m,i. O < m \to mod n m \neq O \to
+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.
intros 5.
elim i.
rewrite < plus_n_O.
apply nat_case p.
change with
- match (mod n m) with
+ match n \mod m with
[ O \Rightarrow pair nat nat O n
| (S a) \Rightarrow pair nat nat O n]
= pair nat nat O n.
-elim (mod n m).simplify.reflexivity.simplify.reflexivity.
+elim (n \mod m).simplify.reflexivity.simplify.reflexivity.
intro.
change with
- match (mod n m) with
+ match n \mod m with
[ O \Rightarrow
- match (p_ord_aux m1 (div n m) m) with
+ match (p_ord_aux m1 (n / m) m) with
[ (pair q r) \Rightarrow pair nat nat (S q) r]
| (S a) \Rightarrow pair nat nat O n]
= pair nat nat O n.
-cut O < mod n m \lor O = mod n m.
-elim Hcut.apply lt_O_n_elim (mod n m) H3.
+cut O < n \mod m \lor O = n \mod m.
+elim Hcut.apply lt_O_n_elim (n \mod m) H3.
intros. simplify.reflexivity.
apply False_ind.
apply H1.apply sym_eq.assumption.
apply nat_case p.intro.apply False_ind.apply not_le_Sn_O n1 H4.
intros.
change with
- match (mod (m \sup (S n1) *n) m) with
+ match ((m \sup (S n1) *n) \mod m) with
[ O \Rightarrow
- match (p_ord_aux m1 (div (m \sup (S n1) *n) m) m) with
+ match (p_ord_aux m1 ((m \sup (S n1) *n) / m) m) with
[ (pair q r) \Rightarrow pair nat nat (S q) r]
| (S a) \Rightarrow pair nat nat O (m \sup (S n1) *n)]
= pair nat nat (S n1) n.
-cut (mod (m \sup (S n1)*n) m) = O.
+cut ((m \sup (S n1)*n) \mod m) = O.
rewrite > Hcut.
change with
-match (p_ord_aux m1 (div (m \sup (S n1)*n) m) m) with
+match (p_ord_aux m1 ((m \sup (S n1)*n) / m) m) with
[ (pair q r) \Rightarrow pair nat nat (S q) r]
= pair nat nat (S n1) n.
-cut div (m \sup (S n1) *n) m = m \sup n1 *n.
+cut (m \sup (S n1) *n) / m = m \sup n1 *n.
rewrite > Hcut1.
rewrite > H2 m1. simplify.reflexivity.
apply le_S_S_to_le.assumption.
(* div_exp *)
-change with div (m* m \sup n1 *n) m = m \sup n1 * n.
+change with (m* m \sup n1 *n) / m = m \sup n1 * n.
rewrite > assoc_times.
apply lt_O_n_elim m H.
intro.apply div_times.
theorem p_ord_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to
match p_ord_aux p n m with
- [ (pair q r) \Rightarrow mod r m \neq O].
+ [ (pair q r) \Rightarrow r \mod m \neq O].
intro.elim p.absurd O < n.assumption.
apply le_to_not_lt.assumption.
change with
match
- (match (mod n1 m) with
+ (match n1 \mod m with
[ O \Rightarrow
- match (p_ord_aux n(div n1 m) m) with
+ match (p_ord_aux n(n1 / m) m) with
[ (pair q r) \Rightarrow pair nat nat (S q) r]
| (S a) \Rightarrow pair nat nat O n1])
with
- [ (pair q r) \Rightarrow mod r m \neq O].
-apply nat_case1 (mod n1 m).intro.
-generalize in match (H (div n1 m) m).
-elim (p_ord_aux n (div n1 m) m).
+ [ (pair q r) \Rightarrow r \mod m \neq O].
+apply nat_case1 (n1 \mod m).intro.
+generalize in match (H (n1 / m) m).
+elim (p_ord_aux n (n1 / m) m).
apply H5.assumption.
apply eq_mod_O_to_lt_O_div.
apply trans_lt ? (S O).simplify.apply le_n.
assumption.assumption.assumption.
apply le_S_S_to_le.
-apply trans_le ? n1.change with div n1 m < n1.
+apply trans_le ? n1.change with n1 / m < n1.
apply lt_div_n_m_n.assumption.assumption.assumption.
intros.
-change with mod n1 m \neq O.
+change with n1 \mod m \neq O.
rewrite > H4.
(* Andrea: META NOT FOUND !!!
rewrite > sym_eq. *)
qed.
theorem p_ord_aux_to_not_mod_O: \forall p,n,m,q,r. (S O) < m \to O < n \to n \le p \to
- pair nat nat q r = p_ord_aux p n m \to mod r m \neq O.
+ pair nat nat q r = p_ord_aux p n m \to r \mod m \neq O.
intros.
change with
match (pair nat nat q r) with
- [ (pair q r) \Rightarrow mod r m \neq O].
+ [ (pair q r) \Rightarrow r \mod m \neq O].
rewrite > H3.
apply p_ord_aux_to_Prop1.
assumption.assumption.assumption.