From e0671ce496760cec78ec904747af76ed55fd03a2 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Wed, 10 Apr 2013 11:32:54 +0000 Subject: [PATCH] commit by user andrea --- weblib/While/semantics.ma | 49 +++- weblib/While/syntax.ma | 2 +- weblib/arithmetics/div_and_mod.ma | 420 ++++++++++++------------------ 3 files changed, 215 insertions(+), 256 deletions(-) diff --git a/weblib/While/semantics.ma b/weblib/While/semantics.ma index 943298444..ec11cf2ec 100644 --- a/weblib/While/semantics.ma +++ b/weblib/While/semantics.ma @@ -1,8 +1,53 @@ (* new script *) -include "While/syntax.ma". +include "While/syntax.ma". +include "arithmetics/div_and_mod.ma. (* state *) -definition state ≝ \ \ No newline at end of file +definition state ≝ a href="cic:/matita/While/syntax/Var.ind(1,0,0)"Var/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. + +(* Semantics of Arithmetic expressions *) + +pre class="smallmargin" style="display: inline;"let rec eval_Aexp a s ≝ + match a with + | Const n => n + | Aid v => s v + | Add a b => a+b + | Sub a b => a-b + | Mul a b => a*b + | Div a b => div a b + | Mod a b => mod a b + . + +interpretation "Aexp plus" 'plus x y = (Add x y). +interpretation "Aexp minus" 'plus x y = (Sub x y). +interpretation "Aexp times" 'times x y = (Mul x y). + +(* Boolean expressions *) +inductive Bexp : Type[0] ≝ + | BFalse : Bexp + | BTtrue : Bexp + | BNot : Bexp → Bexp + | BAnd : Bexp → Bexp → Bexp + | BOr : Bexp → Bexp → Bexp + | Eq : a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"Aexp/a → a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"Aexp/a → Bexp + | LE : a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"Aexp/a → a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"Aexp/a → Bexp +. + +interpretation "Bexp not" 'not x = (BNot x). +interpretation "Bexp and" 'and x y = (BAnd x y). +interpretation "Bexp or" 'or x y = (BOr x y). +interpretation "Bexp 'less or equal to'" 'leq x y = (LE x y). + +(* Commands *) +inductive Cmd : Type[0] ≝ + | Skip : Cmd + | Assign : Var → a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"Aexp/a → Cmd + | Seq : Cmd → Cmd → Cmd + | If : a href="cic:/matita/While/syntax/Bexp.ind(1,0,0)"Bexp/a → Cmd → Cmd → Cmd + | While : a href="cic:/matita/While/syntax/Bexp.ind(1,0,0)"Bexp/a → Cmd → Cmd +. + +/pre \ No newline at end of file diff --git a/weblib/While/syntax.ma b/weblib/While/syntax.ma index b55d89d43..95c93c7e4 100644 --- a/weblib/While/syntax.ma +++ b/weblib/While/syntax.ma @@ -7,7 +7,7 @@ include "arithmetics/nat.ma". (* Variables *) -inductive Var : Type[0] ≝ + inductive Var : Type[0] ≝ Id : nat → Var. (* Arithmetic expressions *) diff --git a/weblib/arithmetics/div_and_mod.ma b/weblib/arithmetics/div_and_mod.ma index 4044695d2..d7c5b4e06 100644 --- a/weblib/arithmetics/div_and_mod.ma +++ b/weblib/arithmetics/div_and_mod.ma @@ -11,158 +11,151 @@ include "arithmetics/nat.ma". -let rec mod_aux p m n: nat ≝ +img class="anchor" src="icons/tick.png" id="mod_aux"let rec mod_aux p m n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a ≝ match p with [ O ⇒ m - | S q ⇒ match (leb m n) with + | S q ⇒ match (a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a m n) with [ true ⇒ m - | false ⇒ mod_aux q (m-(S n)) n]]. + | false ⇒ mod_aux q (ma title="natural minus" href="cic:/fakeuri.def(1)"-/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n)) n]]. -definition mod : nat → nat → nat ≝ +img class="anchor" src="icons/tick.png" id="mod"definition mod : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a ≝ λn,m. match m with [ O ⇒ n - | S p ⇒ mod_aux n n p]. + | S p ⇒ a href="cic:/matita/arithmetics/div_and_mod/mod_aux.fix(0,0,2)"mod_aux/a n n p]. interpretation "natural remainder" 'module x y = (mod x y). -let rec div_aux p m n : nat ≝ +img class="anchor" src="icons/tick.png" id="div_aux"let rec div_aux p m n : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a ≝ match p with - [ O ⇒ O - | S q ⇒ match (leb m n) with - [ true ⇒ O - | false ⇒ S (div_aux q (m-(S n)) n)]]. + [ O ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a + | S q ⇒ match (a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a m n) with + [ true ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a + | false ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (div_aux q (ma title="natural minus" href="cic:/fakeuri.def(1)"-/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n)) n)]]. -definition div : nat → nat → nat ≝ +img class="anchor" src="icons/tick.png" id="div"definition div : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a ≝ λn,m.match m with - [ O ⇒ S n - | S p ⇒ div_aux n n p]. + [ O ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n + | S p ⇒ a href="cic:/matita/arithmetics/div_and_mod/div_aux.fix(0,0,2)"div_aux/a n n p]. interpretation "natural divide" 'divide x y = (div x y). -theorem le_mod_aux_m_m: -∀p,n,m. n ≤ p → mod_aux p n m ≤ m. +img class="anchor" src="icons/tick.png" id="le_mod_aux_m_m"theorem le_mod_aux_m_m: +∀p,n,m. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a p → a href="cic:/matita/arithmetics/div_and_mod/mod_aux.fix(0,0,2)"mod_aux/a p n m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m. #p (elim p) -[ normalize #n #m #lenO @(le_n_O_elim …lenO) // +[ normalize #n #m #lenO @(a href="cic:/matita/arithmetics/nat/le_n_O_elim.def(4)"le_n_O_elim/a …lenO) // | #q #Hind #n #m #len normalize - @(leb_elim n m) normalize // - #notlenm @Hind @le_plus_to_minus - @(transitive_le … len) /2/ + @(a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"leb_elim/a n m) normalize // + #notlenm @Hind @a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(10)"le_plus_to_minus/a + @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a … len) /span class="autotactic"2span class="autotrace" trace /span/span/ qed. -theorem lt_mod_m_m: ∀n,m. O < m → n \mod m < m. +img class="anchor" src="icons/tick.png" id="lt_mod_m_m"theorem lt_mod_m_m: ∀n,m. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m. #n #m (cases m) - [#abs @False_ind /2/ - |#p #_ normalize @le_S_S /2/ + [#abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ + |#p #_ normalize @a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a, a href="cic:/matita/arithmetics/div_and_mod/le_mod_aux_m_m.def(11)"le_mod_aux_m_m/a/span/span/ ] qed. -theorem div_aux_mod_aux: ∀p,n,m:nat. -n=(div_aux p n m)*(S m) + (mod_aux p n m). +img class="anchor" src="icons/tick.png" id="div_aux_mod_aux"theorem div_aux_mod_aux: ∀p,n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. +na title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a(a href="cic:/matita/arithmetics/div_and_mod/div_aux.fix(0,0,2)"div_aux/a p n m)a title="natural times" href="cic:/fakeuri.def(1)"*/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m) a title="natural plus" href="cic:/fakeuri.def(1)"+/a (a href="cic:/matita/arithmetics/div_and_mod/mod_aux.fix(0,0,2)"mod_aux/a p n m). #p (elim p) [#n #m normalize // |#q #Hind #n #m normalize - @(leb_elim n m) #lenm normalize // - >associative_plus <(Hind (n-(S m)) m) - applyS plus_minus_m_m (* bello *) /2/ + @(a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"leb_elim/a n m) #lenm normalize // + >a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"associative_plus/a <(Hind (na title="natural minus" href="cic:/fakeuri.def(1)"-/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m)) m) + applyS a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"plus_minus_m_m/a (* bello *) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a/span/span/ qed. -theorem div_mod: ∀n,m:nat. n=(n / m)*m+(n \mod m). +img class="anchor" src="icons/tick.png" id="div_mod"theorem div_mod: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. na title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a(n a title="natural divide" href="cic:/fakeuri.def(1)"//a m)a title="natural times" href="cic:/fakeuri.def(1)"*/ama title="natural plus" href="cic:/fakeuri.def(1)"+/a(n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a m). #n #m (cases m) normalize // qed. -theorem eq_times_div_minus_mod: -∀a,b:nat. (a / b) * b = a - (a \mod b). -#a #b (applyS minus_plus_m_m) qed. +img class="anchor" src="icons/tick.png" id="eq_times_div_minus_mod"theorem eq_times_div_minus_mod: +∀a,b:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. (a a title="natural divide" href="cic:/fakeuri.def(1)"//a b) a title="natural times" href="cic:/fakeuri.def(1)"*/a b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a a title="natural minus" href="cic:/fakeuri.def(1)"-/a (a a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a b). +#a #b (applyS a href="cic:/matita/arithmetics/nat/minus_plus_m_m.def(6)"minus_plus_m_m/a) qed. -inductive div_mod_spec (n,m,q,r:nat) : Prop ≝ -div_mod_spec_intro: r < m → n=q*m+r → div_mod_spec n m q r. +img class="anchor" src="icons/tick.png" id="div_mod_spec"inductive div_mod_spec (n,m,q,r:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) : Prop ≝ +div_mod_spec_intro: r a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → na title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aqa title="natural times" href="cic:/fakeuri.def(1)"*/ama title="natural plus" href="cic:/fakeuri.def(1)"+/ar → div_mod_spec n m q r. -theorem div_mod_spec_to_not_eq_O: - ∀n,m,q,r.div_mod_spec n m q r → m ≠ O. -#n #m #q #r * /2/ +img class="anchor" src="icons/tick.png" id="div_mod_spec_to_not_eq_O"theorem div_mod_spec_to_not_eq_O: + ∀n,m,q,r.a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.ind(1,0,4)"div_mod_spec/a n m q r → m a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a. +#n #m #q #r * /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a/span/span/ qed. -theorem div_mod_spec_div_mod: - ∀n,m. O < m → div_mod_spec n m (n / m) (n \mod m). -#n #m #posm % /2/ qed. +img class="anchor" src="icons/tick.png" id="div_mod_spec_div_mod"theorem div_mod_spec_div_mod: + ∀n,m. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.ind(1,0,4)"div_mod_spec/a n m (n a title="natural divide" href="cic:/fakeuri.def(1)"//a m) (n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a m). +#n #m #posm % /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"lt_mod_m_m/a/span/span/ qed. -theorem div_mod_spec_to_eq :∀ a,b,q,r,q1,r1. -div_mod_spec a b q r → div_mod_spec a b q1 r1 → q = q1. +img class="anchor" src="icons/tick.png" id="div_mod_spec_to_eq"theorem div_mod_spec_to_eq :∀ a,b,q,r,q1,r1. +a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.ind(1,0,4)"div_mod_spec/a a b q r → a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.ind(1,0,4)"div_mod_spec/a a b q1 r1 → q a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a q1. #a #b #q #r #q1 #r1 * #ltrb #spec * #ltr1b #spec1 -@(leb_elim q q1) #leqq1 - [(elim (le_to_or_lt_eq … leqq1)) // - #ltqq1 @False_ind @(absurd ?? (not_le_Sn_n a)) - @(lt_to_le_to_lt ? ((S q)*b) ?) - [>spec (applyS (monotonic_lt_plus_r … ltrb)) - |@(transitive_le ? (q1*b)) /2/ +@(a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"leb_elim/a q q1) #leqq1 + [(elim (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … leqq1)) // + #ltqq1 @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a ?? (a href="cic:/matita/arithmetics/nat/not_le_Sn_n.def(6)"not_le_Sn_n/a a)) + @(a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"lt_to_le_to_lt/a ? ((a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a q)a title="natural times" href="cic:/fakeuri.def(1)"*/ab) ?) + [>spec (applyS (a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_r.def(9)"monotonic_lt_plus_r/a … ltrb)) + |@(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a ? (q1a title="natural times" href="cic:/fakeuri.def(1)"*/ab)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"monotonic_le_times_r/a/span/span/ ] (* this case is symmetric *) - |@False_ind @(absurd ?? (not_le_Sn_n a)) - @(lt_to_le_to_lt ? ((S q1)*b) ?) - [>spec1 (applyS (monotonic_lt_plus_r … ltr1b)) - |cut (q1 < q) [/2/] #ltq1q @(transitive_le ? (q*b)) /2/ + |@a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a ?? (a href="cic:/matita/arithmetics/nat/not_le_Sn_n.def(6)"not_le_Sn_n/a a)) + @(a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"lt_to_le_to_lt/a ? ((a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a q1)a title="natural times" href="cic:/fakeuri.def(1)"*/ab) ?) + [>spec1 (applyS (a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_r.def(9)"monotonic_lt_plus_r/a … ltr1b)) + |cut (q1 a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a q) [/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a/span/span/] #ltq1q @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a ? (qa title="natural times" href="cic:/fakeuri.def(1)"*/ab)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"monotonic_le_times_r/a/span/span/ ] ] qed. -theorem div_mod_spec_to_eq2: ∀a,b,q,r,q1,r1. - div_mod_spec a b q r → div_mod_spec a b q1 r1 → r = r1. +img class="anchor" src="icons/tick.png" id="div_mod_spec_to_eq2"theorem div_mod_spec_to_eq2: ∀a,b,q,r,q1,r1. + a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.ind(1,0,4)"div_mod_spec/a a b q r → a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.ind(1,0,4)"div_mod_spec/a a b q1 r1 → r a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a r1. #a #b #q #r #q1 #r1 #spec #spec1 -cut (q=q1) [@(div_mod_spec_to_eq … spec spec1)] +cut (qa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aq1) [@(a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq.def(10)"div_mod_spec_to_eq/a … spec spec1)] #eqq (elim spec) #_ #eqa (elim spec1) #_ #eqa1 -@(injective_plus_r (q*b)) // +@(a href="cic:/matita/arithmetics/nat/injective_plus_r.def(5)"injective_plus_r/a (qa title="natural times" href="cic:/fakeuri.def(1)"*/ab)) // qed. -(* boh -theorem div_mod_spec_times : ∀ n,m:nat.div_mod_spec ((S n)*m) (S n) m O. -intros.constructor 1. -unfold lt.apply le_S_S.apply le_O_n. demodulate. reflexivity. -(*rewrite < plus_n_O.rewrite < sym_times.reflexivity.*) -qed. *) - -lemma div_plus_times: ∀m,q,r:nat. r < m → (q*m+r)/ m = q. +img class="anchor" src="icons/tick.png" id="div_plus_times"lemma div_plus_times: ∀m,q,r:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. r a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → (qa title="natural times" href="cic:/fakeuri.def(1)"*/ama title="natural plus" href="cic:/fakeuri.def(1)"+/ar)a title="natural divide" href="cic:/fakeuri.def(1)"//a m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a q. #m #q #r #ltrm -@(div_mod_spec_to_eq … (div_mod_spec_div_mod ???)) /2/ +@(a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq.def(10)"div_mod_spec_to_eq/a … (a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"div_mod_spec_div_mod/a ???)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/ltn_to_ltO.def(5)"ltn_to_ltO/a, a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"div_mod_spec_intro/a/span/span/ qed. -lemma mod_plus_times: ∀m,q,r:nat. r < m → (q*m+r) \mod m = r. +img class="anchor" src="icons/tick.png" id="mod_plus_times"lemma mod_plus_times: ∀m,q,r:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. r a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → (qa title="natural times" href="cic:/fakeuri.def(1)"*/ama title="natural plus" href="cic:/fakeuri.def(1)"+/ar) a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a r. #m #q #r #ltrm -@(div_mod_spec_to_eq2 … (div_mod_spec_div_mod ???)) /2/ +@(a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq2.def(11)"div_mod_spec_to_eq2/a … (a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"div_mod_spec_div_mod/a ???)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/ltn_to_ltO.def(5)"ltn_to_ltO/a, a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"div_mod_spec_intro/a/span/span/ qed. (* some properties of div and mod *) -theorem div_times: ∀a,b:nat. O < b → a*b/b = a. +img class="anchor" src="icons/tick.png" id="div_times"theorem div_times: ∀a,b:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a b → aa title="natural times" href="cic:/fakeuri.def(1)"*/aba title="natural divide" href="cic:/fakeuri.def(1)"//ab a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a. #a #b #posb -@(div_mod_spec_to_eq (a*b) b … O (div_mod_spec_div_mod …)) -// @div_mod_spec_intro // qed. +@(a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq.def(10)"div_mod_spec_to_eq/a (aa title="natural times" href="cic:/fakeuri.def(1)"*/ab) b … a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a (a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"div_mod_spec_div_mod/a …)) +// @a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"div_mod_spec_intro/a // qed. -theorem div_n_n: ∀n:nat. O < n → n / n = 1. -/2/ qed. +img class="anchor" src="icons/tick.png" id="div_n_n"theorem div_n_n: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → n a title="natural divide" href="cic:/fakeuri.def(1)"//a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="natural number" href="cic:/fakeuri.def(1)"1/a. +/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/div_and_mod/div_times.def(14)"div_times/a/span/span/ qed. -theorem eq_div_O: ∀n,m. n < m → n / m = O. +img class="anchor" src="icons/tick.png" id="eq_div_O"theorem eq_div_O: ∀n,m. n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → n a title="natural divide" href="cic:/fakeuri.def(1)"//a m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a. #n #m #ltnm -@(div_mod_spec_to_eq n m (n/m) … n (div_mod_spec_div_mod …)) -/2/ qed. +@(a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq.def(10)"div_mod_spec_to_eq/a n m (na title="natural divide" href="cic:/fakeuri.def(1)"//am) … n (a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"div_mod_spec_div_mod/a …)) +/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/ltn_to_ltO.def(5)"ltn_to_ltO/a, a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"div_mod_spec_intro/a/span/span/ qed. -theorem mod_n_n: ∀n:nat. O < n → n \mod n = O. +img class="anchor" src="icons/tick.png" id="mod_n_n"theorem mod_n_n: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a. #n #posn -@(div_mod_spec_to_eq2 n n … 1 0 (div_mod_spec_div_mod …)) -/2/ qed. +@(a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq2.def(11)"div_mod_spec_to_eq2/a n n … a title="natural number" href="cic:/fakeuri.def(1)"1/a a title="natural number" href="cic:/fakeuri.def(1)"0/a (a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"div_mod_spec_div_mod/a …)) +/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"div_mod_spec_intro/a/span/span/ qed. -theorem mod_S: ∀n,m:nat. O < m → S (n \mod m) < m → -((S n) \mod m) = S (n \mod m). +img class="anchor" src="icons/tick.png" id="mod_S"theorem mod_S: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a m) a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → +((a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n) a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a m) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a m). #n #m #posm #H -@(div_mod_spec_to_eq2 (S n) m … (n / m) ? (div_mod_spec_div_mod …)) -// @div_mod_spec_intro// (applyS eq_f) // +@(a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq2.def(11)"div_mod_spec_to_eq2/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n) m … (n a title="natural divide" href="cic:/fakeuri.def(1)"//a m) ? (a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"div_mod_spec_div_mod/a …)) +// @a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"div_mod_spec_intro/a// (applyS a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a) // qed. -theorem mod_O_n: ∀n:nat.O \mod n = O. -/2/ qed. +img class="anchor" src="icons/tick.png" id="mod_O_n"theorem mod_O_n: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a. +/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/plus_minus.def(5)"plus_minus/a/span/span/ qed. -theorem lt_to_eq_mod: ∀n,m:nat. n < m → n \mod m = n. +img class="anchor" src="icons/tick.png" id="lt_to_eq_mod"theorem lt_to_eq_mod: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n. #n #m #ltnm -@(div_mod_spec_to_eq2 n m (n/m) … O n (div_mod_spec_div_mod …)) -/2/ qed. +@(a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq2.def(11)"div_mod_spec_to_eq2/a n m (na title="natural divide" href="cic:/fakeuri.def(1)"//am) … a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a n (a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"div_mod_spec_div_mod/a …)) +/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/ltn_to_ltO.def(5)"ltn_to_ltO/a, a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"div_mod_spec_intro/a/span/span/ qed. (* theorem mod_1: ∀n:nat. mod n 1 = O. @@ -172,26 +165,26 @@ theorem mod_1: ∀n:nat. mod n 1 = O. theorem div_1: ∀n:nat. div n 1 = n. #n @sym_eq napplyS (div_mod n 1) qed. *) -theorem or_div_mod: ∀n,q. O < q → - ((S (n \mod q)=q) ∧ S n = (S (div n q)) * q ∨ - ((S (n \mod q)(div_mod n m) in ⊢ (? % ?) >commutative_plus -@monotonic_lt_plus_l @lt_mod_m_m // +img class="anchor" src="icons/tick.png" id="lt_div_S"theorem lt_div_S: ∀n,m. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a(n a title="natural divide" href="cic:/fakeuri.def(1)"//a m)a title="natural times" href="cic:/fakeuri.def(1)"*/am. +#n #m #posm (change with (n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m a title="natural plus" href="cic:/fakeuri.def(1)"+/a(na title="natural divide" href="cic:/fakeuri.def(1)"//am)a title="natural times" href="cic:/fakeuri.def(1)"*/am)) +>(a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"div_mod/a n m) in ⊢ (? % ?); >a href="cic:/matita/arithmetics/nat/commutative_plus.def(5)"commutative_plus/a +@a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_l.def(9)"monotonic_lt_plus_l/a @a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"lt_mod_m_m/a // qed. -theorem le_div: ∀n,m. O < n → m/n ≤ m. +img class="anchor" src="icons/tick.png" id="le_div"theorem le_div: ∀n,m. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → ma title="natural divide" href="cic:/fakeuri.def(1)"//an a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m. #n #m #posn ->(div_mod m n) in ⊢ (? ? %) @(transitive_le ? (m/n*n)) /2/ +>(a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"div_mod/a m n) in ⊢ (? ? %); @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a ? (ma title="natural divide" href="cic:/fakeuri.def(1)"//ana title="natural times" href="cic:/fakeuri.def(1)"*/an)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"monotonic_le_times_r/a/span/span/ qed. -theorem le_plus_mod: ∀m,n,q. O < q → -(m+n) \mod q ≤ m \mod q + n \mod q . +img class="anchor" src="icons/tick.png" id="le_plus_mod"theorem le_plus_mod: ∀m,n,q. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a q → +(ma title="natural plus" href="cic:/fakeuri.def(1)"+/an) a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a q a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a q a title="natural plus" href="cic:/fakeuri.def(1)"+/a n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a q . #m #n #q #posq -(elim (decidable_le q (m \mod q + n \mod q))) #Hle - [@(transitive_le … Hle) @le_S_S_to_le @le_S /2/ - |cut ((m+n)\mod q = m\mod q+n\mod q) // - @(div_mod_spec_to_eq2 … (m/q + n/q) ? (div_mod_spec_div_mod … posq)). - @div_mod_spec_intro - [@not_le_to_lt // - |>(div_mod n q) in ⊢ (? ? (? ? %) ?) - (applyS (eq_f … (λx.plus x (n \mod q)))) - >(div_mod m q) in ⊢ (? ? (? % ?) ?) - (applyS (eq_f … (λx.plus x (m \mod q)))) // +(elim (a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"decidable_le/a q (m a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a q a title="natural plus" href="cic:/fakeuri.def(1)"+/a n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a q))) #Hle + [@(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a … Hle) @a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a @a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"lt_mod_m_m/a/span/span/ + |cut ((ma title="natural plus" href="cic:/fakeuri.def(1)"+/an)a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a q a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a ma title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a qa title="natural plus" href="cic:/fakeuri.def(1)"+/ana title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a q) // + @(a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq2.def(11)"div_mod_spec_to_eq2/a … (ma title="natural divide" href="cic:/fakeuri.def(1)"//aq a title="natural plus" href="cic:/fakeuri.def(1)"+/a na title="natural divide" href="cic:/fakeuri.def(1)"//aq) ? (a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"div_mod_spec_div_mod/a … posq)). + @a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"div_mod_spec_intro/a + [@a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a // + |>(a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"div_mod/a n q) in ⊢ (? ? (? ? %) ?); + (applyS (a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a … (λx.a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"plus/a x (n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a q)))) + >(a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"div_mod/a m q) in ⊢ (? ? (? % ?) ?); + (applyS (a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a … (λx.a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"plus/a x (m a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a q)))) // ] ] qed. -theorem le_plus_div: ∀m,n,q. O < q → - m/q + n/q \le (m+n)/q. -#m #n #q #posq @(le_times_to_le … posq) -@(le_plus_to_le_r ((m+n) \mod q)) +img class="anchor" src="icons/tick.png" id="le_plus_div"theorem le_plus_div: ∀m,n,q. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a q → + ma title="natural divide" href="cic:/fakeuri.def(1)"//aq a title="natural plus" href="cic:/fakeuri.def(1)"+/a na title="natural divide" href="cic:/fakeuri.def(1)"//aq a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\le/a (ma title="natural plus" href="cic:/fakeuri.def(1)"+/an)a title="natural divide" href="cic:/fakeuri.def(1)"//aq. +#m #n #q #posq @(a href="cic:/matita/arithmetics/nat/le_times_to_le.def(9)"le_times_to_le/a … posq) +@(a href="cic:/matita/arithmetics/nat/le_plus_to_le_r.def(6)"le_plus_to_le_r/a ((ma title="natural plus" href="cic:/fakeuri.def(1)"+/an) a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a q)) (* bruttino *) ->commutative_times in ⊢ (? ? %) (div_mod m q) in ⊢ (? ? (? % ?)) >(div_mod n q) in ⊢ (? ? (? ? %)) ->commutative_plus in ⊢ (? ? (? % ?)) >associative_plus in ⊢ (? ? %) -a href="cic:/matita/arithmetics/nat/commutative_times.def(8)"commutative_times/a in ⊢ (? ? %); <a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"div_mod/a +>(a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"div_mod/a m q) in ⊢ (? ? (? % ?)); >(a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"div_mod/a n q) in ⊢ (? ? (? ? %)); +>a href="cic:/matita/arithmetics/nat/commutative_plus.def(5)"commutative_plus/a in ⊢ (? ? (? % ?)); >a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"associative_plus/a in ⊢ (? ? %); +<a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"associative_plus/a in ⊢ (? ? (? ? %)); (applyS a href="cic:/matita/arithmetics/nat/monotonic_le_plus_l.def(6)"monotonic_le_plus_l/a) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/div_and_mod/le_plus_mod.def(14)"le_plus_mod/a/span/span/ qed. -theorem le_times_to_le_div: ∀a,b,c:nat. - O < b → b*c ≤ a → c ≤ a/b. +img class="anchor" src="icons/tick.png" id="le_times_to_le_div"theorem le_times_to_le_div: ∀a,b,c:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. + a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a b → ba title="natural times" href="cic:/fakeuri.def(1)"*/ac a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a → c a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a aa title="natural divide" href="cic:/fakeuri.def(1)"//ab. #a #b #c #posb #Hle -@le_S_S_to_le @(lt_times_n_to_lt_l b) @(le_to_lt_to_lt ? a)/2/ +@a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a @(a href="cic:/matita/arithmetics/nat/lt_times_n_to_lt_l.def(9)"lt_times_n_to_lt_l/a b) @(a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"le_to_lt_to_lt/a ? a)/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/div_and_mod/lt_div_S.def(13)"lt_div_S/a/span/span/ qed. -theorem le_times_to_le_div2: ∀m,n,q. O < q → - n ≤ m*q → n/q ≤ m. +img class="anchor" src="icons/tick.png" id="le_times_to_le_div2"theorem le_times_to_le_div2: ∀m,n,q. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a q → + n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a ma title="natural times" href="cic:/fakeuri.def(1)"*/aq → na title="natural divide" href="cic:/fakeuri.def(1)"//aq a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m. #m #n #q #posq #Hle -@(le_times_to_le q ? ? posq) @(le_plus_to_le (n \mod q)) /2/ +@(a href="cic:/matita/arithmetics/nat/le_times_to_le.def(9)"le_times_to_le/a q ? ? posq) @(a href="cic:/matita/arithmetics/nat/le_plus_to_le.def(5)"le_plus_to_le/a (n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a q)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_a.def(8)"le_plus_a/a/span/span/ qed. (* da spostare theorem lt_m_nm: ∀n,m. O < m → 1 < n → m < n*m. /2/ qed. *) -theorem lt_times_to_lt_div: ∀m,n,q. n < m*q → n/q < m. +img class="anchor" src="icons/tick.png" id="lt_times_to_lt_div"theorem lt_times_to_lt_div: ∀m,n,q. n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a ma title="natural times" href="cic:/fakeuri.def(1)"*/aq → na title="natural divide" href="cic:/fakeuri.def(1)"//aq a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m. #m #n #q #Hlt -@(lt_times_n_to_lt_l q …) @(lt_plus_to_lt_l (n \mod q)) /2/ +@(a href="cic:/matita/arithmetics/nat/lt_times_n_to_lt_l.def(9)"lt_times_n_to_lt_l/a q …) @(a href="cic:/matita/arithmetics/nat/lt_plus_to_lt_l.def(6)"lt_plus_to_lt_l/a (n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a q)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"lt_to_le_to_lt/a/span/span/ qed. (* @@ -282,24 +275,24 @@ theorem le_div_plus_S: ∀m,n,q. O < q → // qed. *) -theorem le_div_S_S_div: ∀n,m. O < m → (S n)/m ≤ S (n /m). -#n #m #posm @le_times_to_le_div2 /2/ +img class="anchor" src="icons/tick.png" id="le_div_S_S_div"theorem le_div_S_S_div: ∀n,m. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n)a title="natural divide" href="cic:/fakeuri.def(1)"//am a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (n a title="natural divide" href="cic:/fakeuri.def(1)"//am). +#n #m #posm @a href="cic:/matita/arithmetics/div_and_mod/le_times_to_le_div2.def(10)"le_times_to_le_div2/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/div_and_mod/lt_div_S.def(13)"lt_div_S/a/span/span/ qed. -theorem le_times_div_div_times: ∀a,n,m.O < m → -a*(n/m) ≤ a*n/m. -#a #n #m #posm @le_times_to_le_div /2/ +img class="anchor" src="icons/tick.png" id="le_times_div_div_times"theorem le_times_div_div_times: ∀a,n,m.a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → +aa title="natural times" href="cic:/fakeuri.def(1)"*/a(na title="natural divide" href="cic:/fakeuri.def(1)"//am) a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a aa title="natural times" href="cic:/fakeuri.def(1)"*/ana title="natural divide" href="cic:/fakeuri.def(1)"//am. +#a #n #m #posm @a href="cic:/matita/arithmetics/div_and_mod/le_times_to_le_div.def(14)"le_times_to_le_div/a /span class="autotactic"2span class="autotrace" trace /span/span/ qed. -theorem monotonic_div: ∀n.O < n → - monotonic nat le (λm.div m n). -#n #posn #a #b #leab @le_times_to_le_div/2/ +img class="anchor" src="icons/tick.png" id="monotonic_div"theorem monotonic_div: ∀n.a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → + a href="cic:/matita/basics/relations/monotonic.def(1)"monotonic/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"le/a (λm.a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"div/a m n). +#n #posn #a #b #leab @a href="cic:/matita/arithmetics/div_and_mod/le_times_to_le_div.def(14)"le_times_to_le_div/a/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a/span/span/ qed. -theorem pos_div: ∀n,m:nat. O < m → O < n → n \mod m = O → - O < n / m. +img class="anchor" src="icons/tick.png" id="pos_div"theorem pos_div: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a → + a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n a title="natural divide" href="cic:/fakeuri.def(1)"//a m. #n #m #posm #posn #mod0 -@(lt_times_n_to_lt_l m)// (* MITICO *) +@(a href="cic:/matita/arithmetics/nat/lt_times_n_to_lt_l.def(9)"lt_times_n_to_lt_l/a m)// (* MITICO *) qed. (* @@ -308,135 +301,56 @@ theorem lt_div_n_m_n: ∀n,m:nat. 1 < m → O < n → n / m < n. @(leb_elim 1 (n / m))/2/ (* MITICO *) qed. *) -theorem eq_div_div_div_times: ∀n,m,q. O < n → O < m → - q/n/m = q/(n*m). +img class="anchor" src="icons/tick.png" id="eq_div_div_div_times"theorem eq_div_div_div_times: ∀n,m,q. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → + qa title="natural divide" href="cic:/fakeuri.def(1)"//ana title="natural divide" href="cic:/fakeuri.def(1)"//am a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a qa title="natural divide" href="cic:/fakeuri.def(1)"//a(na title="natural times" href="cic:/fakeuri.def(1)"*/am). #n #m #q #posn #posm -@(div_mod_spec_to_eq … (q\mod n+n*(q/n\mod m)) … (div_mod_spec_div_mod …)) /2/ -@div_mod_spec_intro // @(lt_to_le_to_lt ? (n*(S (q/n\mod m)))) - [(applyS monotonic_lt_plus_l) /2/ - |@monotonic_le_times_r/2/ +@(a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq.def(10)"div_mod_spec_to_eq/a … (qa title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a na title="natural plus" href="cic:/fakeuri.def(1)"+/ana title="natural times" href="cic:/fakeuri.def(1)"*/a(qa title="natural divide" href="cic:/fakeuri.def(1)"//ana title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a m)) … (a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"div_mod_spec_div_mod/a …)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/lt_times.def(13)"lt_times/a/span/span/ +@a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"div_mod_spec_intro/a // @(a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"lt_to_le_to_lt/a ? (na title="natural times" href="cic:/fakeuri.def(1)"*/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (qa title="natural divide" href="cic:/fakeuri.def(1)"//ana title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a m)))) + [(applyS a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_l.def(9)"monotonic_lt_plus_l/a) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"lt_mod_m_m/a/span/span/ + |@a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"monotonic_le_times_r/a/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"lt_mod_m_m/a/span/span/ ] qed. -theorem eq_div_div_div_div: ∀n,m,q. O < n → O < m → -q/n/m = q/m/n. +img class="anchor" src="icons/tick.png" id="eq_div_div_div_div"theorem eq_div_div_div_div: ∀n,m,q. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → +qa title="natural divide" href="cic:/fakeuri.def(1)"//ana title="natural divide" href="cic:/fakeuri.def(1)"//am a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a qa title="natural divide" href="cic:/fakeuri.def(1)"//ama title="natural divide" href="cic:/fakeuri.def(1)"//an. #n #m #q #posn #posm -@(trans_eq ? ? (q/(n*m))) - [/2/ - |@sym_eq (applyS eq_div_div_div_times) // +@(a href="cic:/matita/basics/logic/trans_eq.def(4)"trans_eq/a ? ? (qa title="natural divide" href="cic:/fakeuri.def(1)"//a(na title="natural times" href="cic:/fakeuri.def(1)"*/am))) + [/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/div_and_mod/eq_div_div_div_times.def(14)"eq_div_div_div_times/a/span/span/ + |@a href="cic:/matita/basics/logic/sym_eq.def(2)"sym_eq/a (applyS a href="cic:/matita/arithmetics/div_and_mod/eq_div_div_div_times.def(14)"eq_div_div_div_times/a) // ] qed. -(* -theorem SSO_mod: \forall n,m. O < m \to (S(S O))*n/m = (n/m)*(S(S O)) + mod ((S(S O))*n/m) (S(S O)). -intros. -rewrite < (lt_O_to_div_times n (S(S O))) in ⊢ (? ? ? (? (? (? % ?) ?) ?)) - [rewrite > eq_div_div_div_div - [rewrite > sym_times in ⊢ (? ? ? (? (? (? (? % ?) ?) ?) ?)). - apply div_mod. - apply lt_O_S - |apply lt_O_S - |assumption - ] - |apply lt_O_S - ] -qed. *) -(* Forall a,b : N. 0 < b \to b * (a/b) <= a < b * (a/b +1) *) -(* The theorem is shown in two different parts: *) -(* -theorem lt_to_div_to_and_le_times_lt_S: \forall a,b,c:nat. -O \lt b \to a/b = c \to (b*c \le a \land a \lt b*(S c)). -intros. -split -[ rewrite < H1. - rewrite > sym_times. - rewrite > eq_times_div_minus_mod - [ apply (le_minus_m a (a \mod b)) - | assumption - ] -| rewrite < (times_n_Sm b c). - rewrite < H1. - rewrite > sym_times. - rewrite > (div_mod a b) in \vdash (? % ?) - [ rewrite > (sym_plus b ((a/b)*b)). - apply lt_plus_r. - apply lt_mod_m_m. - assumption - | assumption - ] -] -qed. *) - -theorem lt_to_le_times_to_lt_S_to_div: ∀a,c,b:nat. -O < b → (b*c) ≤ a → a < (b*(S c)) → a/b = c. +img class="anchor" src="icons/tick.png" id="lt_to_le_times_to_lt_S_to_div"theorem lt_to_le_times_to_lt_S_to_div: ∀a,c,b:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. +a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a b → (ba title="natural times" href="cic:/fakeuri.def(1)"*/ac) a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a → a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a (ba title="natural times" href="cic:/fakeuri.def(1)"*/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a c)) → aa title="natural divide" href="cic:/fakeuri.def(1)"//ab a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a c. #a #c #b #posb#lea #lta -@(div_mod_spec_to_eq … (a-b*c) (div_mod_spec_div_mod … posb …)) -@div_mod_spec_intro [@lt_plus_to_minus // |/2/] +@(a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq.def(10)"div_mod_spec_to_eq/a … (aa title="natural minus" href="cic:/fakeuri.def(1)"-/aba title="natural times" href="cic:/fakeuri.def(1)"*/ac) (a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"div_mod_spec_div_mod/a … posb …)) +@a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"div_mod_spec_intro/a [@a href="cic:/matita/arithmetics/nat/lt_plus_to_minus.def(11)"lt_plus_to_minus/a // |/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/plus_minus.def(5)"plus_minus/a/span/span/] qed. -theorem div_times_times: ∀a,b,c:nat. O < c → O < b → - (a/b) = (a*c)/(b*c). +img class="anchor" src="icons/tick.png" id="div_times_times"theorem div_times_times: ∀a,b,c:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c → a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a b → + (aa title="natural divide" href="cic:/fakeuri.def(1)"//ab) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (aa title="natural times" href="cic:/fakeuri.def(1)"*/ac)a title="natural divide" href="cic:/fakeuri.def(1)"//a(ba title="natural times" href="cic:/fakeuri.def(1)"*/ac). #a #b #c #posc #posb ->(commutative_times b) div_times // +>(a href="cic:/matita/arithmetics/nat/commutative_times.def(8)"commutative_times/a b) <a href="cic:/matita/arithmetics/div_and_mod/eq_div_div_div_times.def(14)"eq_div_div_div_times/a // +>a href="cic:/matita/arithmetics/div_and_mod/div_times.def(14)"div_times/a // qed. -theorem times_mod: ∀a,b,c:nat. -O < c → O < b → (a*c) \mod (b*c) = c*(a\mod b). +img class="anchor" src="icons/tick.png" id="times_mod"theorem times_mod: ∀a,b,c:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. +a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c → a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a b → (aa title="natural times" href="cic:/fakeuri.def(1)"*/ac) a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a (ba title="natural times" href="cic:/fakeuri.def(1)"*/ac) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a ca title="natural times" href="cic:/fakeuri.def(1)"*/a(aa title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a b). #a #b #c #posc #posb -@(div_mod_spec_to_eq2 (a*c) (b*c) (a/b) ((a*c) \mod (b*c)) (a/b) (c*(a \mod b))) - [>(div_times_times … posc) // @div_mod_spec_div_mod /2/ - |@div_mod_spec_intro - [applyS (monotonic_lt_times_r … c posc) /2/ - |(applyS (eq_f …(λx.x*c))) // +@(a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq2.def(11)"div_mod_spec_to_eq2/a (aa title="natural times" href="cic:/fakeuri.def(1)"*/ac) (ba title="natural times" href="cic:/fakeuri.def(1)"*/ac) (aa title="natural divide" href="cic:/fakeuri.def(1)"//ab) ((aa title="natural times" href="cic:/fakeuri.def(1)"*/ac) a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a (ba title="natural times" href="cic:/fakeuri.def(1)"*/ac)) (aa title="natural divide" href="cic:/fakeuri.def(1)"//ab) (ca title="natural times" href="cic:/fakeuri.def(1)"*/a(a a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a b))) + [>(a href="cic:/matita/arithmetics/div_and_mod/div_times_times.def(15)"div_times_times/a … posc) // @a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"div_mod_spec_div_mod/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/lt_times.def(13)"lt_times/a/span/span/ + |@a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"div_mod_spec_intro/a + [applyS (a href="cic:/matita/arithmetics/nat/monotonic_lt_times_r.def(10)"monotonic_lt_times_r/a … c posc) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"lt_mod_m_m/a/span/span/ + |(applyS (a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a …(λx.xa title="natural times" href="cic:/fakeuri.def(1)"*/ac))) // ] ] qed. -theorem le_div_times_m: ∀a,i,m. O < i → O < m → - (a * (m / i)) / m ≤ a / i. +img class="anchor" src="icons/tick.png" id="le_div_times_m"theorem le_div_times_m: ∀a,i,m. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a i → a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → + (a a title="natural times" href="cic:/fakeuri.def(1)"*/a (m a title="natural divide" href="cic:/fakeuri.def(1)"//a i)) a title="natural divide" href="cic:/fakeuri.def(1)"//a m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a a title="natural divide" href="cic:/fakeuri.def(1)"//a i. #a #i #m #posi #posm -@(transitive_le ? ((a*m/i)/m)) - [@monotonic_div /2/ - |>eq_div_div_div_div // >div_times // +@(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a ? ((aa title="natural times" href="cic:/fakeuri.def(1)"*/ama title="natural divide" href="cic:/fakeuri.def(1)"//ai)a title="natural divide" href="cic:/fakeuri.def(1)"//am)) + [@a href="cic:/matita/arithmetics/div_and_mod/monotonic_div.def(15)"monotonic_div/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/div_and_mod/le_times_div_div_times.def(15)"le_times_div_div_times/a/span/span/ + |>a href="cic:/matita/arithmetics/div_and_mod/eq_div_div_div_div.def(15)"eq_div_div_div_div/a // >a href="cic:/matita/arithmetics/div_and_mod/div_times.def(14)"div_times/a // ] qed. - -(* serve ? -theorem le_div_times_Sm: ∀a,i,m. O < i → O < m → -a / i ≤ (a * S (m / i))/m. -intros. -apply (trans_le ? ((a * S (m/i))/((S (m/i))*i))) - [rewrite < (eq_div_div_div_times ? i) - [rewrite > lt_O_to_div_times - [apply le_n - |apply lt_O_S - ] - |apply lt_O_S - |assumption - ] - |apply le_times_to_le_div - [assumption - |apply (trans_le ? (m*(a*S (m/i))/(S (m/i)*i))) - [apply le_times_div_div_times. - rewrite > (times_n_O O). - apply lt_times - [apply lt_O_S - |assumption - ] - |rewrite > sym_times. - apply le_times_to_le_div2 - [rewrite > (times_n_O O). - apply lt_times - [apply lt_O_S - |assumption - ] - |apply le_times_r. - apply lt_to_le. - apply lt_div_S. - assumption - ] - ] - ] - ] -qed. *) -- 2.39.2