From 5e1fd9ee5ced5737c7fd4f25fca47feda1fda8e9 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 19 Jul 2005 11:11:52 +0000 Subject: [PATCH] New naming policy for local variables. --- helm/matita/library/Z/orders.ma | 173 ++++++++++++++++ helm/matita/library/Z/times.ma | 276 +++++++++++++++++++++++++ helm/matita/library/Z/z.ma | 34 +-- helm/matita/library/nat/div_and_mod.ma | 178 ++++++++++++++++ helm/matita/library/nat/nat.ma | 2 +- helm/matita/library/nat/orders.ma | 4 +- helm/matita/library/nat/times.ma | 17 +- 7 files changed, 658 insertions(+), 26 deletions(-) create mode 100644 helm/matita/library/Z/orders.ma create mode 100644 helm/matita/library/Z/times.ma create mode 100644 helm/matita/library/nat/div_and_mod.ma diff --git a/helm/matita/library/Z/orders.ma b/helm/matita/library/Z/orders.ma new file mode 100644 index 000000000..1a2d65a4f --- /dev/null +++ b/helm/matita/library/Z/orders.ma @@ -0,0 +1,173 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/Z/orders". + +include "Z/z.ma". + +definition Zle : Z \to Z \to Prop \def +\lambda x,y:Z. + match x with + [ OZ \Rightarrow + match y with + [ OZ \Rightarrow True + | (pos m) \Rightarrow True + | (neg m) \Rightarrow False ] + | (pos n) \Rightarrow + match y with + [ OZ \Rightarrow False + | (pos m) \Rightarrow (le n m) + | (neg m) \Rightarrow False ] + | (neg n) \Rightarrow + match y with + [ OZ \Rightarrow True + | (pos m) \Rightarrow True + | (neg m) \Rightarrow (le m n) ]]. + + +definition Zlt : Z \to Z \to Prop \def +\lambda x,y:Z. + match x with + [ OZ \Rightarrow + match y with + [ OZ \Rightarrow False + | (pos m) \Rightarrow True + | (neg m) \Rightarrow False ] + | (pos n) \Rightarrow + match y with + [ OZ \Rightarrow False + | (pos m) \Rightarrow (lt n m) + | (neg m) \Rightarrow False ] + | (neg n) \Rightarrow + match y with + [ OZ \Rightarrow True + | (pos m) \Rightarrow True + | (neg m) \Rightarrow (lt m n) ]]. + +theorem irreflexive_Zlt: irreflexive Z Zlt. +change with \forall x:Z. Zlt x x \to False. +intro.elim x.exact H. +cut (Zlt (neg n) (neg n)) \to False. +apply Hcut.apply H.simplify.apply not_le_Sn_n. +cut (Zlt (pos n) (pos n)) \to False. +apply Hcut.apply H.simplify.apply not_le_Sn_n. +qed. + +theorem irrefl_Zlt: irreflexive Z Zlt +\def irreflexive_Zlt. + +definition Z_compare : Z \to Z \to compare \def +\lambda x,y:Z. + match x with + [ OZ \Rightarrow + match y with + [ OZ \Rightarrow EQ + | (pos m) \Rightarrow LT + | (neg m) \Rightarrow GT ] + | (pos n) \Rightarrow + match y with + [ OZ \Rightarrow GT + | (pos m) \Rightarrow (nat_compare n m) + | (neg m) \Rightarrow GT] + | (neg n) \Rightarrow + match y with + [ OZ \Rightarrow LT + | (pos m) \Rightarrow LT + | (neg m) \Rightarrow nat_compare m n ]]. + +theorem Zlt_neg_neg_to_lt: +\forall n,m:nat. Zlt (neg n) (neg m) \to lt m n. +intros.apply H. +qed. + +theorem lt_to_Zlt_neg_neg: \forall n,m:nat.lt m n \to Zlt (neg n) (neg m). +intros. +simplify.apply H. +qed. + +theorem Zlt_pos_pos_to_lt: +\forall n,m:nat. Zlt (pos n) (pos m) \to lt n m. +intros.apply H. +qed. + +theorem lt_to_Zlt_pos_pos: \forall n,m:nat.lt n m \to Zlt (pos n) (pos m). +intros. +simplify.apply H. +qed. + +theorem Z_compare_to_Prop : +\forall x,y:Z. match (Z_compare x y) with +[ LT \Rightarrow (Zlt x y) +| EQ \Rightarrow (eq Z x y) +| GT \Rightarrow (Zlt y x)]. +intros. +elim x. elim y. +simplify.apply refl_eq. +simplify.exact I. +simplify.exact I. +elim y. simplify.exact I. +simplify. +cut match (nat_compare n1 n) with +[ LT \Rightarrow (lt n1 n) +| EQ \Rightarrow (eq nat n1 n) +| GT \Rightarrow (lt n n1)] \to +match (nat_compare n1 n) with +[ LT \Rightarrow (le (S n1) n) +| EQ \Rightarrow (eq Z (neg n) (neg n1)) +| GT \Rightarrow (le (S n) n1)]. +apply Hcut. apply nat_compare_to_Prop. +elim (nat_compare n1 n). +simplify.exact H. +simplify.exact H. +simplify.apply eq_f.apply sym_eq.exact H. +simplify.exact I. +elim y.simplify.exact I. +simplify.exact I. +simplify. +cut match (nat_compare n n1) with +[ LT \Rightarrow (lt n n1) +| EQ \Rightarrow (eq nat n n1) +| GT \Rightarrow (lt n1 n)] \to +match (nat_compare n n1) with +[ LT \Rightarrow (le (S n) n1) +| EQ \Rightarrow (eq Z (pos n) (pos n1)) +| GT \Rightarrow (le (S n1) n)]. +apply Hcut. apply nat_compare_to_Prop. +elim (nat_compare n n1). +simplify.exact H. +simplify.exact H. +simplify.apply eq_f.exact H. +qed. + +theorem Zlt_to_Zle: \forall x,y:Z. Zlt x y \to Zle (Zsucc x) y. +intros 2.elim x. +cut (Zlt OZ y) \to (Zle (Zsucc OZ) y). +apply Hcut. assumption.simplify.elim y. +simplify.exact H1. +simplify.exact H1. +simplify.apply le_O_n. +cut (Zlt (neg n) y) \to (Zle (Zsucc (neg n)) y). +apply Hcut. assumption.elim n. +cut (Zlt (neg O) y) \to (Zle (Zsucc (neg O)) y). +apply Hcut. assumption.simplify.elim y. +simplify.exact I.simplify.apply not_le_Sn_O n1 H2. +simplify.exact I. +cut (Zlt (neg (S n1)) y) \to (Zle (Zsucc (neg (S n1))) y). +apply Hcut. assumption.simplify. +elim y. +simplify.exact I. +simplify.apply le_S_S_to_le n2 n1 H3. +simplify.exact I. +exact H. +qed. diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma new file mode 100644 index 000000000..6e7a59d16 --- /dev/null +++ b/helm/matita/library/Z/times.ma @@ -0,0 +1,276 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/Z/times". + +include "Z/z.ma". + +definition Ztimes :Z \to Z \to Z \def +\lambda x,y. + match x with + [ OZ \Rightarrow OZ + | (pos m) \Rightarrow + match y with + [ OZ \Rightarrow OZ + | (pos n) \Rightarrow (pos (pred (times (S m) (S n)))) + | (neg n) \Rightarrow (neg (pred (times (S m) (S n))))] + | (neg m) \Rightarrow + match y with + [ OZ \Rightarrow OZ + | (pos n) \Rightarrow (neg (pred (times (S m) (S n)))) + | (neg n) \Rightarrow (pos (pred (times (S m) (S n))))]]. + +theorem Ztimes_z_OZ: \forall z:Z. eq Z (Ztimes z OZ) OZ. +intro.elim z. +simplify.reflexivity. +simplify.reflexivity. +simplify.reflexivity. +qed. + +(* da spostare in nat/order *) +theorem S_pred: \forall n:nat.lt O n \to eq nat n (S (pred n)). +intro.elim n.apply False_ind.exact not_le_Sn_O O H. +apply eq_f.apply pred_Sn. +qed. + +(* +theorem symmetric_Ztimes : symmetric Z Ztimes. +change with \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x). +intros.elim x.rewrite > Ztimes_z_OZ.reflexivity. +elim y.simplify.reflexivity. +change with eq Z (pos (pred (times (S e1) (S e)))) (pos (pred (times (S e) (S e1)))). +rewrite < sym_times.reflexivity. +change with eq Z (neg (pred (times (S e1) (S e2)))) (neg (pred (times (S e2) (S e1)))). +rewrite < sym_times.reflexivity. +elim y.simplify.reflexivity. +change with eq Z (neg (pred (times (S e2) (S e1)))) (neg (pred (times (S e1) (S e2)))). +rewrite < sym_times.reflexivity. +change with eq Z (pos (pred (times (S e2) (S e)))) (pos (pred (times (S e) (S e2)))). +rewrite < sym_times.reflexivity. +qed. + +variant sym_Ztimes : \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x) +\def symmetric_Ztimes. + +theorem associative_Ztimes: associative Z Ztimes. +change with \forall x,y,z:Z.eq Z (Ztimes (Ztimes x y) z) (Ztimes x (Ztimes y z)). +intros. +elim x.simplify.reflexivity. +elim y.simplify.reflexivity. +elim z.simplify.reflexivity. +change with +eq Z (neg (pred (times (S (pred (times (S e1) (S e)))) (S e2)))) + (neg (pred (times (S e1) (S (pred (times (S e) (S e2))))))). +rewrite < S_pred_S. + +theorem Zpred_Zplus_neg_O : \forall z:Z. eq Z (Zpred z) (Zplus (neg O) z). +intros.elim z. +simplify.reflexivity. +simplify.reflexivity. +elim e2.simplify.reflexivity. +simplify.reflexivity. +qed. + +theorem Zsucc_Zplus_pos_O : \forall z:Z. eq Z (Zsucc z) (Zplus (pos O) z). +intros.elim z. +simplify.reflexivity. +elim e1.simplify.reflexivity. +simplify.reflexivity. +simplify.reflexivity. +qed. + +theorem Zplus_pos_pos: +\forall n,m. eq Z (Zplus (pos n) (pos m)) (Zplus (Zsucc (pos n)) (Zpred (pos m))). +intros. +elim n.elim m. +simplify.reflexivity. +simplify.reflexivity. +elim m. +simplify. +rewrite < plus_n_O.reflexivity. +simplify. +rewrite < plus_n_Sm.reflexivity. +qed. + +theorem Zplus_pos_neg: +\forall n,m. eq Z (Zplus (pos n) (neg m)) (Zplus (Zsucc (pos n)) (Zpred (neg m))). +intros.reflexivity. +qed. + +theorem Zplus_neg_pos : +\forall n,m. eq Z (Zplus (neg n) (pos m)) (Zplus (Zsucc (neg n)) (Zpred (pos m))). +intros. +elim n.elim m. +simplify.reflexivity. +simplify.reflexivity. +elim m. +simplify.reflexivity. +simplify.reflexivity. +qed. + +theorem Zplus_neg_neg: +\forall n,m. eq Z (Zplus (neg n) (neg m)) (Zplus (Zsucc (neg n)) (Zpred (neg m))). +intros. +elim n.elim m. +simplify.reflexivity. +simplify.reflexivity. +elim m. +simplify.rewrite < plus_n_Sm.reflexivity. +simplify.rewrite > plus_n_Sm.reflexivity. +qed. + +theorem Zplus_Zsucc_Zpred: +\forall x,y. eq Z (Zplus x y) (Zplus (Zsucc x) (Zpred y)). +intros. +elim x. elim y. +simplify.reflexivity. +simplify.reflexivity. +rewrite < Zsucc_Zplus_pos_O. +rewrite > Zsucc_Zpred.reflexivity. +elim y.rewrite < sym_Zplus.rewrite < sym_Zplus (Zpred OZ). +rewrite < Zpred_Zplus_neg_O. +rewrite > Zpred_Zsucc. +simplify.reflexivity. +rewrite < Zplus_neg_neg.reflexivity. +apply Zplus_neg_pos. +elim y.simplify.reflexivity. +apply Zplus_pos_neg. +apply Zplus_pos_pos. +qed. + +theorem Zplus_Zsucc_pos_pos : +\forall n,m. eq Z (Zplus (Zsucc (pos n)) (pos m)) (Zsucc (Zplus (pos n) (pos m))). +intros.reflexivity. +qed. + +theorem Zplus_Zsucc_pos_neg: +\forall n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m))). +intros. +apply nat_elim2 +(\lambda n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m)))).intro. +intros.elim n1. +simplify. reflexivity. +elim e1.simplify. reflexivity. +simplify. reflexivity. +intros. elim n1. +simplify. reflexivity. +simplify.reflexivity. +intros. +rewrite < (Zplus_pos_neg ? m1). +elim H.reflexivity. +qed. + +theorem Zplus_Zsucc_neg_neg : +\forall n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m))). +intros. +apply nat_elim2 +(\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m)))).intro. +intros.elim n1. +simplify. reflexivity. +elim e1.simplify. reflexivity. +simplify. reflexivity. +intros. elim n1. +simplify. reflexivity. +simplify.reflexivity. +intros. +rewrite < (Zplus_neg_neg ? m1). +reflexivity. +qed. + +theorem Zplus_Zsucc_neg_pos: +\forall n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m))). +intros. +apply nat_elim2 +(\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m)))). +intros.elim n1. +simplify. reflexivity. +elim e1.simplify. reflexivity. +simplify. reflexivity. +intros. elim n1. +simplify. reflexivity. +simplify.reflexivity. +intros. +rewrite < H. +rewrite < (Zplus_neg_pos ? (S m1)). +reflexivity. +qed. + +theorem Zplus_Zsucc : \forall x,y:Z. eq Z (Zplus (Zsucc x) y) (Zsucc (Zplus x y)). +intros.elim x.elim y. +simplify. reflexivity. +rewrite < Zsucc_Zplus_pos_O.reflexivity. +simplify.reflexivity. +elim y.rewrite < sym_Zplus.rewrite < sym_Zplus OZ.simplify.reflexivity. +apply Zplus_Zsucc_neg_neg. +apply Zplus_Zsucc_neg_pos. +elim y. +rewrite < sym_Zplus OZ.reflexivity. +apply Zplus_Zsucc_pos_neg. +apply Zplus_Zsucc_pos_pos. +qed. + +theorem Zplus_Zpred: \forall x,y:Z. eq Z (Zplus (Zpred x) y) (Zpred (Zplus x y)). +intros. +cut eq Z (Zpred (Zplus x y)) (Zpred (Zplus (Zsucc (Zpred x)) y)). +rewrite > Hcut. +rewrite > Zplus_Zsucc. +rewrite > Zpred_Zsucc. +reflexivity. +rewrite > Zsucc_Zpred. +reflexivity. +qed. + + +theorem associative_Zplus: associative Z Zplus. +change with \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z)). + +intros.elim x.simplify.reflexivity. +elim e1.rewrite < (Zpred_Zplus_neg_O (Zplus y z)). +rewrite < (Zpred_Zplus_neg_O y). +rewrite < Zplus_Zpred. +reflexivity. +rewrite > Zplus_Zpred (neg e). +rewrite > Zplus_Zpred (neg e). +rewrite > Zplus_Zpred (Zplus (neg e) y). +apply eq_f.assumption. +elim e2.rewrite < Zsucc_Zplus_pos_O. +rewrite < Zsucc_Zplus_pos_O. +rewrite > Zplus_Zsucc. +reflexivity. +rewrite > Zplus_Zsucc (pos e1). +rewrite > Zplus_Zsucc (pos e1). +rewrite > Zplus_Zsucc (Zplus (pos e1) y). +apply eq_f.assumption. +qed. + +variant assoc_Zplus : \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z)) +\def associative_Zplus. + +definition Zopp : Z \to Z \def +\lambda x:Z. match x with +[ OZ \Rightarrow OZ +| (pos n) \Rightarrow (neg n) +| (neg n) \Rightarrow (pos n) ]. + +theorem Zplus_Zopp: \forall x:Z. (eq Z (Zplus x (Zopp x)) OZ). +intro.elim x. +apply refl_eq. +simplify. +rewrite > nat_compare_n_n. +simplify.apply refl_eq. +simplify. +rewrite > nat_compare_n_n. +simplify.apply refl_eq. +qed. +*) diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma index afe80e736..5aa5d9083 100644 --- a/helm/matita/library/Z/z.ma +++ b/helm/matita/library/Z/z.ma @@ -56,13 +56,13 @@ match OZ_test z with intros.elim z. simplify.reflexivity. simplify.intros. -cut match neg e1 with +cut match neg n with [ OZ \Rightarrow True | (pos n) \Rightarrow False | (neg n) \Rightarrow False]. apply Hcut.rewrite > H.simplify.exact I. simplify.intros. -cut match pos e2 with +cut match pos n with [ OZ \Rightarrow True | (pos n) \Rightarrow False | (neg n) \Rightarrow False]. @@ -89,7 +89,7 @@ definition Zpred \def theorem Zpred_Zsucc: \forall z:Z. eq Z (Zpred (Zsucc z)) z. intros.elim z.reflexivity. -elim e1.reflexivity. +elim n.reflexivity. reflexivity. reflexivity. qed. @@ -97,7 +97,7 @@ qed. theorem Zsucc_Zpred: \forall z:Z. eq Z (Zsucc (Zpred z)) z. intros.elim z.reflexivity. reflexivity. -elim e2.reflexivity. +elim n.reflexivity. reflexivity. qed. @@ -155,14 +155,14 @@ theorem Zpred_Zplus_neg_O : \forall z:Z. eq Z (Zpred z) (Zplus (neg O) z). intros.elim z. simplify.reflexivity. simplify.reflexivity. -elim e2.simplify.reflexivity. +elim n.simplify.reflexivity. simplify.reflexivity. qed. theorem Zsucc_Zplus_pos_O : \forall z:Z. eq Z (Zsucc z) (Zplus (pos O) z). intros.elim z. simplify.reflexivity. -elim e1.simplify.reflexivity. +elim n.simplify.reflexivity. simplify.reflexivity. simplify.reflexivity. qed. @@ -238,7 +238,7 @@ apply nat_elim2 (\lambda n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m)))).intro. intros.elim n1. simplify. reflexivity. -elim e1.simplify. reflexivity. +elim n2.simplify. reflexivity. simplify. reflexivity. intros. elim n1. simplify. reflexivity. @@ -255,7 +255,7 @@ apply nat_elim2 (\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m)))).intro. intros.elim n1. simplify. reflexivity. -elim e1.simplify. reflexivity. +elim n2.simplify. reflexivity. simplify. reflexivity. intros. elim n1. simplify. reflexivity. @@ -272,7 +272,7 @@ apply nat_elim2 (\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m)))). intros.elim n1. simplify. reflexivity. -elim e1.simplify. reflexivity. +elim n2.simplify. reflexivity. simplify. reflexivity. intros. elim n1. simplify. reflexivity. @@ -313,21 +313,21 @@ theorem associative_Zplus: associative Z Zplus. change with \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z)). (* simplify. *) intros.elim x.simplify.reflexivity. -elim e1.rewrite < (Zpred_Zplus_neg_O (Zplus y z)). +elim n.rewrite < (Zpred_Zplus_neg_O (Zplus y z)). rewrite < (Zpred_Zplus_neg_O y). rewrite < Zplus_Zpred. reflexivity. -rewrite > Zplus_Zpred (neg e). -rewrite > Zplus_Zpred (neg e). -rewrite > Zplus_Zpred (Zplus (neg e) y). +rewrite > Zplus_Zpred (neg n1). +rewrite > Zplus_Zpred (neg n1). +rewrite > Zplus_Zpred (Zplus (neg n1) y). apply eq_f.assumption. -elim e2.rewrite < Zsucc_Zplus_pos_O. +elim n.rewrite < Zsucc_Zplus_pos_O. rewrite < Zsucc_Zplus_pos_O. rewrite > Zplus_Zsucc. reflexivity. -rewrite > Zplus_Zsucc (pos e1). -rewrite > Zplus_Zsucc (pos e1). -rewrite > Zplus_Zsucc (Zplus (pos e1) y). +rewrite > Zplus_Zsucc (pos n1). +rewrite > Zplus_Zsucc (pos n1). +rewrite > Zplus_Zsucc (Zplus (pos n1) y). apply eq_f.assumption. qed. diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma new file mode 100644 index 000000000..2b00a97ab --- /dev/null +++ b/helm/matita/library/nat/div_and_mod.ma @@ -0,0 +1,178 @@ +(**************************************************************************) +(* ___ *) +(* ||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 diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma index ff41ba62e..f84ffef44 100644 --- a/helm/matita/library/nat/nat.ma +++ b/helm/matita/library/nat/nat.ma @@ -1,5 +1,5 @@ (**************************************************************************) -(* ___ *) +(* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma index b8e92fa2b..d4979231d 100644 --- a/helm/matita/library/nat/orders.ma +++ b/helm/matita/library/nat/orders.ma @@ -64,7 +64,7 @@ qed. theorem le_S_S_to_le : \forall n,m:nat. le (S n) (S m) \to le n m. intros.change with le (pred (S n)) (pred (S m)). -elim H.apply le_n.apply trans_le ? (pred e2).assumption. +elim H.apply le_n.apply trans_le ? (pred n1).assumption. apply le_pred_n. qed. @@ -78,7 +78,7 @@ intros.simplify.intros.apply leS_to_not_zero ? ? H. qed. theorem not_le_Sn_n: \forall n:nat. Not (le (S n) n). -intros.elim n.apply not_le_Sn_O.simplify.intros.cut le (S e1) e1. +intros.elim n.apply not_le_Sn_O.simplify.intros.cut le (S n1) n1. apply H.assumption. apply le_S_S_to_le.assumption. qed. diff --git a/helm/matita/library/nat/times.ma b/helm/matita/library/nat/times.ma index 44f73b71a..953b3a1b6 100644 --- a/helm/matita/library/nat/times.ma +++ b/helm/matita/library/nat/times.ma @@ -34,8 +34,8 @@ theorem times_n_Sm : intros.elim n. simplify.reflexivity. simplify.apply eq_f.rewrite < H. -transitivity (plus (plus e1 m) (times e1 m)).symmetry.apply assoc_plus. -transitivity (plus (plus m e1) (times e1 m)). +transitivity (plus (plus n1 m) (times n1 m)).symmetry.apply assoc_plus. +transitivity (plus (plus m n1) (times n1 m)). apply eq_f2. apply sym_plus. reflexivity. @@ -52,11 +52,16 @@ simplify.apply times_n_O. simplify.rewrite > H.apply times_n_Sm. qed. -theorem times_plus_distr: \forall n,m,p:nat. -eq nat (times n (plus m p)) (plus (times n m) (times n p)). -intros.elim n. +theorem distributive_times_plus : distributive nat times plus. +simplify. +intros.elim x. simplify.reflexivity. simplify.rewrite > H. rewrite > assoc_plus.rewrite > assoc_plus. -apply eq_f.rewrite < assoc_plus. rewrite < sym_plus ? p. +apply eq_f.rewrite < assoc_plus. rewrite < sym_plus ? z. rewrite > assoc_plus.reflexivity. qed. + +variant times_plus_distr: \forall n,m,p:nat. +eq nat (times n (plus m p)) (plus (times n m) (times n p)) +\def distributive_times_plus. + -- 2.39.2