From b8f8fdbf7c1714e3332b71952b9610b8cd8e8841 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 28 Dec 2008 16:10:34 +0000 Subject: [PATCH] Proof that \Omega \sup A is an overlap algebra, up to universe inconsistency :-( --- .../formal_topology/overlap/categories.ma | 2 +- .../contribs/formal_topology/overlap/depends | 3 +- .../formal_topology/overlap/o-algebra.ma | 4 +- .../formal_topology/overlap/subsets.ma | 64 ++++++++++++++++++- 4 files changed, 68 insertions(+), 5 deletions(-) diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma index 655c50760..3e03cb093 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma @@ -112,7 +112,7 @@ definition setoid2_of_setoid1: setoid1 → setoid2. | apply (trans1 s)]] qed. -coercion setoid2_of_setoid1. +(*coercion setoid2_of_setoid1.*) (* definition Leibniz: Type → setoid. diff --git a/helm/software/matita/contribs/formal_topology/overlap/depends b/helm/software/matita/contribs/formal_topology/overlap/depends index 377b1d243..1ff1aea9c 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/depends +++ b/helm/software/matita/contribs/formal_topology/overlap/depends @@ -1,9 +1,10 @@ o-basic_pairs.ma datatypes/categories.ma o-algebra.ma o-concrete_spaces.ma o-basic_pairs.ma o-saturations.ma o-saturations.ma o-algebra.ma -o-algebra.ma datatypes/categories.ma logic/cprop_connectives.ma +o-algebra.ma categories.ma logic/cprop_connectives.ma o-formal_topologies.ma o-basic_topologies.ma categories.ma logic/cprop_connectives.ma +subsets.ma categories.ma o-algebra.ma o-basic_topologies.ma o-algebra.ma o-saturations.ma datatypes/categories.ma logic/cprop_connectives.ma 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 5f99153ba..bcd1aae1b 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma @@ -60,7 +60,6 @@ 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 : Type2 := { oa_P :> SET1; @@ -122,6 +121,8 @@ interpretation "o-algebra meet" 'oa_meet f = interpretation "o-algebra meet with explicit function" 'oa_meet_mk f = (fun11 __ (oa_meet __) (mk_unary_morphism _ _ f _)). +(* + definition binary_meet : ∀O:OAlgebra. binary_morphism1 O O O. intros; split; [ intros (p q); @@ -316,3 +317,4 @@ split; | intros; split; unfold ORelation_composition; simplify; apply id_neutral_left1; | intros; split; unfold ORelation_composition; simplify; apply id_neutral_right1;] qed. +*) \ No newline at end of file diff --git a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma index 7eb2d1e94..5803e6906 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "logic/cprop_connectives.ma". include "categories.ma". record powerset_carrier (A: objs1 SET) : Type1 ≝ { mem_operator: unary_morphism1 A CPROP }. @@ -140,4 +139,65 @@ definition singleton: ∀A:setoid. unary_morphism1 A (Ω \sup A). [ apply a |4: apply a'] try assumption; apply sym; assumption] qed. -interpretation "singleton" 'singl a = (fun11 __ (singleton _) a). \ No newline at end of file +interpretation "singleton" 'singl a = (fun11 __ (singleton _) a). + +definition big_intersects: + ∀A:SET.∀I:SET.unary_morphism2 (setoid1_of_setoid I ⇒ Ω \sup A) (setoid2_of_setoid1 (Ω \sup A)). + intros; constructor 1; + [ intro; whd; whd in I; + apply ({x | ∀i:I. x ∈ t i}); + simplify; intros; split; intros; [ apply (. (e‡#)); | apply (. (e \sup -1‡#)); ] + apply H; + | intros; split; intros 2; simplify in f ⊢ %; intro; + [ apply (. (#‡(e i))); apply f; + | apply (. (#‡(e i)\sup -1)); apply f]] +qed. + +definition big_union: + ∀A:SET.∀I:SET.unary_morphism2 (setoid1_of_setoid I ⇒ Ω \sup A) (setoid2_of_setoid1 (Ω \sup A)). + intros; constructor 1; + [ intro; whd; whd in I; + apply ({x | ∃i:I. x ∈ t i}); + simplify; intros; split; intros; cases H; clear H; exists; [1,3:apply w] + [ apply (. (e‡#)); | apply (. (e \sup -1‡#)); ] + apply x; + | intros; split; intros 2; simplify in f ⊢ %; cases f; clear f; exists; [1,3:apply w] + [ apply (. (#‡(e w))); apply x; + | apply (. (#‡(e w)\sup -1)); apply x]] +qed. + +(* incluso prima non funziona piu' nulla *) +include "o-algebra.ma". + + +axiom daemon: False. +definition SUBSETS: SET → OAlgebra. + intro A; constructor 1; + [ apply (Ω \sup A); + | apply subseteq; + | apply overlaps; + | apply big_intersects; + | apply big_union; + | apply ({x | True}); + simplify; intros; apply (refl1 ? (eq1 CPROP)); + | apply ({x | False}); + simplify; intros; apply (refl1 ? (eq1 CPROP)); + | intros; whd; intros; assumption + | intros; whd; split; assumption + | intros; apply transitive_subseteq_operator; [2: apply f; | skip | assumption] + | intros; cases f; exists [apply w] assumption + | intros; intros 2; apply (f ? f1 i); + | intros; intros 2; apply f; exists; [apply i] assumption; + | intros 3; cases f; + | intros 3; constructor 1; + | intros; cases f; exists; [apply w] + [ assumption + | whd; intros; cases i; simplify; assumption] + | intros; split; intro; + [ cases f; cases x1; exists [apply w1] exists [apply w] assumption; + | cases H; cases x; exists; [apply w1] [assumption | exists; [apply w] assumption]] + | intros; intros 2; cases (H (singleton ? a) ?); + [ exists; [apply a] [assumption | change with (a = a); apply refl1;] + | change in x1 with (a = w); change with (mem A a q); apply (. (x1 \sup -1‡#)); + assumption]] +qed. \ No newline at end of file -- 2.39.2