qed.
theorem divides_to_div_mod_spec :
-\forall n,m. O < n \to n \divides m \to div_mod_spec m n (div m n) O.
+\forall n,m. O < n \to n \divides m \to div_mod_spec m n (m / n) O.
intros.elim H1.rewrite > H2.
constructor 1.assumption.
apply lt_O_n_elim n H.intros.
qed.
theorem divides_to_mod_O:
-\forall n,m. O < n \to n \divides m \to (mod m n) = O.
-intros.apply div_mod_spec_to_eq2 m n (div m n) (mod m n) (div m n) O.
+\forall n,m. O < n \to n \divides m \to (m \mod n) = O.
+intros.apply div_mod_spec_to_eq2 m n (m / n) (m \mod n) (m / n) O.
apply div_mod_spec_div_mod.assumption.
apply divides_to_div_mod_spec.assumption.assumption.
qed.
theorem mod_O_to_divides:
-\forall n,m. O< n \to (mod m n) = O \to n \divides m.
+\forall n,m. O< n \to (m \mod n) = O \to n \divides m.
intros.
-apply witness n m (div m n).
-rewrite > plus_n_O (n*div m n).
+apply witness n m (m / n).
+rewrite > plus_n_O (n * (m / n)).
rewrite < H1.
rewrite < sym_times.
(* Andrea: perche' hint non lo trova ?*)
intro. apply witness n O O.apply times_n_O.
qed.
+theorem divides_n_n: \forall n:nat. n \divides n.
+intro. apply witness n n (S O).apply times_n_SO.
+qed.
+
theorem divides_SO_n: \forall n:nat. (S O) \divides n.
intro. apply witness (S O) n n. simplify.apply plus_n_O.
qed.
variant trans_divides: \forall n,m,p.
n \divides m \to m \divides p \to n \divides p \def transitive_divides.
+theorem eq_mod_to_divides:\forall n,m,p. O< p \to
+mod n p = mod m p \to divides p (n-m).
+intros.
+cut n \le m \or \not n \le m.
+elim Hcut.
+cut n-m=O.
+rewrite > Hcut1.
+apply witness p O O.
+apply times_n_O.
+apply eq_minus_n_m_O.
+assumption.
+apply witness p (n-m) ((div n p)-(div m p)).
+rewrite > distr_times_minus.
+rewrite > sym_times.
+rewrite > sym_times p.
+cut (div n p)*p = n - (mod n p).
+rewrite > Hcut1.
+rewrite > eq_minus_minus_minus_plus.
+rewrite > sym_plus.
+rewrite > H1.
+rewrite < div_mod.reflexivity.
+assumption.
+apply sym_eq.
+apply plus_to_minus.
+rewrite > sym_plus.
+apply div_mod.
+assumption.
+apply decidable_le n m.
+qed.
+
(* divides le *)
theorem divides_to_le : \forall n,m. O < m \to n \divides m \to n \le m.
intros. elim H1.rewrite > H2.cut O < n2.
(* boolean divides *)
definition divides_b : nat \to nat \to bool \def
-\lambda n,m :nat. (eqb (mod m n) O).
+\lambda n,m :nat. (eqb (m \mod n) O).
theorem divides_b_to_Prop :
\forall n,m:nat. O < n \to
| false \Rightarrow n \ndivides m].
intros.
change with
-match eqb (mod m n) O with
+match eqb (m \mod n) O with
[ true \Rightarrow n \divides m
| false \Rightarrow n \ndivides m].
apply eqb_elim.
qed.
(* divides and pi *)
-theorem divides_f_pi_f : \forall f:nat \to nat.\forall n,i:nat.
-i < n \to f i \divides pi n f.
-intros 3.elim n.apply False_ind.apply not_le_Sn_O i H.
+theorem divides_f_pi_f : \forall f:nat \to nat.\forall n,m,i:nat.
+m \le i \to i \le n+m \to f i \divides pi n f m.
+intros 5.elim n.simplify.
+cut i = m.rewrite < Hcut.apply divides_n_n.
+apply antisymmetric_le.assumption.assumption.
simplify.
-apply le_n_Sm_elim (S i) n1 H1.
-intro.
-apply transitive_divides ? (pi n1 f).
-apply H.simplify.apply le_S_S_to_le. assumption.
-apply witness ? ? (f n1).apply sym_times.
-intro.cut i = n1.
-rewrite > Hcut.
-apply witness ? ? (pi n1 f).reflexivity.
-apply inj_S.assumption.
+cut i < S n1+m \lor i = S n1 + m.
+elim Hcut.
+apply transitive_divides ? (pi n1 f m).
+apply H1.apply le_S_S_to_le. assumption.
+apply witness ? ? (f (S n1+m)).apply sym_times.
+rewrite > H3.
+apply witness ? ? (pi n1 f m).reflexivity.
+apply le_to_or_lt_eq.assumption.
qed.
+(*
theorem mod_S_pi: \forall f:nat \to nat.\forall n,i:nat.
-i < n \to (S O) < (f i) \to mod (S (pi n f)) (f i) = (S O).
-intros.cut mod (pi n f) (f i) = O.
+i < n \to (S O) < (f i) \to (S (pi n f)) \mod (f i) = (S O).
+intros.cut (pi n f) \mod (f i) = O.
rewrite < Hcut.
apply mod_S.apply trans_lt O (S O).apply le_n (S O).assumption.
rewrite > Hcut.assumption.
apply divides_to_mod_O.apply trans_lt O (S O).apply le_n (S O).assumption.
apply divides_f_pi_f.assumption.
qed.
+*)
(* divides and fact *)
theorem divides_fact : \forall n,i:nat.
qed.
theorem mod_S_fact: \forall n,i:nat.
-(S O) < i \to i \le n \to mod (S n!) i = (S O).
-intros.cut mod n! i = O.
+(S O) < i \to i \le n \to (S n!) \mod i = (S O).
+intros.cut n! \mod i = O.
rewrite < Hcut.
apply mod_S.apply trans_lt O (S O).apply le_n (S O).assumption.
rewrite > Hcut.assumption.
intros.
apply divides_b_false_to_not_divides.
apply trans_lt O (S O).apply le_n (S O).assumption.
-change with (eqb (mod (S n!) i) O) = false.
+change with (eqb ((S n!) \mod i) O) = false.
rewrite > mod_S_fact.simplify.reflexivity.
assumption.assumption.
qed.
| (S p) \Rightarrow
match p with
[ O \Rightarrow (S O)
- | (S q) \Rightarrow min_aux q (S(S q)) (\lambda m.(eqb (mod (S(S q)) m) O))]].
+ | (S q) \Rightarrow min_aux q (S(S q)) (\lambda m.(eqb ((S(S q)) \mod m) O))]].
(* it works !
theorem example1 : smallest_prime_factor (S(S(S O))) = (S(S(S O))).
intro.apply nat_case m.intro. apply False_ind.apply not_le_Sn_n (S O) H.
intros.
change with
-S O < min_aux m1 (S(S m1)) (\lambda m.(eqb (mod (S(S m1)) m) O)).
+S O < min_aux m1 (S(S m1)) (\lambda m.(eqb ((S(S m1)) \mod m) O)).
apply lt_to_le_to_lt ? (S (S O)).
apply le_n (S(S O)).
cut (S(S O)) = (S(S m1)) - m1.
rewrite > Hcut.
apply le_min_aux.
-apply sym_eq.apply plus_to_minus.apply le_S.apply le_n_Sn.
+apply sym_eq.apply plus_to_minus.
rewrite < sym_plus.simplify.reflexivity.
qed.
apply divides_b_true_to_divides.
apply lt_O_smallest_factor ? H.
change with
-eqb (mod (S(S m1)) (min_aux m1 (S(S m1))
- (\lambda m.(eqb (mod (S(S m1)) m) O)))) O = true.
+eqb ((S(S m1)) \mod (min_aux m1 (S(S m1))
+ (\lambda m.(eqb ((S(S m1)) \mod m) O)))) O = true.
apply f_min_aux_true.
apply ex_intro nat ? (S(S m1)).
split.split.
intros.
apply divides_b_false_to_not_divides.
apply trans_lt O (S O).apply le_n (S O).assumption.
-change with (eqb (mod (S(S m1)) i) O) = false.
+change with (eqb ((S(S m1)) \mod i) O) = false.
apply lt_min_aux_to_false
-(\lambda i:nat.eqb (mod (S(S m1)) i) O) (S(S m1)) m1 i.
+(\lambda i:nat.eqb ((S(S m1)) \mod i) O) (S(S m1)) m1 i.
cut (S(S O)) = (S(S m1)-m1).
rewrite < Hcut.exact H1.
apply sym_eq. apply plus_to_minus.
-apply le_S.apply le_n_Sn.
rewrite < sym_plus.simplify.reflexivity.
exact H2.
qed.
projects / helm.git / blobdiff