From db068aa35cc47bb881ec810bf3b904c3d7cc9379 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 7 Jan 2008 10:22:10 +0000 Subject: [PATCH] matitadep sould be ok, outputs warning regarding issues and uses the right paths to include files --- matita/.depend | 12 +- matita/.depend.opt | 12 +- matita/dama/Q_is_orded_divisble_group.ma | 272 ++++++++++++++++++ matita/dama/attic/fields.ma | 2 +- matita/dama/attic/integration_algebras.ma | 16 +- matita/dama/attic/ordered_fields_ch0.ma | 6 +- matita/dama/attic/reals.ma | 2 +- matita/dama/attic/rings.ma | 6 +- matita/dama/attic/vector_spaces.ma | 4 +- .../dama/classical_pointfree/ordered_sets.ma | 6 +- .../dama/classical_pointfree/ordered_sets2.ma | 4 +- matita/dama/classical_pointwise/sets.ma | 24 +- .../dama/classical_pointwise/sigma_algebra.ma | 2 +- matita/dama/classical_pointwise/topology.ma | 2 +- matita/dama/constructive_connectives.ma | 2 +- .../constructive_higher_order_relations.ma | 5 +- .../dama/constructive_pointfree/lebesgue.ma | 2 +- matita/dama/divisible_group.ma | 2 +- matita/dama/excess.ma | 4 +- matita/dama/group.ma | 2 +- matita/dama/lattice.ma | 2 +- matita/dama/metric_lattice.ma | 2 +- matita/dama/metric_space.ma | 2 +- matita/dama/ordered_divisible_group.ma | 2 +- matita/dama/ordered_group.ma | 2 +- matita/dama/premetric_lattice.ma | 2 +- matita/dama/prevalued_lattice.ma | 2 +- matita/dama/sandwich.ma | 2 +- matita/dama/sequence.ma | 2 +- matita/matitac.ml | 2 +- matita/matitadep.ml | 30 +- 31 files changed, 361 insertions(+), 76 deletions(-) create mode 100644 matita/dama/Q_is_orded_divisble_group.ma diff --git a/matita/.depend b/matita/.depend index d6d6aefc4..84e4f1d2e 100644 --- a/matita/.depend +++ b/matita/.depend @@ -56,12 +56,12 @@ matitaprover.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ buildTimeConf.cmo matitaprover.cmi matitaprover.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \ buildTimeConf.cmx matitaprover.cmi -matitaScript.cmo: matitaTypes.cmi matitaMisc.cmi matitaGtkMisc.cmi \ - matitaEngine.cmi buildTimeConf.cmo applyTransformation.cmi \ - matitaScript.cmi -matitaScript.cmx: matitaTypes.cmx matitaMisc.cmx matitaGtkMisc.cmx \ - matitaEngine.cmx buildTimeConf.cmx applyTransformation.cmx \ - matitaScript.cmi +matitaScript.cmo: matitacLib.cmi matitaTypes.cmi matitaMisc.cmi \ + matitaGtkMisc.cmi matitaEngine.cmi buildTimeConf.cmo \ + applyTransformation.cmi matitaScript.cmi +matitaScript.cmx: matitacLib.cmx matitaTypes.cmx matitaMisc.cmx \ + matitaGtkMisc.cmx matitaEngine.cmx buildTimeConf.cmx \ + applyTransformation.cmx matitaScript.cmi matitaTypes.cmo: matitaTypes.cmi matitaTypes.cmx: matitaTypes.cmi matitaWiki.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ diff --git a/matita/.depend.opt b/matita/.depend.opt index db22851e4..d8ff0ac75 100644 --- a/matita/.depend.opt +++ b/matita/.depend.opt @@ -56,12 +56,12 @@ matitaprover.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ buildTimeConf.cmx matitaprover.cmi matitaprover.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \ buildTimeConf.cmx matitaprover.cmi -matitaScript.cmo: matitaTypes.cmi matitaMisc.cmi matitaGtkMisc.cmi \ - matitaEngine.cmi buildTimeConf.cmx applyTransformation.cmi \ - matitaScript.cmi -matitaScript.cmx: matitaTypes.cmx matitaMisc.cmx matitaGtkMisc.cmx \ - matitaEngine.cmx buildTimeConf.cmx applyTransformation.cmx \ - matitaScript.cmi +matitaScript.cmo: matitacLib.cmi matitaTypes.cmi matitaMisc.cmi \ + matitaGtkMisc.cmi matitaEngine.cmi buildTimeConf.cmx \ + applyTransformation.cmi matitaScript.cmi +matitaScript.cmx: matitacLib.cmx matitaTypes.cmx matitaMisc.cmx \ + matitaGtkMisc.cmx matitaEngine.cmx buildTimeConf.cmx \ + applyTransformation.cmx matitaScript.cmi matitaTypes.cmo: matitaTypes.cmi matitaTypes.cmx: matitaTypes.cmi matitaWiki.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ diff --git a/matita/dama/Q_is_orded_divisble_group.ma b/matita/dama/Q_is_orded_divisble_group.ma new file mode 100644 index 000000000..762554dd0 --- /dev/null +++ b/matita/dama/Q_is_orded_divisble_group.ma @@ -0,0 +1,272 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + + + +include "Q/q.ma". +include "ordered_divisible_group.ma". + +definition strong_decidable ≝ + λA:Prop.A ∨ ¬ A. + +theorem strong_decidable_to_Not_Not_eq: + ∀T:Type.∀eq: T → T → Prop.∀x,y:T. + strong_decidable (x=y) → ¬x≠y → x=y. + intros; + cases s; + [ assumption + | elim (H H1) + ] +qed. + +definition apartness_of_strong_decidable: + ∀T:Type.(∀x,y:T.strong_decidable (x=y)) → apartness. + intros; + constructor 1; + [ apply T + | apply (λx,y:T.x ≠ y); + | simplify; + intros 2; + apply (H (refl_eq ??)); + | simplify; + intros 4; + apply H; + symmetry; + assumption + | simplify; + intros; + elim (f x z); + [ elim (f z y); + [ elim H; + transitivity z; + assumption + | right; + assumption + ] + | left; + assumption + ] + ] +qed. + +theorem strong_decidable_to_strong_ext: + ∀T:Type.∀sd:∀x,y:T.strong_decidable (x=y). + ∀op:T→T. strong_ext (apartness_of_strong_decidable ? sd) op. + intros 6; + intro; + apply a; + apply eq_f; + assumption; +qed. + +theorem strong_decidable_to_transitive_to_cotransitive: + ∀T:Type.∀le:T→T→Prop.(∀x,y:T.strong_decidable (le x y)) → + transitive ? le → cotransitive ? (λx,y.¬ (le x y)). + intros; + whd; + simplify; + intros; + elim (f x z); + [ elim (f z y); + [ elim H; + apply (t ? z); + assumption + | right; + assumption + ] + | left; + assumption + ] +qed. + +theorem reflexive_to_coreflexive: + ∀T:Type.∀le:T→T→Prop.reflexive ? le → coreflexive ? (λx,y.¬(le x y)). + intros; + unfold; + simplify; + intros 2; + apply H1; + apply H; +qed. + +definition ordered_set_of_strong_decidable: + ∀T:Type.∀le:T→T→Prop.(∀x,y:T.strong_decidable (le x y)) → + transitive ? le → reflexive ? le → excess. + intros; + constructor 1; + [ apply T + | apply (λx,y.¬(le x y)); + | apply reflexive_to_coreflexive; + assumption + | apply strong_decidable_to_transitive_to_cotransitive; + assumption + ] +qed. + +definition abelian_group_of_strong_decidable: + ∀T:Type.∀plus:T→T→T.∀zero:T.∀opp:T→T. + (∀x,y:T.strong_decidable (x=y)) → + associative ? plus (eq T) → + commutative ? plus (eq T) → + (∀x:T. plus zero x = x) → + (∀x:T. plus (opp x) x = zero) → + abelian_group. + intros; + constructor 1; + [apply (apartness_of_strong_decidable ? f);] + try assumption; + [ change with (associative ? plus (λx,y:T.¬x≠y)); + simplify; + intros; + intro; + apply H2; + apply a; + | intros 2; + intro; + apply a1; + apply c; + | intro; + intro; + apply a1; + apply H + | intro; + intro; + apply a1; + apply H1 + | intros; + apply strong_decidable_to_strong_ext; + assumption + ] +qed. + +definition left_neutral ≝ λC:Type.λop.λe:C. ∀x:C. op e x = x. +definition left_inverse ≝ λC:Type.λop.λe:C.λinv:C→C. ∀x:C. op (inv x) x = e. + +record nabelian_group : Type ≝ + { ncarr:> Type; + nplus: ncarr → ncarr → ncarr; + nzero: ncarr; + nopp: ncarr → ncarr; + nplus_assoc: associative ? nplus (eq ncarr); + nplus_comm: commutative ? nplus (eq ncarr); + nzero_neutral: left_neutral ? nplus nzero; + nopp_inverse: left_inverse ? nplus nzero nopp + }. + +definition abelian_group_of_nabelian_group: + ∀G:nabelian_group.(∀x,y:G.strong_decidable (x=y)) → abelian_group. + intros; + apply abelian_group_of_strong_decidable; + [2: apply (nplus G) + | skip + | apply (nzero G) + | apply (nopp G) + | assumption + | apply nplus_assoc; + | apply nplus_comm; + | apply nzero_neutral; + | apply nopp_inverse + ] +qed. + +definition Z_abelian_group: abelian_group. + apply abelian_group_of_nabelian_group; + [ constructor 1; + [ apply Z + | apply Zplus + | apply OZ + | apply Zopp + | whd; + intros; + symmetry; + apply associative_Zplus + | apply sym_Zplus + | intro; + reflexivity + | intro; + rewrite > sym_Zplus; + apply Zplus_Zopp; + ] + | simplify; + intros; + unfold; + generalize in match (eqZb_to_Prop x y); + elim (eqZb x y); + simplify in H; + [ left ; assumption + | right; assumption + ] + ] +qed. + +record nordered_set: Type ≝ + { nos_carr:> Type; + nos_le: nos_carr → nos_carr → Prop; + nos_reflexive: reflexive ? nos_le; + nos_transitive: transitive ? nos_le + }. + +definition excess_of_nordered_group: + ∀O:nordered_set.(∀x,y:O. strong_decidable (nos_le ? x y)) → excess. + intros; + constructor 1; + [ apply (nos_carr O) + | apply (λx,y.¬(nos_le ? x y)) + | apply reflexive_to_coreflexive; + apply nos_reflexive + | apply strong_decidable_to_transitive_to_cotransitive; + [ assumption + | apply nos_transitive + ] + ] +qed. + +lemma non_deve_stare_qui: reflexive ? Zle. + intro; + elim x; + [ exact I + |2,3: simplify; + apply le_n; + ] +qed. + +axiom non_deve_stare_qui3: ∀x,y:Z. x < y → x ≤ y. + +axiom non_deve_stare_qui4: ∀x,y:Z. x < y → y ≰ x. + +definition Z_excess: excess. + apply excess_of_nordered_group; + [ constructor 1; + [ apply Z + | apply Zle + | apply non_deve_stare_qui + | apply transitive_Zle + ] + | simplify; + intros; + unfold; + generalize in match (Z_compare_to_Prop x y); + cases (Z_compare x y); simplify; intro; + [ left; + apply non_deve_stare_qui3; + assumption + | left; + rewrite > H; + apply non_deve_stare_qui + | right; + apply non_deve_stare_qui4; + assumption + ] + ] +qed. \ No newline at end of file diff --git a/matita/dama/attic/fields.ma b/matita/dama/attic/fields.ma index 194a39110..824fdfa9e 100644 --- a/matita/dama/attic/fields.ma +++ b/matita/dama/attic/fields.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/fields/". + include "attic/rings.ma". diff --git a/matita/dama/attic/integration_algebras.ma b/matita/dama/attic/integration_algebras.ma index 50bf063a4..1b775fa78 100644 --- a/matita/dama/attic/integration_algebras.ma +++ b/matita/dama/attic/integration_algebras.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/integration_algebras/". + include "attic/vector_spaces.ma". include "lattice.ma". @@ -60,7 +60,7 @@ lemma rs_lattice: ∀K.pre_riesz_space K → lattice. ]. qed. -coercion cic:/matita/integration_algebras/rs_lattice.con. +coercion cic:/matita/attic/integration_algebras/rs_lattice.con. lemma rs_ordered_abelian_group: ∀K.pre_riesz_space K → ordered_abelian_group. intros (K V); @@ -99,7 +99,7 @@ lemma rs_ordered_abelian_group: ∀K.pre_riesz_space K → ordered_abelian_group ] qed. -coercion cic:/matita/integration_algebras/rs_ordered_abelian_group.con. +coercion cic:/matita/attic/integration_algebras/rs_ordered_abelian_group.con. record is_riesz_space (K:ordered_field_ch0) (V:pre_riesz_space K) : Prop ≝ { rs_compat_le_times: ∀a:K.∀f:V. 0≤a → 0≤f → 0≤a*f @@ -141,7 +141,7 @@ definition rn_function ≝ λR:real.λV:riesz_space R.λnorm:riesz_norm ? V. n_function R V (rn_norm ? ? norm). -coercion cic:/matita/integration_algebras/rn_function.con 1. +coercion cic:/matita/attic/integration_algebras/rn_function.con 1. (************************** L-SPACES *************************************) (* @@ -313,14 +313,14 @@ record algebra (K: field) : Type \def }. interpretation "Algebra product" 'times a b = - (cic:/matita/integration_algebras/a_mult.con _ a b). + (cic:/matita/attic/integration_algebras/a_mult.con _ a b). definition ring_of_algebra ≝ λK.λA:algebra K. mk_ring A (a_mult ? A) (a_one ? A) (a_ring ? ? ? ? (a_algebra_properties ? A)). -coercion cic:/matita/integration_algebras/ring_of_algebra.con. +coercion cic:/matita/attic/integration_algebras/ring_of_algebra.con. record pre_f_algebra (K:ordered_field_ch0) : Type ≝ { fa_archimedean_riesz_space:> archimedean_riesz_space K; @@ -338,7 +338,7 @@ lemma fa_algebra: ∀K:ordered_field_ch0.pre_f_algebra K → algebra K. ] qed. -coercion cic:/matita/integration_algebras/fa_algebra.con. +coercion cic:/matita/attic/integration_algebras/fa_algebra.con. record is_f_algebra (K) (A:pre_f_algebra K) : Prop ≝ { compat_mult_le: ∀f,g:A.0 ≤ f → 0 ≤ g → 0 ≤ f*g; @@ -365,4 +365,4 @@ record integration_f_algebra (R:real) : Type \def axiom ifa_f_algebra: ∀R:real.integration_f_algebra R → f_algebra R. -coercion cic:/matita/integration_algebras/ifa_f_algebra.con. +coercion cic:/matita/attic/integration_algebras/ifa_f_algebra.con. diff --git a/matita/dama/attic/ordered_fields_ch0.ma b/matita/dama/attic/ordered_fields_ch0.ma index 5be3c9da4..898148d6c 100644 --- a/matita/dama/attic/ordered_fields_ch0.ma +++ b/matita/dama/attic/ordered_fields_ch0.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/ordered_fields_ch0/". + include "attic/fields.ma". include "ordered_group.ma". @@ -55,7 +55,7 @@ lemma of_ordered_abelian_group: pre_ordered_field_ch0 → ordered_abelian_group. ] qed. -coercion cic:/matita/ordered_fields_ch0/of_ordered_abelian_group.con. +coercion cic:/matita/attic/ordered_fields_ch0/of_ordered_abelian_group.con. (*CSC: I am not able to prove this since unfold is undone by coercion composition*) axiom of_with1: @@ -74,7 +74,7 @@ lemma of_cotransitively_ordered_set : pre_ordered_field_ch0 → cotransitively_o ] qed. -coercion cic:/matita/ordered_fields_ch0/of_cotransitively_ordered_set.con. +coercion cic:/matita/attic/ordered_fields_ch0/of_cotransitively_ordered_set.con. record is_ordered_field_ch0 (F:pre_ordered_field_ch0) : Type \def { of_mult_compat: ∀a,b:F. 0≤a → 0≤b → 0≤a*b; diff --git a/matita/dama/attic/reals.ma b/matita/dama/attic/reals.ma index eaa6a2437..872cfea50 100644 --- a/matita/dama/attic/reals.ma +++ b/matita/dama/attic/reals.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/reals/". + include "attic/ordered_fields_ch0.ma". diff --git a/matita/dama/attic/rings.ma b/matita/dama/attic/rings.ma index 2ea188847..d4db003dc 100644 --- a/matita/dama/attic/rings.ma +++ b/matita/dama/attic/rings.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/rings/". + include "group.ma". @@ -66,13 +66,13 @@ theorem not_eq_zero_one: ∀R:ring.0 ≠ one R. qed. interpretation "Ring mult" 'times a b = - (cic:/matita/rings/mult.con _ a b). + (cic:/matita/attic/rings/mult.con _ a b). notation "1" with precedence 89 for @{ 'one }. interpretation "Ring one" 'one = - (cic:/matita/rings/one.con _). + (cic:/matita/attic/rings/one.con _). lemma eq_mult_zero_x_zero: ∀R:ring.∀x:R.0*x=0. intros; diff --git a/matita/dama/attic/vector_spaces.ma b/matita/dama/attic/vector_spaces.ma index 1e29bee24..5002b022c 100644 --- a/matita/dama/attic/vector_spaces.ma +++ b/matita/dama/attic/vector_spaces.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/vector_spaces/". + include "attic/reals.ma". @@ -31,7 +31,7 @@ record vector_space (K:field): Type \def }. interpretation "Vector space external product" 'times a b = - (cic:/matita/vector_spaces/emult.con _ _ a b). + (cic:/matita/attic/vector_spaces/emult.con _ _ a b). record is_semi_norm (R:real) (V: vector_space R) (semi_norm:V→R) : Prop \def { sn_positive: ∀x:V. zero R ≤ semi_norm x; diff --git a/matita/dama/classical_pointfree/ordered_sets.ma b/matita/dama/classical_pointfree/ordered_sets.ma index 5d9c2da67..2630da77c 100644 --- a/matita/dama/classical_pointfree/ordered_sets.ma +++ b/matita/dama/classical_pointfree/ordered_sets.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/classical_pointwise/ordered_sets/". + include "excess.ma". @@ -320,10 +320,10 @@ notation "hvbox(〈a〉)" for @{ 'hide_everything_but $a }. interpretation "mk_bounded_above_sequence" 'hide_everything_but a -= (cic:/matita/ordered_set/bounded_above_sequence.ind#xpointer(1/1/1) _ _ a _). += (cic:/matita/classical_pointfree/ordered_sets/bounded_above_sequence.ind#xpointer(1/1/1) _ _ a _). interpretation "mk_bounded_below_sequence" 'hide_everything_but a -= (cic:/matita/ordered_set/bounded_below_sequence.ind#xpointer(1/1/1) _ _ a _). += (cic:/matita/classical_pointfree/ordered_sets/bounded_below_sequence.ind#xpointer(1/1/1) _ _ a _). theorem eq_f_sup_sup_f: ∀O':dedekind_sigma_complete_ordered_set. diff --git a/matita/dama/classical_pointfree/ordered_sets2.ma b/matita/dama/classical_pointfree/ordered_sets2.ma index d85a02cf4..7e74cbba2 100644 --- a/matita/dama/classical_pointfree/ordered_sets2.ma +++ b/matita/dama/classical_pointfree/ordered_sets2.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/classical_pointfree/ordered_sets2". + include "classical_pointfree/ordered_sets.ma". @@ -61,7 +61,7 @@ theorem le_to_le_sup_sup: qed. interpretation "mk_bounded_sequence" 'hide_everything_but a -= (cic:/matita/ordered_set/bounded_sequence.ind#xpointer(1/1/1) _ _ a _ _). += (cic:/matita/classical_pointfree/ordered_sets/bounded_sequence.ind#xpointer(1/1/1) _ _ a _ _). lemma reduce_bas_seq: ∀O:ordered_set.∀a:nat→O.∀p.∀i. diff --git a/matita/dama/classical_pointwise/sets.ma b/matita/dama/classical_pointwise/sets.ma index ec6a1c774..f03c3e7f2 100644 --- a/matita/dama/classical_pointwise/sets.ma +++ b/matita/dama/classical_pointwise/sets.ma @@ -12,9 +12,11 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/sets/". + include "nat/nat.ma". +include "logic/connectives.ma". + definition set ≝ λX:Type.X → Prop. @@ -24,21 +26,21 @@ notation "hvbox(x break ∈ A)" with precedence 60 for @{ 'member_of $x $A }. interpretation "Member of" 'member_of x A = - (cic:/matita/sets/member_of.con _ A x). + (cic:/matita/classical_pointwise/sets/member_of.con _ A x). notation "hvbox(x break ∉ A)" with precedence 60 for @{ 'not_member_of $x $A }. interpretation "Not member of" 'not_member_of x A = (cic:/matita/logic/connectives/Not.con - (cic:/matita/sets/member_of.con _ A x)). + (cic:/matita/classical_pointwise/sets/member_of.con _ A x)). definition emptyset : ∀X.set X ≝ λX:Type.λx:X.False. notation "∅︀" with precedence 100 for @{ 'emptyset }. interpretation "Emptyset" 'emptyset = - (cic:/matita/sets/emptyset.con _). + (cic:/matita/classical_pointwise/sets/emptyset.con _). definition subset: ∀X. set X → set X → Prop≝ λX.λA,B:set X.∀x. x ∈ A → x ∈ B. @@ -46,7 +48,7 @@ notation "hvbox(A break ⊆ B)" with precedence 60 for @{ 'subset $A $B }. interpretation "Subset" 'subset A B = - (cic:/matita/sets/subset.con _ A B). + (cic:/matita/classical_pointwise/sets/subset.con _ A B). definition intersection: ∀X. set X → set X → set X ≝ λX.λA,B:set X.λx. x ∈ A ∧ x ∈ B. @@ -55,7 +57,7 @@ notation "hvbox(A break ∩ B)" with precedence 70 for @{ 'intersection $A $B }. interpretation "Intersection" 'intersection A B = - (cic:/matita/sets/intersection.con _ A B). + (cic:/matita/classical_pointwise/sets/intersection.con _ A B). definition union: ∀X. set X → set X → set X ≝ λX.λA,B:set X.λx. x ∈ A ∨ x ∈ B. @@ -63,7 +65,7 @@ notation "hvbox(A break ∪ B)" with precedence 65 for @{ 'union $A $B }. interpretation "Union" 'union A B = - (cic:/matita/sets/union.con _ A B). + (cic:/matita/classical_pointwise/sets/union.con _ A B). definition seq ≝ λX:Type.nat → X. @@ -73,7 +75,7 @@ notation "hvbox(A \sub i)" with precedence 100 for @{ 'nth $A $i }. interpretation "nth" 'nth A i = - (cic:/matita/sets/nth.con _ A i). + (cic:/matita/classical_pointwise/sets/nth.con _ A i). definition countable_union: ∀X. seq (set X) → set X ≝ λX.λA:seq (set X).λx.∃j.x ∈ A \sub j. @@ -82,7 +84,7 @@ notation "∪ \sub (ident i opt (: ty)) B" with precedence 65 for @{ 'big_union ${default @{(λ${ident i}:$ty.$B)} @{(λ${ident i}.$B)}}}. interpretation "countable_union" 'big_union η.t = - (cic:/matita/sets/countable_union.con _ t). + (cic:/matita/classical_pointwise/sets/countable_union.con _ t). definition complement: ∀X. set X \to set X ≝ λX.λA:set X.λx. x ∉ A. @@ -90,7 +92,7 @@ notation "A \sup 'c'" with precedence 100 for @{ 'complement $A }. interpretation "Complement" 'complement A = - (cic:/matita/sets/complement.con _ A). + (cic:/matita/classical_pointwise/sets/complement.con _ A). definition inverse_image: ∀X,Y.∀f: X → Y.set Y → set X ≝ λX,Y,f,B,x. f x ∈ B. @@ -99,4 +101,4 @@ notation "hvbox(f \sup (-1))" with precedence 100 for @{ 'finverse $f }. interpretation "Inverse image" 'finverse f = - (cic:/matita/sets/inverse_image.con _ _ f). \ No newline at end of file + (cic:/matita/classical_pointwise/sets/inverse_image.con _ _ f). diff --git a/matita/dama/classical_pointwise/sigma_algebra.ma b/matita/dama/classical_pointwise/sigma_algebra.ma index 21db34e38..580fe9645 100644 --- a/matita/dama/classical_pointwise/sigma_algebra.ma +++ b/matita/dama/classical_pointwise/sigma_algebra.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/sigma_algebra/". + include "classical_pointwise/topology.ma". diff --git a/matita/dama/classical_pointwise/topology.ma b/matita/dama/classical_pointwise/topology.ma index c5ba9bbd6..72c9dbb4d 100644 --- a/matita/dama/classical_pointwise/topology.ma +++ b/matita/dama/classical_pointwise/topology.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/topology/". + include "classical_pointwise/sets.ma". diff --git a/matita/dama/constructive_connectives.ma b/matita/dama/constructive_connectives.ma index 8518d7ede..78e2ec571 100644 --- a/matita/dama/constructive_connectives.ma +++ b/matita/dama/constructive_connectives.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/constructive_connectives/". +include "logic/connectives.ma". inductive Or (A,B:Type) : Type ≝ Left : A → Or A B diff --git a/matita/dama/constructive_higher_order_relations.ma b/matita/dama/constructive_higher_order_relations.ma index 789c7c9c5..8d195396c 100644 --- a/matita/dama/constructive_higher_order_relations.ma +++ b/matita/dama/constructive_higher_order_relations.ma @@ -12,9 +12,10 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/constructive_higher_order_relations". + include "constructive_connectives.ma". +include "higher_order_defs/relations.ma". definition cotransitive ≝ λC:Type.λlt:C→C→Type.∀x,y,z:C. lt x y → lt x z ∨ lt z y. @@ -47,4 +48,4 @@ lemma Or_symmetric: symmetric ? Or. unfold; intros (x y H); cases H; [right|left] assumption; qed. - \ No newline at end of file + diff --git a/matita/dama/constructive_pointfree/lebesgue.ma b/matita/dama/constructive_pointfree/lebesgue.ma index 766412819..c7e5d7c5d 100644 --- a/matita/dama/constructive_pointfree/lebesgue.ma +++ b/matita/dama/constructive_pointfree/lebesgue.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/lebesgue/". + include "metric_lattice.ma". include "sequence.ma". diff --git a/matita/dama/divisible_group.ma b/matita/dama/divisible_group.ma index 6830ef4e1..4f54545c8 100644 --- a/matita/dama/divisible_group.ma +++ b/matita/dama/divisible_group.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/divisible_group/". + include "nat/orders.ma". include "group.ma". diff --git a/matita/dama/excess.ma b/matita/dama/excess.ma index d8cf09766..6db7e22e6 100644 --- a/matita/dama/excess.ma +++ b/matita/dama/excess.ma @@ -12,12 +12,12 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/excess/". + include "higher_order_defs/relations.ma". include "nat/plus.ma". -include "constructive_connectives.ma". include "constructive_higher_order_relations.ma". +include "constructive_connectives.ma". record excess : Type ≝ { exc_carr:> Type; diff --git a/matita/dama/group.ma b/matita/dama/group.ma index 0e2668c2d..9da386ef7 100644 --- a/matita/dama/group.ma +++ b/matita/dama/group.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/group/". + include "excess.ma". diff --git a/matita/dama/lattice.ma b/matita/dama/lattice.ma index 768c86df1..787ee3e8e 100644 --- a/matita/dama/lattice.ma +++ b/matita/dama/lattice.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/lattice/". + include "excess.ma". diff --git a/matita/dama/metric_lattice.ma b/matita/dama/metric_lattice.ma index 0bfc3db67..36742163b 100644 --- a/matita/dama/metric_lattice.ma +++ b/matita/dama/metric_lattice.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/metric_lattice/". + include "metric_space.ma". include "lattice.ma". diff --git a/matita/dama/metric_space.ma b/matita/dama/metric_space.ma index e2112d65b..d36e90a68 100644 --- a/matita/dama/metric_space.ma +++ b/matita/dama/metric_space.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/metric_space/". + include "ordered_divisible_group.ma". diff --git a/matita/dama/ordered_divisible_group.ma b/matita/dama/ordered_divisible_group.ma index a6c13e189..a9671d934 100644 --- a/matita/dama/ordered_divisible_group.ma +++ b/matita/dama/ordered_divisible_group.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/ordered_divisible_group/". + include "nat/orders.ma". include "nat/times.ma". diff --git a/matita/dama/ordered_group.ma b/matita/dama/ordered_group.ma index 2129aa5c7..9a066a80e 100644 --- a/matita/dama/ordered_group.ma +++ b/matita/dama/ordered_group.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/ordered_group/". + include "group.ma". diff --git a/matita/dama/premetric_lattice.ma b/matita/dama/premetric_lattice.ma index d985ec24f..bfba3710a 100644 --- a/matita/dama/premetric_lattice.ma +++ b/matita/dama/premetric_lattice.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/premetric_lattice/". + include "metric_space.ma". diff --git a/matita/dama/prevalued_lattice.ma b/matita/dama/prevalued_lattice.ma index 5f1a062e0..53b2b0a1b 100644 --- a/matita/dama/prevalued_lattice.ma +++ b/matita/dama/prevalued_lattice.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/prevalued_lattice/". + include "ordered_group.ma". diff --git a/matita/dama/sandwich.ma b/matita/dama/sandwich.ma index 21499ee72..037d3d7dc 100644 --- a/matita/dama/sandwich.ma +++ b/matita/dama/sandwich.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/sandwich/". + include "nat/plus.ma". include "nat/orders.ma". diff --git a/matita/dama/sequence.ma b/matita/dama/sequence.ma index 9990f8c7d..7536901ba 100644 --- a/matita/dama/sequence.ma +++ b/matita/dama/sequence.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/sequence/". + include "excess.ma". diff --git a/matita/matitac.ml b/matita/matitac.ml index c31c22874..6836e44a2 100644 --- a/matita/matitac.ml +++ b/matita/matitac.ml @@ -93,7 +93,7 @@ let main_compiler () = match targets with | [] -> (match Librarian.find_roots_in_dir (Sys.getcwd ()) with - | [x] -> [], x + | [x] -> [], Filename.dirname x | [] -> prerr_endline "No targets and no root found"; exit 1 | roots -> diff --git a/matita/matitadep.ml b/matita/matitadep.ml index cf1519eae..0186a245a 100644 --- a/matita/matitadep.ml +++ b/matita/matitadep.ml @@ -37,23 +37,24 @@ let main () = let baseuri_of_inv = Hashtbl.create 13 in let dot_file = ref "" in (* helpers *) - let include_paths = - Helm_registry.get_list Helm_registry.string "matita.includes" - in + let include_paths = ref [] in let baseuri_of_script s = try Hashtbl.find baseuri_of s with Not_found -> - let _,b,_,_ = Librarian.baseuri_of_script ~include_paths s in + let _,b,_,_ = + Librarian.baseuri_of_script ~include_paths:!include_paths s + in Hashtbl.add baseuri_of s b; Hashtbl.add baseuri_of_inv b s; b in - let script_of_baseuri b = - try Hashtbl.find baseuri_of_inv b + let script_of_baseuri ma b = + try Some (Hashtbl.find baseuri_of_inv b) with Not_found -> - assert false - (* should be called only after baseuri_of_script is - * called on every file *) + HLog.error ("Skipping dependency of '"^ma^"' over '"^b^"'"); + HLog.error ("Plase include the file defining such baseuri, or fix"); + HLog.error ("possibly incorrect verbatim URIs in the .ma file."); + None in let buri alias = U.buri_of_uri (U.uri_of_string alias) in let resolve alias current_buri = @@ -74,6 +75,11 @@ let main () = exit 1 | [x] -> Sys.chdir (Filename.dirname x); + let opts = Librarian.load_root_file "root" in + include_paths := + (try Str.split (Str.regexp " ") (List.assoc "include_paths" opts) + with Not_found -> []) @ + (Helm_registry.get_list Helm_registry.string "matita.includes"); HExtlib.find ~test:(fun x -> Filename.check_suffix x ".ma") "." | _ -> let roots = List.map (HExtlib.chop_prefix (Sys.getcwd()^"/")) roots in @@ -100,8 +106,12 @@ let main () = let dep = resolve uri ma_baseuri in (match dep with | None -> () - | Some u -> Hashtbl.add include_deps ma_file (script_of_baseuri u)) + | Some u -> + match script_of_baseuri ma_file u with + | Some d -> Hashtbl.add include_deps ma_file d + | None -> ()) | DependenciesParser.IncludeDep path -> + ignore (baseuri_of_script path); Hashtbl.add include_deps ma_file path) dependencies) ma_files; -- 2.39.2