--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
+(* ||A|| E.Tassi, S.Zacchiroli *)
+(* \ / *)
+(* \ / Matita is distributed under the terms of the *)
+(* v GNU Lesser General Public License Version 2.1 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/nat/gcd".
+
+include "nat/primes.ma".
+include "higher_order_defs/functions.ma".
+
+let rec gcd_aux p m n: nat \def
+match divides_b n m with
+[ true \Rightarrow n
+| false \Rightarrow
+ match p with
+ [O \Rightarrow n
+ |(S q) \Rightarrow gcd_aux q n (mod m n)]].
+
+definition gcd : nat \to nat \to nat \def
+\lambda n,m:nat.
+ match leb n m with
+ [ true \Rightarrow
+ match n with
+ [ O \Rightarrow m
+ | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
+ | false \Rightarrow
+ match m with
+ [ 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).
+intros.elim H1.elim H2.
+apply witness ? ? (n2 - n1*(div m n)).
+rewrite > distr_times_minus.
+rewrite < H3.
+rewrite < assoc_times.
+rewrite < H4.
+apply sym_eq.
+apply plus_to_minus.
+rewrite > div_mod m n in \vdash (? ? %).
+rewrite > sym_times.
+apply eq_plus_to_le ? ? (mod m n).
+reflexivity.
+rewrite > sym_times.
+apply div_mod.assumption. assumption.
+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.
+intros.elim H1.elim H2.
+apply witness p m ((n1*(div m n))+n2).
+rewrite > distr_times_plus.
+rewrite < H3.
+rewrite < assoc_times.
+rewrite < H4.rewrite < sym_times.
+apply div_mod.assumption.
+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.
+intro.elim p.
+absurd O < n.assumption.apply le_to_not_lt.assumption.
+cut (divides n1 m) \lor \not (divides n1 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
+(match divides_b n1 m with
+[ true \Rightarrow n1
+| false \Rightarrow gcd_aux n n1 (mod m n1)]) n1).
+elim Hcut.rewrite > divides_to_divides_b_true.
+simplify.
+split.assumption.apply witness n1 n1 (S O).apply times_n_SO.
+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)).
+elim Hcut1.
+split.apply divides_mod_to_divides ? ? n1.
+assumption.assumption.assumption.assumption.
+apply H.
+cut O \lt mod m n1 \lor O = mod m n1.
+elim Hcut1.assumption.
+apply False_ind.apply H4.apply mod_O_to_divides.
+assumption.apply sym_eq.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 mod m n1 < n1.
+apply lt_mod_m_m.assumption.assumption.
+apply decidable_divides n1 m.assumption.
+apply lt_to_le_to_lt ? n1.assumption.reflexivity.
+assumption.
+assumption.assumption.
+qed.
+
+theorem divides_gcd_nm: \forall n,m.
+divides (gcd n m) m \land divides (gcd n m) n.
+intros.
+change with
+divides
+(match leb n m with
+ [ true \Rightarrow
+ match n with
+ [ O \Rightarrow m
+ | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
+ | false \Rightarrow
+ match m with
+ [ O \Rightarrow n
+ | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]) m
+\land
+ divides
+(match leb n m with
+ [ true \Rightarrow
+ match n with
+ [ O \Rightarrow m
+ | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
+ | false \Rightarrow
+ match m with
+ [ O \Rightarrow n
+ | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]) 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
+\land
+divides (gcd_aux (S m1) m (S m1)) (S m1).
+apply divides_gcd_aux_mn.
+simplify.apply le_S_S.apply le_O_n.
+assumption.apply le_n.
+simplify.intro.
+apply nat_case1 m.
+simplify.intros.split.
+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)
+\land
+divides (gcd_aux (S m1) n (S m1)) n.
+cut divides (gcd_aux (S m1) n (S m1)) n
+\land
+divides (gcd_aux (S m1) n (S m1)) (S m1).
+elim Hcut.split.assumption.assumption.
+apply divides_gcd_aux_mn.
+simplify.apply le_S_S.apply le_O_n.
+apply not_lt_to_le.simplify.intro.apply H.
+rewrite > H1.apply trans_le ? (S n).
+apply le_n_Sn.assumption.apply le_n.
+qed.
+
+theorem divides_gcd_n: \forall n,m.
+divides (gcd n m) n.
+intros.
+exact proj2 ? ? (divides_gcd_nm n m).
+qed.
+
+theorem divides_gcd_m: \forall n,m.
+divides (gcd n m) 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).
+intro.elim p.
+absurd O < n.assumption.apply le_to_not_lt.assumption.
+change with
+divides d
+(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).
+elim Hcut.
+rewrite > divides_to_divides_b_true.
+simplify.assumption.
+rewrite > not_divides_to_divides_b_false.
+change with divides d (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.
+assumption.apply sym_eq.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 mod m n1 < n1.
+apply lt_mod_m_m.assumption.assumption.
+assumption.
+apply divides_mod.assumption.assumption.assumption.
+apply decidable_divides n1 m.assumption.
+apply lt_to_le_to_lt ? n1.assumption.reflexivity.
+assumption.assumption.assumption.
+qed.
+
+theorem divides_d_gcd: \forall m,n,d.
+divides d m \to divides d n \to divides d (gcd n m).
+intros.
+change with
+divides d (
+match leb n m with
+ [ true \Rightarrow
+ match n with
+ [ O \Rightarrow m
+ | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
+ | false \Rightarrow
+ match m with
+ [ O \Rightarrow n
+ | (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)).
+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)).
+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.
+rewrite < H2.assumption.
+qed.
+
+theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to
+ex nat (\lambda a. ex nat (\lambda 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 (divides n1 m) \lor \not (divides n1 m).
+change with
+ex nat (\lambda a. ex nat (\lambda b.
+a*n1 - b*m = match divides_b n1 m with
+[ true \Rightarrow n1
+| false \Rightarrow gcd_aux n n1 (mod m n1)]
+\lor
+b*m - a*n1 = match divides_b n1 m with
+[ true \Rightarrow n1
+| false \Rightarrow gcd_aux n n1 (mod m n1)])).
+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.
+rewrite > not_divides_to_divides_b_false.
+change with
+ex nat (\lambda a. ex nat (\lambda b.
+a*n1 - b*m = gcd_aux n n1 (mod m n1)
+\lor
+b*m - a*n1 = gcd_aux n n1 (mod m n1))).
+cut
+ex nat (\lambda a. ex nat (\lambda b.
+a*(mod m n1) - b*n1= gcd_aux n n1 (mod m n1)
+\lor
+b*n1 - a*(mod m n1) = gcd_aux n n1 (mod m n1))).
+elim Hcut2.elim H5.elim H6.
+(* first case *)
+rewrite < H7.
+apply ex_intro ? ? (a1+a*(div 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.
+(* second case *)
+rewrite < H7.
+apply ex_intro ? ? (a1+a*(div m n1)).
+apply ex_intro ? ? a.
+left.
+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.
+(* end second case *)
+apply H n1 (mod m n1).
+(* a lot of trivialities left *)
+cut O \lt mod m n1 \lor O = mod m n1.
+elim Hcut2.assumption.
+absurd divides n1 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.
+apply lt_mod_m_m.assumption.
+apply le_S_S_to_le.
+apply trans_le ? n1.
+change with mod m n1 < n1.
+apply lt_mod_m_m.assumption.assumption.
+apply decidable_divides n1 m.assumption.
+apply lt_to_le_to_lt ? n1.assumption.assumption.
+assumption.assumption.assumption.assumption.assumption.
+apply le_n.assumption.
+apply le_n.
+qed.
+
+theorem eq_minus_gcd: \forall m,n.
+ex nat (\lambda a. ex nat (\lambda b.
+a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m))).
+intros.
+change with
+ex nat (\lambda a. ex nat (\lambda b.
+a*n - b*m =
+match leb n m with
+ [ true \Rightarrow
+ match n with
+ [ O \Rightarrow m
+ | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
+ | false \Rightarrow
+ match m with
+ [ O \Rightarrow n
+ | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]
+\lor b*m - a*n =
+match leb n m with
+ [ true \Rightarrow
+ match n with
+ [ O \Rightarrow m
+ | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
+ | false \Rightarrow
+ match m with
+ [ O \Rightarrow n
+ | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]
+)).
+apply leb_elim n m.
+apply nat_case1 n.
+simplify.intros.
+apply ex_intro ? ? O.
+apply ex_intro ? ? (S O).
+right.simplify.
+rewrite < plus_n_O.
+apply sym_eq.apply minus_n_O.
+intros.
+change with
+ex nat (\lambda a. ex nat (\lambda b.
+a*(S m1) - b*m = (gcd_aux (S m1) m (S m1))
+\lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1)))).
+apply eq_minus_gcd_aux.
+simplify. apply le_S_S.apply le_O_n.
+assumption.apply le_n.
+apply nat_case1 m.
+simplify.intros.
+apply ex_intro ? ? (S O).
+apply ex_intro ? ? O.
+left.simplify.
+rewrite < plus_n_O.
+apply sym_eq.apply minus_n_O.
+intros.
+change with
+ex nat (\lambda a. ex nat (\lambda b.
+a*n - b*(S m1) = (gcd_aux (S m1) n (S m1))
+\lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1)))).
+cut
+ex nat (\lambda a. ex nat (\lambda b.
+a*(S m1) - b*n = (gcd_aux (S m1) n (S m1))
+\lor
+b*n - a*(S m1) = (gcd_aux (S m1) n (S m1)))).
+elim Hcut.elim H2.elim H3.
+apply ex_intro ? ? a1.
+apply ex_intro ? ? a.
+right.assumption.
+apply ex_intro ? ? a1.
+apply ex_intro ? ? a.
+left.assumption.
+apply eq_minus_gcd_aux.
+simplify. apply le_S_S.apply le_O_n.
+apply lt_to_le.apply not_le_to_lt.assumption.
+apply le_n.
+qed.
+
+(* some properties of gcd *)
+
+theorem gcd_O_n: \forall n:nat. gcd O n = n.
+intro.simplify.reflexivity.
+qed.
+
+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.
+elim Hcut.elim H2.split.
+assumption.elim H1.assumption.
+rewrite < H.
+apply divides_gcd_nm.
+qed.
+
+theorem symmetric_gcd: symmetric nat gcd.
+change with
+\forall n,m:nat. gcd n m = gcd m n.
+intros.
+cut O < (gcd n m) \lor O = (gcd n m).
+elim Hcut.
+cut O < (gcd m n) \lor O = (gcd m n).
+elim Hcut1.
+apply antisym_le.
+apply divides_to_le.assumption.
+apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
+apply divides_to_le.assumption.
+apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
+rewrite < H1.
+cut m=O \land n=O.
+elim Hcut2.rewrite > H2.rewrite > H3.reflexivity.
+apply gcd_O_to_eq_O.apply sym_eq.assumption.
+apply le_to_or_lt_eq.apply le_O_n.
+rewrite < H.
+cut n=O \land m=O.
+elim Hcut1.rewrite > H1.rewrite > H2.reflexivity.
+apply gcd_O_to_eq_O.apply sym_eq.assumption.
+apply le_to_or_lt_eq.apply le_O_n.
+qed.
+
+variant sym_gcd: \forall n,m:nat. gcd n m = gcd m n \def
+symmetric_gcd.
+
+theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
+intro.
+apply antisym_le.apply divides_to_le.simplify.apply le_n.
+apply divides_gcd_n.
+cut O < gcd (S O) n \lor O = gcd (S O) n.
+elim Hcut.assumption.
+apply False_ind.
+apply not_eq_O_S O.
+cut (S O)=O \land n=O.
+elim Hcut1.apply sym_eq.assumption.
+apply gcd_O_to_eq_O.apply sym_eq.assumption.
+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
+gcd n m = (S O).
+intros.simplify in H.change with gcd n m = (S O).
+elim H.
+apply antisym_le.
+apply not_lt_to_le.
+change with (S (S O)) \le gcd n m \to False.intro.
+apply H1.rewrite < H3 (gcd n m).
+apply divides_gcd_m.
+cut O < gcd n m \lor O = gcd n m.
+elim Hcut.assumption.
+apply False_ind.
+apply not_le_Sn_O (S O).
+cut n=O \land m=O.
+elim Hcut1.rewrite < H5 in \vdash (? ? %).assumption.
+apply gcd_O_to_eq_O.apply sym_eq.assumption.
+apply le_to_or_lt_eq.apply le_O_n.
+apply divides_gcd_n.assumption.
+qed.
+
+(* esempio di sfarfallalmento !!! *)
+(*
+theorem bad: \forall n,p,q:nat.prime n \to divides n (p*q) \to
+divides n p \lor divides n q.
+intros.
+cut divides n p \lor \not (divides n p).
+elim Hcut.left.assumption.
+right.
+cut ex nat (\lambda a. ex nat (\lambda b.
+a*n - b*p = (S O) \lor b*p - a*n = (S O))).
+elim Hcut1.elim H3.*)
+
+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.
+intros.
+cut divides n p \lor \not (divides n p).
+elim Hcut.
+left.assumption.
+right.
+cut ex nat (\lambda a. ex nat (\lambda b.
+a*n - b*p = (S O) \lor b*p - a*n = (S O))).
+elim Hcut1.elim H3.elim H4.
+(* first case *)
+rewrite > times_n_SO q.rewrite < H5.
+rewrite > distr_times_minus.
+rewrite > sym_times q (a1*p).
+rewrite > assoc_times a1.
+elim H1.rewrite > H6.
+rewrite < sym_times n.rewrite < assoc_times.
+rewrite > sym_times q.rewrite > assoc_times.
+rewrite < assoc_times a1.rewrite < sym_times n.
+rewrite > assoc_times n.
+rewrite < distr_times_minus.
+apply witness ? ? (q*a-a1*n2).reflexivity.
+(* second case *)
+rewrite > times_n_SO q.rewrite < H5.
+rewrite > distr_times_minus.
+rewrite > sym_times q (a1*p).
+rewrite > assoc_times a1.
+elim H1.rewrite > H6.
+rewrite < sym_times.rewrite > assoc_times.
+rewrite < assoc_times q.
+rewrite < sym_times n.
+rewrite < distr_times_minus.
+apply witness ? ? (n2*a1-q*a).reflexivity.
+(* end second case *)
+rewrite < prime_to_gcd_SO n p.
+apply eq_minus_gcd.
+apply decidable_divides n p.
+apply trans_lt ? (S O).simplify.apply le_n.
+simplify in H.elim H. assumption.
+assumption.assumption.
+qed.
projects / helm.git / blobdiff