From 1c2cadee5d666f0e31085a4ff358d667379c4f25 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 15 Jul 2008 09:08:15 +0000 Subject: [PATCH 1/1] Using Prop conjuction on Props lowers the universes. SigT instead of ExT --- .../contribs/dama/dama/cprop_connectives.ma | 20 +++++++++++++++++++ .../matita/contribs/dama/dama/lebesgue.ma | 18 ++++++++--------- .../dama/dama/models/discrete_uniformity.ma | 2 +- .../contribs/dama/dama/ordered_uniform.ma | 8 +++++--- .../matita/contribs/dama/dama/supremum.ma | 3 +-- 5 files changed, 36 insertions(+), 15 deletions(-) diff --git a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma index 09b9a6c67..f9de36d1f 100644 --- a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma +++ b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma @@ -62,6 +62,26 @@ interpretation "constructive quaternary and" 'and4 x y z t = (And4 x y z t). inductive exT (A:Type) (P:A→CProp) : CProp ≝ ex_introT: ∀w:A. P w → exT A P. +record sigT (A:Type) (P:A→CProp) : Type ≝ { + fstT:A; + sndT:P fstT +}. + +interpretation "sigT \fst" 'pi1 = (fstT _ _). +interpretation "sigT \fst" 'pi1a x = (fstT _ _ x). +interpretation "sigT \fst" 'pi1b x y = (fstT _ _ x y). +interpretation "sigT \snd" 'pi2 = (sndT _ _). +interpretation "sigT \snd" 'pi2a x = (sndT _ _ x). +interpretation "sigT \snd" 'pi2b x y = (sndT _ _ x y). + +notation "\ll term 19 a, break term 19 b \gg" +with precedence 90 for @{'dependent_pair $a $b}. +interpretation "dependent pair" 'dependent_pair a b = + (ex_introT _ _ a b). + +interpretation "dependent set" 'dependent_pair a b = + (mk_sigT _ _ a b). + interpretation "CProp exists" 'exists \eta.x = (exT _ x). notation "\ll term 19 a, break term 19 b \gg" diff --git a/helm/software/matita/contribs/dama/dama/lebesgue.ma b/helm/software/matita/contribs/dama/dama/lebesgue.ma index e1fbd0a5a..6daebfa0c 100644 --- a/helm/software/matita/contribs/dama/dama/lebesgue.ma +++ b/helm/software/matita/contribs/dama/dama/lebesgue.ma @@ -38,7 +38,7 @@ cases (H3 j); clear H3; cases H2; cases H7; clear H2 H7; intro H2; cases (H10 ? H2); cases (H (w1+j)); apply (H11 H7); qed. - + (* Theorem 3.10 *) theorem lebesgue_oc: ∀C:ordered_uniform_space. @@ -65,10 +65,10 @@ split; [1: apply (le_transitive ???? (H8 0)); cases (Hyi 0); assumption |2: apply (le_transitive ????? (H4 0)); cases (Hxi 0); assumption] |2: intros 3 (h); - letin Xi ≝ (⌊n,≪xi n,Hxi n≫⌋); - letin Yi ≝ (⌊n,≪yi n,Hyi n≫⌋); - letin Ai ≝ (⌊n,≪a n,H1 n≫⌋); - apply (sandwich {[l,u]} ≪?,h≫ Xi Yi Ai); try assumption; + letin Xi ≝ (⌊n,mk_sigT ?? (xi n) (Hxi n)⌋); + letin Yi ≝ (⌊n,mk_sigT ?? (yi n) (Hyi n)⌋); + letin Ai ≝ (⌊n,mk_sigT ?? (a n) (H1 n)⌋); + apply (sandwich {[l,u]} (mk_sigT ?? x h) Xi Yi Ai); try assumption; [1: intro j; cases (Hxy j); cases H3; cases H4; split; [apply (H5 0);|apply (H7 0)] |2: cases (H l u Xi ≪?,h≫) (Ux Uy); apply Ux; cases Hx; split; [apply H3;] @@ -108,10 +108,10 @@ split; |2: intros 3; lapply (uparrow_upperlocated ? xi x Hx)as Ux; lapply (downarrow_lowerlocated ? yi x Hy)as Uy; - letin Xi ≝ (⌊n,≪xi n,Hxi n≫⌋); - letin Yi ≝ (⌊n,≪yi n,Hyi n≫⌋); - letin Ai ≝ (⌊n,≪a n,H1 n≫⌋); - apply (sandwich {[l,u]} ≪x,h≫ Xi Yi Ai); try assumption; + letin Xi ≝ (⌊n,mk_sigT ?? (xi n) (Hxi n)⌋); + letin Yi ≝ (⌊n,mk_sigT ?? (yi n) (Hyi n)⌋); + letin Ai ≝ (⌊n,mk_sigT ?? (a n) (H1 n)⌋); + apply (sandwich {[l,u]} (mk_sigT ?? x h) Xi Yi Ai); try assumption; [1: intro j; cases (Hxy j); cases H3; cases H4; split; [apply (H5 0);|apply (H7 0)] |2: cases (restrict_uniform_convergence_uparrow ? S ?? (H l u) Xi x Hx); diff --git a/helm/software/matita/contribs/dama/dama/models/discrete_uniformity.ma b/helm/software/matita/contribs/dama/dama/models/discrete_uniformity.ma index 412b5407d..01890a416 100644 --- a/helm/software/matita/contribs/dama/dama/models/discrete_uniformity.ma +++ b/helm/software/matita/contribs/dama/dama/models/discrete_uniformity.ma @@ -21,7 +21,7 @@ intro C; apply (mk_uniform_space C); alias symbol "pi2" = "pair pi2". alias symbol "pi1" = "pair pi1". alias symbol "and" = "logical and". - apply (∃_:unit.∀n:C square.(\fst n ≈ \snd n → P n) ∧ (P n → \fst n ≈ \snd n)); + apply (∃d:unit.∀n:C square.(\fst n ≈ \snd n → P n) ∧ (P n → \fst n ≈ \snd n)); |2: intros 4 (U H x Hx); simplify in Hx; cases H (_ H1); cases (H1 x); apply H2; apply Hx; |3: intros; cases H (_ PU); cases H1 (_ PV); diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma index bf0260a51..2ffda533a 100644 --- a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma +++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma @@ -53,8 +53,8 @@ qed. coercion cic:/matita/dama/ordered_uniform/segment_square_of_ordered_set_square.con 0 2. -alias symbol "pi1" (instance 4) = "exT \fst". -alias symbol "pi1" (instance 2) = "exT \fst". +alias symbol "pi1" (instance 4) = "sigT \fst". +alias symbol "pi1" (instance 2) = "sigT \fst". lemma ordered_set_square_of_segment_square : ∀O:ordered_set.∀u,v:O.{[u,v]} square → O square ≝ λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈\fst(\fst b),\fst(\snd b)〉. @@ -100,6 +100,8 @@ notation < "x \sub \neq" with precedence 91 for @{'bsss $x}. interpretation "bs_of_ss" 'bsss x = (bs_of_ss _ _ _ x). alias symbol "square" (instance 7) = "ordered set square". +alias symbol "square" (instance 13) = "ordered set square". +alias symbol "dependent_pair" = "dependent set". lemma ss_of_bs: ∀O:ordered_set.∀u,v:O. ∀b:O square.\fst b ∈ [u,v] → \snd b ∈ [u,v] → {[u,v]} square ≝ @@ -159,7 +161,7 @@ interpretation "Ordered uniform space segment" 'segment_set a b = (segment_ordered_uniform_space _ a b). (* Lemma 3.2 *) -alias symbol "pi1" = "exT \fst". +alias symbol "pi1" = "sigT \fst". lemma restric_uniform_convergence: ∀O:ordered_uniform_space.∀l,u:O. ∀x:{[l,u]}. diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma index a492c8f32..b4430d6ed 100644 --- a/helm/software/matita/contribs/dama/dama/supremum.ma +++ b/helm/software/matita/contribs/dama/dama/supremum.ma @@ -227,7 +227,6 @@ notation > "a 'order_converges' x" non associative with precedence 45 interpretation "Order convergence" 'order_converge s u = (order_converge _ s u). (* Definition 2.8 *) -alias symbol "and" = "constructive and". definition segment ≝ λO:ordered_set.λa,b:O.λx:O.(x ≤ b) ∧ (a ≤ x). notation "[a,b]" left associative with precedence 70 for @{'segment $a $b}. @@ -239,7 +238,7 @@ interpretation "Ordered set sergment in" 'segment_in a b x= (segment _ a b x). lemma segment_ordered_set: ∀O:ordered_set.∀u,v:O.ordered_set. -intros (O u v); apply (mk_ordered_set (∃x.x ∈ [u,v])); +intros (O u v); apply (mk_ordered_set (sigT ? (λx.x ∈ [u,v]))); [1: intros (x y); apply (\fst x ≰ \fst y); |2: intro x; cases x; simplify; apply os_coreflexive; |3: intros 3 (x y z); cases x; cases y ; cases z; simplify; apply os_cotransitive] -- 2.39.2