From bec691ac68b66ca288ac0280871afb6597259446 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 24 Jul 2006 14:50:33 +0000
Subject: [PATCH] A compiling version of the library.

---
 matita/library/Z/plus.ma                      |   4 +
 matita/library/Z/z.ma                         |   6 +-
 matita/library/datatypes/constructors.ma      |  11 ++
 matita/library/higher_order_defs/relations.ma |  26 ++++-
 matita/library/logic/equality.ma              |   2 +-
 matita/library/nat/div_and_mod.ma             |   1 +
 matita/library/nat/ord.ma                     | 105 +++++++++++++++++-
 matita/library/nat/times.ma                   |   7 ++
 8 files changed, 151 insertions(+), 11 deletions(-)

diff --git a/matita/library/Z/plus.ma b/matita/library/Z/plus.ma
index 976f6cfb3..2b439b92e 100644
--- a/matita/library/Z/plus.ma
+++ b/matita/library/Z/plus.ma
@@ -299,3 +299,7 @@ rewrite > nat_compare_n_n.
 simplify.apply refl_eq.
 qed.
 
+(* minus *)
+definition Zminus : Z \to Z \to Z \def \lambda x,y:Z. x + (-y).
+
+interpretation "integer minus" 'minus x y = (cic:/matita/Z/plus/Zminus.con x y).
diff --git a/matita/library/Z/z.ma b/matita/library/Z/z.ma
index ea50a2cd9..9532ea95d 100644
--- a/matita/library/Z/z.ma
+++ b/matita/library/Z/z.ma
@@ -38,8 +38,8 @@ definition abs \def
 \lambda z.
  match z with 
 [ OZ \Rightarrow O
-| (pos n) \Rightarrow n
-| (neg n) \Rightarrow n].
+| (pos n) \Rightarrow (S n)
+| (neg n) \Rightarrow (S n)].
 
 definition OZ_test \def
 \lambda z.
@@ -64,6 +64,7 @@ qed.
 theorem injective_pos: injective nat Z pos.
 unfold injective.
 intros.
+apply inj_S.
 change with (abs (pos x) = abs (pos y)).
 apply eq_f.assumption.
 qed.
@@ -74,6 +75,7 @@ variant inj_pos : \forall n,m:nat. pos n = pos m \to n = m
 theorem injective_neg: injective nat Z neg.
 unfold injective.
 intros.
+apply inj_S.
 change with (abs (neg x) = abs (neg y)).
 apply eq_f.assumption.
 qed.
diff --git a/matita/library/datatypes/constructors.ma b/matita/library/datatypes/constructors.ma
index 2ac1cb376..3f74db5ad 100644
--- a/matita/library/datatypes/constructors.ma
+++ b/matita/library/datatypes/constructors.ma
@@ -36,3 +36,14 @@ qed.
 inductive Sum (A,B:Set) : Set \def
   inl : A \to Sum A B
 | inr : B \to Sum A B.
+
+inductive ProdT (A,B:Type) : Type \def
+pairT : A \to B \to ProdT A B.
+
+definition fstT \def \lambda A,B:Type.\lambda p: ProdT A B.
+match p with
+[(pairT a b) \Rightarrow a]. 
+
+definition sndT \def \lambda A,B:Type.\lambda p: ProdT A B.
+match p with
+[(pairT a b) \Rightarrow b].
\ No newline at end of file
diff --git a/matita/library/higher_order_defs/relations.ma b/matita/library/higher_order_defs/relations.ma
index 029b229dc..3e92649c1 100644
--- a/matita/library/higher_order_defs/relations.ma
+++ b/matita/library/higher_order_defs/relations.ma
@@ -16,18 +16,36 @@ set "baseuri" "cic:/matita/higher_order_defs/relations/".
 
 include "logic/connectives.ma".
 
-definition reflexive: \forall A:Type.\forall R:A \to A \to Prop.Prop
+definition relation : Type \to Type
+\def \lambda A:Type.A \to A \to Prop. 
+
+definition reflexive: \forall A:Type.\forall R :relation A.Prop
 \def 
 \lambda A.\lambda R.\forall x:A.R x x.
 
-definition symmetric: \forall A:Type.\forall R:A \to A \to Prop.Prop
+definition symmetric: \forall A:Type.\forall R: relation A.Prop
 \def 
 \lambda A.\lambda R.\forall x,y:A.R x y \to R y x.
 
