From 68a2f8d0a8c34cb7ea0438c7db9222a853a38826 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 24 Jul 2006 14:50:33 +0000 Subject: [PATCH] A compiling version of the library. --- helm/software/matita/library/Z/plus.ma | 4 + helm/software/matita/library/Z/z.ma | 6 +- .../matita/library/datatypes/constructors.ma | 11 ++ .../library/higher_order_defs/relations.ma | 26 ++++- .../software/matita/library/logic/equality.ma | 2 +- .../matita/library/nat/div_and_mod.ma | 1 + helm/software/matita/library/nat/ord.ma | 105 +++++++++++++++++- helm/software/matita/library/nat/times.ma | 7 ++ 8 files changed, 151 insertions(+), 11 deletions(-) diff --git a/helm/software/matita/library/Z/plus.ma b/helm/software/matita/library/Z/plus.ma index 976f6cfb3..2b439b92e 100644 --- a/helm/software/matita/library/Z/plus.ma +++ b/helm/software/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/helm/software/matita/library/Z/z.ma b/helm/software/matita/library/Z/z.ma index ea50a2cd9..9532ea95d 100644 --- a/helm/software/matita/library/Z/z.ma +++ b/helm/software/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/helm/software/matita/library/datatypes/constructors.ma b/helm/software/matita/library/datatypes/constructors.ma index 2ac1cb376..3f74db5ad 100644 --- a/helm/software/matita/library/datatypes/constructors.ma +++ b/helm/software/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/helm/software/matita/library/higher_order_defs/relations.ma b/helm/software/matita/library/higher_order_defs/relations.ma index 029b229dc..3e92649c1 100644 --- a/helm/software/matita/library/higher_order_defs/relations.ma +++ b/helm/software/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/helm/software/matita/library/logic/equality.ma b/helm/software/matita/library/logic/equality.ma index 95cb97307..129b00189 100644 --- a/helm/software/matita/library/logic/equality.ma +++ b/helm/software/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/helm/software/matita/library/nat/div_and_mod.ma b/helm/software/matita/library/nat/div_and_mod.ma index a9f40cc89..73ff78998 100644 --- a/helm/software/matita/library/nat/div_and_mod.ma +++ b/helm/software/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/helm/software/matita/library/nat/ord.ma b/helm/software/matita/library/nat/ord.ma index 807d26733..e9353ba5b 100644 --- a/helm/software/matita/library/nat/ord.ma +++ b/helm/software/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/helm/software/matita/library/nat/times.ma b/helm/software/matita/library/nat/times.ma index 2ae5ffd74..c2f25e731 100644 --- a/helm/software/matita/library/nat/times.ma +++ b/helm/software/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