From e39b9a73fa95490d29237e31cfd3ff7f6aa07e3d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 28 Dec 2008 15:14:43 +0000 Subject: [PATCH] o-algebra defined again --- .../formal_topology/overlap/categories.ma | 23 +++++++++-- .../formal_topology/overlap/o-algebra.ma | 39 +++++++++++-------- 2 files changed, 42 insertions(+), 20 deletions(-) diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma index 0d5d02afb..655c50760 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma @@ -100,6 +100,20 @@ record setoid2: Type3 ≝ eq2: equivalence_relation2 carr2 }. +definition setoid2_of_setoid1: setoid1 → setoid2. + intro; + constructor 1; + [ apply (carr1 s) + | constructor 1; + [ apply (eq_rel1 s); + apply (eq1 s) + | apply (refl1 s) + | apply (sym1 s) + | apply (trans1 s)]] +qed. + +coercion setoid2_of_setoid1. + (* definition Leibniz: Type → setoid. intro; @@ -182,6 +196,7 @@ definition CPROP: setoid1. [ apply (H4 (H2 x1)) | apply (H3 (H5 z1))]]] qed. +alias symbol "eq" = "setoid1 eq". definition if': ∀A,B:CPROP. A = B → A → B. intros; apply (if ?? e); assumption. qed. @@ -287,7 +302,7 @@ definition unary_morphism_setoid: setoid → setoid → setoid. constructor 1; [ apply (unary_morphism s s1); | constructor 1; - [ intros (f g); apply (∀a:s. f a = g a); + [ intros (f g); apply (∀a:s. eq ? (f a) (g a)); | intros 1; simplify; intros; apply refl; | simplify; intros; apply sym; apply H; | simplify; intros; apply trans; [2: apply H; | skip | apply H1]]] @@ -336,7 +351,9 @@ definition unary_morphism1_setoid1: setoid1 → setoid1 → setoid2. constructor 1; [ apply (unary_morphism1 s s1); | constructor 1; - [ intros (f g); apply (∀a: carr1 s. f a = g a); + [ intros (f g); + alias symbol "eq" = "setoid1 eq". + apply (∀a: carr1 s. f a = g a); | intros 1; simplify; intros; apply refl1; | simplify; intros; apply sym1; apply H; | simplify; intros; apply trans1; [2: apply H; | skip | apply H1]]] @@ -378,4 +395,4 @@ coercion hint. interpretation "SET dagger" 'prop1 h = (prop11_SET1 _ _ _ _ _ h). notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }. interpretation "unary morphism1" 'Imply a b = (arrows2 SET1 a b). -interpretation "SET1 eq" 'eq x y = (eq_rel1 _ (eq'' _) x y). \ No newline at end of file +interpretation "SET1 eq" 'eq x y = (eq_rel1 _ (eq'' _) x y). diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma index 617c58b60..5f99153ba 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma @@ -27,12 +27,12 @@ constructor 1; [apply bool] constructor 1; qed. lemma IF_THEN_ELSE_p : - ∀S:setoid.∀a,b:S.∀x,y:BOOL.x = y → + ∀S:setoid1.∀a,b:S.∀x,y:BOOL.x = y → (λm.match m with [ true ⇒ a | false ⇒ b ]) x = (λm.match m with [ true ⇒ a | false ⇒ b ]) y. whd in ⊢ (?→?→?→%→?); -intros; cases x in H; cases y; simplify; intros; try apply refl; whd in H; cases H; -qed. +intros; cases x in e; cases y; simplify; intros; try apply refl1; whd in e; cases e; +qed. interpretation "unary morphism comprehension with no proof" 'comprehension T P = (mk_unary_morphism T _ P _). @@ -49,20 +49,25 @@ interpretation "unary morphism comprehension with proof" 'comprehension_by s \et interpretation "unary morphism1 comprehension with proof" 'comprehension_by s \eta.f p = (mk_unary_morphism1 s _ f p). -definition Type_of_SET: SET → Type0 := λS.carr S. -coercion Type_of_SET. +definition hint: Type_OF_category2 SET1 → setoid2. + intro; apply (setoid2_of_setoid1 t); qed. +coercion hint. + +definition hint2: Type_OF_category1 SET → objs2 SET1. + intro; apply (setoid1_of_setoid t); qed. +coercion hint2. (* per il set-indexing vedere capitolo BPTools (foundational tools), Sect. 0.3.4 complete lattices, Definizione 0.9 *) (* USARE L'ESISTENZIALE DEBOLE *) (* Far salire SET usando setoidi1 *) -alias symbol "comprehension_by" = "unary morphism comprehension with proof". -record OAlgebra : Type1 := { - oa_P :> SET; - oa_leq : binary_morphism1 (setoid1_of_setoid oa_P) (setoid1_of_setoid oa_P) CPROP; (* CPROP is setoid1, CPROP importante che sia small *) - oa_overlap: binary_morphism1 (setoid1_of_setoid oa_P) (setoid1_of_setoid oa_P) CPROP; - oa_meet: ∀I:SET.unary_morphism1 (arrows1 SET I oa_P) (setoid1_of_setoid oa_P); - oa_join: ∀I:SET.unary_morphism1 (arrows1 SET I oa_P) (setoid1_of_setoid oa_P); +(*alias symbol "comprehension_by" = "unary morphism comprehension with proof".*) +record OAlgebra : Type2 := { + oa_P :> SET1; + oa_leq : binary_morphism1 oa_P oa_P CPROP; (* CPROP is setoid1, CPROP importante che sia small *) + oa_overlap: binary_morphism1 oa_P oa_P CPROP; + oa_meet: ∀I:SET.unary_morphism2 (arrows2 SET1 I oa_P) oa_P; + oa_join: ∀I:SET.unary_morphism2 (arrows2 SET1 I oa_P) oa_P; oa_one: oa_P; oa_zero: oa_P; oa_leq_refl: ∀a:oa_P. oa_leq a a; @@ -74,13 +79,13 @@ record OAlgebra : Type1 := { oa_join_sup: ∀I.∀p_i.∀p:oa_P.oa_leq (oa_join I p_i) p → ∀i:I.oa_leq (p_i i) p; oa_zero_bot: ∀p:oa_P.oa_leq oa_zero p; oa_one_top: ∀p:oa_P.oa_leq p oa_one; - (* preservers!! (typo) *) - oa_overlap_preservers_meet_: + oa_overlap_preserves_meet_: ∀p,q:oa_P.oa_overlap p q → oa_overlap p (oa_meet ? { x ∈ BOOL | match x with [ true ⇒ p | false ⇒ q ] | IF_THEN_ELSE_p oa_P p q }); (* ⇔ deve essere =, l'esiste debole *) oa_join_split: - ∀I:SET.∀p.∀q:arrows1 SET I oa_P.oa_overlap p (oa_join I q) ⇔ ∃i:I.oa_overlap p (q i); + ∀I:SET.∀p.∀q:arrows2 SET1 I oa_P. + oa_overlap p (oa_join I q) ⇔ ∃i:I.oa_overlap p (q i); (*oa_base : setoid; 1) enum non e' il nome giusto perche' non e' suriettiva 2) manca (vedere altro capitolo) la "suriettivita'" come immagine di insiemi di oa_base @@ -91,11 +96,11 @@ record OAlgebra : Type1 := { ∀p,q.(∀r.oa_overlap p r → oa_overlap q r) → oa_leq p q }. -interpretation "o-algebra leq" 'leq a b = (fun1 ___ (oa_leq _) a b). +interpretation "o-algebra leq" 'leq a b = (fun21 ___ (oa_leq _) a b). notation "hovbox(a mpadded width -150% (>)< b)" non associative with precedence 45 for @{ 'overlap $a $b}. -interpretation "o-algebra overlap" 'overlap a b = (fun1 ___ (oa_overlap _) a b). +interpretation "o-algebra overlap" 'overlap a b = (fun22 ___ (oa_overlap _) a b). notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (\emsp) \nbsp term 90 p)" non associative with precedence 50 for @{ 'oa_meet $p }. -- 2.39.2