From bd3b9cc44e65e316159ab56d3099949224413d66 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 28 Dec 2008 16:28:58 +0000 Subject: [PATCH] The universe inconsistency comes from big union, that uses the existential. --- .../contribs/formal_topology/overlap/subsets.ma | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma index 5803e6906..4bbe7fdbe 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma @@ -153,10 +153,10 @@ definition big_intersects: | apply (. (#‡(e i)\sup -1)); apply f]] qed. -definition big_union: +axiom (*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; +(* intros; constructor 1; + [ intro; whd; whd in A; 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‡#)); ] @@ -164,14 +164,14 @@ definition big_union: | 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. +qed.*) (* incluso prima non funziona piu' nulla *) include "o-algebra.ma". axiom daemon: False. -definition SUBSETS: SET → OAlgebra. +definition SUBSETS: objs1 SET → OAlgebra. intro A; constructor 1; [ apply (Ω \sup A); | apply subseteq; @@ -187,17 +187,18 @@ definition SUBSETS: SET → OAlgebra. | 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; 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; + |(* 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]] + | 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]] +cases daemon; qed. \ No newline at end of file -- 2.39.2