From a99ab6bf4e5bb993d363a9e62985371ba14cf71a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 15 Jul 2008 12:01:23 +0000 Subject: [PATCH] Since CProp_i = Type_i everything lowered without 2 distinct Sigma. --- .../contribs/dama/dama/cprop_connectives.ma | 15 --------------- .../matita/contribs/dama/dama/lebesgue.ma | 16 ++++++++-------- .../dama/models/nat_dedekind_sigma_complete.ma | 4 ++-- .../matita/contribs/dama/dama/ordered_uniform.ma | 15 ++++++--------- .../matita/contribs/dama/dama/property_sigma.ma | 1 - .../matita/contribs/dama/dama/supremum.ma | 2 +- 6 files changed, 17 insertions(+), 36 deletions(-) diff --git a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma index bd528521d..93fbac9b2 100644 --- a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma +++ b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma @@ -61,27 +61,12 @@ 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→Prop) : 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 6daebfa0c..d0fcae691 100644 --- a/helm/software/matita/contribs/dama/dama/lebesgue.ma +++ b/helm/software/matita/contribs/dama/dama/lebesgue.ma @@ -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,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; + 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; [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,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; + 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; [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/nat_dedekind_sigma_complete.ma b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma index 7bb312aff..b5610cbe0 100644 --- a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma +++ b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma @@ -17,7 +17,7 @@ include "supremum.ma". include "nat/le_arith.ma". include "russell_support.ma". -alias symbol "pi1" = "sigT \fst". +alias symbol "pi1" = "exT \fst". alias symbol "leq" = "natural 'less or equal to'". lemma nat_dedekind_sigma_complete: ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing → @@ -114,7 +114,7 @@ apply le_to_le_to_eq; rewrite < (H4 ?); [2: reflexivity] apply le_n;] qed. -alias symbol "pi1" = "sigT \fst". +alias symbol "pi1" = "exT \fst". alias symbol "leq" = "natural 'less or equal to'". alias symbol "nat" = "ordered set N". axiom nat_dedekind_sigma_complete_r: diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma index 2ffda533a..66bcf6f0b 100644 --- a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma +++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma @@ -30,7 +30,7 @@ unfold bishop_set_OF_ordered_uniform_space_; |5: cases (with_ X); simplify; apply (us_phi4 (ous_us_ X))] qed. -coercion cic:/matita/dama/ordered_uniform/ous_unifspace.con. +coercion ous_unifspace. record ordered_uniform_space : Type ≝ { ous_stuff :> ordered_uniform_space_; @@ -51,15 +51,15 @@ lemma segment_square_of_ordered_set_square: intros; split; exists; [1: apply (\fst x) |3: apply (\snd x)] assumption; qed. -coercion cic:/matita/dama/ordered_uniform/segment_square_of_ordered_set_square.con 0 2. +coercion segment_square_of_ordered_set_square with 0 2. -alias symbol "pi1" (instance 4) = "sigT \fst". -alias symbol "pi1" (instance 2) = "sigT \fst". +alias symbol "pi1" (instance 4) = "exT \fst". +alias symbol "pi1" (instance 2) = "exT \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)〉. -coercion cic:/matita/dama/ordered_uniform/ordered_set_square_of_segment_square.con. +coercion ordered_set_square_of_segment_square. lemma restriction_agreement : ∀O:ordered_uniform_space.∀l,r:O.∀P:{[l,r]} square → Prop.∀OP:O square → Prop.Prop. @@ -99,9 +99,6 @@ lemma bs_of_ss: 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 ≝ @@ -161,7 +158,7 @@ interpretation "Ordered uniform space segment" 'segment_set a b = (segment_ordered_uniform_space _ a b). (* Lemma 3.2 *) -alias symbol "pi1" = "sigT \fst". +alias symbol "pi1" = "exT \fst". lemma restric_uniform_convergence: ∀O:ordered_uniform_space.∀l,u:O. ∀x:{[l,u]}. diff --git a/helm/software/matita/contribs/dama/dama/property_sigma.ma b/helm/software/matita/contribs/dama/dama/property_sigma.ma index 2e0e73bc6..241882bdd 100644 --- a/helm/software/matita/contribs/dama/dama/property_sigma.ma +++ b/helm/software/matita/contribs/dama/dama/property_sigma.ma @@ -63,7 +63,6 @@ lemma sigma_cauchy: ∀C:ordered_uniform_space.property_sigma C → ∀a:sequence C.∀l:C.(a ↑ l ∨ a ↓ l) → a is_cauchy → a uniform_converges l. intros 8; cases (H ? H3) (w H5); cases H5 (H8 H9); clear H5; -alias symbol "pair" = "Pair construction". letin spec ≝ (λz,k:nat.∀i,j,l:nat.k ≤ i → k ≤ j → l ≤ z → w l 〈a i,a j〉); letin m ≝ (hide ? (let rec aux (i:nat) : nat ≝ match i with diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma index b4430d6ed..f0260471f 100644 --- a/helm/software/matita/contribs/dama/dama/supremum.ma +++ b/helm/software/matita/contribs/dama/dama/supremum.ma @@ -238,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 (sigT ? (λx.x ∈ [u,v]))); +intros (O u v); apply (mk_ordered_set (∃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