From 1ed4fe0f28d3b0b915387330cd722bfb80fb1063 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 7 Jul 2010 16:08:18 +0000 Subject: [PATCH] moved formal_topology into library" --- helm/software/matita/library/depends | 59 +++-- .../formal_topology}/apply_functor.ma | 4 +- .../formal_topology}/basic_pairs.ma | 4 +- .../basic_pairs.ma.dontcompile | 179 ------------- .../basic_pairs_to_basic_topologies.ma | 16 +- .../basic_pairs_to_o-basic_pairs.ma | 6 +- .../formal_topology}/basic_topologies.ma | 4 +- .../basic_topologies.ma.dontcompile | 199 -------------- .../basic_topologies_to_o-basic_topologies.ma | 12 +- .../formal_topology}/categories.ma | 2 +- .../formal_topology}/concrete_spaces.ma | 6 +- .../concrete_spaces.ma.dontcompile | 120 --------- .../concrete_spaces_to_o-concrete_spaces.ma | 6 +- .../formal_topology}/cprop_connectives.ma | 0 .../formal_topology}/formal_topologies.ma | 2 +- .../formal_topologies.ma.dontcompile | 121 --------- .../formal_topology}/notation.ma | 0 .../formal_topology}/o-algebra.ma | 2 +- .../formal_topology}/o-basic_pairs.ma | 4 +- .../o-basic_pairs_to_o-basic_topologies.ma | 6 +- .../formal_topology}/o-basic_topologies.ma | 4 +- .../formal_topology}/o-concrete_spaces.ma | 4 +- .../formal_topology}/o-formal_topologies.ma | 2 +- .../formal_topology}/o-saturations.ma | 2 +- .../formal_topology}/r-o-basic_pairs.ma | 8 +- .../formal_topology}/relations.ma | 2 +- .../formal_topology/relations.ma.dontcompile | 247 ------------------ .../relations_to_o-algebra.ma | 4 +- .../formal_topology}/saturations.ma | 2 +- .../saturations_reductions.ma.dontcompile | 41 --- .../saturations_to_o-saturations.ma | 6 +- .../formal_topology}/subsets.ma | 2 +- helm/software/matita/nlibrary/re/re.ma | 152 ++++++++++- 33 files changed, 242 insertions(+), 986 deletions(-) rename helm/software/matita/{contribs/formal_topology/overlap => library/formal_topology}/apply_functor.ma (98%) rename helm/software/matita/{contribs/formal_topology/overlap => library/formal_topology}/basic_pairs.ma (99%) delete mode 100644 helm/software/matita/library/formal_topology/basic_pairs.ma.dontcompile rename helm/software/matita/{contribs/formal_topology/overlap => library/formal_topology}/basic_pairs_to_basic_topologies.ma (86%) rename helm/software/matita/{contribs/formal_topology/overlap => library/formal_topology}/basic_pairs_to_o-basic_pairs.ma (97%) rename helm/software/matita/{contribs/formal_topology/overlap => library/formal_topology}/basic_topologies.ma (99%) delete mode 100644 helm/software/matita/library/formal_topology/basic_topologies.ma.dontcompile rename helm/software/matita/{contribs/formal_topology/overlap => library/formal_topology}/basic_topologies_to_o-basic_topologies.ma (95%) rename helm/software/matita/{contribs/formal_topology/overlap => library/formal_topology}/categories.ma (99%) rename helm/software/matita/{contribs/formal_topology/overlap => library/formal_topology}/concrete_spaces.ma (97%) delete mode 100644 helm/software/matita/library/formal_topology/concrete_spaces.ma.dontcompile rename helm/software/matita/{contribs/formal_topology/overlap => library/formal_topology}/concrete_spaces_to_o-concrete_spaces.ma (93%) rename helm/software/matita/{contribs/formal_topology/overlap => library/formal_topology}/cprop_connectives.ma (100%) rename helm/software/matita/{contribs/formal_topology/overlap => library/formal_topology}/formal_topologies.ma (98%) delete mode 100644 helm/software/matita/library/formal_topology/formal_topologies.ma.dontcompile rename helm/software/matita/{contribs/formal_topology/overlap => library/formal_topology}/notation.ma (100%) rename helm/software/matita/{contribs/formal_topology/overlap => library/formal_topology}/o-algebra.ma (99%) rename helm/software/matita/{contribs/formal_topology/overlap => library/formal_topology}/o-basic_pairs.ma (99%) rename helm/software/matita/{contribs/formal_topology/overlap => library/formal_topology}/o-basic_pairs_to_o-basic_topologies.ma (97%) rename helm/software/matita/{contribs/formal_topology/overlap => library/formal_topology}/o-basic_topologies.ma (99%) rename helm/software/matita/{contribs/formal_topology/overlap => library/formal_topology}/o-concrete_spaces.ma (98%) rename helm/software/matita/{contribs/formal_topology/overlap => library/formal_topology}/o-formal_topologies.ma (98%) rename helm/software/matita/{contribs/formal_topology/overlap => library/formal_topology}/o-saturations.ma (97%) rename helm/software/matita/{contribs/formal_topology/overlap => library/formal_topology}/r-o-basic_pairs.ma (98%) rename helm/software/matita/{contribs/formal_topology/overlap => library/formal_topology}/relations.ma (99%) delete mode 100644 helm/software/matita/library/formal_topology/relations.ma.dontcompile rename helm/software/matita/{contribs/formal_topology/overlap => library/formal_topology}/relations_to_o-algebra.ma (99%) rename helm/software/matita/{contribs/formal_topology/overlap => library/formal_topology}/saturations.ma (97%) delete mode 100644 helm/software/matita/library/formal_topology/saturations_reductions.ma.dontcompile rename helm/software/matita/{contribs/formal_topology/overlap => library/formal_topology}/saturations_to_o-saturations.ma (91%) rename helm/software/matita/{contribs/formal_topology/overlap => library/formal_topology}/subsets.ma (99%) diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends index 4e5374dc7..0c04be486 100644 --- a/helm/software/matita/library/depends +++ b/helm/software/matita/library/depends @@ -1,73 +1,85 @@ -dama/sandwich.ma dama/ordered_uniform.ma +formal_topology/formal_topologies.ma formal_topology/basic_topologies.ma demo/formal_topology.ma logic/cprop_connectives.ma logic/equality.ma +dama/sandwich.ma dama/ordered_uniform.ma Q/ratio/rtimes.ma Q/fraction/ftimes.ma Q/ratio/rinv.ma demo/power_derivative.ma nat/compare.ma nat/orders.ma nat/plus.ma nat/compare.ma datatypes/bool.ma datatypes/compare.ma nat/orders.ma dama/ordered_uniform.ma dama/uniform.ma nat/lt_arith.ma nat/div_and_mod.ma +formal_topology/o-basic_pairs_to_o-basic_topologies.ma formal_topology/notation.ma formal_topology/o-basic_pairs.ma formal_topology/o-basic_topologies.ma demo/propositional_sequent_calculus.ma datatypes/constructors.ma list/sort.ma nat/compare.ma nat/plus.ma Z/inversion.ma Z/dirichlet_product.ma Z/moebius.ma +formal_topology/basic_topologies_to_o-basic_topologies.ma formal_topology/basic_topologies.ma formal_topology/notation.ma formal_topology/o-basic_topologies.ma formal_topology/relations_to_o-algebra.ma dama/models/nat_order_continuous.ma dama/models/increasing_supremum_stabilizes.ma dama/models/nat_ordered_uniform.ma nat/factorial2.ma nat/exp.ma nat/factorial.ma nat/orders.ma higher_order_defs/ordering.ma nat/nat.ma -nat/sieve.ma list/sort.ma nat/primes.ma technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic/connectives2.ma +nat/sieve.ma list/sort.ma nat/primes.ma +formal_topology/subsets.ma formal_topology/categories.ma nat/div_and_mod_diseq.ma nat/lt_arith.ma logic/cprop_connectives.ma logic/connectives.ma algebra/groups.ma algebra/monoids.ma datatypes/bool.ma nat/compare.ma nat/le_arith.ma nat/chinese_reminder.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma Q/q/qinv.ma Q/q/q.ma Q/ratio/rinv.ma nat/exp.ma nat/div_and_mod.ma nat/lt_arith.ma -dama/models/nat_uniform.ma dama/models/discrete_uniformity.ma dama/nat_ordered_set.ma list/in.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma datatypes/compare.ma +dama/models/nat_uniform.ma dama/models/discrete_uniformity.ma dama/nat_ordered_set.ma didactic/exercises/natural_deduction_fst_order.ma didactic/support/natural_deduction.ma didactic/exercises/substitution.ma nat/minus.ma nat/factorization2.ma list/list.ma nat/factorization.ma nat/sieve.ma +formal_topology/basic_topologies.ma formal_topology/relations.ma formal_topology/saturations.ma dama/models/increasing_supremum_stabilizes.ma dama/models/nat_uniform.ma dama/russell_support.ma dama/supremum.ma nat/le_arith.ma logic/connectives.ma Q/nat_fact/times.ma nat/factorization.ma decidable_kit/fintype.ma decidable_kit/eqtype.ma decidable_kit/list_aux.ma didactic/exercises/duality.ma nat/minus.ma nat/ord.ma datatypes/constructors.ma nat/exp.ma nat/gcd.ma nat/nth_prime.ma nat/relevant_equations.ma +formal_topology/cprop_connectives.ma logic/connectives.ma dama/supremum.ma dama/nat_ordered_set.ma dama/sequence.ma datatypes/constructors.ma nat/plus.ma nat/totient1.ma nat/gcd_properties1.ma nat/iteration2.ma nat/totient.ma -R/Rexp.ma R/root.ma Z/times.ma nat/orders.ma didactic/exercises/natural_deduction1.ma didactic/support/natural_deduction.ma +R/Rexp.ma R/root.ma Z/times.ma nat/orders.ma nat/times.ma nat/plus.ma nat/chebyshev_thm.ma nat/neper.ma Z/z.ma datatypes/bool.ma nat/nat.ma demo/cantor.ma datatypes/constructors.ma demo/formal_topology.ma -dama/models/nat_ordered_uniform.ma dama/bishop_set_rewrite.ma dama/models/nat_uniform.ma dama/ordered_uniform.ma +decidable_kit/fgraph.ma decidable_kit/fintype.ma nat/nth_prime.ma nat/lt_arith.ma nat/primes.ma nat/le_arith.ma nat/orders.ma nat/times.ma -decidable_kit/fgraph.ma decidable_kit/fintype.ma +dama/models/nat_ordered_uniform.ma dama/bishop_set_rewrite.ma dama/models/nat_uniform.ma dama/ordered_uniform.ma dama/bishop_set.ma dama/ordered_set.ma nat/euler_theorem.ma nat/map_iter_p.ma nat/totient.ma Q/fraction/ftimes.ma Q/fraction/finv.ma Q/nat_fact/times.ma Q/ratio/ratio.ma Z/times.ma nat/factorial.ma nat/le_arith.ma Z/plus.ma Z/z.ma nat/minus.ma Q/ratio/rinv.ma Q/fraction/finv.ma Q/ratio/ratio.ma -dama/ordered_set.ma datatypes/constructors.ma logic/cprop_connectives.ma decidable_kit/streicher.ma logic/connectives.ma logic/equality.ma +dama/ordered_set.ma datatypes/constructors.ma logic/cprop_connectives.ma nat/fermat_little_theorem.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma -Q/q/qplus.ma nat/factorization.ma decidable_kit/list_aux.ma decidable_kit/eqtype.ma list/list.ma nat/plus.ma +Q/q/qplus.ma nat/factorization.ma R/r.ma Z/z.ma datatypes/constructors.ma logic/coimplication.ma logic/cprop_connectives.ma logic/equality.ma nat/orders.ma +Z/orders.ma Z/z.ma nat/orders.ma nat/map_iter_p.ma nat/count.ma nat/permutation.ma Q/q.ma Q/fraction/fraction.ma Z/compare.ma Z/plus.ma nat/factorization.ma -Z/orders.ma Z/z.ma nat/orders.ma nat/permutation.ma nat/compare.ma nat/sigma_and_pi.ma +formal_topology/saturations.ma formal_topology/relations.ma demo/realisability.ma datatypes/constructors.ma logic/connectives.ma -list/list.ma datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma nat/nat.ma nat/orders.ma nat/plus.ma +formal_topology/saturations_to_o-saturations.ma formal_topology/o-saturations.ma formal_topology/relations_to_o-algebra.ma formal_topology/saturations.ma +list/list.ma datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma nat/orders.ma nat/plus.ma nat/totient.ma nat/chinese_reminder.ma nat/iteration2.ma didactic/support/natural_deduction.ma nat/sigma_and_pi.ma nat/exp.ma nat/factorial.ma nat/lt_arith.ma nat/count.ma nat/permutation.ma nat/relevant_equations.ma nat/sigma_and_pi.ma +formal_topology/o-algebra.ma formal_topology/categories.ma +formal_topology/basic_pairs.ma formal_topology/notation.ma formal_topology/relations.ma Q/frac.ma Q/q/qinv.ma didactic/exercises/shannon.ma nat/minus.ma Q/q/qtimes.ma Q/q/qinv.ma Q/ratio/rtimes.ma +formal_topology/concrete_spaces.ma formal_topology/basic_pairs.ma nat/minus.ma nat/compare.ma nat/le_arith.ma +formal_topology/o-saturations.ma formal_topology/o-algebra.ma Q/ratio/ratio.ma Q/fraction/fraction.ma nat/chebyshev_teta.ma nat/binomial.ma nat/pi_p.ma algebra/finite_groups.ma algebra/groups.ma nat/relevant_equations.ma @@ -76,60 +88,73 @@ nat/pi_p.ma nat/generic_iter_p.ma nat/iteration2.ma nat/primes.ma algebra/semigroups.ma higher_order_defs/functions.ma dama/lebesgue.ma dama/ordered_set.ma dama/property_exhaustivity.ma dama/sandwich.ma dama/models/discrete_uniformity.ma dama/bishop_set_rewrite.ma dama/uniform.ma +formal_topology/relations.ma formal_topology/subsets.ma higher_order_defs/relations.ma logic/connectives.ma nat/factorization.ma nat/ord.ma nat/neper.ma nat/binomial.ma nat/chebyshev.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/log.ma Z/moebius.ma Z/sigma_p.ma nat/factorization.ma +formal_topology/r-o-basic_pairs.ma formal_topology/apply_functor.ma formal_topology/basic_pairs_to_o-basic_pairs.ma formal_topology/o-basic_pairs_to_o-basic_topologies.ma logic/equality.ma demo/toolbox.ma logic/cprop_connectives.ma nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma logic/coimplication.ma logic/connectives.ma nat/minimization.ma nat/minus.ma +formal_topology/apply_functor.ma formal_topology/categories.ma formal_topology/notation.ma logic/connectives2.ma higher_order_defs/relations.ma datatypes/subsets.ma datatypes/categories.ma logic/cprop_connectives.ma -nat/chebyshev.ma nat/factorial2.ma nat/factorization.ma nat/log.ma nat/o.ma nat/pi_p.ma decidable_kit/eqtype.ma datatypes/constructors.ma decidable_kit/decidable.ma +nat/chebyshev.ma nat/factorial2.ma nat/factorization.ma nat/log.ma nat/o.ma nat/pi_p.ma Q/q/q.ma Q/fraction/numerator_denominator.ma Q/ratio/ratio.ma dama/models/nat_lebesgue.ma dama/lebesgue.ma dama/models/nat_order_continuous.ma nat/bertrand.ma list/in.ma list/sort.ma nat/chebyshev.ma nat/chebyshev_teta.ma nat/o.ma nat/sieve.ma nat/sqrt.ma nat/nat.ma higher_order_defs/functions.ma +formal_topology/basic_pairs_to_basic_topologies.ma formal_topology/basic_pairs.ma formal_topology/basic_pairs_to_o-basic_pairs.ma formal_topology/basic_topologies.ma formal_topology/o-basic_pairs_to_o-basic_topologies.ma Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma dama/uniform.ma dama/supremum.ma demo/natural_deduction.ma didactic/support/natural_deduction.ma higher_order_defs/ordering.ma logic/equality.ma nat/congruence.ma nat/primes.ma nat/relevant_equations.ma logic/equality.ma higher_order_defs/relations.ma +formal_topology/o-concrete_spaces.ma formal_topology/o-basic_pairs.ma formal_topology/o-saturations.ma +formal_topology/o-basic_topologies.ma formal_topology/o-algebra.ma formal_topology/o-saturations.ma +formal_topology/concrete_spaces_to_o-concrete_spaces.ma formal_topology/basic_pairs_to_o-basic_pairs.ma formal_topology/concrete_spaces.ma formal_topology/o-concrete_spaces.ma dama/property_exhaustivity.ma dama/ordered_uniform.ma dama/property_sigma.ma +Z/compare.ma Z/orders.ma nat/compare.ma nat/gcd.ma nat/lt_arith.ma nat/primes.ma datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma -Z/compare.ma Z/orders.ma nat/compare.ma +Z/dirichlet_product.ma Z/sigma_p.ma Z/times.ma nat/primes.ma algebra/monoids.ma algebra/semigroups.ma nat/div_and_mod.ma datatypes/constructors.ma nat/minus.ma -Z/dirichlet_product.ma Z/sigma_p.ma Z/times.ma nat/primes.ma nat/sqrt.ma nat/compare.ma nat/log.ma nat/times.ma datatypes/categories.ma logic/cprop_connectives.ma +formal_topology/o-basic_pairs.ma formal_topology/notation.ma formal_topology/o-algebra.ma +formal_topology/categories.ma formal_topology/cprop_connectives.ma logic/equality.ma nat/relevant_equations.ma nat/gcd.ma nat/minus.ma nat/times.ma +formal_topology/notation.ma dama/nat_ordered_set.ma nat/orders.ma dama/bishop_set.ma nat/compare.ma -dama/russell_support.ma logic/cprop_connectives.ma nat/nat.ma Q/fraction/finv.ma Q/fraction/fraction.ma Z/plus.ma +dama/russell_support.ma logic/cprop_connectives.ma nat/nat.ma +formal_topology/relations_to_o-algebra.ma formal_topology/o-algebra.ma formal_topology/relations.ma nat/binomial.ma nat/factorial2.ma nat/iteration2.ma -R/root.ma logic/connectives.ma Q/q/q.ma R/r.ma nat/log.ma datatypes/constructors.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/minimization.ma nat/primes.ma nat/relevant_equations.ma +R/root.ma logic/connectives.ma Q/q/q.ma R/r.ma higher_order_defs/functions.ma logic/equality.ma Q/fraction/numerator_denominator.ma Q/fraction/finv.ma nat/generic_iter_p.ma nat/div_and_mod_diseq.ma nat/ord.ma nat/primes.ma datatypes/constructors.ma logic/equality.ma didactic/exercises/natural_deduction_theories.ma didactic/support/natural_deduction.ma nat/plus.ma -nat/plus.ma nat/nat.ma Q/fraction/fraction.ma Z/compare.ma nat/factorization.ma +nat/plus.ma nat/nat.ma +formal_topology/o-formal_topologies.ma formal_topology/o-basic_topologies.ma dama/sequence.ma nat/nat.ma nat/primes.ma nat/div_and_mod.ma nat/factorial.ma nat/minimization.ma nat/sigma_and_pi.ma nat/gcd_properties1.ma nat/gcd.ma list/sort.ma datatypes/bool.ma datatypes/constructors.ma list/in.ma didactic/exercises/natural_deduction.ma didactic/support/natural_deduction.ma +formal_topology/basic_pairs_to_o-basic_pairs.ma formal_topology/basic_pairs.ma formal_topology/o-basic_pairs.ma formal_topology/relations_to_o-algebra.ma dama/bishop_set_rewrite.ma dama/bishop_set.ma Z/times.ma Z/plus.ma nat/lt_arith.ma -R/Rlog.ma R/Rexp.ma Z/sigma_p.ma Z/times.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma +R/Rlog.ma R/Rexp.ma nat/o.ma nat/binomial.ma nat/sqrt.ma dama/property_sigma.ma dama/ordered_uniform.ma dama/russell_support.ma Q/inv.ma Q/fraction/finv.ma Q/q.ma Q/q/q.ma diff --git a/helm/software/matita/contribs/formal_topology/overlap/apply_functor.ma b/helm/software/matita/library/formal_topology/apply_functor.ma similarity index 98% rename from helm/software/matita/contribs/formal_topology/overlap/apply_functor.ma rename to helm/software/matita/library/formal_topology/apply_functor.ma index 81cf6d8e2..89f3400a2 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/apply_functor.ma +++ b/helm/software/matita/library/formal_topology/apply_functor.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "categories.ma". -include "notation.ma". +include "formal_topology/categories.ma". +include "formal_topology/notation.ma". record Fo (C1,C2:CAT2) (F:arrows3 CAT2 C1 C2) : Type2 ≝ { F2: C2; diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma b/helm/software/matita/library/formal_topology/basic_pairs.ma similarity index 99% rename from helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma rename to helm/software/matita/library/formal_topology/basic_pairs.ma index 8e5421c1f..8235b2571 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma +++ b/helm/software/matita/library/formal_topology/basic_pairs.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "relations.ma". -include "notation.ma". +include "formal_topology/relations.ma". +include "formal_topology/notation.ma". record basic_pair: Type1 ≝ { concr: REL; form: REL; rel: concr ⇒_\r1 form diff --git a/helm/software/matita/library/formal_topology/basic_pairs.ma.dontcompile b/helm/software/matita/library/formal_topology/basic_pairs.ma.dontcompile deleted file mode 100644 index 0d51724de..000000000 --- a/helm/software/matita/library/formal_topology/basic_pairs.ma.dontcompile +++ /dev/null @@ -1,179 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 "formal_topology/relations.ma". -include "datatypes/categories.ma". - -record basic_pair: Type ≝ - { concr: REL; - form: REL; - rel: arrows1 ? concr form - }. - -notation "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y}. -notation "⊩" with precedence 60 for @{'Vdash}. - -interpretation "basic pair relation" 'Vdash2 x y = (rel _ x y). -interpretation "basic pair relation (non applied)" 'Vdash = (rel _). - -record relation_pair (BP1,BP2: basic_pair): Type ≝ - { concr_rel: arrows1 ? (concr BP1) (concr BP2); - form_rel: arrows1 ? (form BP1) (form BP2); - commute: ⊩ ∘ concr_rel = form_rel ∘ ⊩ - }. - -notation "hvbox (r \sub \c)" with precedence 90 for @{'concr_rel $r}. -notation "hvbox (r \sub \f)" with precedence 90 for @{'form_rel $r}. - -interpretation "concrete relation" 'concr_rel r = (concr_rel __ r). -interpretation "formal relation" 'form_rel r = (form_rel __ r). - -definition relation_pair_equality: - ∀o1,o2. equivalence_relation1 (relation_pair o1 o2). - intros; - constructor 1; - [ apply (λr,r'. ⊩ ∘ r \sub\c = ⊩ ∘ r' \sub\c); - | simplify; - intros; - apply refl1; - | simplify; - intros 2; - apply sym1; - | simplify; - intros 3; - apply trans1; - ] -qed. - -definition relation_pair_setoid: basic_pair → basic_pair → setoid1. - intros; - constructor 1; - [ apply (relation_pair b b1) - | apply relation_pair_equality - ] -qed. - -lemma eq_to_eq': ∀o1,o2.∀r,r': relation_pair_setoid o1 o2. r=r' → r \sub\f ∘ ⊩ = r'\sub\f ∘ ⊩. - intros 7 (o1 o2 r r' H c1 f2); - split; intro H1; - [ lapply (fi ?? (commute ?? r c1 f2) H1) as H2; - lapply (if ?? (H c1 f2) H2) as H3; - apply (if ?? (commute ?? r' c1 f2) H3); - | lapply (fi ?? (commute ?? r' c1 f2) H1) as H2; - lapply (fi ?? (H c1 f2) H2) as H3; - apply (if ?? (commute ?? r c1 f2) H3); - ] -qed. - -definition id_relation_pair: ∀o:basic_pair. relation_pair o o. - intro; - constructor 1; - [1,2: apply id1; - | lapply (id_neutral_right1 ? (concr o) ? (⊩)) as H; - lapply (id_neutral_left1 ?? (form o) (⊩)) as H1; - apply (.= H); - apply (H1 \sup -1);] -qed. - -definition relation_pair_composition: - ∀o1,o2,o3. binary_morphism1 (relation_pair_setoid o1 o2) (relation_pair_setoid o2 o3) (relation_pair_setoid o1 o3). - intros; - constructor 1; - [ intros (r r1); - constructor 1; - [ apply (r1 \sub\c ∘ r \sub\c) - | apply (r1 \sub\f ∘ r \sub\f) - | lapply (commute ?? r) as H; - lapply (commute ?? r1) as H1; - apply (.= ASSOC1); - apply (.= #‡H1); - apply (.= ASSOC1\sup -1); - apply (.= H‡#); - apply ASSOC1] - | intros; - change with (⊩ ∘ (b\sub\c ∘ a\sub\c) = ⊩ ∘ (b'\sub\c ∘ a'\sub\c)); - change in H with (⊩ ∘ a \sub\c = ⊩ ∘ a' \sub\c); - change in H1 with (⊩ ∘ b \sub\c = ⊩ ∘ b' \sub\c); - apply (.= ASSOC1); - apply (.= #‡H1); - apply (.= #‡(commute ?? b')); - apply (.= ASSOC1 \sup -1); - apply (.= H‡#); - apply (.= ASSOC1); - apply (.= #‡(commute ?? b')\sup -1); - apply (ASSOC1 \sup -1)] -qed. - -definition BP: category1. - constructor 1; - [ apply basic_pair - | apply relation_pair_setoid - | apply id_relation_pair - | apply relation_pair_composition - | intros; - change with (⊩ ∘ (a34\sub\c ∘ (a23\sub\c ∘ a12\sub\c)) = - ⊩ ∘ ((a34\sub\c ∘ a23\sub\c) ∘ a12\sub\c)); - apply (ASSOC1‡#); - | intros; - change with (⊩ ∘ (a\sub\c ∘ (id_relation_pair o1)\sub\c) = ⊩ ∘ a\sub\c); - apply ((id_neutral_right1 ????)‡#); - | intros; - change with (⊩ ∘ ((id_relation_pair o2)\sub\c ∘ a\sub\c) = ⊩ ∘ a\sub\c); - apply ((id_neutral_left1 ????)‡#);] -qed. - -definition BPext: ∀o: BP. form o ⇒ Ω \sup (concr o). - intros; constructor 1; - [ apply (ext ? ? (rel o)); - | intros; - apply (.= #‡H); - apply refl1] -qed. - -definition BPextS: ∀o: BP. Ω \sup (form o) ⇒ Ω \sup (concr o) ≝ - λo.extS ?? (rel o). - -definition fintersects: ∀o: BP. binary_morphism1 (form o) (form o) (Ω \sup (form o)). - intros (o); constructor 1; - [ apply (λa,b: form o.{c | BPext o c ⊆ BPext o a ∩ BPext o b }); - intros; simplify; apply (.= (†H)‡#); apply refl1 - | intros; split; simplify; intros; - [ apply (. #‡((†H)‡(†H1))); assumption - | apply (. #‡((†H\sup -1)‡(†H1\sup -1))); assumption]] -qed. - -interpretation "fintersects" 'fintersects U V = (fun1 ___ (fintersects _) U V). - -definition fintersectsS: - ∀o:BP. binary_morphism1 (Ω \sup (form o)) (Ω \sup (form o)) (Ω \sup (form o)). - intros (o); constructor 1; - [ apply (λo: basic_pair.λa,b: Ω \sup (form o).{c | BPext o c ⊆ BPextS o a ∩ BPextS o b }); - intros; simplify; apply (.= (†H)‡#); apply refl1 - | intros; split; simplify; intros; - [ apply (. #‡((†H)‡(†H1))); assumption - | apply (. #‡((†H\sup -1)‡(†H1\sup -1))); assumption]] -qed. - -interpretation "fintersectsS" 'fintersects U V = (fun1 ___ (fintersectsS _) U V). - -definition relS: ∀o: BP. binary_morphism1 (concr o) (Ω \sup (form o)) CPROP. - intros (o); constructor 1; - [ apply (λx:concr o.λS: Ω \sup (form o).∃y: form o.y ∈ S ∧ x ⊩ y); - | intros; split; intros; cases H2; exists [1,3: apply w] - [ apply (. (#‡H1)‡(H‡#)); assumption - | apply (. (#‡H1 \sup -1)‡(H \sup -1‡#)); assumption]] -qed. - -interpretation "basic pair relation for subsets" 'Vdash2 x y = (fun1 (concr _) __ (relS _) x y). -interpretation "basic pair relation for subsets (non applied)" 'Vdash = (fun1 ___ (relS _)). diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_basic_topologies.ma b/helm/software/matita/library/formal_topology/basic_pairs_to_basic_topologies.ma similarity index 86% rename from helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_basic_topologies.ma rename to helm/software/matita/library/formal_topology/basic_pairs_to_basic_topologies.ma index b557bedae..ac137748f 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_basic_topologies.ma +++ b/helm/software/matita/library/formal_topology/basic_pairs_to_basic_topologies.ma @@ -12,10 +12,10 @@ (* *) (**************************************************************************) -include "basic_pairs_to_o-basic_pairs.ma". -include "o-basic_pairs_to_o-basic_topologies.ma". -include "basic_pairs.ma". -include "basic_topologies.ma". +include "formal_topology/basic_pairs_to_o-basic_pairs.ma". +include "formal_topology/o-basic_pairs_to_o-basic_topologies.ma". +include "formal_topology/basic_pairs.ma". +include "formal_topology/basic_topologies.ma". definition basic_topology_of_basic_pair: basic_pair → basic_topology. intro bp; @@ -47,11 +47,12 @@ alias symbol "compose" (instance 3) = "category1 composition". record functor1 (C1: category1) (C2: category1) : Type2 ≝ { map_objs1:1> C1 → C2; map_arrows1: ∀S,T. unary_morphism1 (arrows1 ? S T) (arrows1 ? (map_objs1 S) (map_objs1 T)); - respects_id1: ∀o:C1. map_arrows1 ?? (id1 ? o) = id1 ? (map_objs1 o); + respects_id1: ∀o:C1. map_arrows1 ?? (id1 ? o) =_1 id1 ? (map_objs1 o); respects_comp1: ∀o1,o2,o3.∀f1:arrows1 ? o1 o2.∀f2:arrows1 ? o2 o3. - map_arrows1 ?? (f2 ∘ f1) = map_arrows1 ?? f2 ∘ map_arrows1 ?? f1}. + map_arrows1 ?? (f2 ∘ f1) =_1 map_arrows1 ?? f2 ∘ map_arrows1 ?? f1}. +(* definition BTop_of_BP: functor1 BP BTop. lapply OR as F; constructor 1; @@ -59,4 +60,5 @@ definition BTop_of_BP: functor1 BP BTop. | intros; constructor 1 [ apply continuous_relation_of_relation_pair; ] | simplify; intro; ] -qed. \ No newline at end of file +qed. +*) \ No newline at end of file diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma b/helm/software/matita/library/formal_topology/basic_pairs_to_o-basic_pairs.ma similarity index 97% rename from helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma rename to helm/software/matita/library/formal_topology/basic_pairs_to_o-basic_pairs.ma index b72e4a5fa..aee034683 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma +++ b/helm/software/matita/library/formal_topology/basic_pairs_to_o-basic_pairs.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "basic_pairs.ma". -include "o-basic_pairs.ma". -include "relations_to_o-algebra.ma". +include "formal_topology/basic_pairs.ma". +include "formal_topology/o-basic_pairs.ma". +include "formal_topology/relations_to_o-algebra.ma". definition o_basic_pair_of_basic_pair: basic_pair → Obasic_pair. intro b; diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_topologies.ma b/helm/software/matita/library/formal_topology/basic_topologies.ma similarity index 99% rename from helm/software/matita/contribs/formal_topology/overlap/basic_topologies.ma rename to helm/software/matita/library/formal_topology/basic_topologies.ma index 5cb82832a..0c153b9d3 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/basic_topologies.ma +++ b/helm/software/matita/library/formal_topology/basic_topologies.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "relations.ma". -include "saturations.ma". +include "formal_topology/relations.ma". +include "formal_topology/saturations.ma". record basic_topology: Type1 ≝ { carrbt:> REL; diff --git a/helm/software/matita/library/formal_topology/basic_topologies.ma.dontcompile b/helm/software/matita/library/formal_topology/basic_topologies.ma.dontcompile deleted file mode 100644 index 36a0d24c8..000000000 --- a/helm/software/matita/library/formal_topology/basic_topologies.ma.dontcompile +++ /dev/null @@ -1,199 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 "formal_topology/relations.ma". -include "datatypes/categories.ma". -include "formal_topology/saturations_reductions.ma". - -record basic_topology: Type ≝ - { carrbt:> REL; - A: unary_morphism (Ω \sup carrbt) (Ω \sup carrbt); - J: unary_morphism (Ω \sup carrbt) (Ω \sup carrbt); - A_is_saturation: is_saturation ? A; - J_is_reduction: is_reduction ? J; - compatibility: ∀U,V. (A U ≬ J V) = (U ≬ J V) - }. - -record continuous_relation (S,T: basic_topology) : Type ≝ - { cont_rel:> arrows1 ? S T; - reduced: ∀U. U = J ? U → image ?? cont_rel U = J ? (image ?? cont_rel U); - saturated: ∀U. U = A ? U → minus_star_image ?? cont_rel U = A ? (minus_star_image ?? cont_rel U) - }. - -definition continuous_relation_setoid: basic_topology → basic_topology → setoid1. - intros (S T); constructor 1; - [ apply (continuous_relation S T) - | constructor 1; - [ apply (λr,s:continuous_relation S T.∀b. A ? (ext ?? r b) = A ? (ext ?? s b)); - | simplify; intros; apply refl1; - | simplify; intros; apply sym1; apply H - | simplify; intros; apply trans1; [2: apply H |3: apply H1; |1: skip]]] -qed. - -definition cont_rel': ∀S,T: basic_topology. continuous_relation_setoid S T → arrows1 ? S T ≝ cont_rel. - -coercion cont_rel'. - -definition cont_rel'': ∀S,T: basic_topology. continuous_relation_setoid S T → binary_relation S T ≝ cont_rel. - -coercion cont_rel''. - -theorem continuous_relation_eq': - ∀o1,o2.∀a,a': continuous_relation_setoid o1 o2. - a = a' → ∀X.minus_star_image ?? a (A o1 X) = minus_star_image ?? a' (A o1 X). - intros; split; intro; unfold minus_star_image; simplify; intros; - [ cut (ext ?? a a1 ⊆ A ? X); [2: intros 2; apply (H1 a2); cases f1; assumption;] - lapply (if ?? (A_is_saturation ???) Hcut); clear Hcut; - cut (A ? (ext ?? a' a1) ⊆ A ? X); [2: apply (. (H ?)‡#); assumption] - lapply (fi ?? (A_is_saturation ???) Hcut); - apply (Hletin1 x); change with (x ∈ ext ?? a' a1); split; simplify; - [ apply I | assumption ] - | cut (ext ?? a' a1 ⊆ A ? X); [2: intros 2; apply (H1 a2); cases f1; assumption;] - lapply (if ?? (A_is_saturation ???) Hcut); clear Hcut; - cut (A ? (ext ?? a a1) ⊆ A ? X); [2: apply (. (H ?)\sup -1‡#); assumption] - lapply (fi ?? (A_is_saturation ???) Hcut); - apply (Hletin1 x); change with (x ∈ ext ?? a a1); split; simplify; - [ apply I | assumption ]] -qed. - -theorem continuous_relation_eq_inv': - ∀o1,o2.∀a,a': continuous_relation_setoid o1 o2. - (∀X.minus_star_image ?? a (A o1 X) = minus_star_image ?? a' (A o1 X)) → a=a'. - intros 6; - cut (∀a,a': continuous_relation_setoid o1 o2. - (∀X.minus_star_image ?? a (A o1 X) = minus_star_image ?? a' (A o1 X)) → - ∀V:o2. A ? (ext ?? a' V) ⊆ A ? (ext ?? a V)); - [2: clear b H a' a; intros; - lapply depth=0 (λV.saturation_expansive ??? (extS ?? a V)); [2: apply A_is_saturation;|skip] - (* fundamental adjunction here! to be taken out *) - cut (∀V:Ω \sup o2.V ⊆ minus_star_image ?? a (A ? (extS ?? a V))); - [2: intro; intros 2; unfold minus_star_image; simplify; intros; - apply (Hletin V1 x); whd; split; [ exact I | exists; [apply a1] split; assumption]] - clear Hletin; - cut (∀V:Ω \sup o2.V ⊆ minus_star_image ?? a' (A ? (extS ?? a V))); - [2: intro; apply (. #‡(H ?)); apply Hcut] clear H Hcut; - (* second half of the fundamental adjunction here! to be taken out too *) - intro; lapply (Hcut1 (singleton ? V)); clear Hcut1; - unfold minus_star_image in Hletin; unfold singleton in Hletin; simplify in Hletin; - whd in Hletin; whd in Hletin:(?→?→%); simplify in Hletin; - apply (if ?? (A_is_saturation ???)); - intros 2 (x H); lapply (Hletin V ? x ?); - [ apply refl | cases H; assumption; ] - change with (x ∈ A ? (ext ?? a V)); - apply (. #‡(†(extS_singleton ????))); - assumption;] - split; apply Hcut; [2: assumption | intro; apply sym1; apply H] -qed. - -definition continuous_relation_comp: - ∀o1,o2,o3. - continuous_relation_setoid o1 o2 → - continuous_relation_setoid o2 o3 → - continuous_relation_setoid o1 o3. - intros (o1 o2 o3 r s); constructor 1; - [ apply (s ∘ r) - | intros; - apply sym1; - apply (.= †(image_comp ??????)); - apply (.= (reduced ?????)\sup -1); - [ apply (.= (reduced ?????)); [ assumption | apply refl1 ] - | apply (.= (image_comp ??????)\sup -1); - apply refl1] - | intros; - apply sym1; - apply (.= †(minus_star_image_comp ??????)); - apply (.= (saturated ?????)\sup -1); - [ apply (.= (saturated ?????)); [ assumption | apply refl1 ] - | apply (.= (minus_star_image_comp ??????)\sup -1); - apply refl1]] -qed. - -definition BTop: category1. - constructor 1; - [ apply basic_topology - | apply continuous_relation_setoid - | intro; constructor 1; - [ apply id1 - | intros; - apply (.= (image_id ??)); - apply sym1; - apply (.= †(image_id ??)); - apply sym1; - assumption - | intros; - apply (.= (minus_star_image_id ??)); - apply sym1; - apply (.= †(minus_star_image_id ??)); - apply sym1; - assumption] - | intros; constructor 1; - [ apply continuous_relation_comp; - | intros; simplify; intro x; simplify; - lapply depth=0 (continuous_relation_eq' ???? H) as H'; - lapply depth=0 (continuous_relation_eq' ???? H1) as H1'; - letin K ≝ (λX.H1' (minus_star_image ?? a (A ? X))); clearbody K; - cut (∀X:Ω \sup o1. - minus_star_image o2 o3 b (A o2 (minus_star_image o1 o2 a (A o1 X))) - = minus_star_image o2 o3 b' (A o2 (minus_star_image o1 o2 a' (A o1 X)))); - [2: intro; apply sym1; apply (.= #‡(†((H' ?)\sup -1))); apply sym1; apply (K X);] - clear K H' H1'; - cut (∀X:Ω \sup o1. - minus_star_image o1 o3 (b ∘ a) (A o1 X) = minus_star_image o1 o3 (b'∘a') (A o1 X)); - [2: intro; - apply (.= (minus_star_image_comp ??????)); - apply (.= #‡(saturated ?????)); - [ apply ((saturation_idempotent ????) \sup -1); apply A_is_saturation ] - apply sym1; - apply (.= (minus_star_image_comp ??????)); - apply (.= #‡(saturated ?????)); - [ apply ((saturation_idempotent ????) \sup -1); apply A_is_saturation ] - apply ((Hcut X) \sup -1)] - clear Hcut; generalize in match x; clear x; - apply (continuous_relation_eq_inv'); - apply Hcut1;] - | intros; simplify; intro; do 2 (unfold continuous_relation_comp); simplify; - apply (.= †(ASSOC1‡#)); - apply refl1 - | intros; simplify; intro; unfold continuous_relation_comp; simplify; - apply (.= †((id_neutral_right1 ????)‡#)); - apply refl1 - | intros; simplify; intro; simplify; - apply (.= †((id_neutral_left1 ????)‡#)); - apply refl1] -qed. - -(*CSC: unused! *) -(* this proof is more logic-oriented than set/lattice oriented *) -theorem continuous_relation_eqS: - ∀o1,o2:basic_topology.∀a,a': continuous_relation_setoid o1 o2. - a = a' → ∀X. A ? (extS ?? a X) = A ? (extS ?? a' X). - intros; - cut (∀a: arrows1 ? o1 ?.∀x. x ∈ extS ?? a X → ∃y:o2.y ∈ X ∧ x ∈ ext ?? a y); - [2: intros; cases f; clear f; cases H1; exists [apply w] cases x1; split; - try assumption; split; assumption] - cut (∀a,a':continuous_relation_setoid o1 o2.eq1 ? a a' → ∀x. x ∈ extS ?? a X → ∃y:o2. y ∈ X ∧ x ∈ A ? (ext ?? a' y)); - [2: intros; cases (Hcut ?? f); exists; [apply w] cases x1; split; try assumption; - apply (. #‡(H1 ?)); - apply (saturation_expansive ?? (A_is_saturation o1) (ext ?? a1 w) x); - assumption;] clear Hcut; - split; apply (if ?? (A_is_saturation ???)); intros 2; - [lapply (Hcut1 a a' H a1 f) | lapply (Hcut1 a' a (H \sup -1) a1 f)] - cases Hletin; clear Hletin; cases x; clear x; - cut (∀a: arrows1 ? o1 ?. ext ?? a w ⊆ extS ?? a X); - [2,4: intros 3; cases f3; clear f3; simplify in f5; split; try assumption; - exists [1,3: apply w] split; assumption;] - cut (∀a. A ? (ext o1 o2 a w) ⊆ A ? (extS o1 o2 a X)); - [2,4: intros; apply saturation_monotone; try (apply A_is_saturation); apply Hcut;] - apply Hcut2; assumption. -qed. diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_topologies_to_o-basic_topologies.ma b/helm/software/matita/library/formal_topology/basic_topologies_to_o-basic_topologies.ma similarity index 95% rename from helm/software/matita/contribs/formal_topology/overlap/basic_topologies_to_o-basic_topologies.ma rename to helm/software/matita/library/formal_topology/basic_topologies_to_o-basic_topologies.ma index bea3207b6..88f9e2393 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/basic_topologies_to_o-basic_topologies.ma +++ b/helm/software/matita/library/formal_topology/basic_topologies_to_o-basic_topologies.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "basic_topologies.ma". -include "o-basic_topologies.ma". -include "relations_to_o-algebra.ma". +include "formal_topology/basic_topologies.ma". +include "formal_topology/o-basic_topologies.ma". +include "formal_topology/relations_to_o-algebra.ma". definition o_basic_topology_of_basic_topology: basic_topology → Obasic_topology. intros (b); constructor 1; @@ -63,9 +63,8 @@ theorem BTop_to_OBTop_faithful: apply sym2; apply e; qed. -*) -include "notation.ma". +include "formal_topology/notation.ma". theorem BTop_to_OBTop_full: ∀S,T.∀f. exT22 ? (λg. map_arrows2 ?? BTop_to_OBTop S T g = f). @@ -84,4 +83,5 @@ theorem BTop_to_OBTop_full: | simplify; unfold BTop_to_OBTop; simplify; unfold o_continuous_relation_of_continuous_relation_morphism; simplify; cases Hg; whd; simplify; intro; -qed. \ No newline at end of file +qed. +*) diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/library/formal_topology/categories.ma similarity index 99% rename from helm/software/matita/contribs/formal_topology/overlap/categories.ma rename to helm/software/matita/library/formal_topology/categories.ma index 65320ae53..a9c2c9d9e 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma +++ b/helm/software/matita/library/formal_topology/categories.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "cprop_connectives.ma". +include "formal_topology/cprop_connectives.ma". notation "hvbox(a break = \sub \ID b)" non associative with precedence 45 for @{ 'eqID $a $b }. diff --git a/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma b/helm/software/matita/library/formal_topology/concrete_spaces.ma similarity index 97% rename from helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma rename to helm/software/matita/library/formal_topology/concrete_spaces.ma index 791af46b3..69ff6f134 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma +++ b/helm/software/matita/library/formal_topology/concrete_spaces.ma @@ -12,10 +12,10 @@ (* *) (**************************************************************************) -include "basic_pairs.ma". +include "formal_topology/basic_pairs.ma". (* carr1 e' necessario perche' ci sega via la coercion per gli oggetti di REL! - (confondendola con la coercion per gli oggetti di SET *) + (confondendola con la coercion per gli oggetti di SET record concrete_space : Type1 ≝ { bp:> BP; converges: ∀a: carr1 (concr bp).∀U,V: carr1 (form bp). a ⊩ U → a ⊩ V → a ⊩ (U ↓ V); @@ -31,7 +31,7 @@ record convergent_relation_pair (CS1,CS2: concrete_space) : Type1 ≝ respects_all_covered: minus_image ?? rp\sub\c (BPextS CS2 (full_subset (form CS2))) = BPextS CS1 (full_subset (form CS1)) }. -(* + definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid1. intros; constructor 1; diff --git a/helm/software/matita/library/formal_topology/concrete_spaces.ma.dontcompile b/helm/software/matita/library/formal_topology/concrete_spaces.ma.dontcompile deleted file mode 100644 index 3c03b4e66..000000000 --- a/helm/software/matita/library/formal_topology/concrete_spaces.ma.dontcompile +++ /dev/null @@ -1,120 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 "formal_topology/basic_pairs.ma". - -record concrete_space : Type ≝ - { bp:> BP; - converges: ∀a: concr bp.∀U,V: form bp. a ⊩ U → a ⊩ V → a ⊩ (U ↓ V); - all_covered: ∀x: concr bp. x ⊩ form bp - }. - -definition bp': concrete_space → basic_pair ≝ λc.bp c. - -coercion bp'. - -record convergent_relation_pair (CS1,CS2: concrete_space) : Type ≝ - { rp:> arrows1 ? CS1 CS2; - respects_converges: - ∀b,c. - extS ?? rp \sub\c (BPextS CS2 (b ↓ c)) = - BPextS CS1 ((extS ?? rp \sub\f b) ↓ (extS ?? rp \sub\f c)); - respects_all_covered: - extS ?? rp\sub\c (BPextS CS2 (form CS2)) = BPextS CS1 (form CS1) - }. - -definition rp' : ∀CS1,CS2. convergent_relation_pair CS1 CS2 → relation_pair CS1 CS2 ≝ - λCS1,CS2,c. rp CS1 CS2 c. - -coercion rp'. - -definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid1. - intros; - constructor 1; - [ apply (convergent_relation_pair c c1) - | constructor 1; - [ intros; - apply (relation_pair_equality c c1 c2 c3); - | intros 1; apply refl1; - | intros 2; apply sym1; - | intros 3; apply trans1]] -qed. - -definition rp'': ∀CS1,CS2.convergent_relation_space_setoid CS1 CS2 → arrows1 BP CS1 CS2 ≝ - λCS1,CS2,c.rp ?? c. - -coercion rp''. - -definition convergent_relation_space_composition: - ∀o1,o2,o3: concrete_space. - binary_morphism1 - (convergent_relation_space_setoid o1 o2) - (convergent_relation_space_setoid o2 o3) - (convergent_relation_space_setoid o1 o3). - intros; constructor 1; - [ intros; whd in c c1 ⊢ %; - constructor 1; - [ apply (fun1 ??? (comp1 BP ???)); [apply (bp o2) |*: apply rp; assumption] - | intros; - change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c1 \sub \c ∘ c \sub \c); - change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? (? ? ? (? ? ? %) ?) ?))) - with (c1 \sub \f ∘ c \sub \f); - change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? ? (? ? ? (? ? ? %) ?)))) - with (c1 \sub \f ∘ c \sub \f); - apply (.= (extS_com ??????)); - apply (.= (†(respects_converges ?????))); - apply (.= (respects_converges ?????)); - apply (.= (†(((extS_com ??????) \sup -1)‡(extS_com ??????)\sup -1))); - apply refl1; - | change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c1 \sub \c ∘ c \sub \c); - apply (.= (extS_com ??????)); - apply (.= (†(respects_all_covered ???))); - apply (.= respects_all_covered ???); - apply refl1] - | intros; - change with (b ∘ a = b' ∘ a'); - change in H with (rp'' ?? a = rp'' ?? a'); - change in H1 with (rp'' ?? b = rp ?? b'); - apply (.= (H‡H1)); - apply refl1] -qed. - -definition CSPA: category1. - constructor 1; - [ apply concrete_space - | apply convergent_relation_space_setoid - | intro; constructor 1; - [ apply id1 - | intros; - unfold id; simplify; - apply (.= (equalset_extS_id_X_X ??)); - apply (.= (†((equalset_extS_id_X_X ??)\sup -1‡ - (equalset_extS_id_X_X ??)\sup -1))); - apply refl1; - | apply (.= (equalset_extS_id_X_X ??)); - apply refl1] - | apply convergent_relation_space_composition - | intros; simplify; - change with (a34 ∘ (a23 ∘ a12) = (a34 ∘ a23) ∘ a12); - apply (.= ASSOC1); - apply refl1 - | intros; simplify; - change with (a ∘ id1 ? o1 = a); - apply (.= id_neutral_right1 ????); - apply refl1 - | intros; simplify; - change with (id1 ? o2 ∘ a = a); - apply (.= id_neutral_left1 ????); - apply refl1] -qed. diff --git a/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces_to_o-concrete_spaces.ma b/helm/software/matita/library/formal_topology/concrete_spaces_to_o-concrete_spaces.ma similarity index 93% rename from helm/software/matita/contribs/formal_topology/overlap/concrete_spaces_to_o-concrete_spaces.ma rename to helm/software/matita/library/formal_topology/concrete_spaces_to_o-concrete_spaces.ma index 3f2417ec9..29ff0754a 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces_to_o-concrete_spaces.ma +++ b/helm/software/matita/library/formal_topology/concrete_spaces_to_o-concrete_spaces.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "concrete_spaces.ma". -include "o-concrete_spaces.ma". -include "basic_pairs_to_o-basic_pairs.ma". +include "formal_topology/concrete_spaces.ma". +include "formal_topology/o-concrete_spaces.ma". +include "formal_topology/basic_pairs_to_o-basic_pairs.ma". (* (* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *) diff --git a/helm/software/matita/contribs/formal_topology/overlap/cprop_connectives.ma b/helm/software/matita/library/formal_topology/cprop_connectives.ma similarity index 100% rename from helm/software/matita/contribs/formal_topology/overlap/cprop_connectives.ma rename to helm/software/matita/library/formal_topology/cprop_connectives.ma diff --git a/helm/software/matita/contribs/formal_topology/overlap/formal_topologies.ma b/helm/software/matita/library/formal_topology/formal_topologies.ma similarity index 98% rename from helm/software/matita/contribs/formal_topology/overlap/formal_topologies.ma rename to helm/software/matita/library/formal_topology/formal_topologies.ma index 24dfb7721..177eb454e 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/formal_topologies.ma +++ b/helm/software/matita/library/formal_topology/formal_topologies.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_topologies.ma". +include "formal_topology/basic_topologies.ma". (* definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S). diff --git a/helm/software/matita/library/formal_topology/formal_topologies.ma.dontcompile b/helm/software/matita/library/formal_topology/formal_topologies.ma.dontcompile deleted file mode 100644 index f47323e00..000000000 --- a/helm/software/matita/library/formal_topology/formal_topologies.ma.dontcompile +++ /dev/null @@ -1,121 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 "formal_topology/basic_topologies.ma". - -definition btop_carr: BTop → Type ≝ λo:BTop. carr (carrbt o). - -coercion btop_carr. - -definition btop_carr': BTop → setoid ≝ λo:BTop. carrbt o. - -coercion btop_carr'. - -definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S). - intros; constructor 1; - [ apply (λU:Ω \sup S.{a | ∃b:carrbt S. b ∈ U ∧ a ∈ A ? (singleton ? b)}); - intros; simplify; split; intro; cases H1; cases x; exists [1,3: apply w] - split; try assumption; [ apply (. H‡#) | apply (. H \sup -1‡#) ] assumption - | intros; split; intros 2; cases f; exists; [1,3: apply w] cases x; split; - try assumption; [ apply (. #‡H) | apply (. #‡H \sup -1)] assumption] -qed. - -interpretation "downarrow" 'downarrow a = (fun_1 __ (downarrow _) a). - -definition ffintersects: ∀S:BTop. binary_morphism1 (Ω \sup S) (Ω \sup S) (Ω \sup S). - intros; constructor 1; - [ apply (λU,V. ↓U ∩ ↓V); - | intros; apply (.= (†H)‡(†H1)); apply refl1] -qed. - -interpretation "ffintersects" 'fintersects U V = (fun1 ___ (ffintersects _) U V). - -record formal_topology: Type ≝ - { bt:> BTop; - converges: ∀U,V: Ω \sup bt. A ? (U ↓ V) = A ? U ∩ A ? V - }. - -definition bt': formal_topology → basic_topology ≝ λo:formal_topology.bt o. - -coercion bt'. - -definition ffintersects': ∀S:BTop. binary_morphism1 S S (Ω \sup S). - intros; constructor 1; - [ apply (λb,c:S. (singleton S b) ↓ (singleton S c)); - | intros; apply (.= (†H)‡(†H1)); apply refl1] -qed. - -interpretation "ffintersects'" 'fintersects U V = (fun1 ___ (ffintersects' _) U V). - -record formal_map (S,T: formal_topology) : Type ≝ - { cr:> continuous_relation_setoid S T; - C1: ∀b,c. extS ?? cr (b ↓ c) = ext ?? cr b ↓ ext ?? cr c; - C2: extS ?? cr T = S - }. - -definition cr': ∀FT1,FT2.formal_map FT1 FT2 → continuous_relation FT1 FT2 ≝ - λFT1,FT2,c. cr FT1 FT2 c. - -coercion cr'. - -definition formal_map_setoid: formal_topology → formal_topology → setoid1. - intros (S T); constructor 1; - [ apply (formal_map S T); - | constructor 1; - [ apply (λf,f1: formal_map S T.f=f1); - | simplify; intros 1; apply refl1 - | simplify; intros 2; apply sym1 - | simplify; intros 3; apply trans1]] -qed. - -definition cr'': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 BTop FT1 FT2 ≝ - λFT1,FT2,c.cr ?? c. - -coercion cr''. - -definition cr''': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 REL FT1 FT2 ≝ - λFT1,FT2:formal_topology.λc:formal_map_setoid FT1 FT2.cont_rel FT1 FT2 (cr' ?? c). - -coercion cr'''. - -axiom C1': - ∀S,T: formal_topology.∀f:formal_map_setoid S T.∀U,V: Ω \sup T. - extS ?? f (U ↓ V) = extS ?? f U ↓ extS ?? f V. - -definition formal_map_composition: - ∀o1,o2,o3: formal_topology. - binary_morphism1 - (formal_map_setoid o1 o2) - (formal_map_setoid o2 o3) - (formal_map_setoid o1 o3). - intros; constructor 1; - [ intros; whd in c c1; constructor 1; - [ apply (comp1 BTop ??? c c1); - | intros; - apply (.= (extS_com ??? c c1 ?)); - apply (.= †(C1 ?????)); - apply (.= (C1' ?????)); - apply (.= ((†((extS_singleton ????) \sup -1))‡(†((extS_singleton ????) \sup -1)))); - apply (.= (extS_com ??????)\sup -1 ‡ (extS_com ??????) \sup -1); - apply (.= (extS_singleton ????)‡(extS_singleton ????)); - apply refl1; - | apply (.= (extS_com ??? c c1 ?)); - apply (.= (†(C2 ???))); - apply (.= (C2 ???)); - apply refl1;] - | intros; simplify; - change with (comp1 BTop ??? a b = comp1 BTop ??? a' b'); - apply prop1; assumption] -qed. - diff --git a/helm/software/matita/contribs/formal_topology/overlap/notation.ma b/helm/software/matita/library/formal_topology/notation.ma similarity index 100% rename from helm/software/matita/contribs/formal_topology/overlap/notation.ma rename to helm/software/matita/library/formal_topology/notation.ma diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma b/helm/software/matita/library/formal_topology/o-algebra.ma similarity index 99% rename from helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma rename to helm/software/matita/library/formal_topology/o-algebra.ma index a86d286bc..ed363cd2d 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma +++ b/helm/software/matita/library/formal_topology/o-algebra.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "categories.ma". +include "formal_topology/categories.ma". inductive bool : Type0 := true : bool | false : bool. diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma b/helm/software/matita/library/formal_topology/o-basic_pairs.ma similarity index 99% rename from helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma rename to helm/software/matita/library/formal_topology/o-basic_pairs.ma index f0e0b712c..3cd9699ac 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma +++ b/helm/software/matita/library/formal_topology/o-basic_pairs.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "o-algebra.ma". -include "notation.ma". +include "formal_topology/o-algebra.ma". +include "formal_topology/notation.ma". record Obasic_pair: Type2 ≝ { Oconcr: OA; Oform: OA; Orel: arrows2 ? Oconcr Oform diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma b/helm/software/matita/library/formal_topology/o-basic_pairs_to_o-basic_topologies.ma similarity index 97% rename from helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma rename to helm/software/matita/library/formal_topology/o-basic_pairs_to_o-basic_topologies.ma index 80fec0348..1806408e0 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma +++ b/helm/software/matita/library/formal_topology/o-basic_pairs_to_o-basic_topologies.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "notation.ma". -include "o-basic_pairs.ma". -include "o-basic_topologies.ma". +include "formal_topology/notation.ma". +include "formal_topology/o-basic_pairs.ma". +include "formal_topology/o-basic_topologies.ma". alias symbol "eq" = "setoid1 eq". diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma b/helm/software/matita/library/formal_topology/o-basic_topologies.ma similarity index 99% rename from helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma rename to helm/software/matita/library/formal_topology/o-basic_topologies.ma index 2fb7a6b1d..03da27c41 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma +++ b/helm/software/matita/library/formal_topology/o-basic_topologies.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "o-algebra.ma". -include "o-saturations.ma". +include "formal_topology/o-algebra.ma". +include "formal_topology/o-saturations.ma". record Obasic_topology: Type2 ≝ { Ocarrbt:> OA; diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma b/helm/software/matita/library/formal_topology/o-concrete_spaces.ma similarity index 98% rename from helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma rename to helm/software/matita/library/formal_topology/o-concrete_spaces.ma index e333d2412..2ff03c8f7 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma +++ b/helm/software/matita/library/formal_topology/o-concrete_spaces.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "o-basic_pairs.ma". -include "o-saturations.ma". +include "formal_topology/o-basic_pairs.ma". +include "formal_topology/o-saturations.ma". definition A : ∀b:OBP. unary_morphism1 (Oform b) (Oform b). intros; constructor 1; diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma b/helm/software/matita/library/formal_topology/o-formal_topologies.ma similarity index 98% rename from helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma rename to helm/software/matita/library/formal_topology/o-formal_topologies.ma index 0e0b02e94..af9da702a 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma +++ b/helm/software/matita/library/formal_topology/o-formal_topologies.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "o-basic_topologies.ma". +include "formal_topology/o-basic_topologies.ma". (* (* diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-saturations.ma b/helm/software/matita/library/formal_topology/o-saturations.ma similarity index 97% rename from helm/software/matita/contribs/formal_topology/overlap/o-saturations.ma rename to helm/software/matita/library/formal_topology/o-saturations.ma index bb193508e..b8d5e9ca1 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-saturations.ma +++ b/helm/software/matita/library/formal_topology/o-saturations.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "o-algebra.ma". +include "formal_topology/o-algebra.ma". definition is_o_saturation: ∀C:OA. C ⇒_1 C → CProp1 ≝ λC:OA.λA:C ⇒_1 C.∀U,V. (U ≤ A V) =_1 (A U ≤ A V). diff --git a/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma b/helm/software/matita/library/formal_topology/r-o-basic_pairs.ma similarity index 98% rename from helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma rename to helm/software/matita/library/formal_topology/r-o-basic_pairs.ma index b3e69b09c..45593605e 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma +++ b/helm/software/matita/library/formal_topology/r-o-basic_pairs.ma @@ -12,12 +12,12 @@ (* *) (**************************************************************************) -include "basic_pairs_to_o-basic_pairs.ma". -include "apply_functor.ma". +include "formal_topology/basic_pairs_to_o-basic_pairs.ma". +include "formal_topology/apply_functor.ma". definition rOBP ≝ Apply (category2_of_category1 BP) OBP BP_to_OBP. -include "o-basic_pairs_to_o-basic_topologies.ma". +include "formal_topology/o-basic_pairs_to_o-basic_topologies.ma". lemma category2_of_category1_respects_comp_r: ∀C:category1.∀o1,o2,o3:C. @@ -128,6 +128,7 @@ variant eq_cones_to_eq_rel': f = g ≝ eq_cones_to_eq_rel. +(* lemma rOR_full : ∀s,t:rOBP.∀f:arrows2 OBTop (OR (ℱ_2 s)) (OR (ℱ_2 t)). exT22 ? (λg:arrows2 rOBP s t. @@ -251,3 +252,4 @@ STOP; *) +*) \ No newline at end of file diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations.ma b/helm/software/matita/library/formal_topology/relations.ma similarity index 99% rename from helm/software/matita/contribs/formal_topology/overlap/relations.ma rename to helm/software/matita/library/formal_topology/relations.ma index b1589a827..301e9487a 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/relations.ma +++ b/helm/software/matita/library/formal_topology/relations.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "subsets.ma". +include "formal_topology/subsets.ma". record binary_relation (A,B: SET) : Type1 ≝ { satisfy:> binary_morphism1 A B CPROP }. diff --git a/helm/software/matita/library/formal_topology/relations.ma.dontcompile b/helm/software/matita/library/formal_topology/relations.ma.dontcompile deleted file mode 100644 index f81e19eec..000000000 --- a/helm/software/matita/library/formal_topology/relations.ma.dontcompile +++ /dev/null @@ -1,247 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 "datatypes/subsets.ma". - -record binary_relation (A,B: setoid) : Type ≝ - { satisfy:> binary_morphism1 A B CPROP }. - -notation < "hvbox (x \nbsp \natur term 90 r \nbsp y)" with precedence 45 for @{'satisfy $r $x $y}. -notation > "hvbox (x \natur term 90 r y)" with precedence 45 for @{'satisfy $r $x $y}. -interpretation "relation applied" 'satisfy r x y = (fun1 ___ (satisfy __ r) x y). - -definition binary_relation_setoid: setoid → setoid → setoid1. - intros (A B); - constructor 1; - [ apply (binary_relation A B) - | constructor 1; - [ apply (λA,B.λr,r': binary_relation A B. ∀x,y. r x y ↔ r' x y) - | simplify; intros 3; split; intro; assumption - | simplify; intros 5; split; intro; - [ apply (fi ?? (H ??)) | apply (if ?? (H ??))] assumption - | simplify; intros 7; split; intro; - [ apply (if ?? (H1 ??)) | apply (fi ?? (H ??)) ] - [ apply (if ?? (H ??)) | apply (fi ?? (H1 ??)) ] - assumption]] -qed. - -definition composition: - ∀A,B,C. - binary_morphism1 (binary_relation_setoid A B) (binary_relation_setoid B C) (binary_relation_setoid A C). - intros; - constructor 1; - [ intros (R12 R23); - constructor 1; - constructor 1; - [ apply (λs1:A.λs3:C.∃s2:B. s1 ♮R12 s2 ∧ s2 ♮R23 s3); - | intros; - split; intro; cases H2 (w H3); clear H2; exists; [1,3: apply w ] - [ apply (. (H‡#)‡(#‡H1)); assumption - | apply (. ((H \sup -1)‡#)‡(#‡(H1 \sup -1))); assumption]] - | intros 8; split; intro H2; simplify in H2 ⊢ %; - cases H2 (w H3); clear H2; exists [1,3: apply w] cases H3 (H2 H4); clear H3; - [ lapply (if ?? (H x w) H2) | lapply (fi ?? (H x w) H2) ] - [ lapply (if ?? (H1 w y) H4)| lapply (fi ?? (H1 w y) H4) ] - exists; try assumption; - split; assumption] -qed. - -definition REL: category1. - constructor 1; - [ apply setoid - | intros (T T1); apply (binary_relation_setoid T T1) - | intros; constructor 1; - constructor 1; unfold setoid1_of_setoid; simplify; - [ intros; apply (c = c1) - | intros; split; intro; - [ apply (trans ????? (H \sup -1)); - apply (trans ????? H2); - apply H1 - | apply (trans ????? H); - apply (trans ????? H2); - apply (H1 \sup -1)]] - | apply composition - | intros 9; - split; intro; - cases f (w H); clear f; cases H; clear H; - [cases f (w1 H); clear f | cases f1 (w1 H); clear f1] - cases H; clear H; - exists; try assumption; - split; try assumption; - exists; try assumption; - split; assumption - |6,7: intros 5; unfold composition; simplify; split; intro; - unfold setoid1_of_setoid in x y; simplify in x y; - [1,3: cases H (w H1); clear H; cases H1; clear H1; unfold; - [ apply (. (H \sup -1 : eq1 ? w x)‡#); assumption - | apply (. #‡(H : eq1 ? w y)); assumption] - |2,4: exists; try assumption; split; first [apply refl | assumption]]] -qed. - -definition full_subset: ∀s:REL. Ω \sup s. - apply (λs.{x | True}); - intros; simplify; split; intro; assumption. -qed. - -coercion full_subset. - -definition setoid1_of_REL: REL → setoid ≝ λS. S. - -coercion setoid1_of_REL. - -definition comprehension: ∀b:REL. (b ⇒ CPROP) → Ω \sup b. - apply (λb:REL. λP: b ⇒ CPROP. {x | x ∈ b ∧ P x}); - intros; simplify; apply (.= (H‡#)‡(†H)); apply refl1. -qed. - -interpretation "subset comprehension" 'comprehension s p = - (comprehension s (mk_unary_morphism __ p _)). - -definition ext: ∀X,S:REL. binary_morphism1 (arrows1 ? X S) S (Ω \sup X). - apply (λX,S.mk_binary_morphism1 ??? (λr:arrows1 ? X S.λf:S.{x ∈ X | x ♮r f}) ?); - [ intros; simplify; apply (.= (H‡#)); apply refl1 - | intros; simplify; split; intros; simplify; intros; cases f; split; try assumption; - [ apply (. (#‡H1)); whd in H; apply (if ?? (H ??)); assumption - | apply (. (#‡H1\sup -1)); whd in H; apply (fi ?? (H ??));assumption]] -qed. - -definition extS: ∀X,S:REL. ∀r: arrows1 ? X S. Ω \sup S ⇒ Ω \sup X. - (* ∃ is not yet a morphism apply (λX,S,r,F.{x ∈ X | ∃a. a ∈ F ∧ x ♮r a});*) - intros (X S r); constructor 1; - [ intro F; constructor 1; constructor 1; - [ apply (λx. x ∈ X ∧ ∃a:S. a ∈ F ∧ x ♮r a); - | intros; split; intro; cases f (H1 H2); clear f; split; - [ apply (. (H‡#)); assumption - |3: apply (. (H\sup -1‡#)); assumption - |2,4: cases H2 (w H3); exists; [1,3: apply w] - [ apply (. (#‡(H‡#))); assumption - | apply (. (#‡(H \sup -1‡#))); assumption]]] - | intros; split; simplify; intros; cases f; cases H1; split; - [1,3: assumption - |2,4: exists; [1,3: apply w] - [ apply (. (#‡H)‡#); assumption - | apply (. (#‡H\sup -1)‡#); assumption]]] -qed. - -lemma equalset_extS_id_X_X: ∀o:REL.∀X.extS ?? (id1 ? o) X = X. - intros; - unfold extS; simplify; - split; simplify; - [ intros 2; change with (a ∈ X); - cases f; clear f; - cases H; clear H; - cases x; clear x; - change in f2 with (eq1 ? a w); - apply (. (f2\sup -1‡#)); - assumption - | intros 2; change in f with (a ∈ X); - split; - [ whd; exact I - | exists; [ apply a ] - split; - [ assumption - | change with (a = a); apply refl]]] -qed. - -lemma extS_com: ∀o1,o2,o3,c1,c2,S. extS o1 o3 (c2 ∘ c1) S = extS o1 o2 c1 (extS o2 o3 c2 S). - intros; unfold extS; simplify; split; intros; simplify; intros; - [ cases f (H1 H2); cases H2 (w H3); clear f H2; split; [assumption] - cases H3 (H4 H5); cases H5 (w1 H6); clear H3 H5; cases H6 (H7 H8); clear H6; - exists; [apply w1] split [2: assumption] constructor 1; [assumption] - exists; [apply w] split; assumption - | cases f (H1 H2); cases H2 (w H3); clear f H2; split; [assumption] - cases H3 (H4 H5); cases H4 (w1 H6); clear H3 H4; cases H6 (w2 H7); clear H6; - cases H7; clear H7; exists; [apply w2] split; [assumption] exists [apply w] split; - assumption] -qed. - -(* the same as ⋄ for a basic pair *) -definition image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V). - intros; constructor 1; - [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∃x:U. x ♮r y ∧ x ∈ S}); - intros; simplify; split; intro; cases H1; exists [1,3: apply w] - [ apply (. (#‡H)‡#); assumption - | apply (. (#‡H \sup -1)‡#); assumption] - | intros; split; simplify; intros; cases H2; exists [1,3: apply w] - [ apply (. #‡(#‡H1)); cases x; split; try assumption; - apply (if ?? (H ??)); assumption - | apply (. #‡(#‡H1 \sup -1)); cases x; split; try assumption; - apply (if ?? (H \sup -1 ??)); assumption]] -qed. - -(* the same as □ for a basic pair *) -definition minus_star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V). - intros; constructor 1; - [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∀x:U. x ♮r y → x ∈ S}); - intros; simplify; split; intros; apply H1; - [ apply (. #‡H \sup -1); assumption - | apply (. #‡H); assumption] - | intros; split; simplify; intros; [ apply (. #‡H1); | apply (. #‡H1 \sup -1)] - apply H2; [ apply (if ?? (H \sup -1 ??)); | apply (if ?? (H ??)) ] assumption] -qed. - -(* minus_image is the same as ext *) - -theorem image_id: ∀o,U. image o o (id1 REL o) U = U. - intros; unfold image; simplify; split; simplify; intros; - [ change with (a ∈ U); - cases H; cases x; change in f with (eq1 ? w a); apply (. f‡#); assumption - | change in f with (a ∈ U); - exists; [apply a] split; [ change with (a = a); apply refl | assumption]] -qed. - -theorem minus_star_image_id: ∀o,U. minus_star_image o o (id1 REL o) U = U. - intros; unfold minus_star_image; simplify; split; simplify; intros; - [ change with (a ∈ U); apply H; change with (a=a); apply refl - | change in f1 with (eq1 ? x a); apply (. f1 \sup -1‡#); apply f] -qed. - -theorem image_comp: ∀A,B,C,r,s,X. image A C (r ∘ s) X = image B C r (image A B s X). - intros; unfold image; simplify; split; simplify; intros; cases H; clear H; cases x; - clear x; [ cases f; clear f; | cases f1; clear f1 ] - exists; try assumption; cases x; clear x; split; try assumption; - exists; try assumption; split; assumption. -qed. - -theorem minus_star_image_comp: - ∀A,B,C,r,s,X. - minus_star_image A C (r ∘ s) X = minus_star_image B C r (minus_star_image A B s X). - intros; unfold minus_star_image; simplify; split; simplify; intros; whd; intros; - [ apply H; exists; try assumption; split; assumption - | change with (x ∈ X); cases f; cases x1; apply H; assumption] -qed. - -(*CSC: unused! *) -theorem ext_comp: - ∀o1,o2,o3: REL. - ∀a: arrows1 ? o1 o2. - ∀b: arrows1 ? o2 o3. - ∀x. ext ?? (b∘a) x = extS ?? a (ext ?? b x). - intros; - unfold ext; unfold extS; simplify; split; intro; simplify; intros; - cases f; clear f; split; try assumption; - [ cases f2; clear f2; cases x1; clear x1; exists; [apply w] split; - [1: split] assumption; - | cases H; clear H; cases x1; clear x1; exists [apply w]; split; - [2: cases f] assumption] -qed. - -theorem extS_singleton: - ∀o1,o2.∀a:arrows1 ? o1 o2.∀x.extS o1 o2 a (singleton o2 x) = ext o1 o2 a x. - intros; unfold extS; unfold ext; unfold singleton; simplify; - split; intros 2; simplify; cases f; split; try assumption; - [ cases H; cases x1; change in f2 with (eq1 ? x w); apply (. #‡f2 \sup -1); - assumption - | exists; try assumption; split; try assumption; change with (x = x); apply refl] -qed. \ No newline at end of file diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma b/helm/software/matita/library/formal_topology/relations_to_o-algebra.ma similarity index 99% rename from helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma rename to helm/software/matita/library/formal_topology/relations_to_o-algebra.ma index 8bf57da98..3a908657b 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma +++ b/helm/software/matita/library/formal_topology/relations_to_o-algebra.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "relations.ma". -include "o-algebra.ma". +include "formal_topology/relations.ma". +include "formal_topology/o-algebra.ma". definition POW': objs1 SET → OAlgebra. intro A; constructor 1; diff --git a/helm/software/matita/contribs/formal_topology/overlap/saturations.ma b/helm/software/matita/library/formal_topology/saturations.ma similarity index 97% rename from helm/software/matita/contribs/formal_topology/overlap/saturations.ma rename to helm/software/matita/library/formal_topology/saturations.ma index cc0db526c..b02a9c053 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/saturations.ma +++ b/helm/software/matita/library/formal_topology/saturations.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "relations.ma". +include "formal_topology/relations.ma". definition is_saturation: ∀C:REL. Ω^C ⇒_1 Ω^C → CProp1 ≝ λC:REL.λA:Ω^C ⇒_1 Ω^C. ∀U,V. (U ⊆ A V) =_1 (A U ⊆ A V). diff --git a/helm/software/matita/library/formal_topology/saturations_reductions.ma.dontcompile b/helm/software/matita/library/formal_topology/saturations_reductions.ma.dontcompile deleted file mode 100644 index 0582bf0b1..000000000 --- a/helm/software/matita/library/formal_topology/saturations_reductions.ma.dontcompile +++ /dev/null @@ -1,41 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 "datatypes/subsets.ma". -include "formal_topology/relations.ma". - -definition is_saturation ≝ - λC:REL.λA:unary_morphism (Ω \sup C) (Ω \sup C). - ∀U,V. (U ⊆ A V) = (A U ⊆ A V). - -definition is_reduction ≝ - λC:REL.λJ:unary_morphism (Ω \sup C) (Ω \sup C). - ∀U,V. (J U ⊆ V) = (J U ⊆ J V). - -theorem saturation_expansive: ∀C,A. is_saturation C A → ∀U. U ⊆ A U. - intros; apply (fi ?? (H ??)); apply subseteq_refl. -qed. - -theorem saturation_monotone: - ∀C,A. is_saturation C A → - ∀U,V. U ⊆ V → A U ⊆ A V. - intros; apply (if ?? (H ??)); apply subseteq_trans; [apply V|3: apply saturation_expansive ] - assumption. -qed. - -theorem saturation_idempotent: ∀C,A. is_saturation C A → ∀U. A (A U) = A U. - intros; split; - [ apply (if ?? (H ??)); apply subseteq_refl - | apply saturation_expansive; assumption] -qed. diff --git a/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma b/helm/software/matita/library/formal_topology/saturations_to_o-saturations.ma similarity index 91% rename from helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma rename to helm/software/matita/library/formal_topology/saturations_to_o-saturations.ma index 4cbca0530..39b4176cb 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma +++ b/helm/software/matita/library/formal_topology/saturations_to_o-saturations.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "saturations.ma". -include "o-saturations.ma". -include "relations_to_o-algebra.ma". +include "formal_topology/saturations.ma". +include "formal_topology/o-saturations.ma". +include "formal_topology/relations_to_o-algebra.ma". (* These are only conversions :-) *) diff --git a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma b/helm/software/matita/library/formal_topology/subsets.ma similarity index 99% rename from helm/software/matita/contribs/formal_topology/overlap/subsets.ma rename to helm/software/matita/library/formal_topology/subsets.ma index 95d0284dc..108e3c767 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma +++ b/helm/software/matita/library/formal_topology/subsets.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "categories.ma". +include "formal_topology/categories.ma". record powerset_carrier (A: objs1 SET) : Type1 ≝ { mem_operator: A ⇒_1 CPROP }. interpretation "powerset low" 'powerset A = (powerset_carrier A). diff --git a/helm/software/matita/nlibrary/re/re.ma b/helm/software/matita/nlibrary/re/re.ma index e939cc04f..6b6a98524 100644 --- a/helm/software/matita/nlibrary/re/re.ma +++ b/helm/software/matita/nlibrary/re/re.ma @@ -20,11 +20,12 @@ include "arithmetics/nat.ma". (*include "Plogic/equality.ma".*) +interpretation "iff" 'iff a b = (iff a b). + nrecord Alpha : Type[1] ≝ { carr :> Type[0]; eqb: carr → carr → bool; - eqb_true: ∀x,y. (eqb x y = true) = (x=y); - eqb_false: ∀x,y. (eqb x y = false) = (x≠y) + eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y) }. notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }. @@ -72,13 +73,15 @@ ninductive in_l (S : Alpha) : word S → re S → Prop ≝ | in_ki: ∀w1,w2,e. w1 ∈ e → w2 ∈ e^* → w1@w2 ∈ e^*. interpretation "in_l" 'mem w l = (in_l ? w l). -(* notation "a || b" left associative with precedence 30 for @{'orb $a $b}. interpretation "orb" 'orb a b = (orb a b). notation "a && b" left associative with precedence 40 for @{'andb $a $b}. interpretation "andb" 'andb a b = (andb a b). +notation "~~ a" non associative with precedence 40 for @{'notb $a}. +interpretation "notb" 'notb a = (notb a). + nlet rec weq (S : Alpha) (l1, l2 : word S) on l1 : bool ≝ match l1 with [ nil ⇒ match l2 with [ nil ⇒ true | cons _ _ ⇒ false ] @@ -87,9 +90,143 @@ match l1 with ndefinition if_then_else ≝ λT:Type[0].λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f]. notation > "'if' term 19 e 'then' term 19 t 'else' term 19 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }. notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }. -interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f). +interpretation "if_then_else" 'if_then_else e t f = (if_then_else ? e t f). + +interpretation "qew" 'eqb a b = (weq ? a b). + +ndefinition is_epsilon ≝ λA.λw:word A. w == [ ]. +ndefinition is_empty ≝ λA.λw:word A.false. +ndefinition is_char ≝ λA,x.λw:word A. w == [ x ]. + +nlemma andP : ∀a,b.(a && b) = true ↔ (a = true ∧ b = true). +#a b; ncases a; ncases b; nnormalize; @; ##[##2,4,6,8: *] /2/; +nqed. + +nlemma orP : ∀a,b.(a || b) = true ↔ (a = true ∨ b = true). +#a b; ncases a; ncases b; nnormalize; @; ##[##2,4,6,8: *] /2/; +nqed. + +nlemma iff_l2r : ∀a,p.a = true ↔ p → a = true → p. +#a p; *; /2/; +nqed. + +nlemma iff_r2l : ∀a,p.a = true ↔ p → p → a = true. +#a p; *; /2/; +nqed. + +ncoercion xx : ∀a,p.∀H:a = true ↔ p. a = true → p ≝ iff_l2r +on _H : (? = true) ↔ ? to ∀_:?. ?. + +ncoercion yy : ∀a,p.∀H:a = true ↔ p. p → a = true ≝ iff_r2l +on _H : (? = true) ↔ ? to ∀_:?. ?. + +ndefinition wAlpha : Alpha → Alpha. #A; @ (word A) (weq A). +#x; nelim x; ##[ #y; ncases y; /2/; #x xs; @; nnormalize; #; ndestruct; ##] +#x xs; #IH y; nelim y; ##[ @; nnormalize; #; ndestruct; ##] +#y ys; *; #H1 H2; @; #H3; +##[ ##2: ncases (IH ys); #_; #H; ndestruct; nrewrite > (iff_r2l ?? (eqb_true ???) ?); //; napply H; //] +nrewrite > (iff_l2r ?? (eqb_true ? x y) ?); nnormalize in H3; ncases (x == y) in H3; nnormalize; /2/; +##[ #H; ncases (IH ys); #E; #_; nrewrite > (E H); //] #; ndestruct; +nqed. + +alias symbol "hint_decl" (instance 1) = "hint_decl_Type1". +unification hint 0 ≔ T; Y ≟ T, X ≟ (wAlpha T) ⊢ carr X ≡ word Y. +unification hint 0 ≔ T; Y ≟ T, X ≟ (wAlpha T) ⊢ carr X ≡ list Y. +unification hint 0 ≔ T,x,y; Y ≟ T, X ≟ (wAlpha T) ⊢ eqb X x y ≡ weq Y x y. + +nlet rec ex_split (A : Alpha) (p1,p2 : word A → bool) (w : word A) on w : bool ≝ + match w with + [ nil ⇒ p1 [ ] && p2 [ ] + | cons x xs ⇒ p1 [ ] && p2 (x::xs) || ex_split … (λw.p1 (x :: w)) p2 xs]. + +nlemma ex_splitP : + ∀A,w,p1,p2. ex_split A p1 p2 w = true ↔ + ∃w1,w2. w = w1 @ w2 ∧ p1 w1 = true ∧ p2 w2 = true. +#A w; nelim w; +##[ #p1 p2; @; + ##[ #H; @[ ]; @[ ]; ncases (iff_l2r ?? (andP ??) H); (* bug coercions *) + #E1 E2; nrewrite > E1; nrewrite > E2; /3/; + ##| *; #w1; *;#w2; *; *; ncases w1; ncases w2; nnormalize; #abs H1 H2; #; + ndestruct; nrewrite > H1 ; nrewrite > H2; //] +##| #x xs IH p1 p2; @; + ##[ #H; ncases (iff_l2r ?? (orP ??) H); + ##[ #H1; ncases (iff_l2r ?? (andP ??) H1); #p1T p2T; + @[ ]; @(x::xs); nnormalize; /3/; + ##| #E; ncases (iff_l2r ?? (IH ??) E); #l1; *; #l2; *; *; #defxs p1T p2T; + @(x :: l1); @l2; ndestruct; /3/; ##] + ##| *; #w1; *; #w2; *; *; ncases w1; + ##[ nnormalize in ⊢ (% → ?); ncases w2; ##[ #; ndestruct] #y ys defw2 p1T p2T; + nchange with ((p1 [ ] && p2 (x::xs) || ex_split ? (λw0.p1 (x::w0)) p2 xs) = true); + napply (iff_r2l ?? (orP ??)); @1; napply (iff_r2l ?? (andP ??)); + ndestruct; /2/; + ##| #y ys; nnormalize in ⊢ (% → ?); #E p1T p2T; + nchange with ((p1 [ ] && p2 (x::xs) || ex_split ? (λw0.p1 (x::w0)) p2 xs) = true); + napply (iff_r2l ?? (orP ??)); @2; napply (iff_r2l ?? (IH ??)); + @ys; @w2; ndestruct; /3/; ##]##]##] +nqed. + +nlet rec allb (A : Alpha) (p,fresh_p : word A → bool) (w : word A) on w : bool ≝ + match w with + [ nil ⇒ p [ ] + | cons x xs ⇒ p [x] && (xs == [ ] || allb … fresh_p fresh_p xs) + || allb … (λw.p (x :: w)) fresh_p xs]. + +nlemma allbP : + ∀A,w,p.allb A p p w = true ↔ + ∃w1,w2.w = w1 @ w2 ∧ p w1 = true ∧ (w2 = [ ] ∨ allb ? p p w2 = true). +#A w; nelim w; +##[ #p; @; + ##[ #H; @[ ]; @[ ]; nnormalize in H; /4/ by conj, or_introl; + ##| *; #w1; *; #w2; ncases w1; + ##[ *; *; nnormalize in ⊢ (% → ?); #defw2 pnil; *; ##[ #; ndestruct] //; + ##| #y ys; *; *; nnormalize in ⊢ (% → ?); #; ndestruct; ##]##] +##| #y ys IH p; @; + ##[ #E; ncases (iff_l2r ?? (orP ??) E); + ##[ #H; ncases (iff_l2r ?? (andP ??) H); #px allys; + nlapply (iff_l2r ?? (orP ??) allys); *; + ##[ #defys; @[y]; @[ ]; nrewrite > (iff_l2r ?? (eqb_true ? ys ?) defys); + /4/ by conj, or_introl; + ##| #IHa; ncases (iff_l2r ?? (IH ?) IHa); #z; *; #zs; *; *; + #defys pz; *; + ##[ #; ndestruct; @[y]; @z; + nrewrite > (append_nil ? z) in IHa; /4/ by or_intror, conj; + ##| #allzs; @[y]; @(z@zs); nrewrite > defys; /3/ by or_intror, conj;##]##] + ##| #allbp; + ; + + + +nlet rec in_lb (A : Alpha) (e : re A) on e : word A → bool ≝ + match e with + [ e ⇒ is_epsilon … + | z ⇒ is_empty … + | s x ⇒ is_char … x + | o e1 e2 ⇒ λw.in_lb … e1 w || in_lb … e2 w + | c e1 e2 ⇒ ex_split … (in_lb A e1) (in_lb A e2) + | k e ⇒ allb … (in_lb A e) (in_lb A e)]. + + +nlemma equiv_l_lb : ∀A,e,w. w ∈ e ↔ in_lb A e w = true. +#A e; nelim e; nnormalize; +##[ #w; @; ##[##2: #; ndestruct] #H; ninversion H; #; ndestruct; +##| #w; @; ##[##2: #H; nrewrite > (l2r ??? H); //; ##] + #H; ninversion H; #; ndestruct; //; +##| #x w; @; ##[ #H; ninversion H; #; ndestruct; nrewrite > (r2l ????); //; ##] + #H; nrewrite > (l2r ??? H); @2; +##| #e1 e2 IH1 IH2 w; @; #E; + ##[ ninversion E; ##[##1,2,4,5,6,7: #; ndestruct] + #w1 w2 e1 e2 w1r1 w2r2 H1 H2 defw defr1r2; ndestruct; + nlapply (IH1 w1); *; #IH1; #_; nlapply (IH1 w1r1); + nlapply (IH2 w2); *; #IH2; #_; nlapply (IH2 w2r2); + nelim w1;nnormalize; ncases w2; //; nnormalize; + + ##[ nelim w; ##[ nnormalize; //] #x xs IH E; nnormalize; + nlapply (IH1 [x]); nlapply (IH2 xs); + ncases (in_lb A e1 [x]); ncases (in_lb A e2 xs); nnormalize; *; #E1 E2; *; #E3 E4; /2/; + ##[ ncases xs in IH E3 E4; nnormalize; //; #xx xs H; #_; + + *; nnormalize; -*) nlemma in_l_inv_e: ∀S.∀w:word S. w ∈ ∅ → w = []. @@ -166,7 +303,7 @@ notation > "w .∈ E" non associative with precedence 40 for @{'in_pl $w $E}. notation < "w\shy .∈\shy E" non associative with precedence 40 for @{'in_pl $w $E}. interpretation "in_prl" 'in_pl w l = (in_prl ? w l). -interpretation "iff" 'iff a b = (iff a b). + nlemma append_eq_nil : ∀S.∀w1,w2:word S. [ ] = w1 @ w2 → w1 = [ ]. @@ -278,9 +415,6 @@ nlemma XXze : ∀S:Alpha.∀w:word S. w .∈ (∅ · ϵ) → False. #S w abs; ninversion abs; #; ndestruct; /2/ by XXz,XXe; nqed. -nlemma eqb_t : ∀S:Alpha.∀a,b:S.∀p:a == b = true. a = b. -#S a b H; nrewrite < (eqb_true ? a b); //. -nqed. naxiom in_move_cat: ∀S.∀w:word S.∀x.∀E1,E2:pitem S. w .∈ \move x (E1 · E2) → -- 2.39.2