\lambda n,m :nat. (eqb (mod m n) O).
theorem divides_b_to_Prop :
-\forall n,m:nat. O < n \to O < m \to
+\forall n,m:nat. O < n \to
match divides_b n m with
[ true \Rightarrow divides n m
| false \Rightarrow \lnot (divides n m)].
| false \Rightarrow \lnot (divides n m)].
apply eqb_elim.
intro.simplify.apply mod_O_to_divides.assumption.assumption.
-intro.simplify.intro.apply H2.apply divides_to_mod_O.assumption.assumption.
+intro.simplify.intro.apply H1.apply divides_to_mod_O.assumption.assumption.
qed.
theorem divides_b_true_to_divides :
-\forall n,m:nat. O < n \to O < m \to
+\forall n,m:nat. O < n \to
(divides_b n m = true ) \to divides n m.
intros.
change with
match true with
[ true \Rightarrow divides n m
| false \Rightarrow \lnot (divides n m)].
-rewrite < H2.apply divides_b_to_Prop.
-assumption.assumption.
+rewrite < H1.apply divides_b_to_Prop.
+assumption.
qed.
theorem divides_b_false_to_not_divides :
-\forall n,m:nat. O < n \to O < m \to
+\forall n,m:nat. O < n \to
(divides_b n m = false ) \to \lnot (divides n m).
intros.
change with
match false with
[ true \Rightarrow divides n m
| false \Rightarrow \lnot (divides n m)].
-rewrite < H2.apply divides_b_to_Prop.
-assumption.assumption.
+rewrite < H1.apply divides_b_to_Prop.
+assumption.
+qed.
+
+theorem decidable_divides: \forall n,m:nat.O < n \to
+decidable (divides n m).
+intros.change with (divides n m) \lor \not (divides n m).
+cut
+match divides_b n m with
+[ true \Rightarrow divides n m
+| false \Rightarrow \not (divides n m)] \to (divides n m) \lor \not (divides n m).
+apply Hcut.apply divides_b_to_Prop.assumption.
+elim (divides_b n m).left.apply H1.right.apply H1.
+qed.
+
+theorem divides_to_divides_b_true : \forall n,m:nat. O < n \to
+divides n m \to divides_b n m = true.
+intros.
+cut match (divides_b n m) with
+[ true \Rightarrow (divides n m)
+| false \Rightarrow \not (divides n m)] \to ((divides_b n m) = true).
+apply Hcut.apply divides_b_to_Prop.assumption.
+elim divides_b n m.reflexivity.
+absurd (divides n m).assumption.assumption.
+qed.
+
+theorem not_divides_to_divides_b_false: \forall n,m:nat. O < n \to
+\not(divides n m) \to (divides_b n m) = false.
+intros.
+cut match (divides_b n m) with
+[ true \Rightarrow (divides n m)
+| false \Rightarrow \not (divides n m)] \to ((divides_b n m) = false).
+apply Hcut.apply divides_b_to_Prop.assumption.
+elim divides_b n m.
+absurd (divides n m).assumption.assumption.
+reflexivity.
qed.
(* divides and pi *)
intros.
apply divides_b_false_to_not_divides.
apply trans_lt O (S O).apply le_n (S O).assumption.
-simplify.apply le_S_S.apply le_O_n.
change with (eqb (mod (S (fact n)) i) O) = false.
rewrite > mod_S_fact.simplify.reflexivity.
assumption.assumption.
simplify.reflexivity.
qed. *)
-(* not sure this is what we need *)
-theorem lt_S_O_smallest_factor:
+theorem lt_SO_smallest_factor:
\forall n:nat. (S O) < n \to (S O) < (smallest_factor n).
intro.
apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S O) H.
rewrite < sym_plus.simplify.reflexivity.
qed.
+theorem lt_O_smallest_factor: \forall n:nat. O < n \to O < (smallest_factor n).
+intro.
+apply nat_case n.intro.apply False_ind.apply not_le_Sn_n O H.
+intro.apply nat_case m.intro.
+simplify.apply le_n.
+intros.apply trans_lt ? (S O).
+simplify. apply le_n.
+apply lt_SO_smallest_factor.simplify. apply le_S_S.
+apply le_S_S.apply le_O_n.
+qed.
+
theorem divides_smallest_factor_n :
-\forall n:nat. (S O) < n \to divides (smallest_factor n) n.
+\forall n:nat. O < n \to divides (smallest_factor n) n.
intro.
-apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S O) H.
-intro.apply nat_case m.intro. apply False_ind.apply not_le_Sn_n (S O) H.
+apply nat_case n.intro.apply False_ind.apply not_le_Sn_O O H.
+intro.apply nat_case m.intro. simplify.
+apply witness ? ? (S O). simplify.reflexivity.
intros.
apply divides_b_true_to_divides.
-apply trans_lt ? (S O).apply le_n (S O).apply lt_S_O_smallest_factor ? H.
-apply trans_lt ? (S O).apply le_n (S O).assumption.
+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.
split.split.
apply le_minus_m.apply le_n.
rewrite > mod_n_n.reflexivity.
-apply trans_lt ? (S O).apply le_n (S O).assumption.
+apply trans_lt ? (S O).apply le_n (S O).simplify.
+apply le_S_S.apply le_S_S.apply le_O_n.
qed.
theorem le_smallest_factor_n :
intro.apply divides_to_le.
simplify.apply le_S_S.apply le_O_n.
apply divides_smallest_factor_n.
-simplify.apply le_S_S.apply le_S_S. apply le_O_n.
+simplify.apply le_S_S.apply le_O_n.
qed.
theorem lt_smallest_factor_to_not_divides: \forall n,i:nat.
intros.
apply divides_b_false_to_not_divides.
apply trans_lt O (S O).apply le_n (S O).assumption.
-apply trans_lt O (S O).apply le_n (S O).assumption.
change with (eqb (mod (S(S m1)) i) O) = false.
apply lt_min_aux_to_false
(\lambda i:nat.eqb (mod (S(S m1)) i) O) (S(S m1)) m1 i.
intro. change with (S(S O)) \le n \to (S O) < (smallest_factor n) \land
(\forall m:nat. divides m (smallest_factor n) \to (S O) < m \to m = (smallest_factor n)).
intro.split.
-apply lt_S_O_smallest_factor.assumption.
+apply lt_SO_smallest_factor.assumption.
intros.
cut le m (smallest_factor n).
elim le_to_or_lt_eq m (smallest_factor n) Hcut.
apply transitive_divides m (smallest_factor n).
assumption.
apply divides_smallest_factor_n.
-exact H.
+apply trans_lt ? (S O). simplify. apply le_n. exact H.
apply lt_smallest_factor_to_not_divides.
exact H.assumption.assumption.assumption.
apply divides_to_le.
apply trans_lt O (S O).
apply le_n (S O).
-apply lt_S_O_smallest_factor.
+apply lt_SO_smallest_factor.
exact H.
assumption.
qed.
smallest_factor (S(S m1)) = (S(S m1)).
intro.elim H.apply H2.
apply divides_smallest_factor_n.
-assumption.
-apply lt_S_O_smallest_factor.
+apply trans_lt ? (S O).simplify. apply le_n.assumption.
+apply lt_SO_smallest_factor.
assumption.
qed.
reflexivity.
qed.
-(* upper bound by Bertrand's conjecture. *)
-(* Too difficult to prove.
-let rec nth_prime n \def
-match n with
- [ O \Rightarrow (S(S O))
- | (S p) \Rightarrow
- let previous_prime \def S (nth_prime p) in
- min_aux previous_prime ((S(S O))*previous_prime) primeb].
-
-theorem example8 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
-normalize.reflexivity.
-qed.
-
-theorem example9 : nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))).
-normalize.reflexivity.
-qed.
-
-theorem example10 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
-normalize.reflexivity.
-qed. *)
-
-theorem smallest_factor_fact: \forall n:nat.
-n < smallest_factor (S (fact n)).
-intros.
-apply not_le_to_lt.
-change with smallest_factor (S (fact n)) \le n \to False.intro.
-apply not_divides_S_fact n (smallest_factor(S (fact n))) ? ?.
-apply divides_smallest_factor_n.
-simplify.apply le_S_S.apply le_SO_fact.
-apply lt_S_O_smallest_factor.
-simplify.apply le_S_S.apply le_SO_fact.
-assumption.
-qed.
-
-(* mi sembra che il problem sia ex *)
-theorem ex_prime: \forall n. (S O) \le n \to ex nat (\lambda m.
-n < m \land m \le (S (fact n)) \land (prime m)).
-intros.
-elim H.
-apply ex_intro nat ? (S(S O)).
-split.split.apply le_n (S(S O)).
-apply le_n (S(S O)).apply primeb_to_Prop (S(S O)).
-apply ex_intro nat ? (smallest_factor (S (fact (S n1)))).
-split.split.
-apply smallest_factor_fact.
-apply le_smallest_factor_n.
-(* ancora hint non lo trova *)
-apply prime_smallest_factor_n.
-change with (S(S O)) \le S (fact (S n1)).
-apply le_S.apply le_SSO_fact.
-simplify.apply le_S_S.assumption.
-qed.
-
-let rec nth_prime n \def
-match n with
- [ O \Rightarrow (S(S O))
- | (S p) \Rightarrow
- let previous_prime \def (nth_prime p) in
- let upper_bound \def S (fact previous_prime) in
- min_aux (upper_bound - (S previous_prime)) upper_bound primeb].
-
-(* it works, but nth_prime 4 takes already a few minutes -
-it must compute factorial of 7 ...
-
-theorem example11 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
-normalize.reflexivity.
-qed.
-
-theorem example12: nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))).
-normalize.reflexivity.
-qed.
-
-theorem example13 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
-normalize.reflexivity.
-*)
-
-theorem prime_nth_prime : \forall n:nat.prime (nth_prime n).
-intro.
-apply nat_case n.
-change with prime (S(S O)).
-apply primeb_to_Prop (S(S O)).
-intro.
-change with
-let previous_prime \def (nth_prime m) in
-let upper_bound \def S (fact previous_prime) in
-prime (min_aux (upper_bound - (S previous_prime)) upper_bound primeb).
-apply primeb_true_to_prime.
-apply f_min_aux_true.
-apply ex_intro nat ? (smallest_factor (S (fact (nth_prime m)))).
-split.split.
-cut S (fact (nth_prime m))-(S (fact (nth_prime m)) - (S (nth_prime m))) = (S (nth_prime m)).
-rewrite > Hcut.exact smallest_factor_fact (nth_prime m).
-(* maybe we could factorize this proof *)
-apply plus_to_minus.
-apply le_minus_m.
-apply plus_minus_m_m.
-apply le_S_S.
-apply le_n_fact_n.
-apply le_smallest_factor_n.
-apply prime_to_primeb_true.
-apply prime_smallest_factor_n.
-change with (S(S O)) \le S (fact (nth_prime m)).
-apply le_S_S.apply le_SO_fact.
-qed.
\ No newline at end of file
projects / helm.git / blobdiff