--- /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/div_and_mod".
+
+include "nat/minus.ma".
+include "nat/orders_op.ma".
+include "nat/compare.ma".
+
+let rec mod_aux p m n: nat \def
+match (leb m n) with
+[ true \Rightarrow m
+| false \Rightarrow
+ match p with
+ [O \Rightarrow m
+ |(S q) \Rightarrow mod_aux q (minus m (S n)) n]].
+
+definition mod : nat \to nat \to nat \def
+\lambda n,m.
+match m with
+[O \Rightarrow m
+| (S p) \Rightarrow mod_aux n n p].
+
+let rec div_aux p m n : nat \def
+match (leb m n) with
+[ true \Rightarrow O
+| false \Rightarrow
+ match p with
+ [O \Rightarrow O
+ |(S q) \Rightarrow S (div_aux q (minus m (S n)) n)]].
+
+definition div : nat \to nat \to nat \def
+\lambda n,m.
+match m with
+[O \Rightarrow S n
+| (S p) \Rightarrow div_aux n n p].
+
+theorem le_mod_aux_m_m:
+\forall p,n,m. (le n p) \to (le (mod_aux p n m) m).
+intro.elim p.
+apply le_n_O_elim n H (\lambda n.(le (mod_aux O n m) m)).
+simplify.apply le_O_n.
+simplify.
+apply leb_elim n1 m.
+simplify.intro.assumption.
+simplify.intro.apply H.
+cut (le n1 (S n)) \to (le (minus n1 (S m)) n).
+apply Hcut.assumption.
+elim n1.
+simplify.apply le_O_n.
+simplify.apply trans_le ? n2 n.
+apply le_minus_m.apply le_S_S_to_le.assumption.
+qed.
+
+theorem lt_mod_m_m: \forall n,m. (lt O m) \to (lt (mod n m) m).
+intros 2.elim m.apply False_ind.
+apply not_le_Sn_O O H.
+simplify.apply le_S_S.apply le_mod_aux_m_m.
+apply le_n.
+qed.
+
+theorem div_aux_mod_aux: \forall p,n,m:nat.
+(eq nat n (plus (times (div_aux p n m) (S m)) (mod_aux p n m) )).
+intro.elim p.
+simplify.elim leb n m.
+simplify.apply refl_eq.
+simplify.apply refl_eq.
+simplify.
+apply leb_elim n1 m.
+simplify.intro.apply refl_eq.
+simplify.intro.
+rewrite > assoc_plus.
+elim (H (minus n1 (S m)) m).
+change with (eq nat n1 (plus (S m) (minus n1 (S m)))).
+rewrite < sym_plus.
+apply plus_minus_m_m.
+change with lt m n1.
+apply not_le_to_lt.exact H1.
+qed.
+
+theorem div_mod: \forall n,m:nat.
+(lt O m) \to (eq nat n (plus (times (div n m) m) (mod n m))).
+intros 2.elim m.elim (not_le_Sn_O O H).
+simplify.
+apply div_aux_mod_aux.
+qed.
+
+inductive div_mod_spec (n,m,q,r:nat) : Prop \def
+div_mod_spec_intro:
+(lt r m) \to (eq nat n (plus (times q m) r)) \to (div_mod_spec n m q r).
+
+(*
+definition div_mod_spec : nat \to nat \to nat \to nat \to Prop \def
+\lambda n,m,q,r:nat.(And (lt r m) (eq nat n (plus (times q m) r))).
+*)
+
+theorem div_mod_spec_to_not_eq_O: \forall n,m,q,r.(div_mod_spec n m q r) \to Not (eq nat m O).
+intros 4.simplify.intros.elim H.absurd le (S r) O.
+rewrite < H1.assumption.
+exact not_le_Sn_O r.
+qed.
+
+theorem div_mod_spec_div_mod:
+\forall n,m. (lt O m) \to (div_mod_spec n m (div n m) (mod n m)).
+intros.
+apply div_mod_spec_intro.
+apply lt_mod_m_m.assumption.
+apply div_mod.assumption.
+qed.
+
+theorem div_mod_spec_to_eq :\forall a,b,q,r,q1,r1.
+(div_mod_spec a b q r) \to (div_mod_spec a b q1 r1) \to
+(eq nat q q1).
+intros.elim H.elim H1.
+apply nat_compare_elim q q1.intro.
+apply False_ind.
+cut eq nat (plus (times (minus q1 q) b) r1) r.
+cut le b (plus (times (minus q1 q) b) r1).
+cut le b r.
+apply lt_to_not_le r b H2 Hcut2.
+elim Hcut.assumption.
+apply trans_le ? (times (minus q1 q) b) ?.
+apply le_times_n.
+apply le_SO_minus.exact H6.
+rewrite < sym_plus.
+apply le_plus_n.
+rewrite < sym_times.
+rewrite > distr_times_minus.
+(* ATTENZIONE ALL' ORDINAMENTO DEI GOALS *)
+rewrite > plus_minus ? ? ? ?.
+rewrite > sym_times.
+rewrite < H5.
+rewrite < sym_times.
+apply plus_to_minus.
+apply eq_plus_to_le ? ? ? H3.
+apply H3.
+apply le_times_r.
+apply lt_to_le.
+apply H6.
+(* eq case *)
+intros.assumption.
+(* the following case is symmetric *)
+intro.
+apply False_ind.
+cut eq nat (plus (times (minus q q1) b) r) r1.
+cut le b (plus (times (minus q q1) b) r).
+cut le b r1.
+apply lt_to_not_le r1 b H4 Hcut2.
+elim Hcut.assumption.
+apply trans_le ? (times (minus q q1) b) ?.
+apply le_times_n.
+apply le_SO_minus.exact H6.
+rewrite < sym_plus.
+apply le_plus_n.
+rewrite < sym_times.
+rewrite > distr_times_minus.
+rewrite > plus_minus ? ? ? ?.
+rewrite > sym_times.
+rewrite < H3.
+rewrite < sym_times.
+apply plus_to_minus.
+apply eq_plus_to_le ? ? ? H5.
+apply H5.
+apply le_times_r.
+apply lt_to_le.
+apply H6.
+qed.
\ No newline at end of file
projects / helm.git / blobdiff