]
]
qed.
-
+
theorem lt_exp: \forall n,m,p:nat. S O < p \to n < m \to exp p n < exp p m.
apply nat_elim2
[intros.
]
qed.
+theorem le_exp_to_le:
+\forall a,n,m. S O < a \to exp a n \le exp a m \to n \le m.
+intro.
+apply nat_elim2;intros
+ [apply le_O_n
+ |apply False_ind.
+ apply (le_to_not_lt ? ? H1).
+ simplify.
+ rewrite > times_n_SO.
+ apply lt_to_le_to_lt_times
+ [assumption
+ |apply lt_O_exp.apply lt_to_le.assumption
+ |apply lt_O_exp.apply lt_to_le.assumption
+ ]
+ |simplify in H2.
+ apply le_S_S.
+ apply H
+ [assumption
+ |apply (le_times_to_le a)
+ [apply lt_to_le.assumption|assumption]
+ ]
+ ]
+qed.
+
+
theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to
\exists a,b. a*n - b*m = gcd_aux p m n \lor b*m - a*n = gcd_aux p m n.
intro.
-elim p.
-absurd (O < n).assumption.apply le_to_not_lt.assumption.
-cut (O < m).
-cut (n1 \divides m \lor n1 \ndivides m).
-simplify.
-elim Hcut1.
-rewrite > divides_to_divides_b_true.
-simplify.
-apply (ex_intro ? ? (S O)).
-apply (ex_intro ? ? O).
-left.simplify.rewrite < plus_n_O.
-apply sym_eq.apply minus_n_O.
-assumption.assumption.
-rewrite > not_divides_to_divides_b_false.
-change with
-(\exists a,b.
-a*n1 - b*m = gcd_aux n n1 (m \mod n1)
-\lor
-b*m - a*n1 = gcd_aux n n1 (m \mod n1)).
-cut
-(\exists a,b.
-a*(m \mod n1) - b*n1= gcd_aux n n1 (m \mod n1)
-\lor
-b*n1 - a*(m \mod n1) = gcd_aux n n1 (m \mod n1)).
-elim Hcut2.elim H5.elim H6.
-(* first case *)
-rewrite < H7.
-apply (ex_intro ? ? (a1+a*(m / n1))).
-apply (ex_intro ? ? a).
-right.
-rewrite < sym_plus.
-rewrite < (sym_times n1).
-rewrite > distr_times_plus.
-rewrite > (sym_times n1).
-rewrite > (sym_times n1).
-rewrite > (div_mod m n1) in \vdash (? ? (? % ?) ?).
-rewrite > assoc_times.
-rewrite < sym_plus.
-rewrite > distr_times_plus.
-rewrite < eq_minus_minus_minus_plus.
-rewrite < sym_plus.
-rewrite < plus_minus.
-rewrite < minus_n_n.reflexivity.
-apply le_n.
-assumption.
-(* second case *)
-rewrite < H7.
-apply (ex_intro ? ? (a1+a*(m / n1))).
-apply (ex_intro ? ? a).
-left.
-(* clear Hcut2.clear H5.clear H6.clear H. *)
-rewrite > sym_times.
-rewrite > distr_times_plus.
-rewrite > sym_times.
-rewrite > (sym_times n1).
-rewrite > (div_mod m n1) in \vdash (? ? (? ? %) ?).
-rewrite > distr_times_plus.
-rewrite > assoc_times.
-rewrite < eq_minus_minus_minus_plus.
-rewrite < sym_plus.
-rewrite < plus_minus.
-rewrite < minus_n_n.reflexivity.
-apply le_n.
-assumption.
-apply (H n1 (m \mod n1)).
-cut (O \lt m \mod n1 \lor O = m \mod n1).
-elim Hcut2.assumption.
-absurd (n1 \divides m).apply mod_O_to_divides.
-assumption.
-symmetry.assumption.assumption.
-apply le_to_or_lt_eq.apply le_O_n.
-apply lt_to_le.
-apply lt_mod_m_m.assumption.
-apply le_S_S_to_le.
-apply (trans_le ? n1).
-change with (m \mod n1 < n1).
-apply lt_mod_m_m.
-assumption.assumption.assumption.assumption.
-apply (decidable_divides n1 m).assumption.
-apply (lt_to_le_to_lt ? n1).assumption.assumption.
+elim p
+ [absurd (O < n)
+ [assumption
+ |apply le_to_not_lt.assumption
+ ]
+ |cut (O < m)
+ [cut (n1 \divides m \lor n1 \ndivides m)
+ [simplify.
+ elim Hcut1
+ [rewrite > divides_to_divides_b_true
+ [simplify.
+ apply (ex_intro ? ? (S O)).
+ apply (ex_intro ? ? O).
+ left.
+ simplify.
+ rewrite < plus_n_O.
+ apply sym_eq.
+ apply minus_n_O
+ |assumption
+ |assumption
+ ]
+ |rewrite > not_divides_to_divides_b_false
+ [change with
+ (\exists a,b.a*n1 - b*m = gcd_aux n n1 (m \mod n1)
+ \lor b*m - a*n1 = gcd_aux n n1 (m \mod n1)).
+ cut
+ (\exists a,b.a*(m \mod n1) - b*n1= gcd_aux n n1 (m \mod n1)
+ \lor b*n1 - a*(m \mod n1) = gcd_aux n n1 (m \mod n1))
+ [elim Hcut2.elim H5.elim H6
+ [(* first case *)
+ rewrite < H7.
+ apply (ex_intro ? ? (a1+a*(m / n1))).
+ apply (ex_intro ? ? a).
+ right.
+ rewrite < sym_plus.
+ rewrite < (sym_times n1).
+ rewrite > distr_times_plus.
+ rewrite > (sym_times n1).
+ rewrite > (sym_times n1).
+ rewrite > (div_mod m n1) in \vdash (? ? (? % ?) ?)
+ [rewrite > assoc_times.
+ rewrite < sym_plus.
+ rewrite > distr_times_plus.
+ rewrite < eq_minus_minus_minus_plus.
+ rewrite < sym_plus.
+ rewrite < plus_minus
+ [rewrite < minus_n_n.reflexivity
+ |apply le_n
+ ]
+ |assumption
+ ]
+ |(* second case *)
+ rewrite < H7.
+ apply (ex_intro ? ? (a1+a*(m / n1))).
+ apply (ex_intro ? ? a).
+ left.
+ (* clear Hcut2.clear H5.clear H6.clear H. *)
+ rewrite > sym_times.
+ rewrite > distr_times_plus.
+ rewrite > sym_times.
+ rewrite > (sym_times n1).
+ rewrite > (div_mod m n1) in \vdash (? ? (? ? %) ?)
+ [rewrite > distr_times_plus.
+ rewrite > assoc_times.
+ rewrite < eq_minus_minus_minus_plus.
+ rewrite < sym_plus.
+ rewrite < plus_minus
+ [rewrite < minus_n_n.reflexivity
+ |apply le_n
+ ]
+ |assumption
+ ]
+ ]
+ |apply (H n1 (m \mod n1))
+ [cut (O \lt m \mod n1 \lor O = m \mod n1)
+ [elim Hcut2
+ [assumption
+ |absurd (n1 \divides m)
+ [apply mod_O_to_divides
+ [assumption
+ |symmetry.assumption
+ ]
+ |assumption
+ ]
+ ]
+ |apply le_to_or_lt_eq.
+ apply le_O_n
+ ]
+ |apply lt_to_le.
+ apply lt_mod_m_m.
+ assumption
+ |apply le_S_S_to_le.
+ apply (trans_le ? n1)
+ [change with (m \mod n1 < n1).
+ apply lt_mod_m_m.
+ assumption
+ |assumption
+ ]
+ ]
+ ]
+ |assumption
+ |assumption
+ ]
+ ]
+ |apply (decidable_divides n1 m).
+ assumption
+ ]
+ |apply (lt_to_le_to_lt ? n1);assumption
+ ]
+ ]
qed.
theorem eq_minus_gcd:
|apply (trans_lt ? (S O))[apply le_n|assumption]
|assumption
]
- |elim (le_to_or_lt_eq O n2 (le_O_n n2))
+ |elim (le_to_or_lt_eq O n2 (le_O_n n2));
[assumption
|apply False_ind.
apply (le_to_not_lt n (S O))
apply le_plus_n.
qed.
+theorem le_plus_to_le:
+\forall a,n,m. a + n \le a + m \to n \le m.
+intro.
+elim a
+ [assumption
+ |apply H.
+ apply le_S_S_to_le.assumption
+ ]
+qed.
+
(* times *)
theorem monotonic_le_times_r:
\forall n:nat.monotonic nat le (\lambda m. n * m).
elim (plus_n_O ?).apply le_n.
simplify.rewrite < sym_plus.apply le_plus_n.
qed.
+
+theorem le_times_to_le:
+\forall a,n,m. S O \le a \to a * n \le a * m \to n \le m.
+intro.
+apply nat_elim2;intros
+ [apply le_O_n
+ |apply False_ind.
+ rewrite < times_n_O in H1.
+ generalize in match H1.
+ apply (lt_O_n_elim ? H).
+ intros.
+ simplify in H2.
+ apply (le_to_not_lt ? ? H2).
+ apply lt_O_S
+ |apply le_S_S.
+ apply H
+ [assumption
+ |rewrite < times_n_Sm in H2.
+ rewrite < times_n_Sm in H2.
+ apply (le_plus_to_le a).
+ assumption
+ ]
+ ]
+qed.
\ No newline at end of file
exact (decidable_lt p q).
qed.
+theorem lt_times_n_to_lt:
+\forall n,p,q:nat. O < n \to p*n < q*n \to p < q.
+intro.
+apply (nat_case n)
+ [intros.apply False_ind.apply (not_le_Sn_n ? H)
+ |intros 4.apply lt_times_to_lt_l
+ ]
+qed.
+
theorem lt_times_to_lt_r:
\forall n,p,q:nat. (S n)*p < (S n)*q \to lt p q.
intros.
assumption.
qed.
+theorem lt_times_n_to_lt_r:
+\forall n,p,q:nat. O < n \to n*p < n*q \to lt p q.
+intro.
+apply (nat_case n)
+ [intros.apply False_ind.apply (not_le_Sn_n ? H)
+ |intros 4.apply lt_times_to_lt_r
+ ]
+qed.
+
theorem nat_compare_times_l : \forall n,p,q:nat.
nat_compare p q = nat_compare ((S n) * p) ((S n) * q).
intros.apply nat_compare_elim.intro.
apply exp_n_SO.
qed.
-(* spostare *)
-theorem le_plus_to_le:
-\forall a,n,m. a + n \le a + m \to n \le m.
-intro.
-elim a
- [assumption
- |apply H.
- apply le_S_S_to_le.assumption
- ]
-qed.
-
-theorem le_times_to_le:
-\forall a,n,m. O < a \to a * n \le a * m \to n \le m.
-intro.
-apply nat_elim2;intros
- [apply le_O_n
- |apply False_ind.
- rewrite < times_n_O in H1.
- generalize in match H1.
- apply (lt_O_n_elim ? H).
- intros.
- simplify in H2.
- apply (le_to_not_lt ? ? H2).
- apply lt_O_S
- |apply le_S_S.
- apply H
- [assumption
- |rewrite < times_n_Sm in H2.
- rewrite < times_n_Sm in H2.
- apply (le_plus_to_le a).
- assumption
- ]
- ]
-qed.
-
-theorem le_exp_to_le:
-\forall a,n,m. S O < a \to exp a n \le exp a m \to n \le m.
-intro.
-apply nat_elim2;intros
- [apply le_O_n
- |apply False_ind.
- apply (le_to_not_lt ? ? H1).
- simplify.
- rewrite > times_n_SO.
- apply lt_to_le_to_lt_times
- [assumption
- |apply lt_O_exp.apply lt_to_le.assumption
- |apply lt_O_exp.apply lt_to_le.assumption
- ]
- |simplify in H2.
- apply le_S_S.
- apply H
- [assumption
- |apply (le_times_to_le a)
- [apply lt_to_le.assumption|assumption]
- ]
- ]
-qed.
-
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
|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.
\ No newline at end of file
unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_n (S O) H1).
qed.
+theorem prime_to_lt_O: \forall p. prime p \to O < p.
+intros.elim H.apply lt_to_le.assumption.
+qed.
+
(* smallest factor *)
definition smallest_factor : nat \to nat \def
\lambda n:nat.
apply assoc_plus.
qed.
+theorem times_O_to_O: \forall n,m:nat.n*m = O \to n = O \lor m= O.
+apply nat_elim2;intros
+ [left.reflexivity
+ |right.reflexivity
+ |apply False_ind.
+ simplify in H1.
+ apply (not_eq_O_S ? (sym_eq ? ? ? H1))
+ ]
+qed.
+
theorem times_n_SO : \forall n:nat. n = n * S O.
intros.
rewrite < times_n_Sm.
projects / helm.git / commitdiff