bs_cotransitive: cotransitive ? bs_apart
}.
-notation "hvbox(a break # b)" non associative with precedence 50
+notation "hvbox(a break # b)" non associative with precedence 45
for @{ 'apart $a $b}.
interpretation "bishop_setapartness" 'apart x y = (bs_apart _ x y).
(* Definition 2.2 (2) *)
definition eq ≝ λA:bishop_set.λa,b:A. ¬ (a # b).
-notation "hvbox(a break ≈ b)" non associative with precedence 50
+notation "hvbox(a break ≈ b)" non associative with precedence 45
for @{ 'napart $a $b}.
interpretation "Bishop set alikeness" 'napart a b = (eq _ a b).
+sandwich.ma ordered_uniform.ma
+property_sigma.ma ordered_uniform.ma
+uniform.ma supremum.ma
bishop_set.ma ordered_set.ma
-extra.ma bishop_set_rewrite.ma
-ordered_set.ma cprop_connectives.ma
-cprop_connectives.ma logic/equality.ma
-bishop_set_rewrite.ma bishop_set.ma
sequence.ma nat/nat.ma
-uniform.ma supremum.ma
-supremum.ma bishop_set.ma cprop_connectives.ma nat/plus.ma nat_ordered_set.ma ordered_set.ma sequence.ma
-nat_ordered_set.ma cprop_connectives.ma nat/compare.ma ordered_set.ma
-property_sigma.ma ordered_uniform.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
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
lebesgue.ma property_exhaustivity.ma sandwich.ma
-sandwich.ma ordered_uniform.ma
+ordered_set.ma cprop_connectives.ma
+models/rationals.ma Q/q/q.ma uniform.ma
+models/uniformnat.ma bishop_set_rewrite.ma datatypes/constructors.ma nat_ordered_set.ma uniform.ma
+Q/q/q.ma
+datatypes/constructors.ma
logic/equality.ma
nat/compare.ma
nat/nat.ma
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "bishop_set_rewrite.ma".
-
-definition strong_ext ≝ λA:bishop_set.λop:A→A.∀x,y. op x # op y → x # y.
-
-
-
-definition lt ≝ λE:excess.λa,b:E. a ≤ b ∧ a # b.
-
-interpretation "ordered sets less than" 'lt a b = (lt _ a b).
-
-lemma lt_coreflexive: ∀E.coreflexive ? (lt E).
-intros 2 (E x); intro H; cases H (_ ABS);
-apply (ap_coreflexive ? x ABS);
-qed.
-
-lemma lt_transitive: ∀E.transitive ? (lt E).
-intros (E); unfold; intros (x y z H1 H2); cases H1 (Lxy Axy); cases H2 (Lyz Ayz);
-split; [apply (le_transitive ???? Lxy Lyz)] clear H1 H2;
-cases Axy (H1 H1); cases Ayz (H2 H2); [1:cases (Lxy H1)|3:cases (Lyz H2)]clear Axy Ayz;
-[1: cases (exc_cotransitive ??? y H1) (X X); [cases (Lxy X)|cases (exc_coreflexive ?? X)]
-|2: cases (exc_cotransitive ??? x H2) (X X); [right;assumption|cases (Lxy X)]]
-qed.
-
-theorem lt_to_excess: ∀E:excess.∀a,b:E. (a < b) → (b ≰ a).
-intros (E a b Lab); cases Lab (LEab Aab); cases Aab (H H);[cases (LEab H)]
-fold normalize (b ≰ a); assumption; (* BUG *)
-qed.
-
-lemma lt_rewr: ∀A:excess.∀x,z,y:A. x ≈ y → z < y → z < x.
-intros (A x y z E H); split; cases H;
-[apply (Le≫ ? (eq_sym ??? E));|apply (Ap≫ ? E)] assumption;
-qed.
-
-lemma lt_rewl: ∀A:excess.∀x,z,y:A. x ≈ y → y < z → x < z.
-intros (A x y z E H); split; cases H;
-[apply (Le≪ ? (eq_sym ??? E));| apply (Ap≪ ? E);] assumption;
-qed.
-
-notation > "'Lt'≪" non associative with precedence 50 for @{'ltrewritel}.
-interpretation "lt_rewl" 'ltrewritel = (lt_rewl _ _ _).
-notation > "'Lt'≫" non associative with precedence 50 for @{'ltrewriter}.
-interpretation "lt_rewr" 'ltrewriter = (lt_rewr _ _ _).
-
-lemma lt_le_transitive: ∀A:excess.∀x,y,z:A.x < y → y ≤ z → x < z.
-intros (A x y z LT LE); cases LT (LEx APx); split; [apply (le_transitive ???? LEx LE)]
-cases APx (EXx EXx); [cases (LEx EXx)]
-cases (exc_cotransitive ??? z EXx) (EXz EXz); [cases (LE EXz)]
-right; assumption;
-qed.
-
-lemma le_lt_transitive: ∀A:excess.∀x,y,z:A.x ≤ y → y < z → x < z.
-intros (A x y z LE LT); cases LT (LEx APx); split; [apply (le_transitive ???? LE LEx)]
-cases APx (EXx EXx); [cases (LEx EXx)]
-cases (exc_cotransitive ??? x EXx) (EXz EXz); [right; assumption]
-cases LE; assumption;
-qed.
-
-lemma le_le_eq: ∀E:excess.∀a,b:E. a ≤ b → b ≤ a → a ≈ b.
-intros (E x y L1 L2); intro H; cases H; [apply L1|apply L2] assumption;
-qed.
-
-lemma eq_le_le: ∀E:excess.∀a,b:E. a ≈ b → a ≤ b ∧ b ≤ a.
-intros (E x y H); whd in H;
-split; intro; apply H; [left|right] assumption.
-qed.
-
-lemma ap_le_to_lt: ∀E:excess.∀a,c:E.c # a → c ≤ a → c < a.
-intros; split; assumption;
-qed.
-
-definition total_order_property : ∀E:excess. Type ≝
- λE:excess. ∀a,b:E. a ≰ b → b < a.
-
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "datatypes/constructors.ma".
+include "nat_ordered_set.ma".
+include "bishop_set_rewrite.ma".
+include "uniform.ma".
+
+definition discrete_uniform_space_of_bishop_set:bishop_set → uniform_space.
+intro C; apply (mk_uniform_space C);
+[1: intro; apply (∃_:unit.∀n:C square.(fst n ≈ snd n → P n) ∧ (P n → fst n ≈ snd n));
+|2: intros 4 (U H x Hx); unfold in Hx;
+ cases H (_ H1); cases (H1 x); apply H2; apply Hx;
+|3: intros; cases H (_ PU); cases H1 (_ PV);
+ exists[apply (λx.U x ∧ V x)] split;
+ [1: exists[apply something] intro; cases (PU n); cases (PV n);
+ split; intros; try split;[apply H2;|apply H4] try assumption;
+ apply H3; cases H6; assumption;
+ |2: simplify; unfold mk_set; intros; assumption;]
+|4: intros; cases H (_ PU); exists [apply U] split;
+ [1: exists [apply something] intro n; cases (PU n);
+ split; intros; try split;[apply H1;|apply H2] assumption;
+ |2: intros 2 (x Hx); cases Hx; cases H1; clear H1;
+ cases (PU 〈(fst x),x1〉); lapply (H4 H2) as H5; simplify in H5;
+ cases (PU 〈x1,(snd x)〉); lapply (H7 H3) as H8; simplify in H8;
+ generalize in match H5; generalize in match H8;
+ generalize in match (PU x); clear H6 H7 H1 H4 H2 H3 H5 H8;
+ cases x; simplify; intros; cases H1; clear H1; apply H4;
+ apply (eq_trans ???? H3 H2);]
+|5: intros; cases H (_ H1); split; cases x;
+ [2: cases (H1 〈b,b1〉); intro; apply H2; cases (H1 〈b1,b〉);
+ lapply (H6 H4) as H7; apply eq_sym; apply H7;
+ |1: cases (H1 〈b1,b〉); intro; apply H2; cases (H1 〈b,b1〉);
+ lapply (H6 H4) as H7; apply eq_sym; apply H7;]]
+qed.
+
+definition nat_uniform_space: uniform_space.
+apply (discrete_uniform_space_of_bishop_set nat_ordered_set);
+qed.
projects / helm.git / commitdiff