From fdc6fe20875e45ea7446516af8904e2fb9b15388 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 6 Jan 2009 02:05:57 +0000 Subject: [PATCH] Basic pairs restored; require renaming to use them together with o-basic_pairs. --- .../formal_topology/overlap/basic_pairs.ma | 73 ++++++++++--------- 1 file changed, 40 insertions(+), 33 deletions(-) diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma index 4d467fc26..071892f6b 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma @@ -40,27 +40,6 @@ 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). -include "o-basic_pairs.ma". -(* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *) -definition o_basic_pair_of_basic_pair: cic:/matita/formal_topology/basic_pairs/basic_pair.ind#xpointer(1/1) → basic_pair. - intro; - constructor 1; - [ apply (SUBSETS (concr b)); - | apply (SUBSETS (form b)); - | apply (orelation_of_relation ?? (rel b)); ] -qed. - -definition o_relation_pair_of_relation_pair: - ∀BP1,BP2.cic:/matita/formal_topology/basic_pairs/relation_pair.ind#xpointer(1/1) BP1 BP2 → - relation_pair (o_basic_pair_of_basic_pair BP1) (o_basic_pair_of_basic_pair BP2). - intros; - constructor 1; - [ apply (orelation_of_relation ?? (r \sub \c)); - | apply (orelation_of_relation ?? (r \sub \f)); - | - ] -qed. - definition relation_pair_equality: ∀o1,o2. equivalence_relation1 (relation_pair o1 o2). intros; @@ -118,23 +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); + alias symbol "trans" = "trans1". + alias symbol "assoc" = "category1 assoc". + apply (.= ASSOC); apply (.= #‡H1); - apply (.= ASSOC1\sup -1); + alias symbol "invert" = "setoid1 symmetry". + apply (.= ASSOC ^ -1); apply (.= H‡#); - apply ASSOC1] + apply ASSOC] | 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 (.= ASSOC); + apply (.= #‡e1); apply (.= #‡(commute ?? b')); - apply (.= ASSOC1 \sup -1); - apply (.= H‡#); - apply (.= ASSOC1); + apply (.= ASSOC ^ -1); + apply (.= e‡#); + apply (.= ASSOC); apply (.= #‡(commute ?? b')\sup -1); - apply (ASSOC1 \sup -1)] + apply (ASSOC ^ -1)] qed. definition BP: category1. @@ -146,7 +128,9 @@ 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‡#); + alias symbol "refl" = "refl1". + alias symbol "prop2" = "prop21". + apply (ASSOC‡#); | intros; change with (⊩ ∘ (a\sub\c ∘ (id_relation_pair o1)\sub\c) = ⊩ ∘ a\sub\c); apply ((id_neutral_right1 ????)‡#); @@ -155,6 +139,7 @@ definition BP: category1. apply ((id_neutral_left1 ????)‡#);] qed. +(* definition BPext: ∀o: BP. form o ⇒ Ω \sup (concr o). intros; constructor 1; [ apply (ext ? ? (rel o)); @@ -199,3 +184,25 @@ 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 _)). +*) + +include "o-basic_pairs.ma". +(* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *) +definition o_basic_pair_of_basic_pair: cic:/matita/formal_topology/basic_pairs/basic_pair.ind#xpointer(1/1) → basic_pair. + intro; + constructor 1; + [ apply (SUBSETS (concr b)); + | apply (SUBSETS (form b)); + | apply (orelation_of_relation ?? (rel b)); ] +qed. + +definition o_relation_pair_of_relation_pair: + ∀BP1,BP2.cic:/matita/formal_topology/basic_pairs/relation_pair.ind#xpointer(1/1) BP1 BP2 → + relation_pair (o_basic_pair_of_basic_pair BP1) (o_basic_pair_of_basic_pair BP2). + intros; + constructor 1; + [ apply (orelation_of_relation ?? (r \sub \c)); + | apply (orelation_of_relation ?? (r \sub \f)); + | + ] +qed. \ No newline at end of file -- 2.39.2