non associative with precedence 45
for @{ 'ngtr $a $b }.
+notation "hvbox(a break \divides b)"
+ non associative with precedence 45
+for @{ 'divides $a $b }.
+
+notation "hvbox(a break \ndivides b)"
+ non associative with precedence 45
+for @{ 'ndivides $a $b }.
+
notation "hvbox(a break + b)"
left associative with precedence 50
for @{ 'plus $a $b }.
for @{ 'uminus $a }.
notation "a !"
- left associative with precedence 65
+ non associative with precedence 80
for @{ 'fact $a }.
notation "(a \sup b)"
interpretation "logical or" 'or x y =
(cic:/matita/logic/connectives/Or.ind#xpointer(1/1) x y).
-definition decidable : Prop \to Prop \def \lambda A:Prop. A \lor \not A.
+definition decidable : Prop \to Prop \def \lambda A:Prop. A \lor \lnot A.
inductive ex (A:Type) (P:A \to Prop) : Prop \def
ex_intro: \forall x:A. P x \to ex A P.
qed.
theorem leb_elim: \forall n,m:nat. \forall P:bool \to Prop.
-(n \leq m \to (P true)) \to (\not (n \leq m) \to (P false)) \to
+(n \leq m \to (P true)) \to (\lnot (n \leq m) \to (P false)) \to
P (leb n m).
intros.
cut
interpretation "factorial" 'fact n = (cic:/matita/nat/factorial/fact.con n).
-theorem le_SO_fact : \forall n. (S O) \le n !.
+theorem le_SO_fact : \forall n. (S O) \le n!.
intro.elim n.simplify.apply le_n.
-change with (S O) \le (S n1)*n1 !.
+change with (S O) \le (S n1)*n1!.
apply trans_le ? ((S n1)*(S O)).simplify.
apply le_S_S.apply le_O_n.
apply le_times_r.assumption.
qed.
-theorem le_SSO_fact : \forall n. (S O) < n \to (S(S O)) \le n !.
+theorem le_SSO_fact : \forall n. (S O) < n \to (S(S O)) \le n!.
intro.apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S O) H.
-intros.change with (S (S O)) \le (S m)*m !.
+intros.change with (S (S O)) \le (S m)*m!.
apply trans_le ? ((S(S O))*(S O)).apply le_n.
apply le_times.exact H.apply le_SO_fact.
qed.
-theorem le_n_fact_n: \forall n. n \le n !.
+theorem le_n_fact_n: \forall n. n \le n!.
intro. elim n.apply le_O_n.
-change with S n1 \le (S n1)*n1 !.
+change with S n1 \le (S n1)*n1!.
apply trans_le ? ((S n1)*(S O)).
rewrite < times_n_SO.apply le_n.
apply le_times.apply le_n.
apply le_SO_fact.
qed.
-theorem lt_n_fact_n: \forall n. (S(S O)) < n \to n < n !.
+theorem lt_n_fact_n: \forall n. (S(S O)) < n \to n < n!.
intro.apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S(S O)) H.
-intros.change with (S m) < (S m)*m !.
+intros.change with (S m) < (S m)*m!.
apply lt_to_le_to_lt ? ((S m)*(S (S O))).
rewrite < sym_times.
simplify.
(* max_prime_factor is indeed a factor *)
theorem divides_max_prime_factor_n: \forall n:nat. (S O) < n \to
-divides (nth_prime (max_prime_factor n)) n.
+nth_prime (max_prime_factor n) \divides n.
intros.apply divides_b_true_to_divides.
apply lt_O_nth_prime_n.
apply f_max_true (\lambda p:nat.eqb (mod n (nth_prime p)) O) n.
apply prime_smallest_factor_n.assumption.
qed.
-theorem divides_to_max_prime_factor : \forall n,m. (S O) < n \to O < m \to divides n m \to
+theorem divides_to_max_prime_factor : \forall n,m. (S O) < n \to O < m \to n \divides m \to
max_prime_factor n \le max_prime_factor m.
intros.change with
(max n (\lambda p:nat.eqb (mod n (nth_prime p)) O)) \le
apply divides_to_divides_b_true.
cut prime (nth_prime (max_prime_factor n)).
apply lt_O_nth_prime_n.apply prime_nth_prime.
-cut divides (nth_prime (max_prime_factor n)) n.
+cut nth_prime (max_prime_factor n) \divides n.
apply transitive_divides ? n.
apply divides_max_prime_factor_n.
assumption.assumption.
cut max_prime_factor r \lt max_prime_factor n \lor
max_prime_factor r = max_prime_factor n.
elim Hcut.assumption.
-absurd (divides (nth_prime (max_prime_factor n)) r).
+absurd nth_prime (max_prime_factor n) \divides r.
rewrite < H4.
apply divides_max_prime_factor_n.
assumption.
-change with (divides (nth_prime (max_prime_factor n)) r) \to False.
+change with nth_prime (max_prime_factor n) \divides r \to False.
intro.
-cut \not (mod r (nth_prime (max_prime_factor n))) = O.
+cut \lnot (mod r (nth_prime (max_prime_factor n))) = O.
apply Hcut1.apply divides_to_mod_O.
apply lt_O_nth_prime_n.assumption.
apply plog_aux_to_not_mod_O n n ? q r.
apply sym_eq. apply S_pred.
cut O < q \lor O = q.
elim Hcut2.assumption.
-absurd divides (nth_prime p) (S (S m1)).
+absurd nth_prime p \divides S (S m1).
apply divides_max_prime_factor_n (S (S m1)).
simplify.apply le_S_S.apply le_S_S. apply le_O_n.
cut (S(S m1)) = r.
rewrite > Hcut3 in \vdash (? (? ? %)).
-change with divides (nth_prime p) r \to False.
+change with nth_prime p \divides r \to False.
intro.
apply plog_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r.
apply lt_SO_nth_prime_n.
| (nf_cons n g) \Rightarrow max_p_exponent g].
theorem divides_max_p_defactorize: \forall f:nat_fact.\forall i:nat.
-divides (nth_prime ((max_p f)+i)) (defactorize_aux f i).
+nth_prime ((max_p f)+i) \divides defactorize_aux f i.
intro.
elim f.simplify.apply witness ? ? ((nth_prime i) \sup n).
reflexivity.
change with
-divides (nth_prime (S(max_p n1)+i))
-((nth_prime i) \sup n *(defactorize_aux n1 (S i))).
+nth_prime (S(max_p n1)+i) \divides
+(nth_prime i) \sup n *(defactorize_aux n1 (S i)).
elim H (S i).
rewrite > H1.
rewrite < sym_times.
theorem divides_exp_to_divides:
\forall p,n,m:nat. prime p \to
-divides p (n \sup m) \to divides p n.
+p \divides n \sup m \to p \divides n.
intros 3.elim m.simplify in H1.
apply transitive_divides p (S O).assumption.
apply divides_SO_n.
-cut divides p n \lor divides p (n \sup n1).
+cut p \divides n \lor p \divides n \sup n1.
elim Hcut.assumption.
apply H.assumption.assumption.
apply divides_times_to_divides.assumption.
theorem divides_exp_to_eq:
\forall p,q,m:nat. prime p \to prime q \to
-divides p (q \sup m) \to p = q.
+p \divides q \sup m \to p = q.
intros.
simplify in H1.
elim H1.apply H4.
qed.
theorem not_divides_defactorize_aux: \forall f:nat_fact. \forall i,j:nat.
-i < j \to \not divides (nth_prime i) (defactorize_aux f j).
+i < j \to nth_prime i \ndivides defactorize_aux f j.
intro.elim f.
change with
-divides (nth_prime i) ((nth_prime j) \sup (S n)) \to False.
+nth_prime i \divides (nth_prime j) \sup (S n) \to False.
intro.absurd (nth_prime i) = (nth_prime j).
apply divides_exp_to_eq ? ? (S n).
apply prime_nth_prime.apply prime_nth_prime.
apply not_le_Sn_n i.rewrite > Hcut in \vdash (? ? %).assumption.
apply injective_nth_prime ? ? H2.
change with
-divides (nth_prime i) ((nth_prime j) \sup n *(defactorize_aux n1 (S j))) \to False.
+nth_prime i \divides (nth_prime j) \sup n *(defactorize_aux n1 (S j)) \to False.
intro.
-cut divides (nth_prime i) ((nth_prime j) \sup n)
-\lor divides (nth_prime i) (defactorize_aux n1 (S j)).
+cut nth_prime i \divides (nth_prime j) \sup n
+\lor nth_prime i \divides defactorize_aux n1 (S j).
elim Hcut.
absurd (nth_prime i) = (nth_prime j).
apply divides_exp_to_eq ? ? n.
absurd defactorize_aux (nf_last n) i =
defactorize_aux (nf_cons n1 n2) i.
rewrite > H2.reflexivity.
-absurd divides (nth_prime (S(max_p n2)+i)) (defactorize_aux (nf_cons n1 n2) i).
+absurd nth_prime (S(max_p n2)+i) \divides defactorize_aux (nf_cons n1 n2) i.
apply divides_max_p_defactorize.
rewrite < H2.
change with
-(divides (nth_prime (S(max_p n2)+i)) ((nth_prime i) \sup (S n))) \to False.
+(nth_prime (S(max_p n2)+i) \divides (nth_prime i) \sup (S n)) \to False.
intro.
absurd nth_prime (S (max_p n2) + i) = nth_prime i.
apply divides_exp_to_eq ? ? (S n).
absurd defactorize_aux (nf_last n2) i =
defactorize_aux (nf_cons n n1) i.
apply sym_eq. assumption.
-absurd divides (nth_prime (S(max_p n1)+i)) (defactorize_aux (nf_cons n n1) i).
+absurd nth_prime (S(max_p n1)+i) \divides defactorize_aux (nf_cons n n1) i.
apply divides_max_p_defactorize.
rewrite > H2.
change with
-(divides (nth_prime (S(max_p n1)+i)) ((nth_prime i) \sup (S n2))) \to False.
+(nth_prime (S(max_p n1)+i) \divides (nth_prime i) \sup (S n2)) \to False.
intro.
absurd nth_prime (S (max_p n1) + i) = nth_prime i.
apply divides_exp_to_eq ? ? (S n2).
[ O \Rightarrow n
| (S p) \Rightarrow gcd_aux (S p) n (S p) ]].
-theorem divides_mod: \forall p,m,n:nat. O < n \to divides p m \to divides p n \to
-divides p (mod m n).
+theorem divides_mod: \forall p,m,n:nat. O < n \to p \divides m \to p \divides n \to
+p \divides mod m n.
intros.elim H1.elim H2.
apply witness ? ? (n2 - n1*(div m n)).
rewrite > distr_times_minus.
qed.
theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
-divides p (mod m n) \to divides p n \to divides p m.
+p \divides mod m n \to p \divides n \to p \divides m.
intros.elim H1.elim H2.
apply witness p m ((n1*(div m n))+n2).
rewrite > distr_times_plus.
qed.
theorem divides_gcd_aux_mn: \forall p,m,n. O < n \to n \le m \to n \le p \to
-divides (gcd_aux p m n) m \land divides (gcd_aux p m n) n.
+gcd_aux p m n \divides m \land gcd_aux p m n \divides n.
intro.elim p.
absurd O < n.assumption.apply le_to_not_lt.assumption.
-cut (divides n1 m) \lor \not (divides n1 m).
+cut (n1 \divides m) \lor (n1 \ndivides m).
change with
-(divides
(match divides_b n1 m with
[ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (mod m n1)]) m) \land
-(divides
+| false \Rightarrow gcd_aux n n1 (mod m n1)]) \divides m \land
(match divides_b n1 m with
[ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (mod m n1)]) n1).
+| false \Rightarrow gcd_aux n n1 (mod m n1)]) \divides n1.
elim Hcut.rewrite > divides_to_divides_b_true.
simplify.
split.assumption.apply witness n1 n1 (S O).apply times_n_SO.
assumption.assumption.
rewrite > not_divides_to_divides_b_false.
change with
-(divides (gcd_aux n n1 (mod m n1)) m) \land
-(divides (gcd_aux n n1 (mod m n1)) n1).
-cut (divides (gcd_aux n n1 (mod m n1)) n1) \land
-(divides (gcd_aux n n1 (mod m n1)) (mod m n1)).
+gcd_aux n n1 (mod m n1) \divides m \land
+gcd_aux n n1 (mod m n1) \divides n1.
+cut gcd_aux n n1 (mod m n1) \divides n1 \land
+gcd_aux n n1 (mod m n1) \divides mod m n1.
elim Hcut1.
split.apply divides_mod_to_divides ? ? n1.
assumption.assumption.assumption.assumption.
qed.
theorem divides_gcd_nm: \forall n,m.
-divides (gcd n m) m \land divides (gcd n m) n.
+gcd n m \divides m \land gcd n m \divides n.
intros.
change with
-divides
-(match leb n m with
+match leb n m with
[ true \Rightarrow
match n with
[ O \Rightarrow m
| false \Rightarrow
match m with
[ O \Rightarrow n
- | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]) m
+ | (S p) \Rightarrow gcd_aux (S p) n (S p) ]] \divides m
\land
- divides
-(match leb n m with
+match leb n m with
[ true \Rightarrow
match n with
[ O \Rightarrow m
| false \Rightarrow
match m with
[ O \Rightarrow n
- | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]) n.
+ | (S p) \Rightarrow gcd_aux (S p) n (S p) ]] \divides n.
apply leb_elim n m.
apply nat_case1 n.
simplify.intros.split.
apply witness m m (S O).apply times_n_SO.
apply witness m O O.apply times_n_O.
intros.change with
-divides (gcd_aux (S m1) m (S m1)) m
+gcd_aux (S m1) m (S m1) \divides m
\land
-divides (gcd_aux (S m1) m (S m1)) (S m1).
+gcd_aux (S m1) m (S m1) \divides (S m1).
apply divides_gcd_aux_mn.
simplify.apply le_S_S.apply le_O_n.
assumption.apply le_n.
apply witness n O O.apply times_n_O.
apply witness n n (S O).apply times_n_SO.
intros.change with
-divides (gcd_aux (S m1) n (S m1)) (S m1)
+gcd_aux (S m1) n (S m1) \divides (S m1)
\land
-divides (gcd_aux (S m1) n (S m1)) n.
-cut divides (gcd_aux (S m1) n (S m1)) n
+gcd_aux (S m1) n (S m1) \divides n.
+cut gcd_aux (S m1) n (S m1) \divides n
\land
-divides (gcd_aux (S m1) n (S m1)) (S m1).
+gcd_aux (S m1) n (S m1) \divides S m1.
elim Hcut.split.assumption.assumption.
apply divides_gcd_aux_mn.
simplify.apply le_S_S.apply le_O_n.
apply le_n_Sn.assumption.apply le_n.
qed.
-theorem divides_gcd_n: \forall n,m.
-divides (gcd n m) n.
+theorem divides_gcd_n: \forall n,m. gcd n m \divides n.
intros.
exact proj2 ? ? (divides_gcd_nm n m).
qed.
-theorem divides_gcd_m: \forall n,m.
-divides (gcd n m) m.
+theorem divides_gcd_m: \forall n,m. gcd n m \divides m.
intros.
exact proj1 ? ? (divides_gcd_nm n m).
qed.
theorem divides_gcd_aux: \forall p,m,n,d. O < n \to n \le m \to n \le p \to
-divides d m \to divides d n \to divides d (gcd_aux p m n).
+d \divides m \to d \divides n \to d \divides gcd_aux p m n.
intro.elim p.
absurd O < n.assumption.apply le_to_not_lt.assumption.
change with
-divides d
+d \divides
(match divides_b n1 m with
[ true \Rightarrow n1
| false \Rightarrow gcd_aux n n1 (mod m n1)]).
-cut divides n1 m \lor \not (divides n1 m).
+cut n1 \divides m \lor n1 \ndivides m.
elim Hcut.
rewrite > divides_to_divides_b_true.
simplify.assumption.
assumption.assumption.
rewrite > not_divides_to_divides_b_false.
-change with divides d (gcd_aux n n1 (mod m n1)).
+change with d \divides gcd_aux n n1 (mod m n1).
apply H.
cut O \lt mod m n1 \lor O = mod m n1.
elim Hcut1.assumption.
-absurd divides n1 m.apply mod_O_to_divides.
+absurd n1 \divides m.apply mod_O_to_divides.
assumption.apply sym_eq.assumption.assumption.
apply le_to_or_lt_eq.apply le_O_n.
apply lt_to_le.
qed.
theorem divides_d_gcd: \forall m,n,d.
-divides d m \to divides d n \to divides d (gcd n m).
+d \divides m \to d \divides n \to d \divides gcd n m.
intros.
change with
-divides d (
+d \divides
match leb n m with
[ true \Rightarrow
match n with
| false \Rightarrow
match m with
[ O \Rightarrow n
- | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]).
+ | (S p) \Rightarrow gcd_aux (S p) n (S p) ]].
apply leb_elim n m.
apply nat_case1 n.simplify.intros.assumption.
intros.
-change with divides d (gcd_aux (S m1) m (S m1)).
+change with d \divides gcd_aux (S m1) m (S m1).
apply divides_gcd_aux.
simplify.apply le_S_S.apply le_O_n.assumption.apply le_n.assumption.
rewrite < H2.assumption.
apply nat_case1 m.simplify.intros.assumption.
intros.
-change with divides d (gcd_aux (S m1) n (S m1)).
+change with d \divides gcd_aux (S m1) n (S m1).
apply divides_gcd_aux.
simplify.apply le_S_S.apply le_O_n.
apply lt_to_le.apply not_le_to_lt.assumption.apply le_n.assumption.
elim p.
absurd O < n.assumption.apply le_to_not_lt.assumption.
cut O < m.
-cut (divides n1 m) \lor \not (divides n1 m).
+cut n1 \divides m \lor n1 \ndivides m.
change with
\exists a,b.
a*n1 - b*m = match divides_b n1 m with
apply H n1 (mod m n1).
cut O \lt mod m n1 \lor O = mod m n1.
elim Hcut2.assumption.
-absurd divides n1 m.apply mod_O_to_divides.
+absurd n1 \divides m.apply mod_O_to_divides.
assumption.
symmetry.assumption.assumption.
apply le_to_or_lt_eq.apply le_O_n.
theorem gcd_O_to_eq_O:\forall m,n:nat. (gcd m n) = O \to
m = O \land n = O.
-intros.cut divides O n \land divides O m.
+intros.cut O \divides n \land O \divides m.
elim Hcut.elim H2.split.
assumption.elim H1.assumption.
rewrite < H.
apply le_to_or_lt_eq.apply le_O_n.
qed.
-theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to \not (divides n m) \to
+theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to
gcd n m = (S O).
intros.simplify in H.change with gcd n m = (S O).
elim H.
apply le_to_or_lt_eq.apply le_O_n.
qed.
-theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to divides n (p*q) \to
-divides n p \lor divides n q.
+theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to n \divides p*q \to
+n \divides p \lor n \divides q.
intros.
-cut divides n p \lor \not (divides n p).
+cut n \divides p \lor n \ndivides p.
elim Hcut.
left.assumption.
right.
assumption.
qed.
(* questo va spostato in primes1.ma *)
-theorem plog_exp: \forall n,m,i. O < m \to \not (mod n m = O) \to
+theorem plog_exp: \forall n,m,i. O < m \to \lnot (mod n m = O) \to
\forall p. i \le p \to plog_aux p (m \sup i * n) m = pair nat nat i n.
intros 5.
elim i.
theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
intros.
-cut m+p \le n \or \not m+p \le n.
+cut m+p \le n \or \lnot m+p \le n.
elim Hcut.
symmetry.apply plus_to_minus.assumption.
rewrite > assoc_plus.rewrite > sym_plus p.rewrite < plus_minus_m_m.
qed. *)
theorem smallest_factor_fact: \forall n:nat.
-n < smallest_factor (S (n !)).
+n < smallest_factor (S n!).
intros.
apply not_le_to_lt.
-change with smallest_factor (S (n !)) \le n \to False.intro.
-apply not_divides_S_fact n (smallest_factor(S (n !))).
+change with smallest_factor (S n!) \le n \to False.intro.
+apply not_divides_S_fact n (smallest_factor(S n!)).
apply lt_SO_smallest_factor.
simplify.apply le_S_S.apply le_SO_fact.
assumption.
qed.
theorem ex_prime: \forall n. (S O) \le n \to \exists m.
-n < m \land m \le (S (n !)) \land (prime m).
+n < m \land m \le S 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 ((S n1) !))).
+apply ex_intro nat ? (smallest_factor (S (S n1)!)).
split.split.
apply smallest_factor_fact.
apply le_smallest_factor_n.
(* Andrea: ancora hint non lo trova *)
apply prime_smallest_factor_n.
-change with (S(S O)) \le S ((S n1) !).
+change with (S(S O)) \le S (S n1)!.
apply le_S.apply le_SSO_fact.
simplify.apply le_S_S.assumption.
qed.
[ O \Rightarrow (S(S O))
| (S p) \Rightarrow
let previous_prime \def (nth_prime p) in
- let upper_bound \def S (previous_prime !) in
+ let upper_bound \def S previous_prime! in
min_aux (upper_bound - (S previous_prime)) upper_bound primeb].
(* it works, but nth_prime 4 takes already a few minutes -
intro.
change with
let previous_prime \def (nth_prime m) in
-let upper_bound \def S (previous_prime !) in
+let upper_bound \def S 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 ((nth_prime m) !))).
+apply ex_intro nat ? (smallest_factor (S (nth_prime m)!)).
split.split.
-cut S ((nth_prime m) !)-(S ((nth_prime m) !) - (S (nth_prime m))) = (S (nth_prime m)).
+cut S (nth_prime m)!-(S (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_smallest_factor_n.
apply prime_to_primeb_true.
apply prime_smallest_factor_n.
-change with (S(S O)) \le S ((nth_prime m) !).
+change with (S(S O)) \le S (nth_prime m)!.
apply le_S_S.apply le_SO_fact.
qed.
intros.
change with
let previous_prime \def (nth_prime n) in
-let upper_bound \def S (previous_prime !) in
+let upper_bound \def S previous_prime! in
(S previous_prime) \le min_aux (upper_bound - (S previous_prime)) upper_bound primeb.
intros.
cut upper_bound - (upper_bound -(S previous_prime)) = (S previous_prime).
qed.
theorem lt_nth_prime_to_not_prime: \forall n,m. nth_prime n < m \to m < nth_prime (S n)
-\to \not (prime m).
+\to \lnot (prime m).
intros.
apply primeb_false_to_not_prime.
letin previous_prime \def nth_prime n.
-letin upper_bound \def S (previous_prime !).
+letin upper_bound \def S previous_prime!.
apply lt_min_aux_to_false primeb upper_bound (upper_bound - (S previous_prime)) m.
-cut S ((nth_prime n) !)-(S ((nth_prime n) !) - (S (nth_prime n))) = (S (nth_prime n)).
+cut S (nth_prime n)!-(S (nth_prime n)! - (S (nth_prime n))) = (S (nth_prime n)).
rewrite > Hcut.assumption.
apply plus_to_minus.
apply le_minus_m.
inductive divides (n,m:nat) : Prop \def
witness : \forall p:nat.m = times n p \to divides n m.
+interpretation "divides" 'divides n m = (cic:/matita/nat/primes/divides.ind#xpointer(1/1) n m).
+interpretation "not divides" 'ndivides n m =
+ (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/primes/divides.ind#xpointer(1/1) n m)).
+
theorem reflexive_divides : reflexive nat divides.
simplify.
intros.
qed.
theorem divides_to_div_mod_spec :
-\forall n,m. O < n \to divides n 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 (div m n) O.
intros.elim H1.rewrite > H2.
constructor 1.assumption.
apply lt_O_n_elim n H.intros.
qed.
theorem div_mod_spec_to_div :
-\forall n,m,p. div_mod_spec m n p O \to divides n m.
+\forall n,m,p. div_mod_spec m n p O \to n \divides m.
intros.elim H.
apply witness n m p.
rewrite < sym_times.
qed.
theorem divides_to_mod_O:
-\forall n,m. O < n \to divides n m \to (mod m n) = 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.
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 divides n m.
+\forall n,m. O< n \to (mod m n) = O \to n \divides m.
intros.
apply witness n m (div m n).
rewrite > plus_n_O (n*div m n).
assumption.
qed.
-theorem divides_n_O: \forall n:nat. divides n O.
+theorem divides_n_O: \forall n:nat. n \divides O.
intro. apply witness n O O.apply times_n_O.
qed.
-theorem divides_SO_n: \forall n:nat. divides (S O) n.
+theorem divides_SO_n: \forall n:nat. (S O) \divides n.
intro. apply witness (S O) n n. simplify.apply plus_n_O.
qed.
theorem divides_plus: \forall n,p,q:nat.
-divides n p \to divides n q \to divides n (p+q).
+n \divides p \to n \divides q \to n \divides p+q.
intros.
elim H.elim H1. apply witness n (p+q) (n2+n1).
rewrite > H2.rewrite > H3.apply sym_eq.apply distr_times_plus.
qed.
theorem divides_times: \forall n,m,p,q:nat.
-divides n p \to divides m q \to divides (n*m) (p*q).
+n \divides p \to m \divides q \to n*m \divides p*q.
intros.
elim H.elim H1. apply witness (n*m) (p*q) (n2*n1).
rewrite > H2.rewrite > H3.
qed.
theorem transitive_divides: \forall n,m,p.
-divides n m \to divides m p \to divides n p.
+n \divides m \to m \divides p \to n \divides p.
intros.
elim H.elim H1. apply witness n p (n2*n1).
rewrite > H3.rewrite > H2.
qed.
(* divides le *)
-theorem divides_to_le : \forall n,m. O < m \to divides n m \to n \le m.
+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.
apply lt_O_n_elim n2 Hcut.intro.rewrite < sym_times.
simplify.rewrite < sym_plus.
apply le_O_n.
qed.
-theorem divides_to_lt_O : \forall n,m. O < m \to divides n m \to O < n.
+theorem divides_to_lt_O : \forall n,m. O < m \to n \divides m \to O < n.
intros.elim H1.
elim le_to_or_lt_eq O n (le_O_n n).
assumption.
theorem divides_b_to_Prop :
\forall n,m:nat. O < n \to
match divides_b n m with
-[ true \Rightarrow divides n m
-| false \Rightarrow \lnot (divides n m)].
+[ true \Rightarrow n \divides m
+| false \Rightarrow n \ndivides m].
intros.
change with
match eqb (mod m n) O with
-[ true \Rightarrow divides n m
-| false \Rightarrow \lnot (divides n m)].
+[ true \Rightarrow n \divides m
+| false \Rightarrow n \ndivides m].
apply eqb_elim.
intro.simplify.apply mod_O_to_divides.assumption.assumption.
intro.simplify.intro.apply H1.apply divides_to_mod_O.assumption.assumption.
theorem divides_b_true_to_divides :
\forall n,m:nat. O < n \to
-(divides_b n m = true ) \to divides n m.
+(divides_b n m = true ) \to n \divides m.
intros.
change with
match true with
-[ true \Rightarrow divides n m
-| false \Rightarrow \lnot (divides n m)].
+[ true \Rightarrow n \divides m
+| false \Rightarrow n \ndivides m].
rewrite < H1.apply divides_b_to_Prop.
assumption.
qed.
theorem divides_b_false_to_not_divides :
\forall n,m:nat. O < n \to
-(divides_b n m = false ) \to \lnot (divides n m).
+(divides_b n m = false ) \to n \ndivides m.
intros.
change with
match false with
-[ true \Rightarrow divides n m
-| false \Rightarrow \lnot (divides n m)].
+[ true \Rightarrow n \divides m
+| false \Rightarrow n \ndivides m].
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).
+decidable (n \divides m).
+intros.change with (n \divides m) \lor n \ndivides 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).
+[ true \Rightarrow n \divides m
+| false \Rightarrow n \ndivides m] \to n \divides m \lor n \ndivides 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.
+n \divides 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).
+[ true \Rightarrow n \divides m
+| false \Rightarrow n \ndivides 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.
+absurd (n \divides 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.
+\lnot(n \divides 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).
+[ true \Rightarrow n \divides m
+| false \Rightarrow n \ndivides 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.
+absurd (n \divides m).assumption.assumption.
reflexivity.
qed.
(* divides and pi *)
theorem divides_f_pi_f : \forall f:nat \to nat.\forall n,i:nat.
-i < n \to divides (f i) (pi n f).
+i < n \to f i \divides pi n f.
intros 3.elim n.apply False_ind.apply not_le_Sn_O i H.
simplify.
apply le_n_Sm_elim (S i) n1 H1.
(* divides and fact *)
theorem divides_fact : \forall n,i:nat.
-O < i \to i \le n \to divides i (n !).
+O < i \to i \le n \to i \divides n!.
intros 3.elim n.absurd O<i.assumption.apply le_n_O_elim i H1.
apply not_le_Sn_O O.
-change with divides i ((S n1)*(n1 !)).
+change with i \divides (S n1)*n1!.
apply le_n_Sm_elim i n1 H2.
intro.
-apply transitive_divides ? (n1 !).
+apply transitive_divides ? n1!.
apply H1.apply le_S_S_to_le. assumption.
apply witness ? ? (S n1).apply sym_times.
intro.
rewrite > H3.
-apply witness ? ? (n1 !).reflexivity.
+apply witness ? ? n1!.reflexivity.
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 mod (S n!) i = (S O).
+intros.cut mod n! i = O.
rewrite < Hcut.
apply mod_S.apply trans_lt O (S O).apply le_n (S O).assumption.
rewrite > Hcut.assumption.
qed.
theorem not_divides_S_fact: \forall n,i:nat.
-(S O) < i \to i \le n \to \not (divides i (S (n !))).
+(S O) < i \to i \le n \to i \ndivides S n!.
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 (mod (S n!) i) O) = false.
rewrite > mod_S_fact.simplify.reflexivity.
assumption.assumption.
qed.
(* prime *)
definition prime : nat \to Prop \def
\lambda n:nat. (S O) < n \land
-(\forall m:nat. divides m n \to (S O) < m \to m = n).
+(\forall m:nat. m \divides n \to (S O) < m \to m = n).
theorem not_prime_O: \lnot (prime O).
simplify.intro.elim H.apply not_le_Sn_O (S O) H1.
qed.
theorem divides_smallest_factor_n :
-\forall n:nat. O < n \to divides (smallest_factor n) n.
+\forall n:nat. O < n \to smallest_factor n \divides n.
intro.
apply nat_case n.intro.apply False_ind.apply not_le_Sn_O O H.
intro.apply nat_case m.intro. simplify.
qed.
theorem lt_smallest_factor_to_not_divides: \forall n,i:nat.
-(S O) < n \to (S O) < i \to i < (smallest_factor n) \to \lnot (divides i n).
+(S O) < n \to (S O) < i \to i < (smallest_factor n) \to i \ndivides n.
intros 2.
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.
theorem prime_smallest_factor_n :
\forall n:nat. (S O) < n \to prime (smallest_factor n).
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)).
+(\forall m:nat. m \divides smallest_factor n \to (S O) < m \to m = (smallest_factor n)).
intro.split.
apply lt_SO_smallest_factor.assumption.
intros.
cut le m (smallest_factor n).
elim le_to_or_lt_eq m (smallest_factor n) Hcut.
-absurd divides m n.
+absurd m \divides n.
apply transitive_divides m (smallest_factor n).
assumption.
apply divides_smallest_factor_n.
intro.
change with
(S O) < (S(S m1)) \land
-(\forall m:nat. divides m (S(S m1)) \to (S O) < m \to m = (S(S m1))) \to
+(\forall m:nat. m \divides S(S m1) \to (S O) < m \to m = (S(S m1))) \to
smallest_factor (S(S m1)) = (S(S m1)).
intro.elim H.apply H2.
apply divides_smallest_factor_n.
theorem primeb_to_Prop: \forall n.
match primeb n with
[ true \Rightarrow prime n
-| false \Rightarrow \not (prime n)].
+| false \Rightarrow \lnot (prime n)].
intro.
apply nat_case n.simplify.intro.elim H.apply not_le_Sn_O (S O) H1.
intro.apply nat_case m.simplify.intro.elim H.apply not_le_Sn_n (S O) H1.
change with
match eqb (smallest_factor (S(S m1))) (S(S m1)) with
[ true \Rightarrow prime (S(S m1))
-| false \Rightarrow \not (prime (S(S m1)))].
+| false \Rightarrow \lnot (prime (S(S m1)))].
apply eqb_elim (smallest_factor (S(S m1))) (S(S m1)).
intro.change with prime (S(S m1)).
rewrite < H.
apply prime_smallest_factor_n.
simplify.apply le_S_S.apply le_S_S.apply le_O_n.
-intro.change with \not (prime (S(S m1))).
+intro.change with \lnot (prime (S(S m1))).
change with prime (S(S m1)) \to False.
intro.apply H.
apply prime_to_smallest_factor.
intros.change with
match true with
[ true \Rightarrow prime n
-| false \Rightarrow \not (prime n)].
+| false \Rightarrow \lnot (prime n)].
rewrite < H.
apply primeb_to_Prop.
qed.
theorem primeb_false_to_not_prime : \forall n:nat.
-primeb n = false \to \not (prime n).
+primeb n = false \to \lnot (prime n).
intros.change with
match false with
[ true \Rightarrow prime n
-| false \Rightarrow \not (prime n)].
+| false \Rightarrow \lnot (prime n)].
rewrite < H.
apply primeb_to_Prop.
qed.
theorem decidable_prime : \forall n:nat.decidable (prime n).
-intro.change with (prime n) \lor \not (prime n).
+intro.change with (prime n) \lor \lnot (prime n).
cut
match primeb n with
[ true \Rightarrow prime n
-| false \Rightarrow \not (prime n)] \to (prime n) \lor \not (prime n).
+| false \Rightarrow \lnot (prime n)] \to (prime n) \lor \lnot (prime n).
apply Hcut.apply primeb_to_Prop.
elim (primeb n).left.apply H.right.apply H.
qed.
intros.
cut match (primeb n) with
[ true \Rightarrow prime n
-| false \Rightarrow \not (prime n)] \to ((primeb n) = true).
+| false \Rightarrow \lnot (prime n)] \to ((primeb n) = true).
apply Hcut.apply primeb_to_Prop.
elim primeb n.reflexivity.
absurd (prime n).assumption.assumption.
qed.
theorem not_prime_to_primeb_false: \forall n:nat.
-\not(prime n) \to primeb n = false.
+\lnot(prime n) \to primeb n = false.
intros.
cut match (primeb n) with
[ true \Rightarrow prime n
-| false \Rightarrow \not (prime n)] \to ((primeb n) = false).
+| false \Rightarrow \lnot (prime n)] \to ((primeb n) = false).
apply Hcut.apply primeb_to_Prop.
elim primeb n.
absurd (prime n).assumption.assumption.
projects / helm.git / commitdiff