From: Claudio Sacerdoti Coen Date: Sat, 3 Jan 2009 18:49:03 +0000 (+0000) Subject: Basic pairs went through with no problems. X-Git-Tag: make_still_working~4302 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bb0fff7ebc68535a75e260082b7db26c1d99f643;p=helm.git Basic pairs went through with no problems. --- diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma index c25e44f03..c5f125ac6 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma @@ -13,12 +13,11 @@ (**************************************************************************) include "o-algebra.ma". -include "datatypes/categories.ma". -record basic_pair: Type ≝ +record basic_pair: Type2 ≝ { concr: OA; form: OA; - rel: arrows1 ? concr form + rel: arrows2 ? concr form }. notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}. @@ -31,9 +30,9 @@ interpretation "basic pair relation (non applied)" 'Vdash c = (rel c). alias symbol "eq" = "setoid1 eq". alias symbol "compose" = "category1 composition". -record relation_pair (BP1,BP2: basic_pair): Type ≝ - { concr_rel: arrows1 ? (concr BP1) (concr BP2); - form_rel: arrows1 ? (form BP1) (form BP2); +record relation_pair (BP1,BP2: basic_pair): Type2 ≝ + { concr_rel: arrows2 ? (concr BP1) (concr BP2); + form_rel: arrows2 ? (form BP1) (form BP2); commute: ⊩ ∘ concr_rel = form_rel ∘ ⊩ }. @@ -44,24 +43,24 @@ 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). + ∀o1,o2. equivalence_relation2 (relation_pair o1 o2). intros; constructor 1; [ apply (λr,r'. ⊩ ∘ r \sub\c = ⊩ ∘ r' \sub\c); | simplify; intros; - apply refl1; + apply refl2; | simplify; intros 2; - apply sym1; + apply sym2; | simplify; intros 3; - apply trans1; + apply trans2; ] qed. -(* qui setoid1 e' giusto *) -definition relation_pair_setoid: basic_pair → basic_pair → setoid1. +(* qui setoid1 e' giusto: ma non lo e'!!! *) +definition relation_pair_setoid: basic_pair → basic_pair → setoid2. intros; constructor 1; [ apply (relation_pair b b1) @@ -74,22 +73,22 @@ lemma eq_to_eq': ∀o1,o2.∀r,r': relation_pair_setoid o1 o2. r=r' → r \sub\f apply (.= ((commute ?? r) \sup -1)); apply (.= H); apply (.= (commute ?? r')); - apply refl1; + apply refl2; 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; + [1,2: apply id2; + | lapply (id_neutral_right2 ? (concr o) ? (⊩)) as H; + lapply (id_neutral_left2 ?? (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). + ∀o1,o2,o3. binary_morphism2 (relation_pair_setoid o1 o2) (relation_pair_setoid o2 o3) (relation_pair_setoid o1 o3). intros; constructor 1; [ intros (r r1); @@ -98,26 +97,26 @@ definition relation_pair_composition: | apply (r1 \sub\f ∘ r \sub\f) | lapply (commute ?? r) as H; lapply (commute ?? r1) as H1; - apply (.= ASSOC1); + apply rule (.= ASSOC1); apply (.= #‡H1); - apply (.= ASSOC1\sup -1); + apply rule (.= ASSOC1\sup -1); apply (.= H‡#); - apply ASSOC1] + apply rule 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); + change in e with (⊩ ∘ a \sub\c = ⊩ ∘ a' \sub\c); + change in e1 with (⊩ ∘ b \sub\c = ⊩ ∘ b' \sub\c); + apply rule (.= ASSOC1); + apply (.= #‡e1); apply (.= #‡(commute ?? b')); - apply (.= ASSOC1 \sup -1); - apply (.= H‡#); - apply (.= ASSOC1); + apply rule (.= ASSOC1 \sup -1); + apply (.= e‡#); + apply rule (.= ASSOC1); apply (.= #‡(commute ?? b')\sup -1); - apply (ASSOC1 \sup -1)] + apply rule (ASSOC1 \sup -1)] qed. -definition BP: category1. +definition BP: category2. constructor 1; [ apply basic_pair | apply relation_pair_setoid @@ -126,13 +125,13 @@ definition BP: category1. | intros; change with (⊩ ∘ (a34\sub\c ∘ (a23\sub\c ∘ a12\sub\c)) = ⊩ ∘ ((a34\sub\c ∘ a23\sub\c) ∘ a12\sub\c)); - apply (ASSOC1‡#); + apply rule (ASSOC1‡#); | intros; change with (⊩ ∘ (a\sub\c ∘ (id_relation_pair o1)\sub\c) = ⊩ ∘ a\sub\c); - apply ((id_neutral_right1 ????)‡#); + apply ((id_neutral_right2 ????)‡#); | intros; change with (⊩ ∘ ((id_relation_pair o2)\sub\c ∘ a\sub\c) = ⊩ ∘ a\sub\c); - apply ((id_neutral_left1 ????)‡#);] + apply ((id_neutral_left2 ????)‡#);] qed. 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 61334e540..6accfaeaa 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 @@ -176,6 +176,9 @@ definition BTop: category2. apply (#‡(id_neutral_left2 : ?));] qed. +definition btop_carr: BTop → Type1 ≝ λo:BTop. carr1 (oa_P (carrbt o)). +coercion btop_carr. + (* (*CSC: unused! *) (* this proof is more logic-oriented than set/lattice oriented *) @@ -201,4 +204,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 +*) diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma index e136821af..4b667546b 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma @@ -14,9 +14,6 @@ include "o-basic_topologies.ma". -definition btop_carr: BTop → Type ≝ λo:BTop. carr1 (oa_P (carrbt o)). -coercion btop_carr. - (* definition btop_carr': BTop → setoid1 ≝ λo:BTop. carrbt o.