From a42d4bd78f10ac8fc725c50c193503a3f29b848f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Nov 2007 11:56:08 +0000 Subject: [PATCH] major reorganization (read cleanup) --- .../matita/dama/{ => attic}/fields.ma | 2 +- .../dama/{ => attic}/integration_algebras.ma | 2 +- .../dama/{ => attic}/ordered_fields_ch0.ma | 4 +-- .../software/matita/dama/{ => attic}/reals.ma | 4 +-- .../software/matita/dama/{ => attic}/rings.ma | 2 +- .../matita/dama/{ => attic}/vector_spaces.ma | 2 +- .../matita/dama/{groups.ma => group.ma} | 26 +++++++++---------- helm/software/matita/dama/metric_space.ma | 2 +- .../{ordered_groups.ma => ordered_group.ma} | 10 +++---- .../matita/dama/preweighted_lattice.ma | 2 +- 10 files changed, 28 insertions(+), 28 deletions(-) rename helm/software/matita/dama/{ => attic}/fields.ma (98%) rename helm/software/matita/dama/{ => attic}/integration_algebras.ma (99%) rename helm/software/matita/dama/{ => attic}/ordered_fields_ch0.ma (98%) rename helm/software/matita/dama/{ => attic}/reals.ma (99%) rename helm/software/matita/dama/{ => attic}/rings.ma (99%) rename helm/software/matita/dama/{ => attic}/vector_spaces.ma (99%) rename helm/software/matita/dama/{groups.ma => group.ma} (93%) rename helm/software/matita/dama/{ordered_groups.ma => ordered_group.ma} (96%) diff --git a/helm/software/matita/dama/fields.ma b/helm/software/matita/dama/attic/fields.ma similarity index 98% rename from helm/software/matita/dama/fields.ma rename to helm/software/matita/dama/attic/fields.ma index 5ab17edae..194a39110 100644 --- a/helm/software/matita/dama/fields.ma +++ b/helm/software/matita/dama/attic/fields.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/fields/". -include "rings.ma". +include "attic/rings.ma". record is_field (R:ring) (inv:∀x:R.x ≠ 0 → R) : Prop ≝ diff --git a/helm/software/matita/dama/integration_algebras.ma b/helm/software/matita/dama/attic/integration_algebras.ma similarity index 99% rename from helm/software/matita/dama/integration_algebras.ma rename to helm/software/matita/dama/attic/integration_algebras.ma index c37a1f0b1..50bf063a4 100644 --- a/helm/software/matita/dama/integration_algebras.ma +++ b/helm/software/matita/dama/attic/integration_algebras.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/integration_algebras/". -include "vector_spaces.ma". +include "attic/vector_spaces.ma". include "lattice.ma". (**************** Riesz Spaces ********************) diff --git a/helm/software/matita/dama/ordered_fields_ch0.ma b/helm/software/matita/dama/attic/ordered_fields_ch0.ma similarity index 98% rename from helm/software/matita/dama/ordered_fields_ch0.ma rename to helm/software/matita/dama/attic/ordered_fields_ch0.ma index d423894d0..b312c31ab 100644 --- a/helm/software/matita/dama/ordered_fields_ch0.ma +++ b/helm/software/matita/dama/attic/ordered_fields_ch0.ma @@ -14,8 +14,8 @@ set "baseuri" "cic:/matita/ordered_fields_ch0/". -include "fields.ma". -include "ordered_groups.ma". +include "attic/fields.ma". +include "ordered_group.ma". (*CSC: non capisco questi alias! Una volta non servivano*) alias id "plus" = "cic:/matita/groups/plus.con". diff --git a/helm/software/matita/dama/reals.ma b/helm/software/matita/dama/attic/reals.ma similarity index 99% rename from helm/software/matita/dama/reals.ma rename to helm/software/matita/dama/attic/reals.ma index d57e6cfba..eaa6a2437 100644 --- a/helm/software/matita/dama/reals.ma +++ b/helm/software/matita/dama/attic/reals.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/reals/". -include "ordered_fields_ch0.ma". +include "attic/ordered_fields_ch0.ma". record is_real (F:ordered_field_ch0) : Type ≝ @@ -169,4 +169,4 @@ lemma abs_x_ge_O: ∀R:real.∀x:R. 0 ≤ abs ? x. (* facile *) elim daemon ]. -qed. \ No newline at end of file +qed. diff --git a/helm/software/matita/dama/rings.ma b/helm/software/matita/dama/attic/rings.ma similarity index 99% rename from helm/software/matita/dama/rings.ma rename to helm/software/matita/dama/attic/rings.ma index 3ed2fab25..2ea188847 100644 --- a/helm/software/matita/dama/rings.ma +++ b/helm/software/matita/dama/attic/rings.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/rings/". -include "groups.ma". +include "group.ma". record is_ring (G:abelian_group) (mult:G→G→G) (one:G) : Prop ≝ diff --git a/helm/software/matita/dama/vector_spaces.ma b/helm/software/matita/dama/attic/vector_spaces.ma similarity index 99% rename from helm/software/matita/dama/vector_spaces.ma rename to helm/software/matita/dama/attic/vector_spaces.ma index 6aaebd12b..1e29bee24 100644 --- a/helm/software/matita/dama/vector_spaces.ma +++ b/helm/software/matita/dama/attic/vector_spaces.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/vector_spaces/". -include "reals.ma". +include "attic/reals.ma". record is_vector_space (K: field) (G:abelian_group) (emult:K→G→G) : Prop ≝ diff --git a/helm/software/matita/dama/groups.ma b/helm/software/matita/dama/group.ma similarity index 93% rename from helm/software/matita/dama/groups.ma rename to helm/software/matita/dama/group.ma index c00740ee9..0d682a268 100644 --- a/helm/software/matita/dama/groups.ma +++ b/helm/software/matita/dama/group.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/groups/". +set "baseuri" "cic:/matita/group/". include "excedence.ma". @@ -46,19 +46,19 @@ record abelian_group : Type ≝ notation "0" with precedence 89 for @{ 'zero }. interpretation "Abelian group zero" 'zero = - (cic:/matita/groups/zero.con _). + (cic:/matita/group/zero.con _). interpretation "Abelian group plus" 'plus a b = - (cic:/matita/groups/plus.con _ a b). + (cic:/matita/group/plus.con _ a b). interpretation "Abelian group opp" 'uminus a = - (cic:/matita/groups/opp.con _ a). + (cic:/matita/group/opp.con _ a). definition minus ≝ λG:abelian_group.λa,b:G. a + -b. interpretation "Abelian group minus" 'minus a b = - (cic:/matita/groups/minus.con _ a b). + (cic:/matita/group/minus.con _ a b). lemma plus_assoc: ∀G:abelian_group.∀x,y,z:G.x+(y+z)≈x+y+z ≝ plus_assoc_. lemma plus_comm: ∀G:abelian_group.∀x,y:G.x+y≈y+x ≝ plus_comm_. @@ -76,7 +76,7 @@ intros (G x y z Eyz); apply (strong_ext_to_ext ?? (plus_strong_ext ? x)); assumption; qed. -coercion cic:/matita/groups/feq_plusl.con nocomposites. +coercion cic:/matita/group/feq_plusl.con nocomposites. lemma plus_strong_extr: ∀G:abelian_group.∀z:G.strong_ext ? (λx.x + z). intros 5 (G z x y A); simplify in A; @@ -90,17 +90,17 @@ intros (G x y z Eyz); apply (strong_ext_to_ext ?? (plus_strong_extr ? x)); assumption; qed. -coercion cic:/matita/groups/feq_plusr.con nocomposites. +coercion cic:/matita/group/feq_plusr.con nocomposites. (* generation of coercions to make *_rew[lr] easier *) lemma feq_plusr_sym_: ∀G:abelian_group.∀x,y,z:G.z ≈ y → y+x ≈ z+x. compose feq_plusr with eq_sym (H); apply H; assumption; qed. -coercion cic:/matita/groups/feq_plusr_sym_.con nocomposites. +coercion cic:/matita/group/feq_plusr_sym_.con nocomposites. lemma feq_plusl_sym_: ∀G:abelian_group.∀x,y,z:G.z ≈ y → x+y ≈ x+z. compose feq_plusl with eq_sym (H); apply H; assumption; qed. -coercion cic:/matita/groups/feq_plusl_sym_.con nocomposites. +coercion cic:/matita/group/feq_plusl_sym_.con nocomposites. lemma fap_plusl: ∀G:abelian_group.∀x,y,z:G. y # z → x+y # x+z. intros (G x y z Ayz); apply (plus_strong_ext ? (-x)); @@ -186,25 +186,25 @@ lemma feq_opp: ∀G:abelian_group.∀x,y:G. x ≈ y → -x ≈ -y. intros (G x y H); apply (feq_oppl ??y ? H); apply eq_reflexive; qed. -coercion cic:/matita/groups/feq_opp.con nocomposites. +coercion cic:/matita/group/feq_opp.con nocomposites. lemma eq_opp_sym: ∀G:abelian_group.∀x,y:G. y ≈ x → -x ≈ -y. compose feq_opp with eq_sym (H); apply H; assumption; qed. -coercion cic:/matita/groups/eq_opp_sym.con nocomposites. +coercion cic:/matita/group/eq_opp_sym.con nocomposites. lemma eq_opp_plusr: ∀G:abelian_group.∀x,y,z:G. x ≈ y → -(x + z) ≈ -(y + z). compose feq_plusr with feq_opp(H); apply H; assumption; qed. -coercion cic:/matita/groups/eq_opp_plusr.con nocomposites. +coercion cic:/matita/group/eq_opp_plusr.con nocomposites. lemma eq_opp_plusl: ∀G:abelian_group.∀x,y,z:G. x ≈ y → -(z + x) ≈ -(z + y). compose feq_plusl with feq_opp(H); apply H; assumption; qed. -coercion cic:/matita/groups/eq_opp_plusl.con nocomposites. +coercion cic:/matita/group/eq_opp_plusl.con nocomposites. lemma plus_cancr_ap: ∀G:abelian_group.∀x,y,z:G. x+z # y+z → x # y. intros (G x y z H); lapply (fap_plusr ? (-z) ?? H) as H1; clear H; diff --git a/helm/software/matita/dama/metric_space.ma b/helm/software/matita/dama/metric_space.ma index 35e0e0066..d529af83c 100644 --- a/helm/software/matita/dama/metric_space.ma +++ b/helm/software/matita/dama/metric_space.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/metric_space/". -include "ordered_groups.ma". +include "ordered_group.ma". record metric_space (R : ogroup) : Type ≝ { ms_carr :> Type; diff --git a/helm/software/matita/dama/ordered_groups.ma b/helm/software/matita/dama/ordered_group.ma similarity index 96% rename from helm/software/matita/dama/ordered_groups.ma rename to helm/software/matita/dama/ordered_group.ma index 74188d8a0..4f7551ccf 100644 --- a/helm/software/matita/dama/ordered_groups.ma +++ b/helm/software/matita/dama/ordered_group.ma @@ -12,10 +12,10 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/ordered_groups/". +set "baseuri" "cic:/matita/ordered_gorup/". include "ordered_set.ma". -include "groups.ma". +include "group.ma". record pre_ogroup : Type ≝ { og_abelian_group_: abelian_group; @@ -30,7 +30,7 @@ unfold apartness_OF_pre_ogroup; cases (og_with G); simplify; [apply plus_assoc|apply plus_comm|apply zero_neutral|apply opp_inverse|apply plus_strong_ext] qed. -coercion cic:/matita/ordered_groups/og_abelian_group.con. +coercion cic:/matita/ordered_gorup/og_abelian_group.con. record ogroup : Type ≝ { og_carr:> pre_ogroup; @@ -64,7 +64,7 @@ apply (Ex≫ (0+y) (plus_comm ???)); apply (Ex≫ y (zero_neutral ??) L); qed. -coercion cic:/matita/ordered_groups/fexc_plusr.con nocomposites. +coercion cic:/matita/ordered_gorup/fexc_plusr.con nocomposites. lemma exc_canc_plusl: ∀G:ogroup.∀f,g,h:G. h+f ≰ h+g → f ≰ g. intros 5 (G x y z L); apply (exc_canc_plusr ??? z); @@ -83,7 +83,7 @@ apply (exc_rewl ???? (zero_neutral ??)); apply (exc_rewr ???? (zero_neutral ??) L); qed. -coercion cic:/matita/ordered_groups/fexc_plusl.con nocomposites. +coercion cic:/matita/ordered_gorup/fexc_plusl.con nocomposites. lemma plus_cancr_le: ∀G:ogroup.∀x,y,z:G.x+z ≤ y + z → x ≤ y. diff --git a/helm/software/matita/dama/preweighted_lattice.ma b/helm/software/matita/dama/preweighted_lattice.ma index 9a46fb319..39105c0fd 100644 --- a/helm/software/matita/dama/preweighted_lattice.ma +++ b/helm/software/matita/dama/preweighted_lattice.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/preweighted_lattice/". -include "ordered_groups.ma". +include "ordered_group.ma". record wlattice (R : ogroup) : Type ≝ { wl_carr:> Type; -- 2.39.2