From: Claudio Sacerdoti Coen Date: Tue, 6 Jan 2009 01:10:01 +0000 (+0000) Subject: Great: some significant progress in fixing universe levels. X-Git-Tag: make_still_working~4288 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c78cbede35ed85575e274864e6b6b9c635c6956d;p=helm.git Great: some significant progress in fixing universe levels. --- diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma index 67db8176c..3a7614fca 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma @@ -12,36 +12,7 @@ (* *) (**************************************************************************) -include "logic/cprop_connectives.ma". - -definition Type0 := Type. -definition Type1 := Type. -definition Type2 := Type. -definition Type3 := Type. -definition Type0_lt_Type1 := (Type0 : Type1). -definition Type1_lt_Type2 := (Type1 : Type2). -definition Type2_lt_Type3 := (Type2 : Type3). - -definition Type_OF_Type0: Type0 → Type := λx.x. -definition Type_OF_Type1: Type1 → Type := λx.x. -definition Type_OF_Type2: Type2 → Type := λx.x. -definition Type_OF_Type3: Type3 → Type := λx.x. -coercion Type_OF_Type0. -coercion Type_OF_Type1. -coercion Type_OF_Type2. -coercion Type_OF_Type3. - -definition CProp0 := Type0. -definition CProp1 := Type1. -definition CProp2 := Type2. -(* -definition CProp0_lt_CProp1 := (CProp0 : CProp1). -definition CProp1_lt_CProp2 := (CProp1 : CProp2). - -definition CProp_OF_CProp0: CProp0 → CProp := λx.x. -definition CProp_OF_CProp1: CProp1 → CProp := λx.x. -definition CProp_OF_CProp2: CProp2 → CProp := λx.x. -*) +include "cprop_connectives.ma". record equivalence_relation (A:Type0) : Type1 ≝ { eq_rel:2> A → A → CProp0; @@ -194,8 +165,8 @@ definition CPROP: setoid1. | constructor 1; [ apply Iff | intros 1; split; intro; assumption - | intros 3; cases H; split; assumption - | intros 5; cases H; cases H1; split; intro; + | intros 3; cases i; split; assumption + | intros 5; cases i; cases i1; split; intro; [ apply (f2 (f x1)) | apply (f1 (f3 z1))]]] qed. @@ -210,10 +181,10 @@ interpretation "if" 'if r = (if' __ r). definition and_morphism: binary_morphism1 CPROP CPROP CPROP. constructor 1; [ apply And - | intros; split; intro; cases H; split; - [ apply (if ?? e a1) + | intros; split; intro; cases a1; split; + [ apply (if ?? e a2) | apply (if ?? e1 b1) - | apply (fi ?? e a1) + | apply (fi ?? e a2) | apply (fi ?? e1 b1)]] qed. @@ -222,7 +193,7 @@ interpretation "and_morphism" 'and a b = (fun21 ___ and_morphism a b). definition or_morphism: binary_morphism1 CPROP CPROP CPROP. constructor 1; [ apply Or - | intros; split; intro; cases H; [1,3:left |2,4: right] + | intros; split; intro; cases o; [1,3:left |2,4: right] [ apply (if ?? e a1) | apply (fi ?? e a1) | apply (if ?? e1 b1) diff --git a/helm/software/matita/contribs/formal_topology/overlap/depends b/helm/software/matita/contribs/formal_topology/overlap/depends index 54bda9a40..4875f5928 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/depends +++ b/helm/software/matita/contribs/formal_topology/overlap/depends @@ -2,10 +2,11 @@ o-basic_pairs.ma o-algebra.ma o-concrete_spaces.ma o-basic_pairs.ma o-saturations.ma o-saturations.ma o-algebra.ma basic_pairs.ma o-basic_pairs.ma relations.ma -o-algebra.ma categories.ma logic/cprop_connectives.ma +o-algebra.ma categories.ma o-formal_topologies.ma o-basic_topologies.ma -categories.ma logic/cprop_connectives.ma +categories.ma cprop_connectives.ma subsets.ma categories.ma o-algebra.ma relations.ma o-algebra.ma subsets.ma o-basic_topologies.ma o-algebra.ma o-saturations.ma -logic/cprop_connectives.ma +cprop_connectives.ma logic/connectives.ma +logic/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 55d692190..6be19d92c 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma @@ -13,7 +13,6 @@ (**************************************************************************) include "categories.ma". -include "logic/cprop_connectives.ma". inductive bool : Type0 := true : bool | false : bool. @@ -76,7 +75,7 @@ record OAlgebra : Type2 := { (* ⇔ deve essere =, l'esiste debole *) oa_join_split: ∀I:SET.∀p.∀q:arrows2 SET1 I oa_P. - oa_overlap p (oa_join I q) ⇔ ∃i:I.oa_overlap p (q i); + oa_overlap p (oa_join I q) ⇔ ∃i:carr 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 @@ -186,14 +185,14 @@ constructor 1; | constructor 1; (* tenere solo una uguaglianza e usare la proposizione 9.9 per le altre (unicita' degli aggiunti e del simmetrico) *) - [ apply (λp,q. And4 (eq2 ? (or_f_minus_star_ ?? p) (or_f_minus_star_ ?? q)) + [ apply (λp,q. And42 (eq2 ? (or_f_minus_star_ ?? p) (or_f_minus_star_ ?? q)) (eq2 ? (or_f_minus_ ?? p) (or_f_minus_ ?? q)) (eq2 ? (or_f_ ?? p) (or_f_ ?? q)) (eq2 ? (or_f_star_ ?? p) (or_f_star_ ?? q))); | whd; simplify; intros; repeat split; intros; apply refl2; - | whd; simplify; intros; cases H; clear H; split; + | whd; simplify; intros; cases a; clear a; split; intro a; apply sym1; generalize in match a;assumption; - | whd; simplify; intros; cases H; cases H1; clear H H1; split; intro a; + | whd; simplify; intros; cases a; cases a1; clear a a1; split; intro a; [ apply (.= (e a)); apply e4; | apply (.= (e1 a)); apply e5; | apply (.= (e2 a)); apply e6; diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations.ma b/helm/software/matita/contribs/formal_topology/overlap/relations.ma index f5141a2ed..e6f816156 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/relations.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/relations.ma @@ -29,10 +29,10 @@ definition binary_relation_setoid: SET → SET → SET1. [ apply (λA,B.λr,r': binary_relation A B. ∀x,y. r x y ↔ r' x y) | simplify; intros 3; split; intro; assumption | simplify; intros 5; split; intro; - [ apply (fi ?? (H ??)) | apply (if ?? (H ??))] assumption + [ apply (fi ?? (f ??)) | apply (if ?? (f ??))] assumption | simplify; intros 7; split; intro; - [ apply (if ?? (H1 ??)) | apply (fi ?? (H ??)) ] - [ apply (if ?? (H ??)) | apply (fi ?? (H1 ??)) ] + [ apply (if ?? (f1 ??)) | apply (fi ?? (f ??)) ] + [ apply (if ?? (f ??)) | apply (fi ?? (f1 ??)) ] assumption]] qed. @@ -48,7 +48,7 @@ definition composition: (* carr to avoid universe inconsistency *) apply (λs1:carr A.λs3:carr C.∃s2:carr B. s1 ♮R12 s2 ∧ s2 ♮R23 s3); | intros; - split; intro; cases H (w H3); clear H; exists; [1,3: apply w ] + split; intro; cases e2 (w H3); clear e2; exists; [1,3: apply w ] [ apply (. (e‡#)‡(#‡e1)); assumption | apply (. ((e \sup -1)‡#)‡(#‡(e1 \sup -1))); assumption]] | intros 8; split; intro H2; simplify in H2 ⊢ %; @@ -87,7 +87,7 @@ definition REL: category1. split; assumption |6,7: intros 5; unfold composition; simplify; split; intro; unfold setoid1_of_setoid in x y; simplify in x y; - [1,3: cases H (w H1); clear H; cases H1; clear H1; unfold; + [1,3: cases e (w H1); clear e; cases H1; clear H1; unfold; [ apply (. (e ^ -1 : eq1 ? w x)‡#); assumption | apply (. #‡(e : eq1 ? w y)); assumption] |2,4: exists; try assumption; split; @@ -210,7 +210,7 @@ definition minus_star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \s apply f; [ apply (if ?? (e ^ -1 ??)); | apply (if ?? (e ??)) ] assumption] qed. -(* the same as * for a basic pair *) +(* the same as Rest for a basic pair *) definition star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup V) (Ω \sup U). intros; constructor 1; [ apply (λr: arrows1 ? U V.λS: Ω \sup V. {x | ∀y:carr V. x ♮r y → y ∈ S}); @@ -221,7 +221,7 @@ definition star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup V) apply f; [ apply (if ?? (e ^ -1 ??)); | apply (if ?? (e ??)) ] assumption] qed. -(* the same as - for a basic pair *) +(* the same as Ext for a basic pair *) definition minus_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup V) (Ω \sup U). intros; constructor 1; [ apply (λr: arrows1 ? U V.λS: Ω \sup V. {x | (*∃x:U. x ♮r y ∧ x ∈ S*) @@ -294,11 +294,11 @@ qed. *) include "o-algebra.ma". - +axiom daemon: False. definition orelation_of_relation: ∀o1,o2:REL. arrows1 ? o1 o2 → ORelation (SUBSETS o1) (SUBSETS o2). intros; constructor 1; - [ constructor 1; + [ constructor 1; [ apply (λU.image ?? t U); | intros; apply (#‡e); ] | constructor 1; diff --git a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma index 73872bfed..6351fead9 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma @@ -203,7 +203,7 @@ definition SUBSETS: objs1 SET → OAlgebra. (* senza questa change, universe inconsistency *) change in ⊢ (? ? (λ_:%.?)) with (carr I); exists [apply w1] exists [apply w] assumption; - | cases H; cases x; exists; [apply w1] + | cases e; cases x; exists; [apply w1] [ assumption | (* senza questa change, universe inconsistency *) whd; change in ⊢ (? ? (λ_:%.?)) with (carr I);