From 5a702cea95883f7095c16b450e065ccb1714fc5a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 19 Sep 2005 09:20:00 +0000 Subject: [PATCH] .ma inclusions corrected/minimized --- helm/matita/library/Q/q.ma | 1 - helm/matita/library/Z/compare.ma | 2 -- helm/matita/library/Z/plus.ma | 1 - helm/matita/library/Z/times.ma | 1 - helm/matita/library/Z/z.ma | 2 +- helm/matita/library/higher_order_defs/functions.ma | 1 - helm/matita/library/logic/equality.ma | 1 - helm/matita/library/nat/div_and_mod.ma | 2 -- helm/matita/library/nat/exp.ma | 11 ++++------- helm/matita/library/nat/factorial.ma | 2 +- helm/matita/library/nat/gcd.ma | 1 - helm/matita/library/nat/le_arith.ma | 2 -- helm/matita/library/nat/log.ma | 3 ++- helm/matita/library/nat/lt_arith.ma | 1 - helm/matita/library/nat/nat.ma | 3 --- helm/matita/library/nat/nth_prime.ma | 1 + helm/matita/library/nat/orders.ma | 2 +- helm/matita/library/nat/primes1.ma | 1 - helm/matita/library/nat/sigma_and_pi.ma | 5 +---- 19 files changed, 11 insertions(+), 32 deletions(-) diff --git a/helm/matita/library/Q/q.ma b/helm/matita/library/Q/q.ma index d7c2816a1..4878078fc 100644 --- a/helm/matita/library/Q/q.ma +++ b/helm/matita/library/Q/q.ma @@ -16,7 +16,6 @@ set "baseuri" "cic:/matita/Q/q". include "Z/compare.ma". include "Z/plus.ma". -include "higher_order_defs/functions.ma". (* a fraction is a list of Z-coefficients for primes, in natural order. The last coefficient must eventually be different from 0 *) diff --git a/helm/matita/library/Z/compare.ma b/helm/matita/library/Z/compare.ma index a8f8aca39..3b259b4f6 100644 --- a/helm/matita/library/Z/compare.ma +++ b/helm/matita/library/Z/compare.ma @@ -14,8 +14,6 @@ set "baseuri" "cic:/matita/Z/compare". -include "datatypes/bool.ma". -include "datatypes/compare.ma". include "Z/orders.ma". include "nat/compare.ma". diff --git a/helm/matita/library/Z/plus.ma b/helm/matita/library/Z/plus.ma index 56b960403..dc743e60b 100644 --- a/helm/matita/library/Z/plus.ma +++ b/helm/matita/library/Z/plus.ma @@ -15,7 +15,6 @@ set "baseuri" "cic:/matita/Z/plus". include "Z/z.ma". -include "nat/compare.ma". include "nat/minus.ma". definition Zplus :Z \to Z \to Z \def diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma index 72e8177b8..c4e965fbf 100644 --- a/helm/matita/library/Z/times.ma +++ b/helm/matita/library/Z/times.ma @@ -16,7 +16,6 @@ set "baseuri" "cic:/matita/Z/times". include "nat/lt_arith.ma". include "Z/plus.ma". -include "higher_order_defs/functions.ma". definition Ztimes :Z \to Z \to Z \def \lambda x,y. diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma index 207457a91..997229763 100644 --- a/helm/matita/library/Z/z.ma +++ b/helm/matita/library/Z/z.ma @@ -14,8 +14,8 @@ set "baseuri" "cic:/matita/Z/z". +include "datatypes/bool.ma". include "nat/nat.ma". -include "higher_order_defs/functions.ma". inductive Z : Set \def OZ : Z diff --git a/helm/matita/library/higher_order_defs/functions.ma b/helm/matita/library/higher_order_defs/functions.ma index 71b6d8459..da90d4211 100644 --- a/helm/matita/library/higher_order_defs/functions.ma +++ b/helm/matita/library/higher_order_defs/functions.ma @@ -15,7 +15,6 @@ set "baseuri" "cic:/matita/higher_order_defs/functions/". include "logic/equality.ma". -include "logic/connectives.ma". definition injective: \forall A,B:Type.\forall f:A \to B.Prop \def \lambda A,B.\lambda f. diff --git a/helm/matita/library/logic/equality.ma b/helm/matita/library/logic/equality.ma index 84f7df2e6..a5d2f0d1e 100644 --- a/helm/matita/library/logic/equality.ma +++ b/helm/matita/library/logic/equality.ma @@ -15,7 +15,6 @@ set "baseuri" "cic:/matita/logic/equality/". include "higher_order_defs/relations.ma". -include "logic/connectives.ma". inductive eq (A:Type) (x:A) : A \to Prop \def refl_eq : eq A x x. diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma index 73f90e553..ede15596a 100644 --- a/helm/matita/library/nat/div_and_mod.ma +++ b/helm/matita/library/nat/div_and_mod.ma @@ -15,8 +15,6 @@ set "baseuri" "cic:/matita/nat/div_and_mod". include "nat/minus.ma". -include "nat/le_arith.ma". -include "nat/compare.ma". let rec mod_aux p m n: nat \def match (leb m n) with diff --git a/helm/matita/library/nat/exp.ma b/helm/matita/library/nat/exp.ma index 2f0bfbeaf..a80a0cee3 100644 --- a/helm/matita/library/nat/exp.ma +++ b/helm/matita/library/nat/exp.ma @@ -14,9 +14,7 @@ set "baseuri" "cic:/matita/nat/exp". -include "nat/times.ma". -include "nat/orders.ma". -include "higher_order_defs/functions.ma". +include "nat/div_and_mod.ma". let rec exp n m on m\def match m with @@ -88,11 +86,10 @@ assumption. intros 2. apply nat_case n. intros.apply False_ind.apply not_le_Sn_O O H3. -intros.apply inj_times_r m1.assumption. +intros. +apply inj_times_r m1.assumption. qed. variant inj_exp_r: \forall p:nat. (S O) < p \to \forall n,m:nat. (exp p n) = (exp p m) \to n = m \def -injective_exp_r. - - +injective_exp_r. \ No newline at end of file diff --git a/helm/matita/library/nat/factorial.ma b/helm/matita/library/nat/factorial.ma index 742ca2a3b..50345ee12 100644 --- a/helm/matita/library/nat/factorial.ma +++ b/helm/matita/library/nat/factorial.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/nat/factorial". -include "nat/lt_arith.ma". +include "nat/le_arith.ma". let rec fact n \def match n with diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma index 921d8853e..587314315 100644 --- a/helm/matita/library/nat/gcd.ma +++ b/helm/matita/library/nat/gcd.ma @@ -15,7 +15,6 @@ set "baseuri" "cic:/matita/nat/gcd". include "nat/primes.ma". -include "higher_order_defs/functions.ma". let rec gcd_aux p m n: nat \def match divides_b n m with diff --git a/helm/matita/library/nat/le_arith.ma b/helm/matita/library/nat/le_arith.ma index a36f96bd4..dbf7b1c42 100644 --- a/helm/matita/library/nat/le_arith.ma +++ b/helm/matita/library/nat/le_arith.ma @@ -14,10 +14,8 @@ set "baseuri" "cic:/matita/nat/le_arith". -include "higher_order_defs/functions.ma". include "nat/times.ma". include "nat/orders.ma". -include "nat/compare.ma". (* plus *) theorem monotonic_le_plus_r: diff --git a/helm/matita/library/nat/log.ma b/helm/matita/library/nat/log.ma index e24c3031f..301c0be8e 100644 --- a/helm/matita/library/nat/log.ma +++ b/helm/matita/library/nat/log.ma @@ -15,8 +15,9 @@ set "baseuri" "cic:/matita/nat/log". include "datatypes/constructors.ma". -include "nat/primes.ma". include "nat/exp.ma". +include "nat/lt_arith.ma". +include "nat/primes.ma". (* this definition of log is based on pairs, with a remainder *) diff --git a/helm/matita/library/nat/lt_arith.ma b/helm/matita/library/nat/lt_arith.ma index 85280fe0f..dd4fdcbf9 100644 --- a/helm/matita/library/nat/lt_arith.ma +++ b/helm/matita/library/nat/lt_arith.ma @@ -14,7 +14,6 @@ set "baseuri" "cic:/matita/nat/lt_arith". -include "nat/exp.ma". include "nat/div_and_mod.ma". (* plus *) diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma index f8ff252ae..100cb0f03 100644 --- a/helm/matita/library/nat/nat.ma +++ b/helm/matita/library/nat/nat.ma @@ -14,9 +14,6 @@ set "baseuri" "cic:/matita/nat/nat". -include "datatypes/bool.ma". -include "logic/equality.ma". -include "logic/connectives.ma". include "higher_order_defs/functions.ma". inductive nat : Set \def diff --git a/helm/matita/library/nat/nth_prime.ma b/helm/matita/library/nat/nth_prime.ma index ee21195dc..37c60b405 100644 --- a/helm/matita/library/nat/nth_prime.ma +++ b/helm/matita/library/nat/nth_prime.ma @@ -15,6 +15,7 @@ set "baseuri" "cic:/matita/nat/nth_prime". include "nat/primes.ma". +include "nat/lt_arith.ma". (* upper bound by Bertrand's conjecture. *) (* Too difficult to prove. diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma index 811706867..a162df9a3 100644 --- a/helm/matita/library/nat/orders.ma +++ b/helm/matita/library/nat/orders.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/nat/orders". -include "nat/plus.ma". +include "nat/nat.ma". include "higher_order_defs/ordering.ma". (* definitions *) diff --git a/helm/matita/library/nat/primes1.ma b/helm/matita/library/nat/primes1.ma index 55d643262..3df3922a4 100644 --- a/helm/matita/library/nat/primes1.ma +++ b/helm/matita/library/nat/primes1.ma @@ -16,7 +16,6 @@ set "baseuri" "cic:/matita/nat/primes1". include "datatypes/constructors.ma". include "nat/primes.ma". -include "nat/exp.ma". (* p is just an upper bound, acc is an accumulator *) let rec n_divides_aux p n m acc \def diff --git a/helm/matita/library/nat/sigma_and_pi.ma b/helm/matita/library/nat/sigma_and_pi.ma index b9b8065aa..29df3a1df 100644 --- a/helm/matita/library/nat/sigma_and_pi.ma +++ b/helm/matita/library/nat/sigma_and_pi.ma @@ -24,7 +24,4 @@ let rec sigma n f \def let rec pi n f \def match n with [ O \Rightarrow (S O) - | (S p) \Rightarrow (f p)*(pi p f)]. - - - + | (S p) \Rightarrow (f p)*(pi p f)]. \ No newline at end of file -- 2.39.2