New naming policy for local variables.

diff --git a/helm/matita/library/Z/orders.ma b/helm/matita/library/Z/orders.ma
new file mode 100644 (file)
index 0000000..1a2d65a
--- /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 (file)
index 0000000..6e7a59d
--- /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 afe80e736030489184d85257a693ecb08316e466..5aa5d90832a7359dc9da1d20d6581c1e1a3b7a21 100644 (file)
--- 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 (file)
index 0000000..2b00a97
--- /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 ff41ba62e25e2844b18240ddf80ba36a0bc52cdf..f84ffef44cd44bb8da092f5011c48b483cb8e8e0 100644 (file)
--- 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 b8e92fa2b6987f34cfecbf81841bee405d10ca0a..d4979231d1d1d46a0b4a7cea579c086fef3bdb62 100644 (file)
--- 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 44f73b71a080b6e253d49b5dfbb2e1b622d45174..953b3a1b630321187f46f9c2199e8b3dde12a928 100644 (file)
--- 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.
+