-definition transitive: \forall A:Type.\forall R:A \to A \to Prop.Prop
+definition transitive: \forall A:Type.\forall R:relation A.Prop
 \def 
 \lambda A.\lambda R.\forall x,y,z:A.R x y \to R y z \to R x z.
 
-definition irreflexive: \forall A:Type.\forall R:A \to A \to Prop.Prop
+definition irreflexive: \forall A:Type.\forall R:relation A.Prop
 \def 
 \lambda A.\lambda R.\forall x:A.\lnot (R x x).
+
+definition cotransitive: \forall A:Type.\forall R:relation A.Prop
+\def
+\lambda A.\lambda R.\forall x,y:A.R x y \to \forall z:A. R x z \lor R z y.
+
+definition tight_apart: \forall A:Type.\forall eq,ap:relation A.Prop
+\def 
+\lambda A.\lambda eq,ap.\forall x,y:A. (\not (ap x y) \to eq x y) \land
+(eq x y \to \not (ap x y)).
+
+definition antisymmetric: \forall A:Type.\forall R:relation A.Prop
+\def 
+\lambda A.\lambda R.\forall x,y:A. R x y \to \not (R y x).
+
+
diff --git a/matita/library/logic/equality.ma b/matita/library/logic/equality.ma
index 95cb97307..129b00189 100644
--- a/matita/library/logic/equality.ma
+++ b/matita/library/logic/equality.ma
@@ -67,7 +67,7 @@ default "equality"
  cic:/matita/logic/equality/eq_ind.con
  cic:/matita/logic/equality/eq_elim_r.con
  cic:/matita/logic/equality/eq_f.con
- cic:/matita/logic/equality/eq_OF_eq.con. (* \x.sym (eq_f x) *)
+ cic:/matita/logic/equality/eq_f1.con. (* \x.sym (eq_f x) *)
 
  
 theorem eq_f: \forall  A,B:Type.\forall f:A\to B.
diff --git a/matita/library/nat/div_and_mod.ma b/matita/library/nat/div_and_mod.ma
index a9f40cc89..73ff78998 100644
--- a/matita/library/nat/div_and_mod.ma
+++ b/matita/library/nat/div_and_mod.ma
@@ -14,6 +14,7 @@
 
 set "baseuri" "cic:/matita/nat/div_and_mod".
 
+include "datatypes/constructors.ma".
 include "nat/minus.ma".
 
 let rec mod_aux p m n: nat \def
diff --git a/matita/library/nat/ord.ma b/matita/library/nat/ord.ma
index 807d26733..e9353ba5b 100644
--- a/matita/library/nat/ord.ma
+++ b/matita/library/nat/ord.ma
@@ -12,12 +12,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/log".
+set "baseuri" "cic:/matita/nat/ord".
 
 include "datatypes/constructors.ma".
 include "nat/exp.ma".
-include "nat/lt_arith.ma".
-include "nat/primes.ma".
+include "nat/gcd.ma".
 
 (* this definition of log is based on pairs, with a remainder *)
 
@@ -68,6 +67,7 @@ rewrite > H1.
 apply p_ord_aux_to_Prop.
 assumption.
 qed.
+
 (* questo va spostato in primes1.ma *)
 theorem p_ord_exp: \forall n,m,i. O < m \to n \mod m \neq O \to
 \forall p. i \le p \to p_ord_aux p (m \sup i * n) m = pair nat nat i n.
@@ -142,4 +142,101 @@ rewrite > H3.
 apply p_ord_aux_to_Prop1.
 assumption.assumption.assumption.
 qed.
