From: Enrico Tassi Date: Mon, 26 Jan 2009 17:12:38 +0000 (+0000) Subject: maction support added to notation, adopted for = AKA = \sub t X-Git-Tag: make_still_working~4231 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8d961585c4ff785d558d5b4c84adf656595ca487;p=helm.git maction support added to notation, adopted for = AKA = \sub t deactivated the library/formal_topology directory since it is completely broken and outdated --- diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo index 8709f0265..fc6a15b06 100644 --- a/helm/software/matita/core_notation.moo +++ b/helm/software/matita/core_notation.moo @@ -47,9 +47,12 @@ notation < "hvbox(a break \to b)" right associative with precedence 20 for @{ \Pi $_:$a.$b }. -notation "hvbox(a break = b)" +notation > "hvbox(a break = b)" non associative with precedence 45 -for @{ 'eq $a $b }. +for @{ 'eq ? $a $b }. +notation < "hvbox(a break maction (=) (=\sub t) b)" + non associative with precedence 45 +for @{ 'eq $t $a $b }. notation "hvbox(a break \leq b)" non associative with precedence 45 @@ -67,9 +70,13 @@ notation "hvbox(a break \gt b)" non associative with precedence 45 for @{ 'gt $a $b }. -notation "hvbox(a break \neq b)" +notation > "hvbox(a break \neq b)" + non associative with precedence 45 +for @{ 'neq ? $a $b }. + +notation < "hvbox(a break maction (\neq) (\neq\sub t) b)" non associative with precedence 45 -for @{ 'neq $a $b }. +for @{ 'neq $t $a $b }. notation "hvbox(a break \nleq b)" non associative with precedence 45 @@ -232,3 +239,6 @@ notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}. notation > "⊩ " with precedence 60 for @{'Vdash ?}. notation "(⊩ \sub term 90 c) " with precedence 60 for @{'Vdash $c}. +notation < "maction (mstyle color #ff0000 (­…­)) (t)" +non associative with precedence 90 for @{'hide $t}. + diff --git a/helm/software/matita/library/algebra/groups.ma b/helm/software/matita/library/algebra/groups.ma index f257951bc..d6e77ae8d 100644 --- a/helm/software/matita/library/algebra/groups.ma +++ b/helm/software/matita/library/algebra/groups.ma @@ -218,8 +218,8 @@ definition left_coset_eq ≝ λG.λC,C':left_coset G. ∀x.((element ? C)·x \sub (subgrp ? C)) ∈ C'. -interpretation "Left cosets equality" 'eq C C' = - (cic:/matita/algebra/groups/left_coset_eq.con _ C C'). +interpretation "Left cosets equality" 'eq t C C' = + (cic:/matita/algebra/groups/left_coset_eq.con t C C'). definition left_coset_disjoint ≝ λG.λC,C':left_coset G. diff --git a/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma b/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma index 6dc55e142..46aa96eb1 100644 --- a/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma +++ b/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma @@ -58,7 +58,7 @@ letin m ≝ (hide ? ( rewrite > (?:x = O); [2: cases Hx; lapply (os_le_to_nat_le ?? H1); apply (symmetric_eq nat O x ?).apply (le_n_O_to_eq x ?).apply (Hletin). - |1: intros; unfold Type_of_ordered_set in sg; + |1: intros; unfold Type_OF_ordered_set in sg a; whd in a:(? %); lapply (H2 O) as K; lapply (sl2l_ ?? (a O) ≪x,Hx≫ K) as P; simplify in P:(???%); lapply (le_transitive ??? P H1) as W; lapply (os_le_to_nat_le ?? W) as R; apply (le_n_O_to_eq (\fst (a O)) R);] diff --git a/helm/software/matita/library/dama/property_exhaustivity.ma b/helm/software/matita/library/dama/property_exhaustivity.ma index 4dec6442e..f76660190 100644 --- a/helm/software/matita/library/dama/property_exhaustivity.ma +++ b/helm/software/matita/library/dama/property_exhaustivity.ma @@ -115,7 +115,7 @@ intros; split; qed. lemma hint_mah1: - ∀C. Type_OF_ordered_uniform_space1 C → hos_carr (os_r C). + ∀C. Type_OF_ordered_uniform_space__1 C → hos_carr (os_r C). intros; assumption; qed. coercion hint_mah1 nocomposites. diff --git a/helm/software/matita/library/dama/supremum.ma b/helm/software/matita/library/dama/supremum.ma index be8495970..2ce417ecc 100644 --- a/helm/software/matita/library/dama/supremum.ma +++ b/helm/software/matita/library/dama/supremum.ma @@ -121,7 +121,7 @@ interpretation "trans_increasing" 'trans_increasing = (h_trans_increasing (os_l interpretation "trans_decreasing" 'trans_decreasing = (h_trans_increasing (os_r _)). lemma hint_nat : - Type_of_ordered_set nat_ordered_set → + Type_OF_ordered_set nat_ordered_set → hos_carr (os_l (nat_ordered_set)). intros; assumption; qed. diff --git a/helm/software/matita/library/datatypes/categories.ma b/helm/software/matita/library/datatypes/categories.ma index 65bc8ac6b..f5b23dfdd 100644 --- a/helm/software/matita/library/datatypes/categories.ma +++ b/helm/software/matita/library/datatypes/categories.ma @@ -80,8 +80,8 @@ qed. coercion Leibniz. *) -interpretation "setoid1 eq" 'eq x y = (eq_rel1 _ (eq1 _) x y). -interpretation "setoid eq" 'eq x y = (eq_rel _ (eq _) x y). +interpretation "setoid1 eq" 'eq t x y = (eq_rel1 _ (eq1 t) x y). +interpretation "setoid eq" 'eq t x y = (eq_rel _ (eq t) x y). interpretation "setoid1 symmetry" 'invert r = (sym1 ____ r). interpretation "setoid symmetry" 'invert r = (sym ____ r). notation ".= r" with precedence 50 for @{'trans $r}. diff --git a/helm/software/matita/library/datatypes/subsets.ma b/helm/software/matita/library/datatypes/subsets.ma index 7c9a13195..8c7963d67 100644 --- a/helm/software/matita/library/datatypes/subsets.ma +++ b/helm/software/matita/library/datatypes/subsets.ma @@ -26,6 +26,8 @@ theorem transitive_subseteq_operator: ∀A. transitive ? (subseteq_operator A). assumption. qed. +(* + definition powerset_setoid: setoid → setoid1. intros (T); constructor 1; @@ -136,3 +138,5 @@ definition singleton: ∀A:setoid. unary_morphism A (Ω \sup A). qed. interpretation "singleton" 'singl a = (fun_1 __ (singleton _) a). + +*) \ No newline at end of file diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends index c06799274..aaf7d6869 100644 --- a/helm/software/matita/library/depends +++ b/helm/software/matita/library/depends @@ -1,4 +1,3 @@ -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 @@ -16,7 +15,6 @@ technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic 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 logic/connectives.ma nat/compare.ma nat/le_arith.ma -formal_topology/saturations_reductions.ma datatypes/subsets.ma formal_topology/relations.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 @@ -26,7 +24,6 @@ dama/models/nat_uniform.ma dama/models/discrete_uniformity.ma dama/nat_ordered_s didactic/exercises/substitution.ma nat/minus.ma didactic/exercises/natural_deduction_fst_order.ma didactic/support/natural_deduction.ma nat/factorization2.ma list/list.ma nat/factorization.ma nat/sieve.ma -formal_topology/basic_topologies.ma datatypes/categories.ma formal_topology/relations.ma formal_topology/saturations_reductions.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 @@ -65,11 +62,9 @@ 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/basic_pairs.ma datatypes/categories.ma formal_topology/relations.ma Q/frac.ma Q/q/q.ma Q/q/qinv.ma nat/factorization.ma nat/nat.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 Q/ratio/ratio.ma Q/fraction/fraction.ma nat/chebyshev_teta.ma nat/binomial.ma nat/pi_p.ma @@ -79,7 +74,6 @@ nat/pi_p.ma nat/generic_iter_p.ma nat/iteration2.ma nat/primes.ma algebra/semigroups.ma higher_order_defs/functions.ma dama/models/discrete_uniformity.ma dama/bishop_set_rewrite.ma dama/uniform.ma dama/lebesgue.ma dama/ordered_set.ma dama/property_exhaustivity.ma dama/sandwich.ma -formal_topology/relations.ma datatypes/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 diff --git a/helm/software/matita/library/formal_topology/basic_pairs.ma b/helm/software/matita/library/formal_topology/basic_pairs.ma deleted file mode 100644 index 0d51724de..000000000 --- a/helm/software/matita/library/formal_topology/basic_pairs.ma +++ /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/library/formal_topology/basic_pairs.ma.dontcompile b/helm/software/matita/library/formal_topology/basic_pairs.ma.dontcompile new file mode 100644 index 000000000..0d51724de --- /dev/null +++ b/helm/software/matita/library/formal_topology/basic_pairs.ma.dontcompile @@ -0,0 +1,179 @@ +(**************************************************************************) +(* ___ *) +(* ||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/library/formal_topology/basic_topologies.ma b/helm/software/matita/library/formal_topology/basic_topologies.ma deleted file mode 100644 index 36a0d24c8..000000000 --- a/helm/software/matita/library/formal_topology/basic_topologies.ma +++ /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/library/formal_topology/basic_topologies.ma.dontcompile b/helm/software/matita/library/formal_topology/basic_topologies.ma.dontcompile new file mode 100644 index 000000000..36a0d24c8 --- /dev/null +++ b/helm/software/matita/library/formal_topology/basic_topologies.ma.dontcompile @@ -0,0 +1,199 @@ +(**************************************************************************) +(* ___ *) +(* ||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/library/formal_topology/concrete_spaces.ma b/helm/software/matita/library/formal_topology/concrete_spaces.ma deleted file mode 100644 index 3c03b4e66..000000000 --- a/helm/software/matita/library/formal_topology/concrete_spaces.ma +++ /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/library/formal_topology/concrete_spaces.ma.dontcompile b/helm/software/matita/library/formal_topology/concrete_spaces.ma.dontcompile new file mode 100644 index 000000000..3c03b4e66 --- /dev/null +++ b/helm/software/matita/library/formal_topology/concrete_spaces.ma.dontcompile @@ -0,0 +1,120 @@ +(**************************************************************************) +(* ___ *) +(* ||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/library/formal_topology/formal_topologies.ma b/helm/software/matita/library/formal_topology/formal_topologies.ma deleted file mode 100644 index f47323e00..000000000 --- a/helm/software/matita/library/formal_topology/formal_topologies.ma +++ /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/library/formal_topology/formal_topologies.ma.dontcompile b/helm/software/matita/library/formal_topology/formal_topologies.ma.dontcompile new file mode 100644 index 000000000..f47323e00 --- /dev/null +++ b/helm/software/matita/library/formal_topology/formal_topologies.ma.dontcompile @@ -0,0 +1,121 @@ +(**************************************************************************) +(* ___ *) +(* ||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/library/formal_topology/relations.ma b/helm/software/matita/library/formal_topology/relations.ma deleted file mode 100644 index f81e19eec..000000000 --- a/helm/software/matita/library/formal_topology/relations.ma +++ /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/library/formal_topology/relations.ma.dontcompile b/helm/software/matita/library/formal_topology/relations.ma.dontcompile new file mode 100644 index 000000000..f81e19eec --- /dev/null +++ b/helm/software/matita/library/formal_topology/relations.ma.dontcompile @@ -0,0 +1,247 @@ +(**************************************************************************) +(* ___ *) +(* ||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/library/formal_topology/saturations_reductions.ma b/helm/software/matita/library/formal_topology/saturations_reductions.ma deleted file mode 100644 index 0582bf0b1..000000000 --- a/helm/software/matita/library/formal_topology/saturations_reductions.ma +++ /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/library/formal_topology/saturations_reductions.ma.dontcompile b/helm/software/matita/library/formal_topology/saturations_reductions.ma.dontcompile new file mode 100644 index 000000000..0582bf0b1 --- /dev/null +++ b/helm/software/matita/library/formal_topology/saturations_reductions.ma.dontcompile @@ -0,0 +1,41 @@ +(**************************************************************************) +(* ___ *) +(* ||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/library/logic/equality.ma b/helm/software/matita/library/logic/equality.ma index cc181dfbf..73728dc92 100644 --- a/helm/software/matita/library/logic/equality.ma +++ b/helm/software/matita/library/logic/equality.ma @@ -19,11 +19,11 @@ inductive eq (A:Type) (x:A) : A \to Prop \def (*CSC: the URI must disappear: there is a bug now *) interpretation "leibnitz's equality" - 'eq x y = (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ x y). + 'eq t x y = (cic:/matita/logic/equality/eq.ind#xpointer(1/1) t x y). (*CSC: the URI must disappear: there is a bug now *) interpretation "leibnitz's non-equality" - 'neq x y = (cic:/matita/logic/connectives/Not.con - (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ x y)). + 'neq t x y = (cic:/matita/logic/connectives/Not.con + (cic:/matita/logic/equality/eq.ind#xpointer(1/1) t x y)). theorem eq_rect': \forall A. \forall x:A. \forall P: \forall y:A. x=y \to Type. diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index 7cb2aa7cb..19eeaf0d7 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -65,9 +65,11 @@ let near (x1, y1) (x2, y2) = let distance = sqrt (((x2 -. x1) ** 2.) +. ((y2 -. y1) ** 2.)) in (distance < 4.) +let mathml_ns = Gdome.domString "http://www.w3.org/1998/Math/MathML" let xlink_ns = Gdome.domString "http://www.w3.org/1999/xlink" let helm_ns = Gdome.domString "http://www.cs.unibo.it/helm" let href_ds = Gdome.domString "href" +let maction_ds = Gdome.domString "maction" let xref_ds = Gdome.domString "xref" let domImpl = Gdome.domImplementation () @@ -163,6 +165,17 @@ let hrefs_of_elt elt = else None +let rec has_maction (elt :Gdome.element) = + (* fix this comparison *) + if elt#get_tagName#to_string = "m:maction" then + true + else + match elt#get_parentNode with + | Some node when node#get_nodeType = GdomeNodeTypeT.ELEMENT_NODE -> + has_maction (new Gdome.element_of_node node) + | _ -> false +;; + class clickableMathView obj = let text_width = 80 in object (self) @@ -176,7 +189,8 @@ object (self) method private cic_info = _cic_info val normal_cursor = Gdk.Cursor.create `LEFT_PTR - val href_cursor = Gdk.Cursor.create `HAND1 + val href_cursor = Gdk.Cursor.create `HAND2 + val maction_cursor = Gdk.Cursor.create `QUESTION_ARROW initializer self#set_font_size !current_font_size; @@ -221,7 +235,11 @@ object (self) button_press_y <- GdkEvent.Button.y gdk_button; selection_changed <- false end else if button = right_button then - self#popup_contextual_menu (GdkEvent.Button.time gdk_button); + self#popup_contextual_menu + (self#get_element_at + (int_of_float (GdkEvent.Button.x gdk_button)) + (int_of_float (GdkEvent.Button.y gdk_button))) + (GdkEvent.Button.time gdk_button); false method private element_over_cb (elt_opt, _, _, _) = @@ -233,6 +251,9 @@ object (self) in match elt_opt with | Some elt -> + if has_maction elt then + Gdk.Window.set_cursor (win ()) maction_cursor + else (match hrefs_of_elt elt with | Some ((_ :: _) as hrefs) -> Gdk.Window.set_cursor (win ()) href_cursor; @@ -274,22 +295,36 @@ object (self) | [] -> assert false (* this method is invoked only if there's a sel. *) | node :: _ -> self#tactic_text_pattern_of_node node - method private popup_contextual_menu time = + method private popup_contextual_menu element time = let menu = GMenu.menu () in let add_menu_item ?(menu = menu) ?stock ?label () = GMenu.image_menu_item ?stock ?label ~packing:menu#append () in let check = add_menu_item ~label:"Check" () in let reductions_menu_item = GMenu.menu_item ~label:"βδιζ-reduce" () in let tactics_menu_item = GMenu.menu_item ~label:"Apply tactic" () in + let hyperlinks_menu_item = GMenu.menu_item ~label:"Hyperlinks" () in menu#append reductions_menu_item; menu#append tactics_menu_item; + menu#append hyperlinks_menu_item; let reductions = GMenu.menu () in let tactics = GMenu.menu () in + let hyperlinks = GMenu.menu () in reductions_menu_item#set_submenu reductions; tactics_menu_item#set_submenu tactics; + hyperlinks_menu_item#set_submenu hyperlinks; let normalize = add_menu_item ~menu:reductions ~label:"Normalize" () in let simplify = add_menu_item ~menu:reductions ~label:"Simplify" () in let whd = add_menu_item ~menu:reductions ~label:"Weak head" () in + (match element with + | None -> hyperlinks_menu_item#misc#set_sensitive false + | Some elt -> + match hrefs_of_elt elt, href_callback with + | Some l, Some f -> + List.iter + (fun h -> + let item = add_menu_item ~menu:hyperlinks ~label:h () in + connect_menu_item item (fun () -> f h)) l + | _ -> hyperlinks_menu_item#misc#set_sensitive false); menu#append (GMenu.separator_item ()); let copy = add_menu_item ~stock:`COPY () in let gui = get_gui () in @@ -329,9 +364,10 @@ object (self) (match self#get_element_at x y with | None -> () | Some elt -> + if has_maction elt then ignore(self#action_toggle elt) else (match hrefs_of_elt elt with | Some hrefs -> self#invoke_href_callback hrefs gdk_button - | None -> ignore (self#action_toggle elt))) + | None -> ())) end; false