X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fo-basic_topologies.ma;h=245fc4fdbf866ee9c9a28d521bb790c5f5cf4489;hb=3cf6181bded05eb63140d1b2ba4f2f5791a73b48;hp=be985a43cefd551e01fd6ea942dcc220dea8b622;hpb=2f57490a8df5e3e5c09b238f99e34067015a7df3;p=helm.git diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma index be985a43c..245fc4fdb 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma @@ -1,4 +1,4 @@ -(**************************************************************************) + (**************************************************************************) (* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) @@ -15,49 +15,37 @@ include "o-algebra.ma". include "o-saturations.ma". -record basic_topology: Type ≝ - { carrbt:> OA; - A: carrbt ⇒ carrbt; - J: carrbt ⇒ carrbt; - A_is_saturation: is_saturation ? A; - J_is_reduction: is_reduction ? J; - compatibility: ∀U,V. (A U >< J V) = (U >< J V) +record Obasic_topology: Type2 ≝ + { Ocarrbt:> OA; + oA: Ocarrbt ⇒ Ocarrbt; + oJ: Ocarrbt ⇒ Ocarrbt; + oA_is_saturation: is_o_saturation ? oA; + oJ_is_reduction: is_o_reduction ? oJ; + Ocompatibility: ∀U,V. (oA U >< oJ V) = (U >< oJ V) }. -lemma hint: OA → objs2 OA. - intro; apply t; -qed. -coercion hint. - -record continuous_relation (S,T: basic_topology) : Type ≝ - { cont_rel:> arrows2 OA S T; +record Ocontinuous_relation (S,T: Obasic_topology) : Type2 ≝ + { Ocont_rel:> arrows2 OA S T; (* reduces uses eq1, saturated uses eq!!! *) - reduced: ∀U. U = J ? U → cont_rel U = J ? (cont_rel U); - saturated: ∀U. U = A ? U → cont_rel⎻* U = A ? (cont_rel⎻* U) + Oreduced: ∀U. U = oJ ? U → Ocont_rel U = oJ ? (Ocont_rel U); + Osaturated: ∀U. U = oA ? U → Ocont_rel⎻* U = oA ? (Ocont_rel⎻* U) }. -definition continuous_relation_setoid: basic_topology → basic_topology → setoid2. +definition Ocontinuous_relation_setoid: Obasic_topology → Obasic_topology → setoid2. intros (S T); constructor 1; - [ apply (continuous_relation S T) + [ apply (Ocontinuous_relation S T) | constructor 1; - [ (*apply (λr,s:continuous_relation S T.∀b. eq1 (oa_P (carrbt S)) (A ? (r⎻ b)) (A ? (s⎻ b)));*) - apply (λr,s:continuous_relation S T.r⎻* ∘ (A S) = s⎻* ∘ (A ?)); + [ alias symbol "eq" = "setoid2 eq". + alias symbol "compose" = "category2 composition". + apply (λr,s:Ocontinuous_relation S T. (r⎻* ) ∘ (oA S) = (s⎻* ∘ (oA ?))); | simplify; intros; apply refl2; | simplify; intros; apply sym2; apply e | simplify; intros; apply trans2; [2: apply e |3: apply e1; |1: skip]]] qed. -definition cont_rel': ∀S,T: basic_topology. continuous_relation_setoid S T → arrows2 ? S T ≝ cont_rel. - -coercion cont_rel'. - -definition cont_rel'': - ∀S,T: basic_topology. - carr2 (continuous_relation_setoid S T) → ORelation_setoid (carrbt S) (carrbt T). - intros; apply rule cont_rel; apply c; -qed. - -coercion cont_rel''. +definition Ocontinuous_relation_of_Ocontinuous_relation_setoid: + ∀P,Q. Ocontinuous_relation_setoid P Q → Ocontinuous_relation P Q ≝ λP,Q,c.c. +coercion Ocontinuous_relation_of_Ocontinuous_relation_setoid. (* theorem continuous_relation_eq': @@ -108,74 +96,70 @@ theorem continuous_relation_eq_inv': qed. *) -axiom daemon: False. -definition continuous_relation_comp: +definition Ocontinuous_relation_comp: ∀o1,o2,o3. - continuous_relation_setoid o1 o2 → - continuous_relation_setoid o2 o3 → - continuous_relation_setoid o1 o3. + Ocontinuous_relation_setoid o1 o2 → + Ocontinuous_relation_setoid o2 o3 → + Ocontinuous_relation_setoid o1 o3. intros (o1 o2 o3 r s); constructor 1; [ apply (s ∘ r); | intros; - apply sym1; + apply sym1; change in match ((s ∘ r) U) with (s (r U)); - (**) unfold FunClass_1_OF_Type_OF_setoid2; - unfold objs2_OF_basic_topology1; unfold hint; - letin reduced := reduced; clearbody reduced; - unfold uncurry_arrows in reduced ⊢ %; (**) - apply (.= (reduced : ?)\sup -1); - [ (*BAD*) change with (eq1 ? (r U) (J ? (r U))); - (* BAD U *) apply (.= (reduced ??? U ?)); [ assumption | apply refl1 ] + apply (.= (Oreduced : ?)^-1); + [ apply (.= (Oreduced :?)); [ assumption | apply refl1 ] | apply refl1] | intros; apply sym1; change in match ((s ∘ r)⎻* U) with (s⎻* (r⎻* U)); - apply (.= (saturated : ?)\sup -1); - [ apply (.= (saturated : ?)); [ assumption | apply refl1 ] + apply (.= (Osaturated : ?)^-1); + [ apply (.= (Osaturated : ?)); [ assumption | apply refl1 ] | apply refl1]] qed. -definition BTop: category2. +definition OBTop: category2. constructor 1; - [ apply basic_topology - | apply continuous_relation_setoid + [ apply Obasic_topology + | apply Ocontinuous_relation_setoid | intro; constructor 1; [ apply id2 | intros; apply e; | intros; apply e;] | intros; constructor 1; - [ apply continuous_relation_comp; + [ apply Ocontinuous_relation_comp; | intros; simplify; - change with ((b⎻* ∘ a⎻* ) ∘ A o1 = ((b'⎻* ∘ a'⎻* ) ∘ A o1)); - change with (b⎻* ∘ (a⎻* ∘ A o1) = b'⎻* ∘ (a'⎻* ∘ A o1)); - change in e with (a⎻* ∘ A o1 = a'⎻* ∘ A o1); - change in e1 with (b⎻* ∘ A o2 = b'⎻* ∘ A o2); + change with ((b⎻* ∘ a⎻* ) ∘ oA o1 = ((b'⎻* ∘ a'⎻* ) ∘ oA o1)); + change with (b⎻* ∘ (a⎻* ∘ oA o1) = b'⎻* ∘ (a'⎻* ∘ oA o1)); + change in e with (a⎻* ∘ oA o1 = a'⎻* ∘ oA o1); + change in e1 with (b⎻* ∘ oA o2 = b'⎻* ∘ oA o2); apply (.= e‡#); - intro x; - change with (b⎻* (a'⎻* (A o1 x)) = b'⎻*(a'⎻* (A o1 x))); - alias symbol "trans" = "trans1". - alias symbol "prop1" = "prop11". - alias symbol "invert" = "setoid1 symmetry". - lapply (.= †(saturated o1 o2 a' (A o1 x) : ?)); - [3: apply (b⎻* ); | 5: apply Hletin; |1,2: skip; - |apply ((saturation_idempotent ?? (A_is_saturation o1) x)^-1); ] - change in e1 with (∀x.b⎻* (A o2 x) = b'⎻* (A o2 x)); - apply (.= (e1 (a'⎻* (A o1 x)))); - alias symbol "invert" = "setoid1 symmetry". - lapply (†((saturated ?? a' (A o1 x) : ?) ^ -1)); - [2: apply (b'⎻* ); |4: apply Hletin; | skip; - |apply ((saturation_idempotent ?? (A_is_saturation o1) x)^-1);]] + intro x; + change with (eq1 ? (b⎻* (a'⎻* (oA o1 x))) (b'⎻*(a'⎻* (oA o1 x)))); + apply (.= †(Osaturated o1 o2 a' (oA o1 x) ?)); [ + apply ((o_saturation_idempotent ?? (oA_is_saturation o1) x)^-1);] + apply (.= (e1 (a'⎻* (oA o1 x)))); + change with (eq1 ? (b'⎻* (oA o2 (a'⎻* (oA o1 x)))) (b'⎻*(a'⎻* (oA o1 x)))); + apply (.= †(Osaturated o1 o2 a' (oA o1 x):?)^-1); [ + apply ((o_saturation_idempotent ?? (oA_is_saturation o1) x)^-1);] + apply rule #;] | intros; simplify; - change with (((a34⎻* ∘ a23⎻* ) ∘ a12⎻* ) ∘ A o1 = ((a34⎻* ∘ (a23⎻* ∘ a12⎻* )) ∘ A o1)); - apply rule (#‡ASSOC1\sup -1); + change with (((a34⎻* ∘ a23⎻* ) ∘ a12⎻* ) ∘ oA o1 = ((a34⎻* ∘ (a23⎻* ∘ a12⎻* )) ∘ oA o1)); + apply rule (#‡ASSOC ^ -1); | intros; simplify; - change with ((a⎻* ∘ (id2 ? o1)⎻* ) ∘ A o1 = a⎻* ∘ A o1); + change with ((a⎻* ∘ (id2 ? o1)⎻* ) ∘ oA o1 = a⎻* ∘ oA o1); apply (#‡(id_neutral_right2 : ?)); | intros; simplify; - change with (((id2 ? o2)⎻* ∘ a⎻* ) ∘ A o1 = a⎻* ∘ A o1); + change with (((id2 ? o2)⎻* ∘ a⎻* ) ∘ oA o1 = a⎻* ∘ oA o1); apply (#‡(id_neutral_left2 : ?));] qed. +definition Obasic_topology_of_OBTop: objs2 OBTop → Obasic_topology ≝ λx.x. +coercion Obasic_topology_of_OBTop. + +definition Ocontinuous_relation_setoid_of_arrows2_OBTop : + ∀P,Q. arrows2 OBTop P Q → Ocontinuous_relation_setoid P Q ≝ λP,Q,x.x. +coercion Ocontinuous_relation_setoid_of_arrows2_OBTop. + (* (*CSC: unused! *) (* this proof is more logic-oriented than set/lattice oriented *) @@ -201,4 +185,4 @@ theorem continuous_relation_eqS: [2,4: intros; apply saturation_monotone; try (apply A_is_saturation); apply Hcut;] apply Hcut2; assumption. qed. -*) \ No newline at end of file +*)