-  
+
+theorem p_ord_exp1: \forall p,n,q,r. O < p \to \lnot p \divides r \to
+n = p \sup q * r \to p_ord n p = pair nat nat q r.
+intros.unfold p_ord.
+rewrite > H2.
+apply p_ord_exp
+ [assumption
+ |unfold.intro.apply H1.
+  apply mod_O_to_divides[assumption|assumption]
+ |apply (trans_le ? (p \sup q)).
+  cut ((S O) \lt p).
+  elim q.simplify.apply le_n_Sn.
+  simplify.
+  generalize in match H3.
+  apply (nat_case n1).simplify.
+  rewrite < times_n_SO.intro.assumption.
+  intros.
+  apply (trans_le ? (p*(S m))).
+  apply (trans_le ? ((S (S O))*(S m))).
+  simplify.rewrite > plus_n_Sm.
+  rewrite < plus_n_O.
+  apply le_plus_n.
+  apply le_times_l.
+  assumption.
+  apply le_times_r.assumption.
+  alias id "not_eq_to_le_to_lt" = "cic:/matita/algebra/finite_groups/not_eq_to_le_to_lt.con".
+apply not_eq_to_le_to_lt.
+  unfold.intro.apply H1.
+  rewrite < H3.
+  apply (witness ? r r ?).simplify.apply plus_n_O.
+  assumption.
+  rewrite > times_n_SO in \vdash (? % ?).
+  apply le_times_r.
+  change with (O \lt r).
+  apply not_eq_to_le_to_lt.
+  unfold.intro.
+  apply H1.rewrite < H3.
+  apply (witness ? ? O ?).rewrite < times_n_O.reflexivity.
+  apply le_O_n.
+  ]
+qed.
+
+theorem p_ord_to_exp1: \forall p,n,q,r. (S O) \lt p \to O \lt n \to p_ord n p = pair nat nat q r\to 
+\lnot p \divides r \land n = p \sup q * r.
+intros.
+unfold p_ord in H2.
+split.unfold.intro.
+apply (p_ord_aux_to_not_mod_O n n p q r).assumption.assumption.
+apply le_n.symmetry.assumption.
+apply divides_to_mod_O.apply (trans_lt ? (S O)).
+unfold.apply le_n.assumption.assumption.
+apply (p_ord_aux_to_exp n).apply (trans_lt ? (S O)).
+unfold.apply le_n.assumption.symmetry.assumption.
+qed.
+
+theorem p_ord_times: \forall p,a,b,qa,ra,qb,rb. prime p 
+\to O \lt a \to O \lt b 
+\to p_ord a p = pair nat nat qa ra  
+\to p_ord b p = pair nat nat qb rb
+\to p_ord (a*b) p = pair nat nat (qa + qb) (ra*rb).
+intros.
+cut ((S O) \lt p).
+elim (p_ord_to_exp1 ? ? ? ? Hcut H1 H3).
+elim (p_ord_to_exp1 ? ? ? ? Hcut H2 H4).
+apply p_ord_exp1.
+apply (trans_lt ? (S O)).unfold.apply le_n.assumption.
+unfold.intro.
+elim (divides_times_to_divides ? ? ? H H9).
+apply (absurd ? ? H10 H5).
+apply (absurd ? ? H10 H7).
+rewrite > H6.
+rewrite > H8.
+auto paramodulation.
+unfold prime in H. elim H. assumption.
+qed.
+
+theorem fst_p_ord_times: \forall p,a,b. prime p 
+\to O \lt a \to O \lt b 
+\to fst ? ? (p_ord (a*b) p) = (fst ? ? (p_ord a p)) + (fst ? ? (p_ord b p)).
+intros.
+rewrite > (p_ord_times p a b (fst ? ? (p_ord a p)) (snd ? ? (p_ord a p))
+(fst ? ? (p_ord b p)) (snd ? ? (p_ord b p)) H H1 H2).
+simplify.reflexivity.
+apply eq_pair_fst_snd.
+apply eq_pair_fst_snd.
+qed.
+
+theorem p_ord_p : \forall p:nat. (S O) \lt p \to p_ord p p = pair ? ? (S O) (S O).
+intros.
+apply p_ord_exp1.
+apply (trans_lt ? (S O)). unfold.apply le_n.assumption.
+unfold.intro.
+apply (absurd ? ? H).
+apply le_to_not_lt.
+apply divides_to_le.unfold.apply le_n.assumption.
+rewrite < times_n_SO.
+apply exp_n_SO.
+qed.
\ No newline at end of file
diff --git a/matita/library/nat/times.ma b/matita/library/nat/times.ma
index 2ae5ffd74..c2f25e731 100644
--- a/matita/library/nat/times.ma
+++ b/matita/library/nat/times.ma
@@ -51,6 +51,13 @@ rewrite < plus_n_O.
 reflexivity.
 qed.
 
+theorem times_SSO_n : \forall n:nat. n + n = S (S O) * n.
+intros.
+simplify.
+rewrite < plus_n_O.
+reflexivity.
+qed.
+
 theorem symmetric_times : symmetric nat times. 
 unfold symmetric.
 intros.elim x.
-- 
2.39.2