From 3c1ca5620048ad842144fba291f8bc5f0dca7061 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Jun 2008 07:14:52 +0000 Subject: [PATCH] more notation --- .../matita/contribs/dama/dama/bishop_set.ma | 3 +- .../contribs/dama/dama/cprop_connectives.ma | 43 ++--- .../matita/contribs/dama/dama/depends | 7 +- .../contribs/dama/dama/nat_ordered_set.ma | 11 +- .../contribs/dama/dama/ordered_uniform.ma | 3 +- .../matita/contribs/dama/dama/sequence.ma | 22 ++- .../matita/contribs/dama/dama/supremum.ma | 153 +++++++++--------- .../matita/contribs/dama/dama/uniform.ma | 39 ++--- 8 files changed, 141 insertions(+), 140 deletions(-) diff --git a/helm/software/matita/contribs/dama/dama/bishop_set.ma b/helm/software/matita/contribs/dama/dama/bishop_set.ma index d57282079..78176d776 100644 --- a/helm/software/matita/contribs/dama/dama/bishop_set.ma +++ b/helm/software/matita/contribs/dama/dama/bishop_set.ma @@ -41,7 +41,7 @@ qed. (* Definition 2.2 (2) *) definition eq ≝ λA:bishop_set.λa,b:A. ¬ (a # b). -notation "hvbox(a break ≈ b)" non associative with precedence 45 +notation "hvbox(a break \approx b)" non associative with precedence 45 for @{ 'napart $a $b}. interpretation "Bishop set alikeness" 'napart a b = (eq _ a b). @@ -57,7 +57,6 @@ qed. lemma eq_sym:∀E:bishop_set.∀x,y:E.x ≈ y → y ≈ x ≝ eq_sym_. lemma eq_trans_: ∀E:bishop_set.transitive ? (eq E). -(* bug. intros k deve fare whd quanto basta *) intros 6 (E x y z Exy Eyz); intro Axy; cases (bs_cotransitive ???y Axy); [apply Exy|apply Eyz] assumption. qed. diff --git a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma index 21c10a4e1..b42eaf61b 100644 --- a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma +++ b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma @@ -15,7 +15,7 @@ include "logic/equality.ma". inductive Or (A,B:CProp) : CProp ≝ - Left : A → Or A B + | Left : A → Or A B | Right : B → Or A B. interpretation "constructive or" 'or x y = (Or x y). @@ -28,14 +28,14 @@ interpretation "constructive and" 'and x y = (And x y). inductive And3 (A,B,C:CProp) : CProp ≝ | Conj3 : A → B → C → And3 A B C. -notation < "a ∧ b ∧ c" left associative with precedence 60 for @{'and3 $a $b $c}. +notation < "a ∧ b ∧ c" left associative with precedence 35 for @{'and3 $a $b $c}. interpretation "constructive ternary and" 'and3 x y z = (Conj3 x y z). -inductive And4 (A,B,C:CProp) : CProp ≝ - | Conj4 : A → B → C → And4 A B C. +inductive And4 (A,B,C,D:CProp) : CProp ≝ + | Conj4 : A → B → C → D → And4 A B C D. -notation < "a ∧ b ∧ c ∧ d" left associative with precedence 60 for @{'and3 $a $b $c $d}. +notation < "a ∧ b ∧ c ∧ d" left associative with precedence 35 for @{'and4 $a $b $c $d}. interpretation "constructive quaternary and" 'and4 x y z t = (Conj4 x y z t). @@ -47,28 +47,35 @@ interpretation "CProp exists" 'exists \eta.x = (exT _ x). inductive exT23 (A:Type) (P:A→CProp) (Q:A→CProp) (R:A→A→CProp) : CProp ≝ ex_introT23: ∀w,p:A. P w → Q p → R w p → exT23 A P Q R. -notation < "'fst' \nbsp x" non associative with precedence 50 for @{'pi1 $x}. -notation < "'snd' \nbsp x" non associative with precedence 50 for @{'pi2 $x}. -notation > "'fst' x" non associative with precedence 50 for @{'pi1 $x}. -notation > "'snd' x" non associative with precedence 50 for @{'pi2 $x}. -notation < "'fst' \nbsp x \nbsp y" non associative with precedence 50 for @{'pi12 $x $y}. -notation < "'snd' \nbsp x \nbsp y" non associative with precedence 50 for @{'pi22 $x $y}. +notation < "'fst' \nbsp x" non associative with precedence 90 for @{'pi1a $x}. +notation < "'snd' \nbsp x" non associative with precedence 90 for @{'pi2a $x}. +notation < "'fst' \nbsp x \nbsp y" non associative with precedence 90 for @{'pi1b $x $y}. +notation < "'snd' \nbsp x \nbsp y" non associative with precedence 90 for @{'pi2b $x $y}. +notation > "'fst'" non associative with precedence 90 for @{'pi1}. +notation > "'snd'" non associative with precedence 90 for @{'pi2}. definition pi1exT ≝ λA,P.λx:exT A P.match x with [ex_introT x _ ⇒ x]. +definition pi2exT ≝ + λA,P.λx:exT A P.match x return λx.P (pi1exT ?? x) with [ex_introT _ p ⇒ p]. -interpretation "exT fst" 'pi1 x = (pi1exT _ _ x). -interpretation "exT fst 2" 'pi12 x y = (pi1exT _ _ x y). +interpretation "exT fst" 'pi1 = (pi1exT _ _). +interpretation "exT fst" 'pi1a x = (pi1exT _ _ x). +interpretation "exT fst" 'pi1b x y = (pi1exT _ _ x y). +interpretation "exT snd" 'pi2 = (pi2exT _ _). +interpretation "exT snd" 'pi2a x = (pi2exT _ _ x). +interpretation "exT snd" 'pi2b x y = (pi2exT _ _ x y). definition pi1exT23 ≝ λA,P,Q,R.λx:exT23 A P Q R.match x with [ex_introT23 x _ _ _ _ ⇒ x]. definition pi2exT23 ≝ λA,P,Q,R.λx:exT23 A P Q R.match x with [ex_introT23 _ x _ _ _ ⇒ x]. - -interpretation "exT2 fst" 'pi1 x = (pi1exT23 _ _ _ _ x). -interpretation "exT2 snd" 'pi2 x = (pi2exT23 _ _ _ _ x). -interpretation "exT2 fst 2" 'pi12 x y = (pi1exT23 _ _ _ _ x y). -interpretation "exT2 snd 2" 'pi22 x y = (pi2exT23 _ _ _ _ x y). +interpretation "exT2 fst" 'pi1 = (pi1exT23 _ _ _ _). +interpretation "exT2 snd" 'pi2 = (pi2exT23 _ _ _ _). +interpretation "exT2 fst" 'pi1a x = (pi1exT23 _ _ _ _ x). +interpretation "exT2 snd" 'pi2a x = (pi2exT23 _ _ _ _ x). +interpretation "exT2 fst" 'pi1b x y = (pi1exT23 _ _ _ _ x y). +interpretation "exT2 snd" 'pi2b x y = (pi2exT23 _ _ _ _ x y). definition Not : CProp → Prop ≝ λx:CProp.x → False. diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends index 368625b80..d00e75e49 100644 --- a/helm/software/matita/contribs/dama/dama/depends +++ b/helm/software/matita/contribs/dama/dama/depends @@ -4,17 +4,16 @@ uniform.ma supremum.ma bishop_set.ma ordered_set.ma sequence.ma nat/nat.ma ordered_uniform.ma uniform.ma -supremum.ma bishop_set.ma cprop_connectives.ma nat/plus.ma nat_ordered_set.ma ordered_set.ma sequence.ma +supremum.ma bishop_set.ma cprop_connectives.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma ordered_set.ma sequence.ma property_exhaustivity.ma ordered_uniform.ma property_sigma.ma bishop_set_rewrite.ma bishop_set.ma cprop_connectives.ma logic/equality.ma -nat_ordered_set.ma cprop_connectives.ma nat/compare.ma ordered_set.ma +nat_ordered_set.ma ordered_set.ma bishop_set.ma cprop_connectives.ma nat/compare.ma lebesgue.ma property_exhaustivity.ma sandwich.ma ordered_set.ma cprop_connectives.ma russell_support.ma cprop_connectives.ma nat/nat.ma -models/uniformnat.ma bishop_set_rewrite.ma datatypes/constructors.ma decidable_kit/decidable.ma nat_ordered_set.ma ordered_uniform.ma russell_support.ma uniform.ma +models/uniformnat.ma bishop_set_rewrite.ma nat_ordered_set.ma ordered_uniform.ma russell_support.ma uniform.ma datatypes/constructors.ma -decidable_kit/decidable.ma logic/equality.ma nat/compare.ma nat/nat.ma diff --git a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma index 18ecf8e60..d625d391d 100644 --- a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma +++ b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma @@ -12,9 +12,8 @@ (* *) (**************************************************************************) -include "bishop_set.ma". include "nat/compare.ma". -include "cprop_connectives.ma". +include "bishop_set.ma". definition nat_excess : nat → nat → CProp ≝ λn,m. m "hvbox(\lfloor ident i, p \rfloor)" + left associative with precedence 70 +for @{ 'sequence (\lambda ${ident i} . $p)}. + +notation "a \sub i" left associative with precedence 70 + for @{ 'sequence_appl $a $i }. + +interpretation "sequence" 'sequence \eta.x = (mk_seq _ x). +interpretation "sequence element" 'sequence_appl s i = (fun_of_seq _ s i). diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma index e6b9dbbc6..ea5c55050 100644 --- a/helm/software/matita/contribs/dama/dama/supremum.ma +++ b/helm/software/matita/contribs/dama/dama/supremum.ma @@ -12,9 +12,11 @@ (* *) (**************************************************************************) -include "sequence.ma". -include "ordered_set.ma". + include "datatypes/constructors.ma". +include "nat/plus.ma". +include "nat_ordered_set.ma". +include "sequence.ma". (* Definition 2.4 *) definition upper_bound ≝ λO:ordered_set.λa:sequence O.λu:O.∀n:nat.a n ≤ u. @@ -28,40 +30,38 @@ definition infimum ≝ definition increasing ≝ λO:ordered_set.λa:sequence O.∀n:nat.a n ≤ a (S n). definition decreasing ≝ λO:ordered_set.λa:sequence O.∀n:nat.a (S n) ≤ a n. -notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 50 +notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 45 for @{'upper_bound $s $x}. -notation < "x \nbsp 'is_lower_bound' \nbsp s" non associative with precedence 50 +notation < "x \nbsp 'is_lower_bound' \nbsp s" non associative with precedence 45 for @{'lower_bound $s $x}. -notation < "s \nbsp 'is_increasing'" non associative with precedence 50 +notation < "s \nbsp 'is_increasing'" non associative with precedence 45 for @{'increasing $s}. -notation < "s \nbsp 'is_decreasing'" non associative with precedence 50 +notation < "s \nbsp 'is_decreasing'" non associative with precedence 45 for @{'decreasing $s}. -notation < "x \nbsp 'is_supremum' \nbsp s" non associative with precedence 50 +notation < "x \nbsp 'is_supremum' \nbsp s" non associative with precedence 45 for @{'supremum $s $x}. -notation < "x \nbsp 'is_infimum' \nbsp s" non associative with precedence 50 +notation < "x \nbsp 'is_infimum' \nbsp s" non associative with precedence 45 for @{'infimum $s $x}. -notation > "x 'is_upper_bound' s" non associative with precedence 50 +notation > "x 'is_upper_bound' s" non associative with precedence 45 for @{'upper_bound $s $x}. -notation > "x 'is_lower_bound' s" non associative with precedence 50 +notation > "x 'is_lower_bound' s" non associative with precedence 45 for @{'lower_bound $s $x}. -notation > "s 'is_increasing'" non associative with precedence 50 +notation > "s 'is_increasing'" non associative with precedence 45 for @{'increasing $s}. -notation > "s 'is_decreasing'" non associative with precedence 50 +notation > "s 'is_decreasing'" non associative with precedence 45 for @{'decreasing $s}. -notation > "x 'is_supremum' s" non associative with precedence 50 +notation > "x 'is_supremum' s" non associative with precedence 45 for @{'supremum $s $x}. -notation > "x 'is_infimum' s" non associative with precedence 50 +notation > "x 'is_infimum' s" non associative with precedence 45 for @{'infimum $s $x}. interpretation "Ordered set upper bound" 'upper_bound s x = (upper_bound _ s x). interpretation "Ordered set lower bound" 'lower_bound s x = (lower_bound _ s x). -interpretation "Ordered set increasing" 'increasing s = (increasing _ s). -interpretation "Ordered set decreasing" 'decreasing s = (decreasing _ s). -interpretation "Ordered set strong sup" 'supremum s x = (supremum _ s x). -interpretation "Ordered set strong inf" 'infimum s x = (infimum _ s x). - -include "bishop_set.ma". +interpretation "Ordered set increasing" 'increasing s = (increasing _ s). +interpretation "Ordered set decreasing" 'decreasing s = (decreasing _ s). +interpretation "Ordered set strong sup" 'supremum s x = (supremum _ s x). +interpretation "Ordered set strong inf" 'infimum s x = (infimum _ s x). lemma uniq_supremum: ∀O:ordered_set.∀s:sequence O.∀t1,t2:O. @@ -87,14 +87,12 @@ intros 7 (C s u Hu v Hv H); cases Hu (_ H1); clear Hu; cases (H1 ? H) (w Hw); apply Hv; assumption; qed. - (* Lemma 2.6 *) definition strictly_increasing ≝ λC:ordered_set.λa:sequence C.∀n:nat.a (S n) ≰ a n. definition strictly_decreasing ≝ λC:ordered_set.λa:sequence C.∀n:nat.a n ≰ a (S n). - notation < "s \nbsp 'is_strictly_increasing'" non associative with precedence 50 for @{'strictly_increasing $s}. notation > "s 'is_strictly_increasing'" non associative with precedence 50 @@ -116,21 +114,17 @@ definition downarrow ≝ λC:ordered_set.λs:sequence C.λu:C. s is_decreasing ∧ u is_infimum s. -notation < "a \uparrow \nbsp u" non associative with precedence 50 for @{'sup_inc $a $u}. -notation > "a \uparrow u" non associative with precedence 50 for @{'sup_inc $a $u}. +notation < "a \uparrow \nbsp u" non associative with precedence 45 for @{'sup_inc $a $u}. +notation > "a \uparrow u" non associative with precedence 45 for @{'sup_inc $a $u}. interpretation "Ordered set uparrow" 'sup_inc s u = (uparrow _ s u). -notation < "a \downarrow \nbsp u" non associative with precedence 50 for @{'inf_dec $a $u}. -notation > "a \downarrow u" non associative with precedence 50 for @{'inf_dec $a $u}. +notation < "a \downarrow \nbsp u" non associative with precedence 45 for @{'inf_dec $a $u}. +notation > "a \downarrow u" non associative with precedence 45 for @{'inf_dec $a $u}. interpretation "Ordered set downarrow" 'inf_dec s u = (downarrow _ s u). -include "nat/plus.ma". -include "nat_ordered_set.ma". - -alias symbol "nleq" = "Ordered set excess". -alias symbol "leq" = "Ordered set less or equal than". lemma trans_increasing: - ∀C:ordered_set.∀a:sequence C.a is_increasing → ∀n,m:nat_ordered_set. n ≤ m → a n ≤ a m. + ∀C:ordered_set.∀a:sequence C.a is_increasing → + ∀n,m:nat_ordered_set. n ≤ m → a n ≤ a m. intros 5 (C a Hs n m); elim m; [ rewrite > (le_n_O_to_eq n (not_lt_to_le O n H)); intro X; cases (os_coreflexive ?? X);] @@ -141,7 +135,8 @@ cases (le_to_or_lt_eq ?? (not_lt_to_le (S n1) n H1)); clear H1; qed. lemma trans_decreasing: - ∀C:ordered_set.∀a:sequence C.a is_decreasing → ∀n,m:nat_ordered_set. n ≤ m → a m ≤ a n. + ∀C:ordered_set.∀a:sequence C.a is_decreasing → + ∀n,m:nat_ordered_set. n ≤ m → a m ≤ a n. intros 5 (C a Hs n m); elim m; [ rewrite > (le_n_O_to_eq n (not_lt_to_le O n H)); intro X; cases (os_coreflexive ?? X);] @@ -152,7 +147,8 @@ cases (le_to_or_lt_eq ?? (not_lt_to_le (S n1) n H1)); clear H1; qed. lemma trans_increasing_exc: - ∀C:ordered_set.∀a:sequence C.a is_increasing → ∀n,m:nat_ordered_set. m ≰ n → a n ≤ a m. + ∀C:ordered_set.∀a:sequence C.a is_increasing → + ∀n,m:nat_ordered_set. m ≰ n → a n ≤ a m. intros 5 (C a Hs n m); elim m; [cases (not_le_Sn_O n H);] intro; apply H; [1: change in n1 with (os_carr nat_ordered_set); (* canonical structures *) @@ -164,7 +160,8 @@ intro; apply H; qed. lemma trans_decreasing_exc: - ∀C:ordered_set.∀a:sequence C.a is_decreasing → ∀n,m:nat_ordered_set. m ≰ n → a m ≤ a n . + ∀C:ordered_set.∀a:sequence C.a is_decreasing → + ∀n,m:nat_ordered_set. m ≰ n → a m ≤ a n . intros 5 (C a Hs n m); elim m; [cases (not_le_Sn_O n H);] intro; apply H; [1: change in n1 with (os_carr nat_ordered_set); (* canonical structures *) @@ -175,6 +172,7 @@ intro; apply H; cases (Hs n1); assumption;] qed. +alias symbol "exists" = "CProp exists". lemma strictly_increasing_reaches: ∀C:ordered_set.∀m:sequence nat_ordered_set. m is_strictly_increasing → ∀w.∃t.m t ≰ w. @@ -193,7 +191,7 @@ qed. lemma selection_uparrow: ∀C:ordered_set.∀m:sequence nat_ordered_set.m is_strictly_increasing → - ∀a:sequence C.∀u.a ↑ u → (λx.a (m x)) ↑ u. + ∀a:sequence C.∀u.a ↑ u → ⌊x,a (m x)⌋ ↑ u. intros (C m Hm a u Ha); cases Ha (Ia Su); cases Su (Uu Hu); repeat split; [1: intro n; simplify; apply trans_increasing_exc; [assumption] apply (Hm n); |2: intro n; simplify; apply Uu; @@ -205,7 +203,7 @@ qed. lemma selection_downarrow: ∀C:ordered_set.∀m:sequence nat_ordered_set.m is_strictly_increasing → - ∀a:sequence C.∀u.a ↓ u → (λx.a (m x)) ↓ u. + ∀a:sequence C.∀u.a ↓ u → ⌊x,a (m x)⌋ ↓ u. intros (C m Hm a u Ha); cases Ha (Ia Su); cases Su (Uu Hu); repeat split; [1: intro n; simplify; apply trans_decreasing_exc; [assumption] apply (Hm n); |2: intro n; simplify; apply Uu; @@ -213,42 +211,41 @@ intros (C m Hm a u Ha); cases Ha (Ia Su); cases Su (Uu Hu); repeat split; cases (strictly_increasing_reaches C ? Hm w); exists [apply w1]; cases (os_cotransitive ??? (a (m w1)) H); [assumption] cases (trans_decreasing_exc C ? Ia ?? H1); assumption;] -qed. +qed. (* Definition 2.7 *) -alias id "ExT23" = "cic:/matita/dama/cprop_connectives/exT23.ind#xpointer(1/1)". definition order_converge ≝ λO:ordered_set.λa:sequence O.λx:O. ExT23 (sequence O) (λl.l ↑ x) (λu.u ↓ x) - (λl,u.∀i:nat. (l i) is_infimum (λw.a (w+i)) ∧ (u i) is_supremum (λw.a (w+i))). + (λl,u.∀i:nat. (l i) is_infimum ⌊w,a (w+i)⌋ ∧ + (u i) is_supremum ⌊w,a (w+i)⌋). -notation < "a \nbsp (\circ \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 50 +notation < "a \nbsp (\circ \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 45 for @{'order_converge $a $x}. -notation > "a 'order_converges' x" non associative with precedence 50 +notation > "a 'order_converges' x" non associative with precedence 45 for @{'order_converge $a $x}. 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). -definition segment ≝ λO:ordered_set.λa,b:O.λx:O. - (cic:/matita/logic/connectives/And.ind#xpointer(1/1) (x ≤ b) (a ≤ x)). - -notation "[a,b]" non associative with precedence 50 - for @{'segment $a $b}. +notation "[a,b]" left associative with precedence 70 for @{'segment $a $b}. interpretation "Ordered set sergment" 'segment a b = (segment _ a b). -notation "hvbox(x \in break [a,b])" non associative with precedence 50 - for @{'segment2 $a $b $x}. -interpretation "Ordered set sergment in" 'segment2 a b x= (segment _ a b x). +notation "hvbox(x \in break [a,b])" non associative with precedence 45 + for @{'segment_in $a $b $x}. +interpretation "Ordered set sergment in" 'segment_in a b x= (segment _ a b x). +(* coinductive sigma (A:Type) (P:A→Prop) : Type ≝ sig_in : ∀x.P x → sigma A P. -definition pi1 : ∀A.∀P.sigma A P → A ≝ λA,P,s.match s with [sig_in x _ ⇒ x]. +definition pi1sig : ∀A.∀P.sigma A P → A ≝ λA,P,s.match s with [sig_in x _ ⇒ x]. -interpretation "sigma pi1" 'pi1 x = (pi1 _ _ x). +interpretation "sigma pi1" 'pi1a x = (pi1sig _ _ x). -interpretation "Type exists" 'exists \eta.x = - (cic:/matita/dama/supremum/sigma.ind#xpointer(1/1) _ x). +interpretation "Type exists" 'exists \eta.x = (sigma _ x). +*) lemma segment_ordered_set: ∀O:ordered_set.∀u,v:O.ordered_set. @@ -258,16 +255,16 @@ intros (O u v); apply (mk_ordered_set (∃x.x ∈ [u,v])); |3: intros 3 (x y z); cases x; cases y ; cases z; simplify; apply os_cotransitive] qed. -notation "hvbox({[a, break b]})" non associative with precedence 80 +notation "hvbox({[a, break b]})" non associative with precedence 90 for @{'segment_set $a $b}. interpretation "Ordered set segment" 'segment_set a b = - (segment_ordered_set _ a b). + (segment_ordered_set _ a b). (* Lemma 2.9 *) lemma segment_preserves_supremum: ∀O:ordered_set.∀l,u:O.∀a:sequence {[l,u]}.∀x:{[l,u]}. - (λn.fst (a n)) is_increasing ∧ - (fst x) is_supremum (λn.fst (a n)) → a ↑ x. + ⌊n,fst (a n)⌋ is_increasing ∧ + (fst x) is_supremum ⌊n,fst (a n)⌋ → a ↑ x. intros; split; cases H; clear H; [1: apply H1; |2: cases H2; split; clear H2; @@ -277,8 +274,8 @@ qed. lemma segment_preserves_infimum: ∀O:ordered_set.∀l,u:O.∀a:sequence {[l,u]}.∀x:{[l,u]}. - (λn.fst (a n)) is_decreasing ∧ - (fst x) is_infimum (λn.fst (a n)) → a ↓ x. + ⌊n,fst (a n)⌋ is_decreasing ∧ + (fst x) is_infimum ⌊n,fst (a n)⌋ → a ↓ x. intros; split; cases H; clear H; [1: apply H1; |2: cases H2; split; clear H2; @@ -286,20 +283,22 @@ intros; split; cases H; clear H; |2: clear H; intro y0; apply (H3 (fst y0));]] qed. - (* Definition 2.10 *) coinductive pair (A,B:Type) : Type ≝ prod : ∀a:A.∀b:B.pair A B. definition first : ∀A.∀P.pair A P → A ≝ λA,P,s.match s with [prod x _ ⇒ x]. definition second : ∀A.∀P.pair A P → P ≝ λA,P,s.match s with [prod _ y ⇒ y]. - -interpretation "pair pi1" 'pi1 x = (first _ _ x). -interpretation "pair pi2" 'pi2 x = (second _ _ x). -notation "hvbox(\langle a, break b\rangle)" non associative with precedence 91 for @{ 'pair $a $b}. +interpretation "pair pi1" 'pi1 = (first _ _). +interpretation "pair pi2" 'pi2 = (second _ _). +interpretation "pair pi1" 'pi1a x = (first _ _ x). +interpretation "pair pi2" 'pi2a x = (second _ _ x). +interpretation "pair pi1" 'pi1b x y = (first _ _ x y). +interpretation "pair pi2" 'pi2b x y = (second _ _ x y). + +notation "hvbox(\langle a, break b\rangle)" left associative with precedence 70 for @{ 'pair $a $b}. interpretation "pair" 'pair a b = (prod _ _ a b). - interpretation "prod" 'product a b = (pair a b). - + lemma square_ordered_set: ordered_set → ordered_set. intro O; apply (mk_ordered_set (O × O)); @@ -312,7 +311,7 @@ apply (mk_ordered_set (O × O)); |2: cases (os_cotransitive ??? z2 H1); [left;right|right;right]assumption]] qed. -notation < "s 2 \atop \nleq" non associative with precedence 90 +notation < "s 2 \atop \nleq" non associative with precedence 90 for @{ 'square $s }. notation > "s 'square'" non associative with precedence 90 for @{ 'square $s }. @@ -320,13 +319,11 @@ interpretation "ordered set square" 'square s = (square_ordered_set s). definition square_segment ≝ λO:ordered_set.λa,b:O.λx:square_ordered_set O. - (cic:/matita/logic/connectives/And.ind#xpointer(1/1) - (cic:/matita/logic/connectives/And.ind#xpointer(1/1) (fst x ≤ b) (a ≤ fst x)) - (cic:/matita/logic/connectives/And.ind#xpointer(1/1) (snd x ≤ b) (a ≤ snd x))). + And4 (fst x ≤ b) (a ≤ fst x) (snd x ≤ b) (a ≤ snd x). definition convex ≝ λO:ordered_set.λU:O square → Prop. - ∀p.U p → fst p ≤ snd p → ∀y. square_segment ? (fst p) (snd p) y → U y. + ∀p.U p → fst p ≤ snd p → ∀y. square_segment ? (fst p) (snd p) y → U y. (* Definition 2.11 *) definition upper_located ≝ @@ -337,18 +334,18 @@ definition lower_located ≝ λO:ordered_set.λa:sequence O.∀x,y:O. x ≰ y → (∃i:nat.x ≰ a i) ∨ (∃b:O.b≰y ∧ ∀i:nat.b ≤ a i). -notation < "s \nbsp 'is_upper_located'" non associative with precedence 50 +notation < "s \nbsp 'is_upper_located'" non associative with precedence 45 for @{'upper_located $s}. -notation > "s 'is_upper_located'" non associative with precedence 50 +notation > "s 'is_upper_located'" non associative with precedence 45 for @{'upper_located $s}. -interpretation "Ordered set upper locatedness" 'upper_located s = +interpretation "Ordered set upper locatedness" 'upper_located s = (upper_located _ s). -notation < "s \nbsp 'is_lower_located'" non associative with precedence 50 +notation < "s \nbsp 'is_lower_located'" non associative with precedence 45 for @{'lower_located $s}. -notation > "s 'is_lower_located'" non associative with precedence 50 +notation > "s 'is_lower_located'" non associative with precedence 45 for @{'lower_located $s}. -interpretation "Ordered set lower locatedness" 'lower_located s = +interpretation "Ordered set lower locatedness" 'lower_located s = (lower_located _ s). (* Lemma 2.12 *) diff --git a/helm/software/matita/contribs/dama/dama/uniform.ma b/helm/software/matita/contribs/dama/dama/uniform.ma index 348b99a81..b8b77572b 100644 --- a/helm/software/matita/contribs/dama/dama/uniform.ma +++ b/helm/software/matita/contribs/dama/dama/uniform.ma @@ -31,11 +31,6 @@ notation "a \subseteq u" left associative with precedence 70 for @{ 'subset $a $u }. interpretation "Bishop subset" 'subset a b = (subset _ a b). -notation "hvbox({ ident x : t | break p })" non associative with precedence 80 - for @{ 'explicitset (\lambda ${ident x} : $t . $p) }. -definition mk_set ≝ λT:bishop_set.λx:T→Prop.x. -interpretation "explicit set" 'explicitset t = (mk_set _ t). - notation < "s 2 \atop \neq" non associative with precedence 90 for @{ 'square2 $s }. notation > "s 'square'" non associative with precedence 90 @@ -43,44 +38,41 @@ notation > "s 'square'" non associative with precedence 90 interpretation "bishop set square" 'square x = (square_bishop_set x). interpretation "bishop set square" 'square2 x = (square_bishop_set x). - alias symbol "exists" = "exists". alias symbol "and" = "logical and". definition compose_relations ≝ λC:bishop_set.λU,V:C square → Prop. λx:C square.∃y:C. U 〈fst x,y〉 ∧ V 〈y,snd x〉. -notation "a \circ b" left associative with precedence 60 +notation "a \circ b" left associative with precedence 70 for @{'compose $a $b}. interpretation "relations composition" 'compose a b = (compose_relations _ a b). -notation "hvbox(x \in break a \circ break b)" non associative with precedence 50 - for @{'compose2 $a $b $x}. -interpretation "relations composition" 'compose2 a b x = - (compose_relations _ a b x). definition invert_relation ≝ λC:bishop_set.λU:C square → Prop. λx:C square. U 〈snd x,fst x〉. -notation < "s \sup (-1)" non associative with precedence 90 +notation < "s \sup (-1)" left associative with precedence 70 for @{ 'invert $s }. -notation < "s \sup (-1) x" non associative with precedence 90 +notation < "s \sup (-1) x" left associative with precedence 70 for @{ 'invert2 $s $x}. -notation > "'inv' s" non associative with precedence 90 - for @{ 'invert $s }. +notation > "'inv'" right associative with precedence 70 + for @{ 'invert0 }. interpretation "relation invertion" 'invert a = (invert_relation _ a). +interpretation "relation invertion" 'invert0 = (invert_relation _). interpretation "relation invertion" 'invert2 a x = (invert_relation _ a x). alias symbol "exists" = "CProp exists". -alias symbol "and" (instance 18) = "constructive and". -alias symbol "and" (instance 10) = "constructive and". +alias symbol "and" (instance 21) = "constructive and". +alias symbol "and" (instance 16) = "constructive and". +alias symbol "and" (instance 9) = "constructive and". record uniform_space : Type ≝ { us_carr:> bishop_set; us_unifbase: (us_carr square → Prop) → CProp; us_phi1: ∀U:us_carr square → Prop. us_unifbase U → - {x:us_carr square|fst x ≈ snd x} ⊆ U; + (λx:us_carr square.fst x ≈ snd x) ⊆ U; us_phi2: ∀U,V:us_carr square → Prop. us_unifbase U → us_unifbase V → - ∃W:us_carr square → Prop.us_unifbase W ∧ (W ⊆ {x:?|U x ∧ V x}); + ∃W:us_carr square → Prop.us_unifbase W ∧ (W ⊆ (λx.U x ∧ V x)); us_phi3: ∀U:us_carr square → Prop. us_unifbase U → ∃W:us_carr square → Prop.us_unifbase W ∧ (W ∘ W) ⊆ U; us_phi4: ∀U:us_carr square → Prop. us_unifbase U → ∀x.(U x → (inv U) x) ∧ ((inv U) x → U x) @@ -121,12 +113,3 @@ apply H; unfold; exists [apply x]; split [2: apply (Hn ? H2)] cases (us_phi4 ?? Hv 〈a i,x〉) (P1 P2); apply P2; apply (Hn ? H1); qed. - -(* Definition 2.17 *) -definition mk_big_set ≝ - λP:CProp.λF:P→CProp.F. -interpretation "explicit big set" 'explicitset t = (mk_big_set _ t). - -definition restrict_uniformity ≝ - λC:uniform_space.λX:C→Prop. - {U:C square → Prop| (U ⊆ {x:C square|X (fst x) ∧ X(snd x)}) ∧ us_unifbase C U}. -- 2.39.2